CODEWITHSUNDEEP
coq
A Question Asker
A Question Asker

Reputation: 3311

How to deal with match in a Coq proof

I'm wondering what are strategies to deal with matches in proof. For example, I have something in the following form:

F match something m' with
  | true => Y m'
  | false => Z m'
  end=Otherside m'

It feels like there should be a number of ways to deal with this...I imagine that it might be possible to refactor things upstream to avoid, but it also feels like the following should be true

match something m' with
| true => F (Y m')
| false => F (Z m')
end=Otherside m'

And then you should be able to to do something like break this into two subgoals, where if

F (Y m')=Otherside m'
F (Z m')=Otherside m'

Then you are good to go.

Is this possible? Or do I need to refactor my functions?

Upvotes: 3

Views: 525

Answers (1)

HTNW
HTNW

Reputation: 29148

This doesn't go through your intermediate step, but you get to your two goals simply by

destruct (something m').

If that term is too big to write, I suppose you can pull it out like so:

match goal with |- _ match ?S with _ => _ end = _ => destruct S end.

or even

match goal with |- context[match ?S with _ => _ end] => destruct S end.

Upvotes: 3

Related Questions