WS0018

signed_table_add_reassociate

Constructing the other parenthesization and applying literal signed-add functionality proves reverse associativity.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Operation tables contain actual beta-coded entries and compare represented signed values, not encodings. The strict sum window is i<l and the separately certified endpoint i=l is unused. Rectangular Fubini and full finite signed Möbius inversion are separate, now-admitted families.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ ab. ∀ bc. ∀ out. SignedAdd(a,b,ab) → SignedAdd(b,c,bc) → SignedAdd(a,bc,out) → SignedAdd(ab,c,out)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedAdd(a,b,c) · 5

Actual proof prerequisites

signed_add_total · checked external prerequisitesigned_add_functional · checked external prerequisitesigned_add_associative · checked external prerequisite
Original expanded first-order statement 
forall a b c ab bc out. (exists dsa_ap_reverse_ab dsa_an_reverse_ab dsa_bp_reverse_ab dsa_bn_reverse_ab dsa_cp_reverse_ab dsa_cn_reverse_ab. (((((a) = 2 * (dsa_ap_reverse_ab) /\ (dsa_an_reverse_ab) = 0) \/ exists ge_signed_half_reverse_ableft. (((a) = 2 * ge_signed_half_reverse_ableft + 1 /\ (dsa_ap_reverse_ab) = 0) /\ (dsa_an_reverse_ab) = S ge_signed_half_reverse_ableft))) /\ ((((((b) = 2 * (dsa_bp_reverse_ab) /\ (dsa_bn_reverse_ab) = 0) \/ exists ge_signed_half_reverse_abright. (((b) = 2 * ge_signed_half_reverse_abright + 1 /\ (dsa_bp_reverse_ab) = 0) /\ (dsa_bn_reverse_ab) = S ge_signed_half_reverse_abright))) /\ ((((((ab) = 2 * (dsa_cp_reverse_ab) /\ (dsa_cn_reverse_ab) = 0) \/ exists ge_signed_half_reverse_aboutput. (((ab) = 2 * ge_signed_half_reverse_aboutput + 1 /\ (dsa_cp_reverse_ab) = 0) /\ (dsa_cn_reverse_ab) = S ge_signed_half_reverse_aboutput))) /\ ((dsa_ap_reverse_ab + dsa_bp_reverse_ab) + dsa_cn_reverse_ab = (dsa_an_reverse_ab + dsa_bn_reverse_ab) + dsa_cp_reverse_ab))))))) -> (exists dsa_ap_reverse_bc dsa_an_reverse_bc dsa_bp_reverse_bc dsa_bn_reverse_bc dsa_cp_reverse_bc dsa_cn_reverse_bc. (((((b) = 2 * (dsa_ap_reverse_bc) /\ (dsa_an_reverse_bc) = 0) \/ exists ge_signed_half_reverse_bcleft. (((b) = 2 * ge_signed_half_reverse_bcleft + 1 /\ (dsa_ap_reverse_bc) = 0) /\ (dsa_an_reverse_bc) = S ge_signed_half_reverse_bcleft))) /\ ((((((c) = 2 * (dsa_bp_reverse_bc) /\ (dsa_bn_reverse_bc) = 0) \/ exists ge_signed_half_reverse_bcright. (((c) = 2 * ge_signed_half_reverse_bcright + 1 /\ (dsa_bp_reverse_bc) = 0) /\ (dsa_bn_reverse_bc) = S ge_signed_half_reverse_bcright))) /\ ((((((bc) = 2 * (dsa_cp_reverse_bc) /\ (dsa_cn_reverse_bc) = 0) \/ exists ge_signed_half_reverse_bcoutput. (((bc) = 2 * ge_signed_half_reverse_bcoutput + 1 /\ (dsa_cp_reverse_bc) = 0) /\ (dsa_cn_reverse_bc) = S ge_signed_half_reverse_bcoutput))) /\ ((dsa_ap_reverse_bc + dsa_bp_reverse_bc) + dsa_cn_reverse_bc = (dsa_an_reverse_bc + dsa_bn_reverse_bc) + dsa_cp_reverse_bc))))))) -> (exists dsa_ap_reverse_out dsa_an_reverse_out dsa_bp_reverse_out dsa_bn_reverse_out dsa_cp_reverse_out dsa_cn_reverse_out. (((((a) = 2 * (dsa_ap_reverse_out) /\ (dsa_an_reverse_out) = 0) \/ exists ge_signed_half_reverse_outleft. (((a) = 2 * ge_signed_half_reverse_outleft + 1 /\ (dsa_ap_reverse_out) = 0) /\ (dsa_an_reverse_out) = S ge_signed_half_reverse_outleft))) /\ ((((((bc) = 2 * (dsa_bp_reverse_out) /\ (dsa_bn_reverse_out) = 0) \/ exists ge_signed_half_reverse_outright. (((bc) = 2 * ge_signed_half_reverse_outright + 1 /\ (dsa_bp_reverse_out) = 0) /\ (dsa_bn_reverse_out) = S ge_signed_half_reverse_outright))) /\ ((((((out) = 2 * (dsa_cp_reverse_out) /\ (dsa_cn_reverse_out) = 0) \/ exists ge_signed_half_reverse_outoutput. (((out) = 2 * ge_signed_half_reverse_outoutput + 1 /\ (dsa_cp_reverse_out) = 0) /\ (dsa_cn_reverse_out) = S ge_signed_half_reverse_outoutput))) /\ ((dsa_ap_reverse_out + dsa_bp_reverse_out) + dsa_cn_reverse_out = (dsa_an_reverse_out + dsa_bn_reverse_out) + dsa_cp_reverse_out))))))) -> (exists dsa_ap_reverse_target dsa_an_reverse_target dsa_bp_reverse_target dsa_bn_reverse_target dsa_cp_reverse_target dsa_cn_reverse_target. (((((ab) = 2 * (dsa_ap_reverse_target) /\ (dsa_an_reverse_target) = 0) \/ exists ge_signed_half_reverse_targetleft. (((ab) = 2 * ge_signed_half_reverse_targetleft + 1 /\ (dsa_ap_reverse_target) = 0) /\ (dsa_an_reverse_target) = S ge_signed_half_reverse_targetleft))) /\ ((((((c) = 2 * (dsa_bp_reverse_target) /\ (dsa_bn_reverse_target) = 0) \/ exists ge_signed_half_reverse_targetright. (((c) = 2 * ge_signed_half_reverse_targetright + 1 /\ (dsa_bp_reverse_target) = 0) /\ (dsa_bn_reverse_target) = S ge_signed_half_reverse_targetright))) /\ ((((((out) = 2 * (dsa_cp_reverse_target) /\ (dsa_cn_reverse_target) = 0) \/ exists ge_signed_half_reverse_targetoutput. (((out) = 2 * ge_signed_half_reverse_targetoutput + 1 /\ (dsa_cp_reverse_target) = 0) /\ (dsa_cn_reverse_target) = S ge_signed_half_reverse_targetoutput))) /\ ((dsa_ap_reverse_target + dsa_bp_reverse_target) + dsa_cn_reverse_target = (dsa_an_reverse_target + dsa_bn_reverse_target) + dsa_cp_reverse_target)))))))

