Library hydras.solutions_exercises.T1_ltNotWf

From hydras Require Import T1.
From Coq Require Import Relations.

Section Proof_of_lt_not_wf.

  Hypothesis lt_wf : well_founded lt.

  Fixpoint s (i:nat) : T1 :=
    match i with
      0 ⇒ phi0 2
    | S j ⇒ cons 1 0 (s j)
    end.

  Lemma s_decr : ∀ i, lt (s (S i)) (s i).


  Section seq_intro.
    Variable A: Type.
    Variable seq : nat → A.
    Variable R : A → A → Prop.
    Hypothesis Rwf : well_founded R.
    Let is_in_seq (x:A) := ∃ i : nat, x = seq i.

    Lemma not_acc : ∀ a b:A, R a b → ¬ Acc R a → ¬ Acc R b.

    Lemma acc_imp : ∀ a b:A, R a b → Acc R b → Acc R a.

    Lemma not_decreasing_aux : ¬ (∀ n:nat, R (seq (S n)) (seq n)).

  End seq_intro.

  Theorem not_decreasing (A:Type)(R: relation A) (Hwf : well_founded R) :
    ¬ (∃ seq : nat → A, (∀ i:nat, R (seq (S i)) (seq i))).

  Lemma contrad : False.

End Proof_of_lt_not_wf.

Lemma lt_not_wf : ¬ well_founded lt.