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: Jun 14 2024 at 17:02 UTC