proofs/nat_extrema.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/nat_extrema.bend as Nat_extrema

Minimum and maximum laws used by interval intersection. Proofs follow the official structural definitions; no bounded dimension is enumerated.

3 imports

import Base
import ./nat_order.bend as Order
import ./word_encoding.bend as WordEncoding

Definitions

def successor_pick source · line 7 · raw

@choice:Bool -> @+left:Nat -> @+right:Nat -> {1n+Bool.pick(Nat, choice, left, right) == Bool.pick(Nat, choice, 1n+left, 1n+right) : Nat}

def minimum_choice source · line 13 · raw

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

def maximum_choice source · line 22 · raw

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

def minimum_when_ordered source · line 31 · raw

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

def minimum_left source · line 38 · raw

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

def minimum_right source · line 44 · raw

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

def maximum_left source · line 50 · raw

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

def maximum_right source · line 56 · raw

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

def pick_upper source · line 62 · raw

@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} -> {Nat.is_le(Bool.pick(Nat, choice, left, right), upper) == True{} : Bool}

def pick_lower source · line 68 · raw

@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} -> {Nat.is_le(lower, Bool.pick(Nat, choice, left, right)) == True{} : Bool}

def pick_strict_lower source · line 74 · raw

@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} -> {Nat.is_lt(lower, Bool.pick(Nat, choice, left, right)) == True{} : Bool}

def maximum_upper source · line 80 · raw

@+left:Nat -> @+right:Nat -> @+upper:Nat -> @left_ok:{Nat.is_le(left, upper) == True{} : Bool} -> @right_ok:{Nat.is_le(right, upper) == True{} : Bool} -> {Nat.is_le(Nat.max(left, right), upper) == True{} : Bool}

def minimum_lower source · line 85 · raw

@+left:Nat -> @+right:Nat -> @+lower:Nat -> @left_ok:{Nat.is_le(lower, left) == True{} : Bool} -> @right_ok:{Nat.is_le(lower, right) == True{} : Bool} -> {Nat.is_le(lower, Nat.min(left, right)) == True{} : Bool}

def minimum_strict_lower source · line 90 · raw

@+left:Nat -> @+right:Nat -> @+lower:Nat -> @left_ok:{Nat.is_lt(lower, left) == True{} : Bool} -> @right_ok:{Nat.is_lt(lower, right) == True{} : Bool} -> {Nat.is_lt(lower, Nat.min(left, right)) == True{} : Bool}

def minimum_monotone source · line 95 · raw

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

def clipped_end source · line 99 · raw

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

def below_zero_right source · line 106 · raw

@choice:Bool -> {False{} == Bool.and(choice, False{}) : Bool}

def below_minimum source · line 112 · raw

@+value:Nat -> @+left:Nat -> @+right:Nat -> {Nat.is_lt(value, Nat.min(left, right)) == Bool.and(Nat.is_lt(value, left), Nat.is_lt(value, right)) : Bool}

A lane belongs to a clipped count exactly when it belongs to both bounds.