Stream: math-comp users

Topic: remember in SSReflect


view this post on Zulip Sebastian Ertel (May 08 2024 at 08:12):

Dear SSReflect'ers,

What is the most idiomatic way to do what the remember tactic does in SSReflect?
The set tactic only introduces a definitional equality but not a propositional one.

view this post on Zulip Sebastian Ertel (May 08 2024 at 08:25):

What I have so far is this:

  set m := x in H;  have Heqm : m = 1. { by rewrite /m. }

where x is some subterm in H.

view this post on Zulip Kenji Maillard (May 08 2024 at 08:39):

The following could work

move Heqm:  x H => m H.

It generalizes x and H then introduce x as m together with an equation Heqm : x = m and reintroduce H.
But 1) you need to be able to push the hypothesis H in the goal (so this won't work if another hypothesis depends on H) 2) it may also capture the occurences of x in the goal. The latter might be mediated with explicit occurence switches, for instance move Heqm: {1}x H => m H..


Last updated: Jul 15 2024 at 21:02 UTC