Coq证明中match结构的处理策略与可行性咨询

Awesome question—this is a super common scenario when working with Coq’s match expressions, and you’re totally on the right track! Let’s break this down clearly:

Short Answer #

Your proposed approach is completely feasible, and you don’t need to refactor your functions to make it work. The equality you’re thinking of (pushing F inside the match) is valid in Coq, and you can split the proof into two subgoals exactly as you described.

How to Do It in Practice #

Let’s say your current goal looks like this:

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

You have two straightforward paths to get to your split subgoals:

1. Direct Case Analysis (The Fastest Way) #

Instead of manually rewriting the match expression, use Coq’s case strategy directly on something m':

case (something m').

This will immediately split your goal into two separate subgoals:

• When something m' = true: Prove F (Y m') = Otherside m'
• When something m' = false: Prove F (Z m') = Otherside m'

This is exactly the outcome you wanted, and Coq handles the "pushing F inside the match" logic automatically behind the scenes.

2. Explicitly Prove the Match Distribution Equality #

If you want to first show that F (match ... end) equals match ... with ... => F ... end (maybe for clarity in your proof script), you can construct that equality directly with a match on something m':

refine (match something m' with | true => eq_refl | false => eq_refl end).

This works because in each branch, the two sides of the equality are definitionally equal—Coq can see they’re the same without extra work.

When Would Refactoring Make Sense? #

Refactoring isn’t required here, but it can simplify proofs in specific cases:

• If this exact match pattern pops up repeatedly across your code, extracting it into a helper function (e.g., Definition foo m' := match something m' with ... end) lets you use unfold foo to clean up goals quickly.
• If F and the match follow a common pattern (like functor or monad laws), refactoring might let you reuse existing library theorems instead of proving things from scratch.

But for your specific scenario? Skip the refactor—case analysis will get you where you need to go cleanly.

Quick Example to Demonstrate #

Here’s a concrete, minimal example of how this works in code:

Definition F (n : nat) := n + 1.
Definition Y (m' : nat) := m'.
Definition Z (m' : nat) := m' * 2.
Definition something (m' : nat) := m' > 0.
Definition Otherside (m' : nat) := if m' > 0 then m' + 1 else m' * 2 + 1.

Goal forall m', F (match something m' with true => Y m' | false => Z m' end) = Otherside m'.
Proof.
  intros m'.
  case (something m'); simpl.
  - reflexivity. (* Proves the true branch *)
  - reflexivity. (* Proves the false branch *)
Qed.

内容的提问来源于stack exchange，提问作者A Question Asker