The Coq mailing list

[franck.barbier AT franckbarbier.com]

I become quite mad on the second proof... I guess there are two solutions. The
proof is "too much trivial" or artificially complicated, even not proovable ?

Help appreciated.


Inductive X : Type := God | cons : X -> X.

Definition father(x : X) : X := match x with
| cons source => source
| _ => God
end.

Lemma Quasi_irreflexivity : forall i : X, i = father i -> i = God. (* solution
by P. Cast�ran *)
Proof.
  induction i;trivial.
  Lemma No_loop : forall i : X, i <> cons i. (* Somehow ugly... *)
  Proof.
    induction i.
    discriminate.
    intro H;injection H;intro H1;destruct IHi;auto.
  Qed.
  simpl;intro H;destruct (No_loop i);auto.
Qed.

Fixpoint ancestor(n : nat) (x : X) : X := match n with
| 0 => father x
| S m => father (ancestor m x)
end.

Lemma Quasi_irreflexivity' : forall i : X, forall n : nat, i = ancestor n i ->
i = God.
Proof.
intros.
induction n.
simpl in H.
apply Quasi_irreflexivity.
exact H.
(* pb from here...
elim IHn.
tauto.
*)
Qed.