Is it possible to do something similar to the `pattern`

tactic but for a subterm of the goal and not the whole goal?

The documentation doesn't seem to allow it: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.pattern

I think I managed to do something like that with a combination of ssreflect's `set h := pattern_for_subterm_in_goal.`

and then using `pattern ... in h`

Oh but `pattern in`

is not documented, I did not know it was possible.

it might be documented here? https://coq.inria.fr/refman/proof-engine/tactics.html#conversion-tactics-applied-to-hypotheses

Oh ok, I thought that each tactic had to implement the variant. Thanks!

I think you're looking for `eval pattern x in y`

I have a goal of the form `is_true (long_expression_depending_on_x)`

. I want to isolate the function `f : nat -> bool`

such that my goal is convertible to `is_true (f x)`

. I thought this thread would provide the answer, but I got stuck. Here is an example:

```
Require Import ssreflect.
Variable x : nat.
Goal is_true (Nat.eqb (x + x + x) (3 * x)).
Proof.
set t := (X in is_true X).
pattern x in t.
set f : nat -> bool := (f in f _) in t *.
Abort.
```

The context becomes

```
f := Nat.eqb (x + x + x) : nat -> bool
t := f (3 * x) : bool
```

instead of my desired

```
f := fun x => Nat.eqb (x + x + x) (3 * x) : nat -> bool
t := f x : bool
```

I also tried some other things, one of which lead to an anomaly. Is there a way of achieving this?

Using 2nd order pattern matching in Ltac seems to do the job if needed:

```
Require Import ssreflect.
Variable x : nat.
Goal is_true (Nat.eqb (x + x + x) (3 * x)).
Proof.
set t := (X in is_true X).
pattern x in t.
let u := eval cbv delta [t] in t in
match u with
| (fun z => @?h z) _ => set f := h
end.
```

It works, thank you! Looks like black magic to my eyes

Here's a version based on unification:

```
set t := (X in is_true X).
pattern x in t.
evar (f: nat -> bool);
let t := (eval cbv delta [t] in t) in
unify (?f x) t.
replace t with (f x) by reflexivity.
```

Interestingly I have to do the unfolding of `t`

manually because unification combines unfolding and beta reduction which leads it to unify `?f`

with `Nat.eqb (x + x + x)`

and `x`

with `3 * x`

.

what about?

```
Goal is_true (Nat.eqb (x + x + x) (3 * x)).
Proof.
set t := (X in is_true X).
pattern x in t; move: @t.
set f := (X in X x) => /=.
```

wonderful! we can make this an ssrlike tactic

```
Require Import ssreflect ssrmatching.
Tactic Notation "dset" ident(f) ssrpatternarg(x) ":=" ssrpatternarg(p) :=
let t := fresh "t" in let s := fresh "s" in
ssrpattern p; ssrpattern x => s t; pattern s in t;
move: @t; set f := (f in f s); rewrite {}/s.
Goal is_true (Nat.eqb (x + x + x) (3 * x)).
Proof.
dset f x := (X in is_true X).
```

@Enrico Tassi it would be better if it were native though, with multiple argument selection à la `elim: arg1 arg2 ... /`

... but with the above syntax (like `set f {1 2}x (y in Nat.eqb _ y) := (X in is_true X)`

which would lead to `f n y := Nat.eqb (n + n + x) y`

for example). I think I've been a client of this one for a long time :laughter_tears:

NB: @Enrico Tassi I tried to use

```
Lemma dset X T P x (g : X -> T) : (let f := g in P x (f x)) -> P x (g x).
```

combined with `elim/dset: x (X in is_true X)`

but it does not work...

Last updated: Jun 16 2024 at 02:41 UTC