## Stream: math-comp users

### Topic: remember in SSReflect

#### 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.

#### 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`.

#### 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