Stream: Coq users

Topic: `let` bindings in hypotheses


view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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