SimpleProof.tla

----------------------------- MODULE SimpleProof -----------------------------
(* 
 * Simple TLA+ Proof Example
 * Demonstrates TLAPS for basic mathematical proofs
 *)

EXTENDS Naturals, TLAPS

(***************************************************************************
 * THEOREM: Basic Arithmetic
 ***************************************************************************)
THEOREM AdditionCommutative ==
    \A a \in Nat : \A b \in Nat : a + b = b + a
PROOF BY SMT

(***************************************************************************
 * THEOREM: Subtraction preserves non-negativity with proper constraint
 ***************************************************************************)
THEOREM SubtractionBounded ==
    \A a \in Nat : \A b \in Nat : (a >= b) => (a - b) \in Nat
PROOF BY SMT

(***************************************************************************
 * THEOREM: Transfer Balance Equation
 * Key theorem for financial systems
 ***************************************************************************)
THEOREM TransferEquation ==
    \A old_from \in Nat :
    \A old_to \in Nat :
    \A amount \in Nat :
    (amount > 0 /\ old_from >= amount) =>
    LET new_from == old_from - amount
        new_to == old_to + amount
    IN (old_from + old_to = new_from + new_to)
PROOF BY SMT

(***************************************************************************
 * THEOREM: Conservation of Total - More Explicit Form
 * Shows that (A - x) + (B + x) = A + B
 ***************************************************************************)
THEOREM ConservationGeneral ==
    \A A \in Nat :
    \A B \in Nat :
    \A x \in Nat :
    (x > 0 /\ A >= x) =>
    ((A - x) + (B + x) = A + B)
PROOF BY SMT

(***************************************************************************
 * THEOREM: No Negative Balances
 * Critical safety property for token systems
 ***************************************************************************)
THEOREM NoNegativeResult ==
    \A balance \in Nat :
    \A amount \in Nat :
    (balance >= amount) => ((balance - amount) >= 0)
PROOF BY SMT

=============================================================================
\* Simple proofs for TLAPS verification