## Stream: Coq users

### Topic: Using 'set' and similar tactics

#### Patrick Nicodemus (Nov 16 2021 at 21:17):

Hello. I am wondering how to use the set tactic to replace a subterm using pattern matching that describes not the subterm itself but what surrounds the subterm. For example if my goal is an equation expr1 =expr2 , I would like to know how to do "set B : Z " where Z captures expr2 by describing it as "the right hand side of the equality".

#### Patrick Nicodemus (Nov 16 2021 at 21:18):

This is probably a standard question so any tutorials on pattern matching in coq would be helpful. I find it hard to read the formal syntax in the coq documentation

#### Patrick Nicodemus (Nov 16 2021 at 21:26):

I am trying to use "let" but it just says that equality is not an inductive type.

#### Kenji Maillard (Nov 16 2021 at 21:43):

Do you mean setting a variable as follows ? (this example uses ssreflect's `set`)

``````From Coq Require Import ssreflect.
Goal forall n m p : nat, n = m + p.
Proof.
intros. (* Goal is n = m + p *)
set Z := (x in _ = x). (* Goal is n = Z *)
``````

#### Patrick Nicodemus (Nov 16 2021 at 21:50):

Yeah, this looks like what I want. Is there a way to do this without importing ssreflect? I guess it's not a big deal I'm just adhering to a certain style guide for the code i'm writing and idk if they'd want me importing these libraries, it's probably fine

#### Kenji Maillard (Nov 16 2021 at 21:55):

yes of course:

``````Goal forall n m p : nat, n = m + p.
Proof.
intros. (* Goal is n = m + p *)
match goal with
| [ |- _ = ?x ] => set (Z := x)
end.
``````

#### Kenji Maillard (Nov 16 2021 at 22:00):

The `match goal` construct has a strange syntax but allows to analyze both the goal and the hypothesis of your proof state.
Here I'm matching on the shape of the goal (so I put a pattern on the right of `|-`), with top constructor `=`. I disregard the left-hand side of `=` with the wildcard `_` and bind the right hand side to the variable `x` with `?x`.

#### Patrick Nicodemus (Nov 16 2021 at 22:03):

Ok. I'm getting the error `[match_hyp] expected after '[' (in [match_context_rule])`
Any ideas?

#### Patrick Nicodemus (Nov 16 2021 at 22:03):

I'll take a look at the match goal documentation.

#### Kenji Maillard (Nov 16 2021 at 22:14):

Without a look at your script, I don't really have a clue.

#### Patrick Nicodemus (Nov 16 2021 at 22:30):

could this be an 8.13 vs 8.14 thing?

#### Patrick Nicodemus (Nov 16 2021 at 22:31):

i'd gladly post my script but i don't see how anything in the surrounding code would interact with it.

#### Paolo Giarrusso (Nov 16 2021 at 22:46):

it’s unlikely to be about 8.14 vs 8.13, but it could be affected by syntax extensions from your dependencies; can you confirm that Kenji’s example works for you in an empty file? Does it still work after importing your dependencies? If not, it’s a syntax extension problem.

#### Patrick Nicodemus (Nov 16 2021 at 22:51):

Thanks, i'll try it out

#### Patrick Nicodemus (Nov 16 2021 at 22:59):

Forget it, lol, I restarted emacs/proof general and it works fine now.

Last updated: Jan 29 2023 at 05:03 UTC