def gcmp_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:70

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

70# G orders like (E, F) lexicographically
71def gcmp_c(+one: Nat, +h1: {one == 1n : Nat}, +E1: Nat, +b1: Bool, +hb1: {Nat.is_eq(E1, 0n) == b1 : Bool}, +c1: Nat, +hc1: {c1 == SF.b2n(Bool.not(b1)) : Nat}, +F1: Nat, +hF1: {C.fits(52n, F1) == True{} : Bool}, +E2: Nat, +b2: Bool, +hb2: {Nat.is_eq(E2, 0n) == b2 : Bool}, +c2: Nat, +hc2: {c2 == SF.b2n(Bool.not(b2)) : Nat}, +F2: Nat, +hF2: {C.fits(52n, F2) == True{} : Bool}, +d: Cmp, +hd: {Nat.cmp(E1, E2) == d : Cmp}) -> {Nat.cmp(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, b2, 1n, E2), Nat.add(F2, C.shift(52n, c2)))) == NC.lex(d, Nat.cmp(F1, F2)) : Cmp}:
72  match d:
73    case LT{}:
74      +hlt = NC.lt_of_cmp(E1, E2, hd)
75      +eb2 = Equal.trans(Bool, b2, Nat.is_eq(E2, 0n), False{}, Equal.sym(Bool, Nat.is_eq(E2, 0n), b2, hb2), N.is_eq_sym_false(0n, E2, N.is_eq_lt(0n, E2, N.le_lt_trans(0n, E1, E2, N.zero_le(E1), hlt))))
76      +hc2b = L.subst(Bool, z => {c2 == SF.b2n(Bool.not(z)) : Nat}, b2, False{}, eb2, hc2)
77      +r = NC.cmp_lt(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, False{}, 1n, E2), Nat.add(F2, C.shift(52n, c2))), gcmp_lt(one, h1, E1, b1, hb1, c1, hc1, F1, hF1, E2, c2, hc2b, F2, hlt))
78      L.subst(Bool, z => {Nat.cmp(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, z, 1n, E2), Nat.add(F2, C.shift(52n, c2)))) == LT{} : Cmp}, False{}, b2, Equal.sym(Bool, b2, False{}, eb2), r)
79    case GT{}:
80      +hgt = NC.lt_of_gt(E1, E2, hd)
81      +eb1 = Equal.trans(Bool, b1, Nat.is_eq(E1, 0n), False{}, Equal.sym(Bool, Nat.is_eq(E1, 0n), b1, hb1), N.is_eq_sym_false(0n, E1, N.is_eq_lt(0n, E1, N.le_lt_trans(0n, E2, E1, N.zero_le(E2), hgt))))
82      +hc1b = L.subst(Bool, z => {c1 == SF.b2n(Bool.not(z)) : Nat}, b1, False{}, eb1, hc1)
83      +r = NC.cmp_gt(C.shift(SF.pick(Nat, False{}, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, b2, 1n, E2), Nat.add(F2, C.shift(52n, c2))), gcmp_lt(one, h1, E2, b2, hb2, c2, hc2, F2, hF2, E1, c1, hc1b, F1, hgt))
84      L.subst(Bool, z => {Nat.cmp(C.shift(SF.pick(Nat, z, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, b2, 1n, E2), Nat.add(F2, C.shift(52n, c2)))) == GT{} : Cmp}, False{}, b1, Equal.sym(Bool, b1, False{}, eb1), r)
85    case EQ{}:
86      +eE = NC.eq_of_cmp(E1, E2, hd)
87      +eb = Equal.trans(Bool, b1, Nat.is_eq(E1, 0n), b2, Equal.sym(Bool, Nat.is_eq(E1, 0n), b1, hb1), Equal.trans(Bool, Nat.is_eq(E1, 0n), Nat.is_eq(E2, 0n), b2, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), E1, E2, eE), hb2))
88      +ec = Equal.trans(Nat, c1, SF.b2n(Bool.not(b1)), c2, hc1, Equal.trans(Nat, SF.b2n(Bool.not(b1)), SF.b2n(Bool.not(b2)), c2, Equal.cong(Bool, Nat, z => SF.b2n(Bool.not(z)), b1, b2, eb), Equal.sym(Nat, c2, SF.b2n(Bool.not(b2)), hc2)))
89      +S1 = C.shift(52n, c1)
90      +p1 = SF.pick(Nat, b1, 1n, E1)
91      +base = Equal.trans(Cmp, Nat.cmp(C.shift(p1, Nat.add(F1, S1)), C.shift(p1, Nat.add(F2, S1))), Nat.cmp(Nat.add(F1, S1), Nat.add(F2, S1)), Nat.cmp(F1, F2), NC.cmp_shift(p1, Nat.add(F1, S1), Nat.add(F2, S1)), NC.cmp_addr(F1, F2, S1))
92      +s1 = L.subst(Nat, z => {Nat.cmp(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F2, C.shift(52n, z)))) == Nat.cmp(F1, F2) : Cmp}, c1, c2, ec, base)
93      +s2 = L.subst(Bool, z => {Nat.cmp(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, z, 1n, E1), Nat.add(F2, C.shift(52n, c2)))) == Nat.cmp(F1, F2) : Cmp}, b1, b2, eb, s1)
94      L.subst(Nat, z => {Nat.cmp(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, b2, 1n, z), Nat.add(F2, C.shift(52n, c2)))) == Nat.cmp(F1, F2) : Cmp}, E1, E2, eE, s2)