The Coq mailing list

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

Thanks.

I am still having some difficulties. In my proof, I am working with a lattice, so I have finite meets and finite joins. So, for example join_b lo hi f = f lo `join` f (lo + 1) `join` ... `join` f hi. I have the following theorem.

Lemma join_b_ext {A : Type} `{Lattice A} `{BoundedLattice A} (lo hi : nat) (f g : nat -> A)
    : (forall a, f a = g a) -> join_b lo hi f = join_b lo hi g.

Now, let's say I have the following goal in some theorem:

 bottom =
  join_b lo (Init.Nat.min i lo)
    (fun j : nat => join_b 0 (Init.Nat.min (i - j) 0) (fun j0 : nat => robustness ϕ τ (i - j - j0)))

I want to rewrite the (Init.Nat.min (i - j) 0) as just 0. Trying `under join_b_ext do replace (min (i-j) 0) with 0.` does not help because `Error: The reference j was not found in the current environment.`

I understand the error, but what is the best way to deal with this?

On Wed, Jul 8, 2020 at 4:01 PM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

On 7/8/20 10:37 PM, Agnishom Chattopadhyay wrote:
> Does loading ssreflect change the standard behaviour of tacticals like
> in/by/with/etc? This is a problem since a large part of my proof script
> uses things like rewrite H in H0.

yes it does, it is explained in

https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html

in particular rewrite has a slighy different semantics
but has some extra capability like a powerful pattern selection.

If you want to do use the standard rewrite, just add <- in front the
first theorem. So rewrite ->H in H0 should work.

--
Laurent