coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] interactively constructing witnesses of sig types

From: Taral <taralx AT gmail.com>
To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] interactively constructing witnesses of sig types
Date: Thu, 5 Mar 2009 12:16:53 -0800
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 :cc:content-type:content-transfer-encoding; b=iHyJTj1+Q+ZHhfq6aQbnFlp1DEtOBO7mjD0/ygAYcBsHFe8DegatwX5vCyA6UdbLuT +F175PAgobkpjpRoOZVpPmPugpB2PNWJ/5LjBqZPcx23Lk06yx1JRA8f/VuFuBgYn59S Km8IrR0lAEKWY257ziI4MsnZJW+Y1Y2B42M8k=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, Mar 5, 2009 at 11:00 AM, Keiko Nakata
<keiko AT kurims.kyoto-u.ac.jp>
wrote:
> Could I interactively construct witnesses of sig types?

Yup, but you need a lemma.

Add Relation nat eq
    reflexivity proved by eq_refl
    symmetry proved by eq_sym
    transitivity proved by eq_trans
    as eq_nat_rel.

Lemma and_build : forall p1 x1 p2 x2, eq (gen p1 x1) (gen p2 x2) -> index
(spec_
and p1 p2).
Proof.
intros.
exists (x1, x2); auto.
Defined.

Lemma and_intro: forall p1 p2 n,
satisfy p1 n -> satisfy p2 n -> satisfy (spec_and p1 p2) n.
Proof.
intros.
destruct H.
destruct H0.
assert (eq (gen p x) (gen p0 x0)).
rewrite H in |- *.
rewrite H0 in |- *.
reflexivity.
constructor 1 with (and_build _ _ _ _ H1).
simpl in |- *; auto.
Qed.

The key part is that and_build is transparent (ends in Defined).

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown

[Coq-Club] interactively constructing witnesses of sig types, Keiko Nakata
- Re: [Coq-Club] interactively constructing witnesses of sig types, Taral
- Re: [Coq-Club] interactively constructing witnesses of sig types, Sean Wilson
  - Re: [Coq-Club] interactively constructing witnesses of sig types, Taral