Std.Proof.IntMath

View source →

Proof-carrying facts about Int, via decidable-Boolean reflection.

Following Idris (So/Oh), Agda (T), and Lean (Decidable), this module reflects a decidable Boolean condition into a proposition: the comparisons already fold to the inductive Bool, so a closed condition reduces to True() and is inhabited by pure computation, while an open condition is carried as evidence by whoever constructs the value. This reflection is the refinement-surface encoding and is entirely generic over the reflected Bool — it does NOT depend on how Int is represented.

(Int is now the inductive family FromNat(Nat) | NegativeSuccessor(Nat) rather than a primitive, so open arithmetic IsTrue-claims can additionally be discharged by structural induction — see Std.Proof.IntOrder. The IsTrue/Confirmed/decide_is_true machinery below is unchanged and continues to coexist as the decidable-Boolean reflector.)

Functions

  • # fn decide_is_true(claim: Bool) -> Decision(IsTrue(claim))

    Decide a condition, carrying checked evidence in either branch.

  • # fn true_is_not_false(proof: IsTrue(False())) -> Empty

    A confirmed condition cannot also be false: matching evidence for the false case is impossible, so the empty match discharges it.