src/tensor/word_injective.bend
bendtorch-core@0.1.0.0 · 93 lines · 11 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
3
4def half(number: Nat) -> Nat:
5 match number:
6 case 0n:
7 0n
8 case 1n:
9 0n
10 case 2n+p:
11 1n+half(p)
12
13def even(number: Nat) -> Bool:
14 match number:
15 case 0n:
16 True{}
17 case 1n:
18 False{}
19 case 2n+p:
20 even(p)
21
22def half_double(+number: Nat) -> {half(Nat.double(number)) == number : Nat}:
23 match number:
24 case 0n:
25 {==}
26 case 1n+p:
27 Equal.cong(Nat, Nat, n => 1n+n, half(Nat.double(p)), p, half_double(p))
28
29def even_double(+number: Nat) -> {even(Nat.double(number)) == True{} : Bool}:
30 match number:
31 case 0n:
32 {==}
33 case 1n+p:
34 even_double(p)
35
36def even_successor_double(+number: Nat) -> {even(1n+Nat.double(number)) == False{} : Bool}:
37 match number:
38 case 0n:
39 {==}
40 case 1n+p:
41 even_successor_double(p)
42
43def double_injective(+left: Nat, +right: Nat, equal: {Nat.double(left) == Nat.double(right) : Nat}) -> {left == right : Nat}:
44 Equal.trans(Nat, left, half(Nat.double(left)), right,
45 Equal.sym(Nat, half(Nat.double(left)), left, half_double(left)),
46 Equal.trans(Nat, half(Nat.double(left)), half(Nat.double(right)), right,
47 Equal.cong(Nat, Nat, n => half(n), Nat.double(left), Nat.double(right), equal), half_double(right)))
48
49def parity_clash(+left: Nat, +right: Nat, equal: {Nat.double(left) == 1n+Nat.double(right) : Nat}) -> Empty:
50 Lifecycle.false_true(Equal.trans(Bool, True{}, even(Nat.double(left)), False{},
51 Equal.sym(Bool, even(Nat.double(left)), True{}, even_double(left)),
52 Equal.trans(Bool, even(Nat.double(left)), even(1n+Nat.double(right)), False{},
53 Equal.cong(Nat, Bool, n => even(n), Nat.double(left), 1n+Nat.double(right), equal), even_successor_double(right))))
54
55def predecessor(number: Nat) -> Nat:
56 match number:
57 case 0n:
58 0n
59 case 1n+p:
60 p
61
62def successor_injective(-left: Nat, -right: Nat, equal: {1n+left == 1n+right : Nat}) -> {left == right : Nat}:
63 Equal.cong(Nat, Nat, n => predecessor(n), 1n+left, 1n+right, equal)
64
65def word_natural_injective(+width: Nat, +left: Word(width), +right: Word(width)) ->
66 {Word.to_nat(width, left) == Word.to_nat(width, right) : Nat} -> {left == right : Word(width)}:
67 match width:
68 case 0n:
69 match left right:
70 case WNil{} WNil{}:
71 equal => {==}
72 case 1n+p:
73 match left right:
74 case WCon{False{}, +lt} WCon{False{}, +rt}:
75 equal => Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, lt, rt,
76 word_natural_injective(p, lt, rt)(double_injective(Word.to_nat(p, lt), Word.to_nat(p, rt), equal)))
77 case WCon{False{}, +lt} WCon{True{}, +rt}:
78 equal => Empty.absurd({WCon{False{}, lt} == WCon{True{}, rt} : Word(1n+p)},
79 parity_clash(Word.to_nat(p, lt), Word.to_nat(p, rt), equal))
80 case WCon{True{}, +lt} WCon{False{}, +rt}:
81 equal => Empty.absurd({WCon{True{}, lt} == WCon{False{}, rt} : Word(1n+p)},
82 parity_clash(Word.to_nat(p, rt), Word.to_nat(p, lt),
83 Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, lt)), Nat.double(Word.to_nat(p, rt)), equal)))
84 case WCon{True{}, +lt} WCon{True{}, +rt}:
85 equal => Equal.cong(Word(p), Word(1n+p), w => WCon{True{}, w}, lt, rt,
86 word_natural_injective(p, lt, rt)(double_injective(Word.to_nat(p, lt), Word.to_nat(p, rt),
87 successor_injective(Nat.double(Word.to_nat(p, lt)), Nat.double(Word.to_nat(p, rt)), equal))))
88
89def u32_natural_injective(+left: U32, +right: U32) ->
90 {U32.to_nat(left) == U32.to_nat(right) : Nat} -> {left == right : U32}:
91 match left right:
92 case U32{+lw} U32{+rw}:
93 equal => Equal.cong(Word(32n), U32, w => U32{w}, lw, rw, word_natural_injective(32n, lw, rw)(equal))