Stream: Coq users

Topic: Match let in Ltac


view this post on Zulip Jacob Salzberg (Dec 17 2023 at 04:03):

Hi,
I want to match a hypothesis of the form
H: let (?x, ?y) := ?p in...
But let is ltac syntax.
How do you match let in ltac?
Thanks.

view this post on Zulip Jacob Salzberg (Dec 17 2023 at 17:48):

For example, this doesn't work:

Ltac destruct_let :=
  match goal with
    | [H : (let _ := ?y in _) |- _] => destruct y
  end.

Definition tactest : forall p : Prop * Prop, forall z : (let (x, y) := p in x), False.
  { intros. destruct_let.  }

view this post on Zulip Gaëtan Gilbert (Dec 17 2023 at 17:49):

let (x, y) := p in x is not a let, it's just a builtin notation for match

view this post on Zulip Jacob Salzberg (Dec 17 2023 at 18:00):

thanks @Gaëtan Gilbert , but

Ltac destruct_let :=
  match goal with
  | [H : (match _ with | ?y => ?z end) |- _] => destruct y
  end.

doesn't work either...


Last updated: Jun 13 2024 at 19:02 UTC