proofs/lib/logic.bend source

proofs/lib/logic.bend on the hub · documented module

import Base# Propositional helpers shared by every proof module.def truth(b: Bool) -> Type:  match b:    case False{}:      Empty    case True{}:      Unitdef false_true(e: {False{} == True{} : Bool}) -> Empty:  %Equal.sym(Bool, False{}, True{}, e) : truth(_)  Unit{}def true_false(e: {True{} == False{} : Bool}) -> Empty:  false_true(Equal.sym(Bool, True{}, False{}, e))def and_left(a: Bool, b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:  match a:    case False{}:      Empty.absurd({False{} == True{} : Bool}, false_true(e))    case True{}:      {==}def and_right(a: Bool, b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:  match a:    case False{}:      Empty.absurd({b == True{} : Bool}, false_true(e))    case True{}:      edef and_intro(a: Bool, b: Bool, ea: {a == True{} : Bool}, eb: {b == True{} : Bool}) -> {Bool.and(a, b) == True{} : Bool}:  %Equal.sym(Bool, a, True{}, ea) : {Bool.and(_, b) == True{} : Bool}  ebdef not_true(b: Bool, e: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:  match b:    case False{}:      {==}    case True{}:      Empty.absurd({True{} == False{} : Bool}, false_true(e))def not_false(b: Bool, e: {b == False{} : Bool}) -> {Bool.not(b) == True{} : Bool}:  %Equal.sym(Bool, b, False{}, e) : {Bool.not(_) == True{} : Bool}  {==}def bool_cases(b: Bool) -> Or({b == True{} : Bool}, {b == False{} : Bool}):  match b:    case True{}:      Inl{{==}}    case False{}:      Inr{{==}}def true_not_false(b: Bool, t: {b == True{} : Bool}, f: {b == False{} : Bool}) -> Empty:  false_true(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, f), t))# Cmp discrimination.def cmp_code(c: Cmp) -> Nat:  match c:    case LT{}:      0n    case EQ{}:      1n    case GT{}:      2ndef cmp_lt_eq(e: {LT{} == EQ{} : Cmp}) -> Empty:  %e : truth(Cmp.is_lt(_))  Unit{}def cmp_lt_gt(e: {LT{} == GT{} : Cmp}) -> Empty:  %e : truth(Cmp.is_lt(_))  Unit{}def cmp_eq_gt(e: {EQ{} == GT{} : Cmp}) -> Empty:  %e : truth(Cmp.is_eq(_))  Unit{}# Maybe discrimination.def none_some(-A: Data, x: A, e: {None{} == Some{x} : Maybe<&2, A>}) -> Empty:  %Equal.sym(Maybe<&2, A>, None{}, Some{x}, e) : truth(Maybe.is_some(&2, A, _))  Unit{}def some_value(-A: Data, m: Maybe<&2, A>, d: A) -> A:  match m:    case None{}:      d    case Some{x}:      xdef some_inj(-A: Data, x: A, y: A, e: {Some{x} == Some{y} : Maybe<&2, A>}) -> {x == y : A}:  Equal.cong(Maybe<&2, A>, A, m => some_value(A, m, x), Some{x}, Some{y}, e)def pair_fst(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {a == c : A}:  Equal.cong(A & B, A, p => Pair.fst(A, B, p), (a, b), (c, d), e)def pair_snd(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {b == d : B}:  Equal.cong(A & B, B, p => Pair.snd(A, B, p), (a, b), (c, d), e)def pair_eq(-A: Type, -B: Type, a: A, b: B, c: A, d: B, ea: {a == c : A}, eb: {b == d : B}) -> {(a, b) == (c, d) : A & B}:  %ea : {(a, b) == (_, d) : A & B}  %eb : {(a, b) == (a, _) : A & B}  {==}# Transport a proof along an equation.def subst(-A: Type, -P: A -> Type, -a: A, -b: A, e: {a == b : A}, pa: P(a)) -> P(b):  %e : P(_)  pa# Dependent pair projections (call results cannot be destructured directly).def sfst(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> A:  match p:    case Tuple{a, b}:      adef ssnd(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> B(sfst(A, B, p)):  match p:    case Tuple{a, b}:      bdef pair_eta(-A: Type, -B: Type, p: A & B) -> {p == (Pair.fst(A, B, p), Pair.snd(A, B, p)) : A & B}:  match p:    case Tuple{a, b}:      {==}