The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

I think you can prove something like

exists x, P(x) /\ (P(x) -> Q(x))

then it is tedious to show

exists x, P(x) /\ Q(x)

in particular, the latter does not require inspection of P(x)

in this particular example:

Lemma monSlider_state {A : Type} : forall mon buf sc l,
    length l > 0 ->
    length buf > 0 ->
    forall bs mon', (eval4 mon l) = (bs, mon') ->
    forall slb' slmon', (eval2 (monSlider mon buf sc) l) = (slb', slmon') ->
    exists buf', buf' = firstn (length buf) (bs ++ buf)
        /\ slmon' = @monSlider A mon' buf' sc
        /\ length buf' = length buf
        /\ (slmon' = @monSlider A mon' buf' sc -> slb' = sc buf').

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Roger Witte <rogerwite AT yahoo.co.uk>
Sent: March 24, 2020 12:24 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proving a multi-part theorem where later parts are a consequence of others

 

You can use the Section Mechanism to make assumptions and proofs sequentially (using Let instead of Lemma) and then have your Lemma statement before the end of section containing the local symbols

Sent from Yahoo Mail on Android

On Tue, 24 Mar 2020 at 16:19, Théo Winterhalter

<theo.winterhalter AT ens-cachan.fr> wrote:

One way is to define a tactic that does it for you:

Ltac split_rem_left h :=

match goal with

| |- ?A /\ ?B =>

assert A as h ; [

| split ; [

exact h

|]

]

end.

Goal forall A B C, A /\ B /\ C.

Proof.

intros A B C.

split_rem_left hA.

- admit.

- split_rem_left hB.

+ admit.

+ admit. (* hA : A, hB : B ⊢ C *)

Abort.

Le 24 mars 2020 à 17:09, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> a écrit :

Often it is customary to phrase a theorem in a way that has multiple parts and each of the parts depend on the others and they may additionally introduce new variables.

For example,

For all sequences s of real numbers,

 s is increasing ->

 for all real number b, s is bounded above by b ->

    exists real number l,

       l = sup(s)

       /\ s converges to l

       /\ s is a cauchy sequence.

One might prove "s is a cauchy sequence" by appealing to some "s converges to l" (and some other theorem which says convergent sequences are Cauchy) but when they switch to the last conjunct, the previous conjuncts are not directly accessible.

How does one get around this issue?

One way might be to write two different lemmas: One talking about the first two conjuncts, and the second talking about just the third. However, this is ugly because in the second lemma one has to repeat a lot of boilerplate in order to even define what l is.

Is there a cleaner way to do this? Any tactics or patterns to make coq remember older conjuncts?

For reference, my actual theorem looks like this:

Lemma monSlider_state {A : Type} : forall mon buf sc l,
    length l > 0 ->
    length buf > 0 ->
    forall bs mon', (eval4 mon l) = (bs, mon') ->
    forall slb' slmon', (eval2 (monSlider mon buf sc) l) = (slb', slmon') ->
    exists buf', buf' = firstn (length buf) (bs ++ buf)
        /\ slmon' = @monSlider A mon' buf' sc
        /\ length buf' = length buf
        /\ slb' = sc buf'.

The proof of `slb' = sc buf'` depends on the fact that `slmon' = @monSlider A mon' buf' sc` but this fact is not accessible when I am proving the last conjunct.

--Agnishom