growth.bend
gralha-bendquest@0.1.0.0 · 177 lines · 13 definitions
1
2import Base
3import gralha-bendquest@0.1.0.0/game.bend as G
4import gralha-bendquest@0.1.0.0/health.bend as H
5
6def Growth.maximum(+level: Nat, +vitality: Nat, bonus: U32, ceiling: U32) -> U32:
7 H.Health.maximum_word(G.Bq.max_hp(level, vitality), bonus, ceiling)
8
9law Growth.le_add_prefix:
10 for +prefix: Nat
11 for +value: Nat
12 {G.Bq.Nat.le(value, G.Bq.Nat.add(prefix, value)) == True{} : Bool}
13
14def Growth.le_add_prefix(prefix, value):
15 match prefix:
16 case Zero{}:
17 H.Health.le_refl(value)
18 case Succ{p}:
19 G.Bq.le_succ_r(value, G.Bq.Nat.add(p, value), Growth.le_add_prefix(p, value))
20
21law Growth.add_left:
22 for +a: Nat
23 for +b: Nat
24 for +extra: Nat
25 for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
26 {G.Bq.Nat.le(G.Bq.Nat.add(a, extra), G.Bq.Nat.add(b, extra)) == True{} : Bool}
27
28def Growth.add_left(a, b, extra, grow):
29 match a:
30 case Zero{}:
31 Growth.le_add_prefix(b, extra)
32 case Succ{p}:
33 match b:
34 case Zero{}:
35 Empty.absurd({G.Bq.Nat.le(Succ{G.Bq.Nat.add(p, extra)}, extra) == True{} : Bool}, G.Bq.Bool.false_ne_true(grow))
36 case Succ{q}:
37 Growth.add_left(p, q, extra, grow)
38
39law Growth.add_right:
40 for +prefix: Nat
41 for +a: Nat
42 for +b: Nat
43 for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
44 {G.Bq.Nat.le(G.Bq.Nat.add(prefix, a), G.Bq.Nat.add(prefix, b)) == True{} : Bool}
45
46def Growth.add_right(prefix, a, b, grow):
47 match prefix:
48 case Zero{}:
49 grow
50 case Succ{p}:
51 Growth.add_right(p, a, b, grow)
52
53law Growth.add_both:
54 for +a: Nat
55 for +b: Nat
56 for +c: Nat
57 for +d: Nat
58 for +ab: {G.Bq.Nat.le(a, b) == True{} : Bool}
59 for +cd: {G.Bq.Nat.le(c, d) == True{} : Bool}
60 {G.Bq.Nat.le(G.Bq.Nat.add(a, c), G.Bq.Nat.add(b, d)) == True{} : Bool}
61
62def Growth.add_both(a, b, c, d, ab, cd):
63 H.Health.le_trans(G.Bq.Nat.add(a, c), G.Bq.Nat.add(b, c), G.Bq.Nat.add(b, d), Growth.add_left(a, b, c, ab), Growth.add_right(b, c, d, cd))
64
65law Growth.mul:
66 for +scale: Nat
67 for +a: Nat
68 for +b: Nat
69 for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
70 {G.Bq.Nat.le(G.Bq.Nat.mul(scale, a), G.Bq.Nat.mul(scale, b)) == True{} : Bool}
71
72def Growth.mul(scale, a, b, grow):
73 match scale:
74 case Zero{}:
75 {==}
76 case Succ{p}:
77 Growth.add_both(a, b, G.Bq.Nat.mul(p, a), G.Bq.Nat.mul(p, b), grow, Growth.mul(p, a, b, grow))
78
79law Growth.double:
80 for +a: Nat
81 for +b: Nat
82 for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
83 {G.Bq.Nat.le(G.Bq.Nat.dbl(a), G.Bq.Nat.dbl(b)) == True{} : Bool}
84
85def Growth.double(a, b, grow):
86 match a:
87 case Zero{}:
88 {==}
89 case Succ{p}:
90 match b:
91 case Zero{}:
92 Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(grow))
93 case Succ{q}:
94 Growth.double(p, q, grow)
95
96law Growth.pred:
97 for +a: Nat
98 for +b: Nat
99 for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
100 {G.Bq.Nat.le(G.Bq.Nat.pred(a), G.Bq.Nat.pred(b)) == True{} : Bool}
101
102def Growth.pred(a, b, grow):
103 match a:
104 case Zero{}:
105 {==}
106 case Succ{p}:
107 match b:
108 case Zero{}:
109 Empty.absurd({G.Bq.Nat.le(p, 0n) == True{} : Bool}, G.Bq.Bool.false_ne_true(grow))
110 case Succ{q}:
111 grow
112
113law Growth.raw_maximum:
114 for +level0: Nat
115 for +level1: Nat
116 for +vit0: Nat
117 for +vit1: Nat
118 for +levels: {G.Bq.Nat.le(level0, level1) == True{} : Bool}
119 for +vitalities: {G.Bq.Nat.le(vit0, vit1) == True{} : Bool}
120 {G.Bq.Nat.le(G.Bq.max_hp(level0, vit0), G.Bq.max_hp(level1, vit1)) == True{} : Bool}
121
122def Growth.raw_maximum(level0, level1, vit0, vit1, levels, vitalities):
123 Growth.add_right(20n, G.Bq.Nat.add(G.Bq.Nat.mul(5n, vit0), G.Bq.Nat.dbl(G.Bq.Nat.pred(level0))), G.Bq.Nat.add(G.Bq.Nat.mul(5n, vit1), G.Bq.Nat.dbl(G.Bq.Nat.pred(level1))), Growth.add_both(G.Bq.Nat.mul(5n, vit0), G.Bq.Nat.mul(5n, vit1), G.Bq.Nat.dbl(G.Bq.Nat.pred(level0)), G.Bq.Nat.dbl(G.Bq.Nat.pred(level1)), Growth.mul(5n, vit0, vit1, vitalities), Growth.double(G.Bq.Nat.pred(level0), G.Bq.Nat.pred(level1), Growth.pred(level0, level1, levels))))
124
125law Growth.maximum_monotone:
126 for +level0: Nat
127 for +level1: Nat
128 for +vit0: Nat
129 for +vit1: Nat
130 for +bonus: U32
131 for +ceiling: U32
132 for +levels: {G.Bq.Nat.le(level0, level1) == True{} : Bool}
133 for +vitalities: {G.Bq.Nat.le(vit0, vit1) == True{} : Bool}
134 {G.Bq.Nat.le(U32.to_nat(Growth.maximum(level0, vit0, bonus, ceiling)), U32.to_nat(Growth.maximum(level1, vit1, bonus, ceiling))) == True{} : Bool}
135
136def Growth.maximum_monotone(level0, level1, vit0, vit1, bonus, ceiling, levels, vitalities):
137 H.Health.maximum_word_monotone(G.Bq.max_hp(level0, vit0), G.Bq.max_hp(level1, vit1), bonus, ceiling, Growth.raw_maximum(level0, level1, vit0, vit1, levels, vitalities))
138
139law Growth.health_preserved:
140 for +hp: U32
141 for +level0: Nat
142 for +level1: Nat
143 for +vit0: Nat
144 for +vit1: Nat
145 for +bonus: U32
146 for +ceiling: U32
147 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level0, vit0, bonus, ceiling))) == True{} : Bool}
148 for +levels: {G.Bq.Nat.le(level0, level1) == True{} : Bool}
149 for +vitalities: {G.Bq.Nat.le(vit0, vit1) == True{} : Bool}
150 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level1, vit1, bonus, ceiling))) == True{} : Bool}
151
152def Growth.health_preserved(hp, level0, level1, vit0, vit1, bonus, ceiling, valid, levels, vitalities):
153 H.Health.le_trans(U32.to_nat(hp), U32.to_nat(Growth.maximum(level0, vit0, bonus, ceiling)), U32.to_nat(Growth.maximum(level1, vit1, bonus, ceiling)), valid, Growth.maximum_monotone(level0, level1, vit0, vit1, bonus, ceiling, levels, vitalities))
154
155law Growth.level_up_preserves_health:
156 for +hp: U32
157 for +level: Nat
158 for +vitality: Nat
159 for +bonus: U32
160 for +ceiling: U32
161 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level, vitality, bonus, ceiling))) == True{} : Bool}
162 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(Succ{level}, vitality, bonus, ceiling))) == True{} : Bool}
163
164def Growth.level_up_preserves_health(hp, level, vitality, bonus, ceiling, valid):
165 Growth.health_preserved(hp, level, Succ{level}, vitality, vitality, bonus, ceiling, valid, G.Bq.le_succ_r(level, level, H.Health.le_refl(level)), H.Health.le_refl(vitality))
166
167law Growth.vitality_up_preserves_health:
168 for +hp: U32
169 for +level: Nat
170 for +vitality: Nat
171 for +bonus: U32
172 for +ceiling: U32
173 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level, vitality, bonus, ceiling))) == True{} : Bool}
174 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level, Succ{vitality}, bonus, ceiling))) == True{} : Bool}
175
176def Growth.vitality_up_preserves_health(hp, level, vitality, bonus, ceiling, valid):
177 Growth.health_preserved(hp, level, level, vitality, Succ{vitality}, bonus, ceiling, valid, H.Health.le_refl(level), G.Bq.le_succ_r(vitality, vitality, H.Health.le_refl(vitality)))