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?

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 `destruct n`

?

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 `simpl`

.

Reasoning about `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: Jun 15 2024 at 05:01 UTC