Stream: Coq users

Topic: match in proof where all branches return same prop


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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2021 at 07:11):

Why don't you just destruct n?

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

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

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

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

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

view this post on Zulip 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: Feb 08 2023 at 22:03 UTC