Complete tactic proof in conservative notation

All 34 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

34 script commands · 7 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–9

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro ab
  5. L5
    intro bc
  6. L6
    intro out
  7. L7
    intro hab
  8. L8
    intro hbc
  9. L9
    intro hout
02Establish hwL10–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed add total.

  1. L10
    have hw : ∃ w. SignedAdd(ab,c,w)Definitions: SignedAdd(ab,c,w)Original native command in the exact edition
  2. L11
    specialize signed_add_total (ab)
  3. L12
    specialize signed_add_total (c)
  4. L13
    apply signed_add_total
03Separate the logical casesL14–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases hw
04Establish heqL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed add functional.

  1. L15
    have heq : x = out
  2. L16
    specialize signed_add_functional (a)
  3. L17
    specialize signed_add_functional (bc)
  4. L18
    specialize signed_add_functional (x)
  5. L19
    specialize signed_add_functional (out)
  6. L20
    apply signed_add_functional
  7. L21
    specialize signed_add_associative (a)
  8. L22
    specialize signed_add_associative (b)
  9. L23
    specialize signed_add_associative (c)
  10. L24
    specialize signed_add_associative (ab)
05Use earlier factsL25–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L25
    specialize signed_add_associative (bc)
  2. L26
    specialize signed_add_associative (x)
  3. L27
    apply signed_add_associative
  4. L28
    exact hab
  5. L29
    exact hw_witness
  6. L30
    exact hbc
  7. L31
    exact hout
06Calculate and transport equalitiesL32–33

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite heq at hw_witness
  2. L33
    rewrite heq at hw_witness
07Use earlier factsL34–34

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L34
    exact hw_witness

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro ab
  5. 0005intro bc
  6. 0006intro out
  7. 0007intro hab
  8. 0008intro hbc
  9. 0009intro hout
  10. 0010have hw : ∃ w. SignedAdd(ab,c,w)
  11. 0011specialize signed_add_total (ab)
  12. 0012specialize signed_add_total (c)
  13. 0013apply signed_add_total
  14. 0014cases hw
  15. 0015have heq : x = out
  16. 0016specialize signed_add_functional (a)
  17. 0017specialize signed_add_functional (bc)
  18. 0018specialize signed_add_functional (x)
  19. 0019specialize signed_add_functional (out)
  20. 0020apply signed_add_functional
  21. 0021specialize signed_add_associative (a)
  22. 0022specialize signed_add_associative (b)
  23. 0023specialize signed_add_associative (c)
  24. 0024specialize signed_add_associative (ab)
  25. 0025specialize signed_add_associative (bc)
  26. 0026specialize signed_add_associative (x)
  27. 0027apply signed_add_associative
  28. 0028exact hab
  29. 0029exact hw_witness
  30. 0030exact hbc
  31. 0031exact hout
  32. 0032rewrite heq at hw_witness
  33. 0033rewrite heq at hw_witness
  34. 0034exact hw_witness