The Coq mailing list

[Vincent <vincent.dema AT gmail.com>]

Le jeudi 10 mars 2011 01:45:45 Adam Chlipala, vous avez écrit :
> 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 ?
> > 
> > Inductive X : Type := God | cons : X ->  X.
> 
> This type is isomorphic to the natural numbers [nat], and your theorem
> is pretty easy to reduce to a set of facts about arithmetic, all of
> which can be proven by the [omega] tactic.  My hint is to write a
> function to translate [X] to [nat] and then characterize the action of
> your [ancestor] function in terms of standard arithmetic operations.
Adam is right: there is nothing more than natural numbers behind God !


Here is one answer:


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

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

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


Fixpoint nat_of_X (x:X) : nat :=
match x with
| God => 0
| cons s => S (nat_of_X s)
end.


Require Import Arith.
Require Import Omega.


Lemma God_is_O i: nat_of_X i = 0 -> i = God.
intro i; case i; clear i; trivial.
intros i H; discriminate H.
Qed.

Lemma father_is_pred i :  nat_of_X (father i) = pred (nat_of_X i).
intro i; case i; trivial.
Qed.

Lemma father_ancestor_commutes n i: (father (ancestor n i)) = ancestor n 
(father i).
induction n; trivial.
simpl; intro i; rewrite IHn; trivial.
Qed.

Lemma ancestor_is_minus n i: nat_of_X (ancestor n i) = (nat_of_X i) - (S n).
induction n; simpl; intro i.
rewrite <- pred_of_minus. apply father_is_pred.
rewrite father_ancestor_commutes, IHn, father_is_pred.
omega.
Qed.



Theorem Quasi_irreflexivity_nat n m: n=n-(S m) -> n=0.
intros; omega.
Qed.

Corollary Quasi_irreflexivity n i : i = ancestor n i -> i = God.
intros.
apply God_is_O.
apply Quasi_irreflexivity_nat with n.
rewrite <- ancestor_is_minus.
rewrite <- H; trivial.
Qed.



------------------
Vincent Demange.