Patrick Nicodemus (Nov 16 2021 at 21:17): 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 *)
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.
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: Apr 19 2024 at 14:02 UTC