The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

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