The Coq mailing list

[Sylvain Heraud <sylvain.heraud AT gmail.com>]

Sorry stronger version :p !

On Tue, Mar 8, 2011 at 16:49, Sylvain Heraud <sylvain.heraud AT gmail.com> wrote:

I proved a weaker version of your Lemma.

and add number of step to find God !

Lemma father_ancestor : forall n x,
  father (ancestor n x) = ancestor (S n) x.
Proof.
 simpl; auto.
Qed.

Lemma ancestor_cons : forall n i,
  ancestor (S n) (cons i) = ancestor n i.
Proof.
 intros; simpl.
 induction n; simpl; trivial.
 f_equal; auto.
Qed.

Fixpoint step i :=
match i with
  | God => 0
  | cons i => S (step i)
end.

Lemma step_correct : forall i,
  ancestor (step i) i = God.
Proof.
 induction i; simpl; auto.
 rewrite father_ancestor.
 rewrite ancestor_cons.
 auto.
Qed.

Lemma Quasi_irreflexivity' : forall (i : X),

  (forall n, i = ancestor n i) ->
  i = God.
Proof.
intros.
induction i; auto.
generalize (H (S (step i))); intros.
rewrite H0.
rewrite ancestor_cons.
apply  step_correct.
Qed.

On Tue, Mar 8, 2011 at 13:40, <franck.barbier AT franckbarbier.com> wrote:

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.