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.

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`

.

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