The Coq mailing list

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

And I found that the culprit was likely to be the omega tactic, or
more precisely your "assert (y < S n) ∨ (y = S n)" (not sure though,
I didn’t check it very deeply).

The following proof makes your stuff computable.

Theorem nz_Acc: forall (n:nz), Acc nz_lt n.
Proof.
  intros []; fix 1; intros [|n].
  + clear; intros []; split.
  + intros H; generalize (nz_Acc n); clear nz_Acc; intros Rec; split.
    intros [y]; unfold nz_lt at 1; simpl; clear H.
    intros P Q; revert Rec.
    change n with (pred (S n)); case Q; clear Q; simpl; auto.
    intros [|m].
    * intros K; refine (match _:False with end).
      change (match O with O => False | _ => True end); case K; auto.
    * intros Hlt Rec.
      case (Rec (fun P => match P with eq_refl => I end)); clear Rec.
      intros Q; apply Q; clear - Hlt.
      assumption.
Defined.

Yes I know, I like low level proofs…

Le Sun, 13 Oct 2013 13:07:43 +0200,
AUGER Cédric 
<sedrikov AT gmail.com>
 a écrit :

> 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. *)
>