The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

Hi,

If you're going to develop with sigma types, you'll probably end up needing proof irrelevance. Proof irrelevance allows you to substitute any proof of a fact by any other proof of that fact. I'm not sure in what cases it's possible to prove proof irrelevance, but I know it's provable for equality and inequality, so it's probably provable for disequality too. If not, you can fall back to the axiom in Coq.Logic.ProofIrrelevance, but then you won't be able to compute your functions from inside Coq. Take a look at http://coq.inria.fr/stdlib/Coq.Logic.Eqdep_dec.html and http://coq.inria.fr/faq?som=12#htoc159. And don't forget to end the proof of your theorems with Defined instead of Qed so they're computable.

Definition nzn : Type := {n1 : nat | n1 <> 0}.

Axiom diff_proof_irr : forall (T1 : Type) (o1 o2 : T1) (H1 H2 : o1 <> o2), H1 = H2.

Axiom diff_S_0 : forall n1, S n1 <> 0.

Definition one : nzn := exist _ 1 (diff_S_0 0).

Definition succ (n1 : nzn) : nzn :=

  match n1 with

  | exist n2 _ => exist _ (S n2) (diff_S_0 n2)

  end.

Theorem nzn_rect : forall P1 : nzn -> Type,

  P1 one ->

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

  forall n1, P1 n1.

Proof.

intros P1 H1 H2.

destruct n1 as [n1 H3].

destruct n1 as [| n1].

  destruct H3.

  apply eq_refl.

  induction n1 as [| n1 H4].

    unfold one in H1.

    replace H3 with (diff_S_0 0).

      apply H1.

      apply diff_proof_irr.

    specialize (H2 (exist _ (S n1) (diff_S_0 n1))).

    unfold succ in H2.

    replace H3 with (diff_S_0 (S n1)).

      apply H2.

      apply H4.

      apply diff_proof_irr.

Defined.

Definition nzn_ind : forall P1 : nzn -> Prop,

  P1 one ->

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

  forall n1, P1 n1 :=

  nzn_rect.

Definition add : nzn -> nzn -> nzn :=

  nzn_rect _ succ (fun n1 H1 n2 => succ (H1 n2)).

Eval compute in add (succ one) (succ one).

On Fri, Jul 19, 2013 at 12:51 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

For example, I have such Type:

Definition nzn: Type := {n: nat | n <> O}.

Can anyone write down all necessary theorems (with Admitted) and anything else that would allow use induction and recursion on that type?