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: Oct 13 2024 at 01:02 UTC