cdepillabout (Nov 18 2021 at 05:48): cdepillabout (Nov 18 2021 at 05:48):I have an inductive type that looks like this:
Inductive nat_one : Type :=
| NO0
| NO1
| NOS (n : nat_one).
I'm working through a proof and I have a context like the following:
P : Prop
n : nat_one
I'm facing the following goal:
match n with
| NO0 | _ => P
end
Intuitively, it seems like Coq should be smart enough to see that regardless of what n is, it should be able to rewrite the goal to just P.
Is there some convenient tactic that can do this?
cdepillabout (Nov 18 2021 at 05:49):I'm a beginner at Coq (currently just a couple chapters into Software Foundations). I apologize if this question doesn't make any sense, or I am asking something completely wrong.
Pierre-Marie Pédrot (Nov 18 2021 at 07:11):Why don't you just destruct n?
cdepillabout (Nov 18 2021 at 09:26):I did end up using destruct n in my proof. It worked.
But I was mostly just wondering if there was some tactic that was smart enough to rewrite match n with | NO0 | _ => P end to P. I would have guessed simpl would do this, but it doesn't appear to be able to.
Théo Winterhalter (Nov 18 2021 at 09:31):simpl will just perform computation. A match expression won't reduce away unless it's argument is a constructor. So that wouldn't be expected of simpl.
Théo Winterhalter (Nov 18 2021 at 09:32):Reasoning about match in generality isn't easy to do, and it's probably easier to do it on a case by case basis.
cdepillabout (Nov 18 2021 at 09:33):Thanks, that does makes sense.
It sounds like there is probably not a tactic like I'm hoping for, and destruct is my best bet!
Paolo Giarrusso (Nov 19 2021 at 19:34):You can also use "assert P" or "enough P", which splits your proof: one branch must prove your goal from P (e.g. via "now destruct P"), the other actually proves P.
cdepillabout (Nov 20 2021 at 14:02):Oh that's smart. That's a tad bit more manual than I was hoping for, but it does sound roughly like what I wanted!
Last updated: Oct 13 2024 at 01:02 UTC