Library not_decreasing
Require
Import
Relations.
Section
Sequences.
Variable
A : Set.
Variable
R : A -> A -> Prop.
Lemma
not_acc : forall a b:A, R a b -> ~ Acc R a -> ~ Acc R b.
Proof
.
intros a b H H0 H1.
absurd (Acc R a); auto.
generalize a H.
elim H1; auto.
Qed
.
Lemma
acc_imp : forall a b:A, R a b -> Acc R b -> Acc R a.
Proof
.
intros a b H H0.
generalize a H.
elim H0; auto.
Qed
.
Hypothesis
W : well_founded R.
Hint
Resolve W.
Section
seq_intro.
Variable
seq : nat -> A.
Let
is_in_seq (x:A) := exists i : nat, x = seq i.
Lemma
not_decreasing_aux : ~ (forall n:nat, R (seq (S n)) (seq n)).
Proof
.
unfold not in |- *; intro dec.
cut (forall a:A, is_in_seq a -> ~ Acc R a).
intro H.
absurd (Acc R (seq 0)).
apply H.
exists 0; trivial.
apply W.
intro a; pattern a in |- *.
apply well_founded_ind with A R.
assumption.
intros x Hx H.
elim H.
intros i egi.
cut (R (seq (S i)) (seq i)).
intro H1.
rewrite egi.
apply not_acc with (seq (S i)); auto.
apply Hx.
rewrite egi; auto.
exists (S i); auto.
auto.
Qed
.
End
seq_intro.
Theorem
not_decreasing :
~ (exists seq : nat -> A, (forall i:nat, R (seq (S i)) (seq i))).
Proof
.
unfold not in |- *; intro H.
case H; intros s Hs.
absurd (forall i:nat, R (s (S i)) (s i)); auto.
apply not_decreasing_aux.
Qed
.
End
Sequences.
Index
This page has been generated by coqdoc