~/bend-docscommunity

proofs/nat_order.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/nat_order.bend as Nat_order

5 imports
import Base
import ./natural_addition.bend as Addition
import ./u32_comparison.bend as Comparison
import ./nat_to_u32_bounds.bend as Bounds
import ./word_encoding.bend as WordEncoding

Types

type UpperBound source · line 82 · raw

@-value:Nat -> @-limit:Nat -> Data

Definitions

def not_below source · line 8 · raw

@+lower:Nat -> @+value:Nat -> @room:{Nat.is_le(lower, value) == True{} : Bool} -> {Nat.is_lt(value, lower) == False{} : Bool}

def cancel_offset_le source · line 15 · raw

@+offset:Nat -> @+left:Nat -> @+right:Nat -> @ordered:{Nat.is_le(Nat.add(offset, left), Nat.add(offset, right)) == True{} : Bool} -> {Nat.is_le(left, right) == True{} : Bool}

def equal_of_is_eq source · line 21 · raw

@+left:Nat -> @+right:Nat -> @equal:{Nat.is_eq(left, right) == True{} : Bool} -> {left == right : Nat}

def subtract_zero source · line 30 · raw

@+value:Nat -> {Nat.sub(value, 0n) == value : Nat}

def zero_subtract source · line 35 · raw

@value:Nat -> {Nat.sub(0n, value) == 0n : Nat}

def subtract_shift source · line 40 · raw

@+first:Nat -> @+row:Nat -> {Nat.sub(Nat.add(first, row), first) == row : Nat}

def restore_shift source · line 45 · raw

@+first:Nat -> @+row:Nat -> @lower:{Nat.is_le(first, row) == True{} : Bool} -> {Nat.add(first, Nat.sub(row, first)) == row : Nat}

def cancel_sum source · line 52 · raw

@+offset:Nat -> @+left:Nat -> @+right:Nat -> @equation:{Nat.add(offset, left) == Nat.add(offset, right) : Nat} -> {left == right : Nat}

def positive_difference source · line 57 · raw

@+end:Nat -> @+begin:Nat -> @positive:{Nat.is_lt(begin, end) == True{} : Bool} -> {Nat.is_lt(0n, Nat.sub(end, begin)) == True{} : Bool}

def positive_has_last source · line 64 · raw

@+size:Nat -> @positive:{Nat.is_lt(0n, size) == True{} : Bool} -> {1n+Nat.sub(size, 1n) == size : Nat}

def split_at_element source · line 71 · raw

@+total:Nat -> @+index:Nat -> @inside:{Nat.is_lt(index, total) == True{} : Bool} -> {Nat.add(index, 1n+Nat.sub(total, 1n+index)) == total : Nat}

def lift_upper_bound source · line 86 · raw

@+value:Nat -> @+limit:Nat -> @bound:UpperBound<value, limit> -> UpperBound<1n+value, 1n+limit>

def upper_bound_cases source · line 91 · raw

@+value:Nat -> @+limit:Nat -> @bounded:{Nat.is_le(value, limit) == True{} : Bool} -> UpperBound<value, limit>

def comparison_not_less source · line 98 · raw

@+comparison:Cmp -> @h:{Cmp.is_lt(comparison) == False{} : Bool} -> {Cmp.is_ge(comparison) == True{} : Bool}

def comparison_less_not_equal source · line 105 · raw

@+comparison:Cmp -> @less:{Cmp.is_lt(comparison) == True{} : Bool} -> {Cmp.is_eq(comparison) == False{} : Bool}

def less_not_equal source · line 111 · raw

@+left:Nat -> @+right:Nat -> @less:{Nat.is_lt(left, right) == True{} : Bool} -> {Nat.is_eq(left, right) == False{} : Bool}

def equal_reflexive source · line 114 · raw

@+value:Nat -> {Nat.is_eq(value, value) == True{} : Bool}

def equal_symmetric source · line 119 · raw

@+left:Nat -> @+right:Nat -> {Nat.is_eq(left, right) == Nat.is_eq(right, left) : Bool}

def zero_le source · line 126 · raw

@+a:Nat -> {Nat.is_le(0n, a) == True{} : Bool}

def reflexive source · line 133 · raw

@+a:Nat -> {Nat.is_le(a, a) == True{} : Bool}

def offset_le source · line 140 · raw

@offset:Nat -> @+left:Nat -> @+right:Nat -> @ordered:{Nat.is_le(left, right) == True{} : Bool} -> {Nat.is_le(Nat.add(offset, left), Nat.add(offset, right)) == True{} : Bool}

