通过简单定理证明理解Coq：andb_true_elim2证明失败求助

Hey there! Let's break down why your proof is hitting that error and get it working properly.

First, let's pinpoint the root issue in your current code:

Proof. intros b c. destruct c. - destruct b. + reflexivity. + reflexivity. - destruct b. + reflexivity. + reflexivity. Qed.

You forgot to introduce the critical premise of the theorem: andb b c = true. That's the key assumption we need to rule out impossible cases! Without it, when you destruct c into false, you're left trying to prove false = true with reflexivity—which is obviously impossible, hence the error about not being able to unify true and false.

Correct Proof Approach #

Let's rewrite the proof properly, using the premise to eliminate contradictory cases. Here's a straightforward version:

Theorem andb_true_elim2 : forall b c : bool, andb b c = true -> c = true.
Proof.
  (* Introduce all variables AND the key premise H: andb b c = true *)
  intros b c H.
  destruct c as [|].
  - (* Case 1: c = true *)
    reflexivity. (* Directly true by definition *)
  - (* Case 2: c = false *)
    (* When c is false, andb b false is always false, which contradicts H *)
    simpl in H. (* Simplify H to get false = true *)
    discriminate H. (* This rule eliminates contradictory assumptions *)
Qed.

What's Happening Here? #

1. intros b c H: This pulls in both boolean variables and the critical assumption H that andb b c equals true. We can't make progress without leveraging this!
2. Destructing c:
   • When c is true, our goal is true = true—reflexivity works perfectly here.
   • When c is false, we use simpl in H to reduce andb b false to false, turning H into false = true. The discriminate tactic tells Coq this is a contradiction, so this case can't exist, and we can dismiss it entirely.

Another Alternative (Destructing b First) #

If you prefer to break down b instead of c, this works just as well:

Theorem andb_true_elim2 : forall b c : bool, andb b c = true -> c = true.
Proof.
  intros b c H.
  destruct b as [|].
  - (* Case 1: b = true *)
    simpl in H. (* H becomes c = true *)
    assumption. (* Use H directly to prove the goal *)
  - (* Case 2: b = false *)
    simpl in H. (* H becomes false = true *)
    discriminate H. (* Contradiction, so case is invalid *)
Qed.

The core takeaway here is always remember to introduce and use your premises—they're not just there for show! Coq can't infer which assumptions to use on its own; you have to explicitly work with them to narrow down valid cases.

内容的提问来源于stack exchange，提问作者Waiting for Dev...