proofs/nat_extrema.bend

stelliferous@0.0.2.0 · 119 lines · 18 definitions

1# Minimum and maximum laws used by interval intersection. Proofs follow the
2# official structural definitions; no bounded dimension is enumerated.
3import Base
4import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
5import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
6
7def 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
13def 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
22def 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
31def 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
38def 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
44def 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
50def 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
56def 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
62def 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
68def 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
74def 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
80def 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
85def 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
90def 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
95def 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
99def 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
106def 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.
112def 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)