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
Is there some convenient tactic that can do this?
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.
Why don't you just
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.
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
match in generality isn't easy to do, and it's probably easier to do it on a case by case basis.
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!
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.
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 01 2023 at 17:01 UTC