coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof obligation involving proj1_sig

From: "Lucian M. Patcas" <lucian.patcas AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Proof obligation involving proj1_sig
Date: Mon, 20 Jun 2011 02:29:51 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:reply-to:sender:from:date:x-google-sender-auth :message-id:subject:to:content-type; b=VhWpsU5JL8Df6QpZCqDGzt2j/+QNruoYIaFROiiNzWgv8vaXGM55s9sveA2zUXr+3P hZPIU9QLFbH3qVXK47Bmb4e1J7efI7GjbiCSyqyJ6oT9TTs7Vz34wZynuTqwIbnYY3kG VqmhDEYvanJ5W4WXMa3lO8V2ihoBfgGFb3T2E=

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