1	# Fold a sequence of conditions and recover any member by one induction.
2	import Base
3	import ./storage_shape.bend as Shape
4	import ./word_encoding.bend as WordEncoding
5	
6	# Evidence is required only for an enabled branch.
7	def When(enabled: Bool,Property: Data) -> Data:
8	  match enabled:
9	    case False{}: Unit
10	    case True{}: Property
11	
12	def choose_matching(-Element: Data,+first: Bool,+rest: Bool,+actual: Element,+wanted: Element,+old: Element,
13	  correct: When(first,{actual == wanted : Element})) ->
14	  {Bool.pick(Element,rest,wanted,Bool.pick(Element,first,actual,old)) == Bool.pick(Element,first || rest,wanted,old) : Element}:
15	  match first rest:
16	    case False{} False{}: {==}
17	    case False{} True{}: {==}
18	    case True{} False{}: correct
19	    case True{} True{}: {==}
20	
21	def left(+first: Bool,+second: Bool,truth: {Bool.and(first,second) == True{} : Bool}) -> {first == True{} : Bool}:
22	  match first:
23	    case False{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(truth))
24	    case True{}: {==}
25	
26	def right(+first: Bool,+second: Bool,truth: {Bool.and(first,second) == True{} : Bool}) -> {second == True{} : Bool}:
27	  match first:
28	    case False{}: Empty.absurd({second == True{} : Bool},WordEncoding.false_true(truth))
29	    case True{}: truth
30	
31	# Stored in reverse evaluation order so all preserves left-associated &&.
32	def all(conditions: List<&2,Bool>) -> Bool:
33	  match conditions:
34	    case Nil{}: True{}
35	    case last <> prefix: Bool.and(all(prefix),last)
36	
37	# Evidence for every condition, in the same reverse order as all.
38	def Holds(conditions: List<&2,Bool>) -> Data:
39	  match conditions:
40	    case Nil{}: Unit
41	    case last <> prefix: Shape.Both<{last == True{} : Bool},Holds(prefix)>
42	
43	def all_hold(+conditions: List<&2,Bool>,+holds: Holds(conditions)) -> {all(conditions) == True{} : Bool}:
44	  match conditions:
45	    case Nil{}: {==}
46	    case +last <> +prefix:
47	      Shape.Both{+here,+rest} = holds
48	      %Equal.sym(Bool,all(prefix),True{},all_hold(prefix,rest)) : {Bool.and(_,last) == True{} : Bool}
49	      here
50	
51	# A missing condition is True, the neutral element, not an array read.
52	def condition_at(conditions: List<&2,Bool>,index: Nat) -> Bool:
53	  match conditions:
54	    case Nil{}: True{}
55	    case last <> prefix:
56	      match index:
57	        case 0n: last
58	        case 1n+previous: condition_at(prefix,previous)
59	
60	law every_condition_holds:
61	  for +conditions: List<&2,Bool>
62	  for +index: Nat
63	  for truth: {all(conditions) == True{} : Bool}
64	  {condition_at(conditions,index) == True{} : Bool}
65	
66	def every_condition_holds(conditions,index,truth):
67	  match conditions:
68	    case Nil{}: {==}
69	    case +last <> +prefix:
70	      match index:
71	        case 0n: right(all(prefix),last,truth)
72	        case 1n+previous:
73	          every_condition_holds(prefix,previous,left(all(prefix),last,truth))
74	
75	# Disjunction identities shared by coverage proofs.
76	def or_true_right(+value: Bool) -> {value || True{} == True{} : Bool}:
77	  match value:
78	    case False{}: {==}
79	    case True{}: {==}
80	
81	def or_false_left(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {first == False{} : Bool}:
82	  match first:
83	    case False{}: {==}
84	    case True{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))
85	
86	def or_false_right(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {second == False{} : Bool}:
87	  match first:
88	    case False{}: proof
89	    case True{}: Empty.absurd({second == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))
90	
91	def or_associative(+first: Bool,+second: Bool,+third: Bool) ->
92	  {first || (second || third) == (first || second) || third : Bool}:
93	  match first:
94	    case False{}: {==}
95	    case True{}: {==}
96	
97	# Boolean predicates agree when each truth witness implies the other.
98	def equivalent(+first: Bool,+second: Bool,
99	  forward: {first == True{} : Bool} -> {second == True{} : Bool},
100	  backward: {second == True{} : Bool} -> {first == True{} : Bool}) -> {first == second : Bool}:
101	  match first second:
102	    case False{} False{}: {==}
103	    case True{} True{}: {==}
104	    case True{} False{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(forward({==})))
105	    case False{} True{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(backward({==})))
106	
107	def and_associative(+first: Bool,+second: Bool,+third: Bool) -> {(first && second) && third == first && (second && third) : Bool}:
108	  match first:
109	    case False{}: {==}
110	    case True{}: {==}
111	
112	def and_true(+a: Bool,+b: Bool,ha: {a == True{} : Bool},hb: {b == True{} : Bool}) -> {a && b == True{} : Bool}:
113	  %Equal.sym(Bool,a,True{},ha) : {_ && b == True{} : Bool}
114	  hb
115	
116	def not_true(value: Bool,evidence: {Bool.not(value) == True{} : Bool}) -> {value == False{} : Bool}:
117	  match value:
118	    case False{}: {==}
119	    case True{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(evidence))
120	
121	def and_false_right(+left: Bool) -> {left && False{} == False{} : Bool}:
122	  match left:
123	    case True{}: {==}
124	    case False{}: {==}