The Coq mailing list

[Jan Bessai <jan.bessai AT tu-dortmund.de>]

Would it be possible for you to prove several lemmas without boilerplate
by collecting your premisses as the variables of a Section?

Section IncreasingReals.
  Variable s : RealSequence.
  Hypothesis increasing: s is increasing.
  Variable b: Real.
  Hypothesis sBounded: s is bounded above by b.
  
  Lemma sup_s_real: IsReal (sup(s)).
  Lemma s_converges: s converges to sup(s).
  Lemma s_cauchy: s is a cauchy sequence.
End Section.

On Tue, Mar 24, 2020 at 11:09:23AM -0500, 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