Kenji Maillard (Oct 24 2020 at 13:53): Kenji Maillard (Oct 24 2020 at 13:53):I'm trying to use the pattern tactic to deal with difficult to handle dependent goals where the standard automated solutions (Program's dependent destruction or Equations's depelim) do not work (because there is some SProp in the middle and that does not play well with the way these tools handle dependency by throwing in equalities).
The manual describes a variant of the pattern tactic abstracting multiple terms, and explains that the tactic abstracts each terms in turn from right to left, but it says nothing about the occurrence selectors.
From the small snippet below, it looks like the order of these occurrences is important, but I can't exactly figure out when it should work or not. In particular how can the last invocation (that works) be different from the 2 precedent invocations that fail ?
Goal forall X (f : X -> nat) (g : forall Y, Y -> nat) (x y : X), f x = g X y.
intros X f g x y.
(*Expected : the X in g X y shouldn't be abstracted *)
Fail pattern X, f, x.
(* X is abstracted in f before being abstracted in x *)
Fail pattern X at 1, 2, f, x.
(* Illegal application: The term "n0" of type "T -> nat" cannot be applied to the term "x0" : "X" *)
(* This term has type "X" which should be coercible to "T". *)
(* X is abstracted in x before being abstracted in f *)
Fail pattern X at 2, 1, f, x.
(* Illegal application: The term "n0" of type "X -> nat" cannot be applied to the term "x0" : "T" *)
(* This term has type "T" which should be coercible to "X". *)
(* There are only 3 occurences of X *)
Fail pattern X at 4, f, x.
(* Invalid occurrence number: 4. *)
(* Magic ! The two occurences are abstracted at once *)
pattern X at -3, f, x.
In particular, is there any solution when there are multiple occurrences that I want to abstrat away and also multiple occurrences that I want to leave as they are as in this slightly modified example ?
Goal forall X (f : X -> nat) (h : forall Y, Y -> Y) (g : forall Y, Y -> nat) (x y : X), f x = g X (h X y).
intros X f h g x y.
Fail pattern X at - 3, 4, f, x.
It managed to cook up a solution for my actual problem with ssreflects set to change selectively the subterms that shouldn't be abstracted away by pattern + some second order Ltac pattern matching but I would still be interested in a more robust solution.
Last updated: Apr 20 2024 at 08:02 UTC