在Coq中分解含match表达式的构造子等式

Hey, let's work through this proof problem step by step. You're dealing with an equality involving a recursively defined function with nested matches, and we can break this down using Coq's induction tactics and helper lemmas to eliminate the impossible branches.

First, let's recap your code for clarity:

Fixpoint positive (n : nat) := 
  match n with 
  | O => Some O 
  | S n => match positive n with 
           | Some n => Some (S n) 
           | None => None (* Note that this never happens *) 
           end 
  end.

Lemma positiveness : forall n : nat, Some (S n) = positive (S n).
Proof.
intro. simpl.
(* Context: n : nat, Goal: Some (S n) = match positive n with Some n0 => Some (S n0) | None => None end *)

The Core Issue #

After simpl, your goal has a match on positive n. Your comment notes the None branch never triggers, so we just need to formalize that fact and use it to simplify the match.

Approach 1: Induction (Cleanest for Recursive Functions) #

Since positive is recursively defined, induction is the most natural fit here. It lets us reuse the property for smaller values of n to prove it for larger ones:

Lemma positiveness : forall n : nat, Some (S n) = positive (S n).
Proof.
induction n.
- (* Base case: n = O *)
  simpl. reflexivity. (* positive (S O) expands directly to Some (S O), matching the left side *)
- (* Inductive case: n = S n' *)
  simpl. rewrite IHn. reflexivity. 
  (* IHn tells us Some (S n') = positive (S n'), so substituting that into the match turns it into Some (S (S n')), which equals the left side *)
Qed.

Approach 2: Use a Helper Lemma to Eliminate the None Branch #

If you want to stick with your original proof flow (after intro + simpl), first prove a helper lemma that guarantees positive n always returns a Some variant:

Lemma positive_always_Some : forall n : nat, exists k : nat, positive n = Some k.
Proof.
induction n.
- (* n = O *) exists O. reflexivity.
- (* n = S n' *) destruct IHn as [k Hk]. rewrite Hk. reflexivity.
Qed.

Then use this to destruct the match and discard the impossible None branch:

Lemma positiveness : forall n : nat, Some (S n) = positive (S n).
Proof.
intro n. simpl.
destruct (positive n) as [k | ] eqn:H.
- (* Branch 1: positive n = Some k *)
  (* Now we just need to show k = n, which we can prove with another quick induction *)
  assert (Hk : k = n). {
    induction n.
    - reflexivity.
    - simpl in H. rewrite IHn in H. inversion H. reflexivity.
  }
  rewrite Hk. reflexivity.
- (* Branch 2: positive n = None *)
  (* Use our helper lemma to show this is impossible *)
  pose proof (positive_always_Some n) as Hsome.
  inversion Hsome. contradiction.
Qed.

Approach 3: Directly Prove positive n = Some n #

An even more straightforward helper lemma is that positive n exactly returns Some n for all n. This lets us substitute directly into the match:

Lemma positive_eq_Some_n : forall n : nat, positive n = Some n.
Proof.
induction n.
- reflexivity.
- simpl. rewrite IHn. reflexivity.
Qed.

Lemma positiveness : forall n : nat, Some (S n) = positive (S n).
Proof.
intro n. simpl. rewrite positive_eq_Some_n. reflexivity.
Qed.

Key Takeaways for Match Expression Equality #

• Induction: Always start with induction when dealing with recursively defined functions—it aligns perfectly with the function's structure.
• Helper Lemmas: Formalize any "obvious" properties (like impossible branches or exact return values) to simplify your goal.
• Destruct + Eqn: Use destruct ... eqn:H to break down match expressions and record the equality for each branch, then eliminate impossible cases with contradiction or helper lemmas.

内容的提问来源于stack exchange，提问作者user1544337