The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

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