def offset_lt source · line 146 · raw

@+offset:Nat -> @+left:Nat -> @+right:Nat -> @ordered:{Nat.is_lt(left, right) == True{} : Bool} -> {Nat.is_lt(Nat.add(offset, left), Nat.add(offset, right)) == True{} : Bool}

def cancel_offset_lt source · line 152 · raw

@+offset:Nat -> @+left:Nat -> @+right:Nat -> @ordered:{Nat.is_lt(Nat.add(offset, left), Nat.add(offset, right)) == True{} : Bool} -> {Nat.is_lt(left, right) == True{} : Bool}

def successor source · line 158 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(a, 1n+b) == True{} : Bool}

def transitive source · line 169 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @ab:{Nat.is_le(a, b) == True{} : Bool} -> @bc:{Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_le(a, c) == True{} : Bool}

def le_add source · line 185 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(a, Nat.add(a, b)) == True{} : Bool}

def le_double source · line 192 · raw

@+a:Nat -> {Nat.is_le(a, Nat.double(a)) == True{} : Bool}

def double_le source · line 196 · raw

@+a:Nat -> @+b:Nat -> @ordered:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(Nat.double(a), Nat.double(b)) == True{} : Bool}

def sub_le source · line 202 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}

def sub_lt source · line 213 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @order:{Nat.is_le(b, a) == True{} : Bool} -> @bound:{Nat.is_lt(a, Nat.add(b, c)) == True{} : Bool} -> {Nat.is_lt(Nat.sub(a, b), c) == True{} : Bool}

def ge_le source · line 225 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}

def ge_true source · line 236 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_ge(a, b) == True{} : Bool} -> {Nat.is_le(b, a) == True{} : Bool}

def ge_false source · line 240 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_ge(a, b) == False{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def digit_lt source · line 251 · raw

@+a:Nat -> @+b:Nat -> @+bit:Bool -> @h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(bit, a), Nat.double(b)) == True{} : Bool}

def digit_bounded source · line 267 · raw

@+a:Nat -> @+b:Nat -> @+bit:Bool -> @+cap:Nat -> @small:{Nat.is_lt(a, b) == True{} : Bool} -> @large:{Nat.is_le(Nat.double(b), cap) == True{} : Bool} -> {Nat.is_le(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(bit, a), cap) == True{} : Bool}

def commutative source · line 272 · raw

@+a:Nat -> @+b:Nat -> {Nat.add(a, b) == Nat.add(b, a) : Nat}

def le_lt_trans source · line 281 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @ab:{Nat.is_le(a, b) == True{} : Bool} -> @bc:{Nat.is_lt(b, c) == True{} : Bool} -> {Nat.is_lt(a, c) == True{} : Bool}

def advance_room source · line 297 · raw

@+i:Nat -> @+tail:Nat -> @+cap:Nat -> @h:{Nat.is_le(Nat.add(i, 1n+tail), cap) == True{} : Bool} -> {Nat.is_le(Nat.add(1n+i, tail), cap) == True{} : Bool}

def room_index source · line 302 · raw

@+i:Nat -> @+tail:Nat -> @+cap:Nat -> @h:{Nat.is_le(Nat.add(i, 1n+tail), cap) == True{} : Bool} -> {Nat.is_lt(i, cap) == True{} : Bool}

def lt_succ source · line 306 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_lt(a, 1n+b) == True{} : Bool}

Order structure shared by padding, allocation and mixed-radix indexing.

def add_le source · line 318 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}

Order structure shared by padding, allocation and mixed-radix indexing.

def add_lt source · line 332 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}

Order structure shared by padding, allocation and mixed-radix indexing.

def strict_follow source · line 346 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(1n+a, b) == True{} : Bool}

Order structure shared by padding, allocation and mixed-radix indexing.

def below_difference source · line 358 · raw

@+offset:Nat -> @+value:Nat -> @+end:Nat -> @ordered:{Nat.is_le(offset, end) == True{} : Bool} -> {Nat.is_lt(value, Nat.sub(end, offset)) == Nat.is_lt(Nat.add(offset, value), end) : Bool}

Translate a comparison against a remaining extent to its absolute position.

def antisymmetric source · line 369 · raw

@+left:Nat -> @+right:Nat -> @forward:{Nat.is_le(left, right) == True{} : Bool} -> @backward:{Nat.is_le(right, left) == True{} : Bool} -> {left == right : Nat}

Two opposite bounds identify a natural number.