coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Depenednt types and equality proofs

From: Evgeny Makarov <emakarov AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Depenednt types and equality proofs
Date: Fri, 3 Sep 2010 00:54:47 +0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=WpwxkOtt6zDg54Y6K8nTOi1l/Wuu8lvcK1snftslxk1gRGyjQgJw1qg0e5/W6snHDN hrbi4RRml0pkvwqpRvc/2nR632HgJpdRYlr0oZ6k9X43oy1IAM+X6k5xkA54c9JlcRP6 RJJO2q3ICZ+qjDEymbfIK1v1sS/jabyjGbckA=

Hi, Ian,

I don't know yet why Qed produces an error after the "Proof completed"
message, but you could finish your development as follows.

Lemma mkThing_equal :
  forall (from to : natSet) (n1 n2 : SignedNat)
    (n1_ok : natOK from to n1) (n2_ok : natOK from to n2),
      n1 = n2 -> mkThing n1 n1_ok = mkThing n2 n2_ok.
Proof.
intros from to n1 n2 n1_ok n2_ok H.
destruct H.
assert (H1 : n1_ok = n2_ok) by apply proof_irrelevance.
rewrite H1; reflexivity.
Qed.

Lemma thingInverseInverseDestructingSign :
      forall {from to : natSet}
             (p : Thing from to),
      thingInverse (thingInverse p) = p.
Proof with auto.
intros from to p. destruct p as [n n_ok]; unfold thingInverse; simpl.
apply mkThing_equal. apply signedNatInverseInverse.
Qed.

Evgeny

[Coq-Club] Depenednt types and equality proofs, Ian Lynagh
- Re: [Coq-Club] Depenednt types and equality proofs, Evgeny Makarov
  - Re: [Coq-Club] Depenednt types and equality proofs, Ian Lynagh
  - Re: [Coq-Club] Depenednt types and equality proofs, Taral