## Stream: Coq users

### Topic: introduce "let" in definition in context

#### Pierre Rousselin (Oct 13 2023 at 07:13):

I was playing around with degree 2 polynomials:

``````Lemma deg2_poly_canonical (a b c : R) : a <> 0 ->
let delta := (b² - 4 * a * c) in
forall x, (a * x² + b * x + c = a * ((x + b / (2 * a))² - delta / (4 * a²))).
Proof. intros H delta x; subst delta; unfold Rsqr; field; exact H. Qed.

Lemma deg2_poly_neg_a_evtly_neg (a b c : R) : a < 0 ->
exists alpha, (forall x, x > alpha -> a * x² + b * x + c < 0).
Proof.
intros H; assert (Hn0 : a <> 0) by (now apply Rlt_not_eq).
pose proof (deg2_poly_canonical a b c Hn0) as Eq.
``````

Now, the proof state is:

``````a, b, c : R
H : a < 0
Hn0 : a <> 0
Eq : let delta := b² - 4 * a * c in
forall x : R,
a * x² + b * x + c = a * ((x + b / (2 * a))² - delta / (4 * a²))

========================= (1 / 1)

exists alpha : R, forall x : R, x > alpha -> a * x² + b * x + c < 0
``````

What I would like to do is `do_something_with Eq` such that `delta` appears with its let-in definition in the context so that I don't have to write it manually. In math this would be "let delta be as in Lemma deg2_poly_canonical".
Is there an easy way to do so? Bonus points if it can be done with an intro pattern at the time of `pose proof`.

#### Pierre Courtieu (Oct 13 2023 at 08:43):

Hi. If you know that the `let` is the top construct of you hypothesis you can write an tactic for this:

``````Require Import Utf8.
Lemma foo: ∀ x y:nat, (let delta := x + y in delta < delta * 2) -> True.
Proof.
intros x y H.
match type of H with
(let xxx := ?c in ?a) =>
pose (xxx := c)
end.
``````

#### Gaëtan Gilbert (Oct 13 2023 at 08:44):

sounds similar to https://github.com/coq/coq/issues/17554

Last updated: Jun 18 2024 at 22:01 UTC