coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Transformations under a binder

From: Taral <taralx AT gmail.com>
To: "JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Transformations under a binder
Date: Mon, 19 Jan 2009 23:50:10 -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=FN1MwRubNSZdXAKhxUaAv94Itcj8h1W9cdiJrjzaGPvdW4ifeh9lMeC3vXdmn/OCRH U6xMuHEV2nio8fKxJy5gbrtbtWHTLY3AgmC72UtPz0DM+aI+r4JKH7O7Vog+Iv4SK5KO 8JN/BNN1XzxMSeV83wLpYoHWWfjoAX0AZlDqU=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, Jan 19, 2009 at 11:22 PM, JAEGER, Eric (SGDN)
<eric.jaeger AT sgdn.gouv.fr>
wrote:
> So here is my question: Provided I have a function leb:bool->bool s.t.
> leb_0:forall (n:nat), leb 0 n=true holds, is there a tactic in Coq to
> rewrite a term of the form (leb 0 n) under a binder capturing n, without
> having to first eliminate this binder? In other words, is there a way to
> prove the theorem test below WITHOUT using intros / destruct?

Nope. To understand why, use Show Proof. before Qed. You can see that
the proof object has to case on n in order to return an object of the
correct type (leb 0 0=leb 0 (S n) vs. leb 0 n'=leb 0 n).

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

[Coq-Club] Transformations under a binder, JAEGER, Eric (SGDN)
- Re: [Coq-Club] Transformations under a binder, Taral
- Re: [Coq-Club] Transformations under a binder, Matthieu Sozeau
  - [Coq-Club] Coq connecting to other provers, Benedikt . AHRENS
    - Re: [Coq-Club] Coq connecting to other provers, Yves Bertot
      - Re: [Coq-Club] Coq connecting to other provers, Thery Laurent