Grace/Cumulus/Int/Operations.g17

Open in Workbench Download source

Imports

Core

Declarations

• integerPairSum def
• integerClassSum def
• integerClassNeg def
• integerPairSum.pair theorem derivation
• integerPairSum.cross_sums theorem derivation
• integerClassSum.well_defined theorem derivation
• integerClassSum.integer theorem derivation
• integerClassNeg.well_defined theorem derivation
• integerClassSum.zero_right theorem derivation
• integerClassSum.commutative theorem derivation
• integerClassSum.neg_right theorem derivation
• integerClassMul def
• integerClassMul.integer theorem derivation
• integerClassMul.commutative theorem derivation
• integerClassMul.transport_left theorem derivation
• integerClassMul.well_defined theorem derivation
• integerClassNeg.integer theorem derivation

Source

1-- Integer operations lifted from natural-pair representatives2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Int.Operations8import Core910def integerPairSum (a b c d : Set) : Set := (add(a, c), add(b, d))11def integerClassSum (a b c d : Set) : Set := integerClass(add(a, c), add(b, d))12def integerClassNeg (a b : Set) : Set := integerClass(b, a)1314theorem integerPairSum.pair (a b c d : Nat)15  shows integerPairSum(a, b, c, d) ∈ integerPairs16proof17  unfold integerPairSum18  have leftNat := add.closed at c, a with *19  have rightNat := add.closed at d, b with *20  exact integerPairs.pair with leftNat, rightNat2122theorem integerPairSum.cross_sums (a b a2 b2 c d c2 d2 : Nat)23  requires leftEquivalent : add(a, b2) = add(a2, b)24  requires rightEquivalent : add(c, d2) = add(c2, d)25  shows add(add(a, c), add(b2, d2)) = add(add(a2, c2), add(b, d))26proof27  ring2829theorem integerClassSum.well_defined (a b a2 b2 c d c2 d2 : Nat)30  requires leftEquivalent : add(a, b2) = add(a2, b)31  requires rightEquivalent : add(c, d2) = add(c2, d)32  shows integerClassSum(a, b, c, d) = integerClassSum(a2, b2, c2, d2)33proof34  unfold integerClassSum35  have sums := integerPairSum.cross_sums at a, b, a2, b2, c, d, c2, d2 with *36  exact integerClass.eq with sums3738theorem integerClassSum.integer (a b c d : Nat)39  shows Integer(integerClassSum(a, b, c, d))40proof41  unfold integerClassSum42  have leftNat := add.closed at c, a with *43  have rightNat := add.closed at d, b with *44  exact integerClass.integer with leftNat, rightNat4546theorem integerClassNeg.well_defined (a b c d : Nat)47  requires equivalent : add(a, d) = add(c, b)48  shows integerClassNeg(a, b) = integerClassNeg(c, d)49proof50  unfold integerClassNeg51  have reverse := integerEquivalent.cross_symmetric with *52  have leftCommute := add.commutative at c, b with *53  have rightCommute := add.commutative at d, a with *54  have negatedSums := reverse55  rewrite ← leftCommute at negatedSums56  rewrite rightCommute at negatedSums57  exact integerClass.eq with *5859theorem integerClassSum.zero_right (a b : Nat)60  shows integerClassSum(a, b, 0, 0) = integerClass(a, b)61proof62  simp [integerClassSum, add.right_unit]6364theorem integerClassSum.commutative (a b c d : Nat)65  shows integerClassSum(a, b, c, d) = integerClassSum(c, d, a, b)66proof67  unfold integerClassSum68  have positive := add.commutative at c, a with *69  have negative := add.commutative at d, b with *70  rewrite positive71  rewrite negative72  rfl7374theorem integerClassSum.neg_right (a b : Nat)75  shows integerClassSum(a, b, b, a) = integerZero76proof77  unfold integerClassSum78  unfold integerZero79  have sumNat := add.closed at b, a with *80  have reverseNat := add.closed at a, b with *81  have commute := add.commutative at b, a with *82  have classes := integerClass.eq with sumNat, reverseNat, Naturals.constructor.zero, Naturals.constructor.zero83  apply classes84  simp [add, add.right_unit, commute]8586-- Multiplication of differences: (a-b)(c-d) = (ac+bd)-(ad+bc).87def integerClassMul (a b c d : Nat) : Integer :=88  integerClass(a * c + b * d, a * d + b * c)8990theorem integerClassMul.integer (a b c d : Nat)91  shows Integer(integerClassMul(a, b, c, d))92proof93  unfold integerClassMul94  exact integerClass.integer with *9596theorem integerClassMul.commutative (a b c d : Nat)97  shows integerClassMul(a, b, c, d) = integerClassMul(c, d, a, b)98proof99  unfold integerClassMul100  apply integerClass.eq with *{4}101  ring102103theorem integerClassMul.transport_left (a b a2 b2 c d : Nat)104  requires equivalent : a + b2 = a2 + b105  shows integerClassMul(a, b, c, d) = integerClassMul(a2, b2, c, d)106proof107  have combined : (a + b2) * c + (a2 + b) * d = (a2 + b) * c + (a + b2) * d108  . rw equivalent109    rfl110  unfold integerClassMul111  apply integerClass.eq with *{4}112  ring113114theorem integerClassMul.well_defined (a b a2 b2 c d c2 d2 : Nat)115  requires leftEquivalent : a + b2 = a2 + b116  requires rightEquivalent : c + d2 = c2 + d117  shows integerClassMul(a, b, c, d) = integerClassMul(a2, b2, c2, d2)118proof119  have first := integerClassMul.transport_left at a, b, a2, b2, c, d with *120  have swap := integerClassMul.commutative at a2, b2, c, d with *121  have second := integerClassMul.transport_left at c, d, c2, d2, a2, b2 with *122  have back := integerClassMul.commutative at c2, d2, a2, b2 with *123  simp124125theorem integerClassNeg.integer (a b : Nat)126  shows Integer(integerClassNeg(a, b))127proof128  unfold integerClassNeg129  exact integerClass.integer with *130