1	# Maximum-health growth, including the exact saturated word representation.
2	import Base
3	import ./game.bend as G
4	import ./health.bend as H
5	
6	def 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	
9	law 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	
14	def 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	
21	law 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	
28	def 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	
39	law 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	
46	def 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	
53	law 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	
62	def 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	
65	law 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	
72	def 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	
79	law 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	
85	def 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	
96	law 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	
102	def 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	
113	law 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	
122	def 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	
125	law 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	
136	def 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	
139	law 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	
152	def 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	
155	law 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	
164	def 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	
167	law 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	
176	def 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)))