Théo Winterhalter (Dec 16 2020 at 20:05): Théo Winterhalter (Dec 16 2020 at 20:05):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
Kenji Maillard (Dec 16 2020 at 20:07):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
Théo Winterhalter (Dec 16 2020 at 20:10):Oh but pattern in is not documented, I did not know it was possible.
Fabian Kunze (Dec 16 2020 at 20:14):it might be documented here? https://coq.inria.fr/refman/proof-engine/tactics.html#conversion-tactics-applied-to-hypotheses
Théo Winterhalter (Dec 16 2020 at 20:21):Oh ok, I thought that each tactic had to implement the variant. Thanks!
Jason Gross (Jan 01 2021 at 13:49):I think you're looking for eval pattern x in y
Ana de Almeida Borges (May 18 2021 at 13:23):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?
Kenji Maillard (May 18 2021 at 13:34):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
Janno (May 18 2021 at 13:57):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.
Laurent Théry (May 18 2021 at 15:56):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: Oct 13 2024 at 01:02 UTC