proofs/word_subtraction.bend
stelliferous@0.0.2.0 · 110 lines · 6 definitions
1import Base
2import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
3import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
4import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
5
6law undo:
7 for +n: Nat
8 for +a: Word(n)
9 for +b: Word(n)
10 for +f: Bool
11 for +c: Bool
12 {Word.adc(n,Word.adc(n,a,b,f,c),b,Bool.not(f),Bool.not(c)) == a : Word(n)}
13def undo(n,a,b,f,c):
14 match n:
15 case 0n:
16 WNil{} = a
17 {==}
18 case 1n+ +p:
19 match a b f c:
20 case WCon{False{},+at} WCon{False{},+bt} False{} False{}:
21 %undo(p,at,bt,False{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{False{},
22 _} : Word(1n+p)}
23 {==}
24 case WCon{False{},+at} WCon{False{},+bt} False{} True{}:
25 %undo(p,at,bt,False{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{False{},
26 _} : Word(1n+p)}
27 {==}
28 case WCon{False{},+at} WCon{False{},+bt} True{} False{}:
29 %undo(p,at,bt,True{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{False{},
30 _} : Word(1n+p)}
31 {==}
32 case WCon{False{},+at} WCon{False{},+bt} True{} True{}:
33 %undo(p,at,bt,True{},True{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{False{},
34 _} : Word(1n+p)}
35 {==}
36 case WCon{False{},+at} WCon{True{},+bt} False{} False{}:
37 %undo(p,at,bt,False{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{False{},
38 _} : Word(1n+p)}
39 {==}
40 case WCon{False{},+at} WCon{True{},+bt} False{} True{}:
41 %undo(p,at,bt,False{},True{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{False{},
42 _} : Word(1n+p)}
43 {==}
44 case WCon{False{},+at} WCon{True{},+bt} True{} False{}:
45 %undo(p,at,bt,True{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{False{},
46 _} : Word(1n+p)}
47 {==}
48 case WCon{False{},+at} WCon{True{},+bt} True{} True{}:
49 %undo(p,at,bt,True{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{False{},
50 _} : Word(1n+p)}
51 {==}
52 case WCon{True{},+at} WCon{False{},+bt} False{} False{}:
53 %undo(p,at,bt,False{},False{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{True{},
54 _} : Word(1n+p)}
55 {==}
56 case WCon{True{},+at} WCon{False{},+bt} False{} True{}:
57 %undo(p,at,bt,False{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{True{},_} : Word(1n+p)}
58 {==}
59 case WCon{True{},+at} WCon{False{},+bt} True{} False{}:
60 %undo(p,at,bt,True{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{True{},_} : Word(1n+p)}
61 {==}
62 case WCon{True{},+at} WCon{False{},+bt} True{} True{}:
63 %undo(p,at,bt,True{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{True{},_} : Word(1n+p)}
64 {==}
65 case WCon{True{},+at} WCon{True{},+bt} False{} False{}:
66 %undo(p,at,bt,False{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{True{},_} : Word(1n+p)}
67 {==}
68 case WCon{True{},+at} WCon{True{},+bt} False{} True{}:
69 %undo(p,at,bt,False{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{True{},_} : Word(1n+p)}
70 {==}
71 case WCon{True{},+at} WCon{True{},+bt} True{} False{}:
72 %undo(p,at,bt,True{},False{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{True{},_} : Word(1n+p)}
73 {==}
74 case WCon{True{},+at} WCon{True{},+bt} True{} True{}:
75 %undo(p,at,bt,True{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{True{},_} : Word(1n+p)}
76 {==}
77
78def subtract_add(+a: U32,+b: U32) -> {U32.sub(U32.add(a,b),b) == a : U32}:
79 match a b:
80 case U32{+x} U32{+y}:
81 %undo(32n,x,y,False{},False{}) : {U32{Word.sub(32n,Word.add(32n,x,y),y)} == U32{_} : U32}
82 {==}
83
84def add_subtract(+a: U32,+b: U32) -> {U32.add(U32.sub(a,b),b) == a : U32}:
85 match a b:
86 case U32{+x} U32{+y}:
87 %undo(32n,x,y,True{},True{}) : {U32{Word.add(32n,Word.sub(32n,x,y),y)} == U32{_} : U32}
88 {==}
89
90def encoded_subtract_add(+a: Nat,+b: Nat) -> {U32.sub(U32.from_nat(Nat.add(a,b)),U32.from_nat(b)) == U32.from_nat(a) : U32}:
91 %WordArithmetic.native_add(a,b) : {U32.sub(_,U32.from_nat(b)) == U32.from_nat(a) : U32}
92 subtract_add(U32.from_nat(a),U32.from_nat(b))
93
94def restore(+a: Nat,+b: Nat,h: {Nat.is_le(b,a) == True{} : Bool}) -> {Nat.add(Nat.sub(a,b),b) == a : Nat}:
95 match a b:
96 case 0n 0n:
97 {==}
98 case 0n 1n+b:
99 Empty.absurd({Nat.add(Nat.sub(0n,1n+b),1n+b) == 0n : Nat},WordEncoding.false_true(h))
100 case 1n+ +a 0n:
101 Addition.zero_right(1n+a)
102 case 1n+ +a 1n+ +b:
103 %Equal.sym(Nat,Nat.add(Nat.sub(a,b),1n+b),1n+Nat.add(Nat.sub(a,b),b),Addition.successor_right(Nat.sub(a,b),b)) : {_ == 1n+a : Nat}
104 %restore(a,b,h) : {1n+Nat.add(Nat.sub(a,b),b) == 1n+_ : Nat}
105 {==}
106
107def encoded_subtract(+a: Nat,+b: Nat,h: {Nat.is_le(b,a) == True{} : Bool}) -> {U32.sub(U32.from_nat(a),
108 U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}:
109 %restore(a,b,h) : {U32.sub(U32.from_nat(_),U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}
110 encoded_subtract_add(Nat.sub(a,b),b)