coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof obligation involving proj1_sig

From: Jacques Garrigue <garrigue AT math.nagoya-u.ac.jp>
To: "Lucian M. Patcas" <lucian.patcas AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof obligation involving proj1_sig
Date: Mon, 20 Jun 2011 16:12:12 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=Vi9aQkuelPm/Jd2mPbNSVY6rrO6rQ0J3eGAbsT16vRq+wYQ5ESce4Ll8eMc7a1REAZ S/4scQqq8RMs038ZgA10XyZdni6nCqkkJRsaVh1pZ8PDCbxicezdNwQtOJykY1BhaFY9 lGCB8GDrnjdFQ79bK050wQtfBGxakOgtvNMlk=

Use the destruct tactic to split your dependent sums.

Program Definition b (t : nat): {x : nat | x = t + 8} :=
  b2 (b1 t).
Next Obligation.
intros.
destruct (b1 t).
simpl.
destruct (b2 x).
simpl.
subst.
ring.
Qed.

On 2011/06/20, at 15:29, Lucian M. Patcas wrote:

> Hi all,
>
> I've been playing with the Program command and tried this:
>
> Variable b1 : forall t : nat, {x : nat | x = t + 5}.
> Variable b2 : forall t : nat, {x : nat | x = t + 3}.
>
> Program Definition b (t : nat): {x : nat | x = t + 8} :=
>   b2 (b1 t).
> Obligation 1.
>
> 1 subgoal
>
>   t : nat
>   ============================
>    proj1_sig (b2 (proj1_sig (b1 t))) = t + 8
>
> Any hints on how I would go about proving this?
>
> Thanks,
> Lucian

[Coq-Club] Proof obligation involving proj1_sig, Lucian M. Patcas
- Re: [Coq-Club] Proof obligation involving proj1_sig, Vincent Siles
- Re: [Coq-Club] Proof obligation involving proj1_sig, Jacques Garrigue