Coq中证明negb_is_not定理遇False无法证明的解决方法咨询

Let's walk through fixing your proof step by step. The core issue here is that once you start case-analyzing a (since it's a boolean with only two possible values: true and false), you need to explicitly handle each subgoal by leveraging the definitions of Is_true, negb, and logical negation.

First, let's recap the key definitions for context:

• Is_true b is defined as b = true
• negb b returns false when b is true, and true when b is false
• Logical negation ~P is shorthand for P → False

Complete Proof with Step-by-Step Explanations #

Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).
Proof.
  intros a. (* Bring the boolean `a` into our proof context *)
  unfold iff. (* Split the biconditional into two separate implications to prove *)
  refine (conj _ _). (* We'll tackle the forward and reverse directions one by one *)

  (* First direction: Is_true (negb a) → ¬Is_true a *)
  case a. (* Split into two subgoals based on `a` being `true` or `false` *)
  - (* Subgoal: Is_true (negb true) → ¬Is_true true *)
    simpl. (* Simplify `negb true` to `false`, making the goal `Is_true false → ¬Is_true true` *)
    unfold Is_true. (* Expand definitions: `false = true → ¬(true = true)` *)
    unfold not. (* Unpack negation: `false = true → (true = true → False)` *)
    intros H. (* Assume the contradiction `false = true` *)
    intros H0. (* Assume the trivial `true = true` from the negation's premise *)
    exact H. (* Use the contradictory assumption to prove False directly *)
  - (* Subgoal: Is_true (negb false) → ¬Is_true false *)
    simpl. (* Simplify `negb false` to `true`, goal becomes `Is_true true → ¬Is_true false` *)
    unfold Is_true. (* Expand to `true = true → ¬(false = true)` *)
    unfold not. (* Unpack to `true = true → (false = true → False)` *)
    intros H. (* Grab the trivial `true = true` assumption (we won't need it) *)
    intros H0. (* Assume the contradiction `false = true` *)
    exact H0. (* This assumption is already a contradiction—use it to prove False *)

  (* Second direction: ¬Is_true a → Is_true (negb a) *)
  unfold not. (* Unpack negation: `(Is_true a → False) → Is_true (negb a)` *)
  intros H. (* Assume the premise: if `Is_true a` holds, we can derive False *)
  case a. (* Split again into `a = true` and `a = false` *)
  - (* Subgoal: (Is_true true → False) → Is_true (negb true) *)
    simpl. (* Simplify to `(true = true → False) → Is_true false` *)
    unfold Is_true. (* Expand to `(true = true → False) → (false = true)` *)
    intros H0. (* Grab the assumption that `true = true` leads to False *)
    apply H0. (* To get `false = true`, we just need to feed `true = true` into H0 *)
    exact eq_refl. (* `true = true` is a trivial equality we can prove with `eq_refl` *)
  - (* Subgoal: (Is_true false → False) → Is_true (negb false) *)
    simpl. (* Simplify to `(false = true → False) → Is_true true` *)
    unfold Is_true. (* Expand to `(false = true → False) → (true = true)` *)
    exact eq_refl. (* `true = true` is always true, no need to use the premise *)
Qed.

Key Fixes for Your Bottleneck #

1. Finish case analysis: You started case A but didn't explicitly handle both true and false subgoals. For boolean values, case (or destruct) always breaks the proof into simple, manageable parts.
2. Unfold definitions strategically: When goals look opaque, unfolding Is_true and not makes the logical structure explicit, so you can see exactly what you need to prove.
3. Leverage contradictions: Assumptions like false = true are direct contradictions—you can use them immediately to prove False.
4. Use trivial equalities: eq_refl proves any term is equal to itself, which is essential for handling the true = true cases that pop up.

For similar boolean proofs, remember that case analysis on the boolean is almost always the first step—since booleans have a finite number of values, this turns complex goals into easy-to-solve subproblems.

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