1	# bend-mathlib/equal.bend: equality lemmas (congruence, substitution, chains).
2	import Base
3	
4	# Applying a two-argument function to equal arguments gives equal results.
5	law 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	
18	def 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.
24	law 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	
33	def 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.
38	law 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	
49	def 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.
55	law cong_succ:
56	  for -a: Nat
57	  for -b: Nat
58	  for e: {a == b : Nat}
59	  {1n+a == 1n+b : Nat}
60	
61	def cong_succ(a, b, e):
62	  %e : {1n+a == 1n+_ : Nat}
63	  {==}