关于Coq语言中二进制加法函数badd的正确性证明求助

Hey there! Let's work through this Coq binary addition proof step by step. First, I spot a problem with your badd function definition—let's fix that first, because as written, it won't behave like a correct binary adder. Then we'll build up the helper lemmas we need to prove the corrected function works correctly.

Your current badd implementation has a recursive logic error: both the true::l1 and false::l1 branches call badd l1 (badd l1 l2), which leads to incorrect results or infinite recursion. A correct least-significant-bit-first binary adder should handle bitwise addition with carry propagation. Here's a revised version that aligns with standard binary addition logic:

Fixpoint badd (l1 l2: list bool): list bool := 
match l1, l2 with 
| [], l => l 
| l, [] => l 
| true :: l1', true :: l2' => false :: bsucc (badd l1' l2')
| true :: l1', false :: l2' => true :: badd l1' l2'
| false :: l1', true :: l2' => true :: badd l1' l2'
| false :: l1', false :: l2' => false :: badd l1' l2'
end.

This version:

• Returns the non-empty list if one input is empty (adding zero to a number leaves it unchanged)
• Handles each bit pair explicitly:
  • Two trues sum to 0 with a carry of 1 (hence false :: bsucc (...))
  • A true and false sum to 1 with no carry
  • Two falses sum to 0 with no carry

Before tackling baddOK, we need a helper lemma to confirm bsucc correctly increments the value of a binary list. This will be key for handling carry cases in badd:

Lemma bsuccOK: forall l, value (bsucc l) = value l + 1.
Proof.
  induction l as [|b l IH].
  - (* Base case: empty list *)
    simpl. reflexivity.
  - (* Inductive case: split on the head bit *)
    destruct b.
    + (* Head is true *)
      simpl. rewrite IH. ring.
    + (* Head is false *)
      simpl. reflexivity.
Qed.

Breakdown of the proof:

1. Structural induction: We induct on the list l since bsucc is defined recursively over lists.
2. Base case: The empty list represents 0; bsucc [] gives [true], which has a value of 1 = 0 + 1.
3. Inductive case:
   • If the head is true, bsucc flips it to false and increments the rest of the list. The induction hypothesis lets us substitute value (bsucc l) with value l + 1, and ring simplifies the arithmetic.
   • If the head is false, bsucc flips it to true (directly adding 1 to the value), so we can immediately confirm equality.

Now we can prove the main correctness lemma for badd, using induction and our bsuccOK helper:

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.
Proof.
  induction l1 as [|b1 l1 IH1]; destruct l2 as [|b2 l2 IH2].
  - (* Both lists empty *)
    simpl. reflexivity.
  - (* l1 empty, l2 non-empty *)
    simpl. reflexivity.
  - (* l2 empty, l1 non-empty *)
    simpl. reflexivity.
  - (* Both lists non-empty: split on head bits *)
    destruct b1, b2.
    + (* true, true *)
      simpl. rewrite bsuccOK. rewrite IH1. ring.
    + (* true, false *)
      simpl. rewrite IH1. ring.
    + (* false, true *)
      simpl. rewrite IH1. ring.
    + (* false, false *)
      simpl. rewrite IH1. ring.
Qed.

Breakdown of the proof:

1. Base cases: When either list is empty, badd returns the other list. Since value [] = 0, the equation value (badd l1 l2) = value l1 + value l2 simplifies to value l = 0 + value l or vice versa, which is trivially true.
2. Inductive case: We split on all combinations of head bits:
   • For the true, true case, we use bsuccOK to expand the carry effect, then apply the induction hypothesis. The ring tactic handles the arithmetic simplification to show both sides are equal.
   • The remaining cases directly use the induction hypothesis and ring to verify the arithmetic equality between the sum of the binary values and the value of the badd result.

If you had a different recursive style in mind (like using repeated bsucc for carry propagation), the original code's recursion structure would need adjustment—right now, it creates a non-terminating cycle for non-empty inputs. Fixing that structure is a prerequisite for any correctness proof.

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