Stream: Coq users

Topic: Using 'set' and similar tactics


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

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

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

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

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

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

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

view this post on Zulip Patrick Nicodemus (Nov 16 2021 at 22:03):

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

view this post on Zulip Patrick Nicodemus (Nov 16 2021 at 22:03):

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

view this post on Zulip Kenji Maillard (Nov 16 2021 at 22:14):

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

view this post on Zulip Patrick Nicodemus (Nov 16 2021 at 22:30):

could this be an 8.13 vs 8.14 thing?

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

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

view this post on Zulip Patrick Nicodemus (Nov 16 2021 at 22:51):

Thanks, i'll try it out

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