~/bend-docscommunity

proofs/lib/order.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as Order

6 imports
import Base
import ../../spec/lib/order.bend as SO
import ./logic.bend as L
import ./nat.bend as N
import ./u32.bend as U
import ./lemmas/proofs/string_compare.bend as NM

Definitions

def flipc source · line 14 · raw

@c:Cmp -> Cmp

def lec source · line 17 · raw

@c:Cmp -> Bool

def self_flip source · line 41 · raw

@+c:Cmp -> @+e:{c == flipc(c) : Cmp} -> {c == EQ{} : Cmp}

def not_le_flip source · line 57 · raw

@+c:Cmp -> @+e:{Cmp.is_le(c) == False{} : Bool} -> {Cmp.is_le(flipc(c)) == True{} : Bool}

def both_le_eq source · line 71 · raw

@+c:Cmp -> @+e1:{Cmp.is_le(c) == True{} : Bool} -> @+e2:{Cmp.is_le(flipc(c)) == True{} : Bool} -> {c == EQ{} : Cmp}

def nat_flip source · line 85 · raw

@+a:Nat -> @+b:Nat -> {Nat.cmp(b, a) == flipc(Nat.cmp(a, b)) : Cmp}

def nat_eq source · line 96 · raw

@+a:Nat -> @+b:Nat -> @+e:{Nat.cmp(a, b) == EQ{} : Cmp} -> {a == b : Nat}

def u32_flip source · line 101 · raw

@+a:U32 -> @+b:U32 -> {U32.cmp(b, a) == flipc(U32.cmp(a, b)) : Cmp}

def u32_antisym source · line 106 · raw

@+a:U32 -> @+b:U32 -> @+e:{U32.cmp(a, b) == EQ{} : Cmp} -> {a == b : U32}

def u32_trans source · line 109 · raw

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

def u32_order source · line 115 · raw

Order(U32, U32.cmp)

def nat_trans source · line 118 · raw

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

def nat_order source · line 121 · raw

Order(Nat, Nat.cmp)

def lex source · line 126 · raw

@c:Cmp -> @r:Cmp -> Cmp

def order_tag source · line 135 · raw

@+a:String -> @+b:String -> {String.order(a, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/string_compare.comparison_tag(String, String.cmp(a, b)) : Cmp}

def so_cons_c source · line 139 · raw

@+x:U32 -> @+t1:String -> @+y:U32 -> @+t2:String -> @+c:Cmp -> @+ec:{U32.cmp(x, y) == c : Cmp} -> {String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}) == lex(c, String.order(t1, t2)) : Cmp}

def so_cons source · line 152 · raw

@+x:U32 -> @+t1:String -> @+y:U32 -> @+t2:String -> {String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}) == lex(U32.cmp(x, y), String.order(t1, t2)) : Cmp}

def flip_lex source · line 155 · raw

@+c:Cmp -> @+r:Cmp -> {lex(flipc(c), flipc(r)) == flipc(lex(c, r)) : Cmp}

def s_flip source · line 164 · raw

@+a:String -> @+b:String -> {String.order(b, a) == flipc(String.order(a, b)) : Cmp}

def s_antisym source · line 179 · raw

@+a:String -> @+b:String -> @+e:{String.order(a, b) == EQ{} : Cmp} -> {a == b : String}

def lt_is source · line 182 · raw

@+c:Cmp -> @+e:{Cmp.is_lt(c) == True{} : Bool} -> {c == LT{} : Cmp}

def u32_lt_le source · line 191 · raw

@+x:U32 -> @+y:U32 -> @+z:U32 -> @+xy:{U32.cmp(x, y) == LT{} : Cmp} -> @+yz:{Cmp.is_le(U32.cmp(y, z)) == True{} : Bool} -> {U32.cmp(x, z) == LT{} : Cmp}

def s_trans_heads source · line 199 · raw

@+x:U32 -> @+y:U32 -> @+z:U32 -> @+o12:Cmp -> @+o23:Cmp -> @+o13:Cmp -> @+cxy:Cmp -> @+exy:{U32.cmp(x, y) == cxy : Cmp} -> @+cyz:Cmp -> @+eyz:{U32.cmp(y, z) == cyz : Cmp} -> @+ab:{Cmp.is_le(lex(cxy, o12)) == True{} : Bool} -> @+bc:{Cmp.is_le(lex(cyz, o23)) == True{} : Bool} -> @ih:(@+ab2:{Cmp.is_le(o12) == True{} : Bool} -> @+bc2:{Cmp.is_le(o23) == True{} : Bool} -> {Cmp.is_le(o13) == True{} : Bool}) -> {Cmp.is_le(lex(U32.cmp(x, z), o13)) == True{} : Bool}

The head-character case of transitivity, given the tails' statement.

def s_trans source · line 220 · raw

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

def string_order source · line 237 · raw

Order(String, String.order)

Templates

template Order source · line 21 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> Type

the laws are stated in spec/lib/order.bend

template flip source · line 24 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @o:Order(A, cmp) -> @+a:A -> @+b:A -> {cmp(b, a) == flipc(cmp(a, b)) : Cmp}

template antisym source · line 29 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @o:Order(A, cmp) -> @+a:A -> @+b:A -> @+e:{cmp(a, b) == EQ{} : Cmp} -> {a == b : A}

template trans source · line 34 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @o:Order(A, cmp) -> @+a:A -> @+b:A -> @+c:A -> @+ab:{Cmp.is_le(cmp(a, b)) == True{} : Bool} -> @+bc:{Cmp.is_le(cmp(b, c)) == True{} : Bool} -> {Cmp.is_le(cmp(a, c)) == True{} : Bool}

template refl source · line 50 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:Order(A, cmp) -> @+a:A -> {cmp(a, a) == EQ{} : Cmp}

template le_refl source · line 53 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:Order(A, cmp) -> @+a:A -> {Cmp.is_le(cmp(a, a)) == True{} : Bool}

template total source · line 67 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:Order(A, cmp) -> @+a:A -> @+b:A -> @+e:{Cmp.is_le(cmp(a, b)) == False{} : Bool} -> {Cmp.is_le(cmp(b, a)) == True{} : Bool}

Totality: not a <= b gives b <= a.

template le_antisym source · line 80 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:Order(A, cmp) -> @+a:A -> @+b:A -> @+ab:{Cmp.is_le(cmp(a, b)) == True{} : Bool} -> @+ba:{Cmp.is_le(cmp(b, a)) == True{} : Bool} -> {a == b : A}