## Stream: Coq users

### Topic: `let` bindings in hypotheses

#### Johannes Hostert (Mar 14 2024 at 15:05):

Hi all,

Is there a simple tactic to deal with a let binding in a hypothesis in a nice way? In particular, do this:

``````Lemma foo : forall k, let kk := k + k in 2 * k = kk. (* example with let *)
Proof.
(* note that intros / simpl and let work nicely together *)
intros k kk. simpl. now rewrite <- plus_n_O.
Qed.

Goal False.
Proof.
pose proof (H := foo 42). (* we use the example with let *)
(* find a nicer way to do this next line *)
pose (kk := 42 + 42). change (2 * 42 = kk) in H.
``````

but with manual `pose` and `change`? (my actual use case is a large formula)
`destruct` does not work since destructs the underlying equality, seeing right through the `let` :sad:

#### Gaëtan Gilbert (Mar 14 2024 at 15:30):

`set (kk := 42 + 42) in H. cbv zeta in H.` ? maybe a `match goal` can let you avoid having to write 42+42

#### Johannes Hostert (Mar 14 2024 at 15:43):

that kind of works, thanks. but it breaks if there's two let-binds
Is there a way in Ltac(2) to substitute the topmost bound variable of a gallina term?

Last updated: Jun 22 2024 at 15:01 UTC