Stream: Coq users

Topic: Using pattern tactic in a subterm


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 20:10):

Oh but pattern in is not documented, I did not know it was possible.

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 20:21):

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

view this post on Zulip Jason Gross (Jan 01 2021 at 13:49):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (May 18 2021 at 13:39):

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

view this post on Zulip 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.

view this post on Zulip 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) => /=.

view this post on Zulip Cyril Cohen (May 20 2021 at 02:03):

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: Feb 09 2023 at 00:03 UTC