The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

you can do this by hand

after your exists, you first assert :

assert (H : s is a cauchy sequence)

then do your split so the assumpition appears in every subgoal.

or you can prove the general lemmas

Lemma and_r (A B : Prop) : B -> (B -> A) -> (A /\ B).

Lemma and_l (A B : Prop) : A -> (A -> B) -> (A /\ B).

and use them instead of the tactic split

--
Laurent


On 3/24/20 5:09 PM, Agnishom Chattopadhyay wrote:
> 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