~/bend-docscommunity

equal.bend checks

raw source on the hub · import bend-mathlib@0.7.0.0/equal.bend as MEqual

bend-mathlib/equal.bend: equality lemmas (congruence, substitution, chains).

1 import
import Base

Laws

law cong2 provedsource · line 5 · raw

@-A:Type -> @-B:Type -> @-C:Type -> @-f:(@_:A -> @_:B -> C) -> @-a1:A -> @-a2:A -> @-b1:B -> @-b2:B -> @ea:{a1 == a2 : A} -> @eb:{b1 == b2 : B} -> {f(a1, b1) == f(a2, b2) : C}

Applying a two-argument function to equal arguments gives equal results.

law subst provedsource · line 24 · raw

@-A:Type -> @-P:(@_:A -> Type) -> @-a:A -> @-b:A -> @e:{a == b : A} -> @p:P(a) -> P(b)

If a equals b, any property of a is also a property of b.

law trans3 provedsource · line 38 · raw

@-A:Type -> @-a:A -> @-b:A -> @-c:A -> @-d:A -> @ab:{a == b : A} -> @bc:{b == c : A} -> @cd:{c == d : A} -> {a == d : A}

Equality chains through three steps: a = b, b = c and c = d give a = d.

law cong_succ provedsource · line 55 · raw

@-a:Nat -> @-b:Nat -> @e:{a == b : Nat} -> {1n+a == 1n+b : Nat}

Equal naturals have equal successors.