The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

There are other ways to go about all of this. Is there a reason you're not using a simpler definition for nz?

Inductive nz : Set :=

  | one : nz

  | succ : nz -> nz.

If there is, you might want to first write functions for nat and add proofs later.

Fixpoint double_aux (n1 : nat) : nat :=

  match n1 with

  | 0 => 0

  | S n2 => S (S (double_aux n2))

  end.

Axiom double_corr : forall n1, n1 <> 0 -> double_aux n1 <> 0.

Definition nz : Set := {n1 : nat | n1 <> 0}.

Definition double (n1 : nz) : nz :=

  match n1 with

  | exist n2 H1 => exist _ (double_aux n2) (double_corr _ H1)

  end.

Another way to do it is to define an nz_rect fold for your set, and use the function's relation to help with the implementation.

Axiom nz : Set.

Axiom one : nz.

Axiom succ : nz -> nz.

Axiom nz_rect : forall P1,

  P1 one ->

  (forall n1, P1 n1 -> P1 (succ n1)) ->

  forall n1, P1 n1.

Inductive double_rel : nz -> nz -> Prop :=

  | double_rel_1 : double_rel one (succ one)

  | double_rel_2 : forall n1 n2, double_rel n1 n2 -> double_rel (succ n1) (succ (succ n2)).

Definition double_strong : forall n1, {n2 | double_rel n1 n2}.

Proof.

refine (nz_rect _ _ _).

refine (exist _ _ _).

refine double_rel_1.

refine (fun n1 => _).

refine (sig_rect _ _).

refine (fun n2 => _).

refine (fun H1 => _).

refine (exist _ _ _).

refine (double_rel_2 _ _ _).

refine H1.

Defined.

Definition double : nz -> nz := fun n1 => proj1_sig (double_strong n1).

On Sun, Oct 13, 2013 at 1:03 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:

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