equal.bend

bend-mathlib@0.1.0.0 · 62 lines · 0 definitions

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