The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Here is some proof what you computed was indeed correct:

Goal (projT1 (nz_double (nz_double nz_one))) = 4.
assert (forall (x : nz), x = exist _ (projT1 x) (projT2 x)).
intros [a b]; simpl.
reflexivity.

rewrite (H (nz_double nz_one)).
generalize (projT2 (nz_double nz_one)).
vm_compute (projT1 (nz_double nz_one)).
unfold nz_double.
unfold Fix.
unfold Fix_F.
intros N.
generalize (nz_lt_wf (exist (fun m => m <> 0) 2 N)).
intros [a].
vm_compute (le_lt_dec 2 (projT1 (exist (fun n : nat => n <> 0) 2 N))).
cbv iota.
unfold Acc_inv.
generalize (a (nz_pred (exist (fun n : nat => n <> 0) 2 N)) (le_n 2)).
intros [b].
vm_compute (le_lt_dec 2 (projT1 (nz_pred (exist (fun n : nat => n <> 0)
2 N)))). cbv iota.
simpl.
clear.
reflexivity.
Qed.


Le Sat, 12 Oct 2013 18:43:25 +0300,
Ilmārs Cīrulis 
<ilmars.cirulis AT gmail.com>
 a écrit :

> Please help to find where I made mistake!
> Thanks in advance!
> 
> 
> Require Import Omega.
> 
> Definition nz: Set := {n:nat | n<>O}.
> Definition nat_to_nz (n:nat) (p:n<>O): nz := exist _ n p.
> Theorem nz_t1 (n:nat): S n<>O. Proof. auto. Defined.
> 
> Definition nz_one: nz := exist _ 1 (nz_t1 O).
> Definition nz_lt (n m:nz) := lt (projT1 n) (projT1 m).
> 
> Definition nz_pred (n:nz): nz := exist _ (S (pred (pred (projT1 n))))
> (nz_t1 _).
> Definition nz_S (n:nz): nz := nat_to_nz (S (projT1 n)) (nz_t1 _).
> 
> Theorem nz_Acc: forall (n:nz), Acc nz_lt n.
> Proof.
>  intro. destruct n as [n pn], n as [|n]. unfold not in pn. destruct
> pn. reflexivity.
>  induction n; split; intros; destruct y as [y py]; unfold nz_lt in *;
> simpl in *.
>    unfold not in py. destruct py. inversion H. tauto. inversion H1.
>    assert (y<S n\/y=S n). omega. destruct H0.
>     assert (S n<>O); auto.
>     assert (nz_lt (exist _ y py) (exist _ (S n) H1)). unfold nz_lt;
> simpl; assumption.
>     fold nz_lt in *. apply Acc_inv with (exist (fun n0:nat=>n0<>O) (S
> n) H1). apply IHn.
>     unfold nz_lt; simpl; assumption.
>     rewrite <- H0 in IHn. apply IHn.
> Defined.
> 
> Theorem nz_lt_wf: well_founded nz_lt. Proof. exact nz_Acc. Defined.
> 
> Definition nz_double: nz -> nz.
>   refine (
>     Fix
>       nz_lt_wf
>       (fun _ => nz)
>       (fun
>          (n: nz)
>          (nz_double: forall n': nz, nz_lt n' n -> nz) =>
>          if le_lt_dec 2 (projT1 n)
>            then nz_S (nz_S (nz_double (nz_pred n) _))
>            else nz_S (nz_one))).
>   unfold nz_lt, nz_pred; destruct n; simpl in *.
>   destruct x. tauto. destruct x. tauto. apply le_n.
> Defined.
> 
> Eval compute in projT1 (nz_double nz_one). (* Correct! It is 2. *)
> Eval compute in projT1 (nz_double (nz_double nz_one)). (* Wtf?!
> Incorrect. *)