Stream: Coq users

Topic: introduce "let" in definition in context


view this post on Zulip 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 := ( - 4 * a * c) in
  forall x, (a *  + b * x + c = a * ((x + b / (2 * a))² - delta / (4 * ))).
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 *  + 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 :=  - 4 * a * c in
     forall x : R,
     a *  + b * x + c = a * ((x + b / (2 * a))² - delta / (4 * ))

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

exists alpha : R, forall x : R, x > alpha -> a *  + 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.

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

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