1	# Minimum and maximum laws used by interval intersection. Proofs follow the
2	# official structural definitions; no bounded dimension is enumerated.
3	import Base
4	import ./nat_order.bend as Order
5	import ./word_encoding.bend as WordEncoding
6	
7	def successor_pick(choice: Bool,+left: Nat,+right: Nat) ->
8	  {1n+Bool.pick(Nat,choice,left,right) == Bool.pick(Nat,choice,1n+left,1n+right) : Nat}:
9	  match choice:
10	    case False{}: {==}
11	    case True{}: {==}
12	
13	def minimum_choice(+left: Nat,+right: Nat) -> {Nat.min(left,right) == Bool.pick(Nat,Nat.is_lt(left,right),left,right) : Nat}:
14	  match left right:
15	    case 0n 0n: {==}
16	    case 0n 1n+right: {==}
17	    case 1n+left 0n: {==}
18	    case 1n+ +left 1n+ +right:
19	      Equal.trans(Nat,1n+Nat.min(left,right),1n+Bool.pick(Nat,Nat.is_lt(left,right),left,right),Bool.pick(Nat,Nat.is_lt(left,right),1n+left,1n+right),
20	        Equal.cong(Nat,Nat,n => 1n+n,Nat.min(left,right),Bool.pick(Nat,Nat.is_lt(left,right),left,right),minimum_choice(left,right)),successor_pick(Nat.is_lt(left,right),left,right))
21	
22	def maximum_choice(+left: Nat,+right: Nat) -> {Nat.max(left,right) == Bool.pick(Nat,Nat.is_lt(left,right),right,left) : Nat}:
23	  match left right:
24	    case 0n 0n: {==}
25	    case 0n 1n+right: {==}
26	    case 1n+left 0n: {==}
27	    case 1n+ +left 1n+ +right:
28	      Equal.trans(Nat,1n+Nat.max(left,right),1n+Bool.pick(Nat,Nat.is_lt(left,right),right,left),Bool.pick(Nat,Nat.is_lt(left,right),1n+right,1n+left),
29	        Equal.cong(Nat,Nat,n => 1n+n,Nat.max(left,right),Bool.pick(Nat,Nat.is_lt(left,right),right,left),maximum_choice(left,right)),successor_pick(Nat.is_lt(left,right),right,left))
30	
31	def minimum_when_ordered(+left: Nat,+right: Nat,ordered: {Nat.is_le(left,right) == True{} : Bool}) -> {Nat.min(left,right) == left : Nat}:
32	  match left right:
33	    case 0n right: {==}
34	    case 1n+left 0n: Empty.absurd({Nat.min(1n+left,0n) == 1n+left : Nat},WordEncoding.false_true(ordered))
35	    case 1n+ +left 1n+ +right:
36	      Equal.cong(Nat,Nat,n => 1n+n,Nat.min(left,right),left,minimum_when_ordered(left,right,ordered))
37	
38	def minimum_left(+left: Nat,+right: Nat) -> {Nat.is_le(Nat.min(left,right),left) == True{} : Bool}:
39	  match left right:
40	    case 0n right: {==}
41	    case 1n+left 0n: {==}
42	    case 1n+left 1n+right: minimum_left(left,right)
43	
44	def minimum_right(+left: Nat,+right: Nat) -> {Nat.is_le(Nat.min(left,right),right) == True{} : Bool}:
45	  match left right:
46	    case 0n right: Order.zero_le(right)
47	    case 1n+left 0n: {==}
48	    case 1n+left 1n+right: minimum_right(left,right)
49	
50	def maximum_left(+left: Nat,+right: Nat) -> {Nat.is_le(left,Nat.max(left,right)) == True{} : Bool}:
51	  match left right:
52	    case 0n right: Order.zero_le(right)
53	    case 1n+ +left 0n: Order.reflexive(left)
54	    case 1n+left 1n+right: maximum_left(left,right)
55	
56	def maximum_right(+left: Nat,+right: Nat) -> {Nat.is_le(right,Nat.max(left,right)) == True{} : Bool}:
57	  match left right:
58	    case 0n +right: Order.reflexive(right)
59	    case 1n+left 0n: {==}
60	    case 1n+left 1n+right: maximum_right(left,right)
61	
62	def pick_upper(choice: Bool,+left: Nat,+right: Nat,+upper: Nat,left_ok: {Nat.is_le(left,upper) == True{} : Bool},right_ok: {Nat.is_le(right,upper) == True{} : Bool}) ->
63	  {Nat.is_le(Bool.pick(Nat,choice,left,right),upper) == True{} : Bool}:
64	  match choice:
65	    case False{}: right_ok
66	    case True{}: left_ok
67	
68	def pick_lower(choice: Bool,+left: Nat,+right: Nat,+lower: Nat,left_ok: {Nat.is_le(lower,left) == True{} : Bool},right_ok: {Nat.is_le(lower,right) == True{} : Bool}) ->
69	  {Nat.is_le(lower,Bool.pick(Nat,choice,left,right)) == True{} : Bool}:
70	  match choice:
71	    case False{}: right_ok
72	    case True{}: left_ok
73	
74	def pick_strict_lower(choice: Bool,+left: Nat,+right: Nat,+lower: Nat,left_ok: {Nat.is_lt(lower,left) == True{} : Bool},right_ok: {Nat.is_lt(lower,right) == True{} : Bool}) ->
75	  {Nat.is_lt(lower,Bool.pick(Nat,choice,left,right)) == True{} : Bool}:
76	  match choice:
77	    case False{}: right_ok
78	    case True{}: left_ok
79	
80	def maximum_upper(+left: Nat,+right: Nat,+upper: Nat,left_ok: {Nat.is_le(left,upper) == True{} : Bool},right_ok: {Nat.is_le(right,upper) == True{} : Bool}) ->
81	  {Nat.is_le(Nat.max(left,right),upper) == True{} : Bool}:
82	  %Equal.sym(Nat,Nat.max(left,right),Bool.pick(Nat,Nat.is_lt(left,right),right,left),maximum_choice(left,right)) : {Nat.is_le(_,upper) == True{} : Bool}
83	  pick_upper(Nat.is_lt(left,right),right,left,upper,right_ok,left_ok)
84	
85	def minimum_lower(+left: Nat,+right: Nat,+lower: Nat,left_ok: {Nat.is_le(lower,left) == True{} : Bool},right_ok: {Nat.is_le(lower,right) == True{} : Bool}) ->
86	  {Nat.is_le(lower,Nat.min(left,right)) == True{} : Bool}:
87	  %Equal.sym(Nat,Nat.min(left,right),Bool.pick(Nat,Nat.is_lt(left,right),left,right),minimum_choice(left,right)) : {Nat.is_le(lower,_) == True{} : Bool}
88	  pick_lower(Nat.is_lt(left,right),left,right,lower,left_ok,right_ok)
89	
90	def minimum_strict_lower(+left: Nat,+right: Nat,+lower: Nat,left_ok: {Nat.is_lt(lower,left) == True{} : Bool},right_ok: {Nat.is_lt(lower,right) == True{} : Bool}) ->
91	  {Nat.is_lt(lower,Nat.min(left,right)) == True{} : Bool}:
92	  %Equal.sym(Nat,Nat.min(left,right),Bool.pick(Nat,Nat.is_lt(left,right),left,right),minimum_choice(left,right)) : {Nat.is_lt(lower,_) == True{} : Bool}
93	  pick_strict_lower(Nat.is_lt(left,right),left,right,lower,left_ok,right_ok)
94	
95	def minimum_monotone(+left: Nat,+right: Nat,+limit: Nat,ordered: {Nat.is_le(left,right) == True{} : Bool}) ->
96	  {Nat.is_le(Nat.min(limit,left),Nat.min(limit,right)) == True{} : Bool}:
97	  minimum_lower(limit,right,Nat.min(limit,left),minimum_left(limit,left),Order.transitive(Nat.min(limit,left),left,right,minimum_right(limit,left),ordered))
98	
99	def clipped_end(+first: Nat,+end: Nat) -> {Nat.add(first,Nat.sub(end,first)) == Nat.max(first,end) : Nat}:
100	  match first end:
101	    case 0n +end: Order.subtract_zero(end)
102	    case 1n+ +first 0n: Order.commutative(1n+first,0n)
103	    case 1n+ +first 1n+ +end:
104	      Equal.cong(Nat,Nat,value => 1n+value,Nat.add(first,Nat.sub(end,first)),Nat.max(first,end),clipped_end(first,end))
105	
106	def below_zero_right(choice: Bool) -> {False{} == choice && False{} : Bool}:
107	  match choice:
108	    case False{}: {==}
109	    case True{}: {==}
110	
111	# A lane belongs to a clipped count exactly when it belongs to both bounds.
112	def below_minimum(+value: Nat,+left: Nat,+right: Nat) ->
113	  {Nat.is_lt(value,Nat.min(left,right)) == Nat.is_lt(value,left) && Nat.is_lt(value,right) : Bool}:
114	  match value left right:
115	    case value 0n right: {==}
116	    case value 1n+left 0n:
117	      below_zero_right(Nat.is_lt(value,1n+left))
118	    case 0n 1n+left 1n+right: {==}
119	    case 1n+value 1n+left 1n+right: below_minimum(value,left,right)