equal.bend

bend-mathlib@0.5.0.0 · 63 lines · 0 definitions

1# bend-mathlib/equal.bend: equality lemmas (congruence, substitution, chains).
2import Base
3
4# Applying a two-argument function to equal arguments gives equal results.
5law cong2:
6  for -A: Type
7  for -B: Type
8  for -C: Type
9  for -f: A -> B -> C
10  for -a1: A
11  for -a2: A
12  for -b1: B
13  for -b2: B
14  for ea: {a1 == a2 : A}
15  for eb: {b1 == b2 : B}
16  {f(a1, b1) == f(a2, b2) : C}
17
18def cong2(A, B, C, f, a1, a2, b1, b2, ea, eb):
19  %ea : {f(a1, b1) == f(_, b2) : C}
20  %eb : {f(a1, b1) == f(a1, _) : C}
21  {==}
22
23# If a equals b, any property of a is also a property of b.
24law subst:
25  for -A: Type
26  for -P: A -> Type
27  for -a: A
28  for -b: A
29  for e: {a == b : A}
30  for p: P(a)
31  P(b)
32
33def subst(A, P, a, b, e, p):
34  %e : P(_)
35  p
36
37# Equality chains through three steps: a = b, b = c and c = d give a = d.
38law trans3:
39  for -A: Type
40  for -a: A
41  for -b: A
42  for -c: A
43  for -d: A
44  for ab: {a == b : A}
45  for bc: {b == c : A}
46  for cd: {c == d : A}
47  {a == d : A}
48
49def trans3(A, a, b, c, d, ab, bc, cd):
50  %cd : {a == _ : A}
51  %bc : {a == _ : A}
52  ab
53
54# Equal naturals have equal successors.
55law cong_succ:
56  for -a: Nat
57  for -b: Nat
58  for e: {a == b : Nat}
59  {1n+a == 1n+b : Nat}
60
61def cong_succ(a, b, e):
62  %e : {1n+a == 1n+_ : Nat}
63  {==}