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".

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

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

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 *)
```

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

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.
```

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`

.

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

Any ideas?

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

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

could this be an 8.13 vs 8.14 thing?

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

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.

Thanks, i'll try it out

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

Last updated: Jun 17 2024 at 22:01 UTC