Stream: Coq users

Topic: As intro pattern

Kenji Maillard (Feb 24 2023 at 10:47):

Sometimes when I use intros with a destructuring pattern I would like to name and keep some intermediate term as a transparent definition, e.g.

Goal forall {A B C}, A * B * C -> True.
Proof.
  (* what I can currently do *)
  intros ??? [[a b] c]. pose (x := (a,b)).
  (* what I would like to do: no explicit naming of the destructured components required, nor rebuilding the possibly large term *)
  intros ??? [([??] as x) ?].

Is there a way to hack some tactic notation to get this kind of behaviour ?

Kenji Maillard (Feb 24 2023 at 10:56):

Ok, one way to get that behaviour is to just bind a variable and use pose + destruct:

  intros ??? [x c].
  let x' := fresh "x" in rename x into x'; pose (x := x'); destruct x' as [??].
  (* Is it possible to write a tactic notation to have `split z as pat.` expand to the tactic above for z:= x and pat := [??] ?*)

Pierre Roux (Feb 24 2023 at 10:58):

Don't know about Ltac, in ssreflect there is /[dup] that may help

Kenji Maillard (Feb 24 2023 at 11:13):

I thought about /[dup] but that loses the definition of pattern. Though there is probably some way to add another notation in ssr_ipat to do what I have in mind..

Pierre Roux (Feb 24 2023 at 11:56):

Have you tried combining it with + (and maybe multiple =>, just wild guess, I haven't tried).

Pierre Roux (Feb 24 2023 at 11:59):

(nevermind, I see what you want now, sorry no idea)

Last updated: Oct 13 2024 at 01:02 UTC