118 lines
4 KiB
Text
118 lines
4 KiB
Text
Set: pp::colors
|
||
Set: pp::unicode
|
||
Assumed: N
|
||
Assumed: h
|
||
Proved: CongrH
|
||
Set: lean::pp::implicit
|
||
Variable h : N → N → N
|
||
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : eq::explicit N a1 b1) (H2 : eq::explicit N a2 b2) : eq::explicit
|
||
N
|
||
(h a1 a2)
|
||
(h b1 b2) :=
|
||
Congr::explicit
|
||
N
|
||
(λ x : N, N)
|
||
(h a1)
|
||
(h b1)
|
||
a2
|
||
b2
|
||
(Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
|
||
H2
|
||
Set: lean::pp::implicit
|
||
Variable h : N → N → N
|
||
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := Congr (Congr (Refl h) H1) H2
|
||
Proved: Example1
|
||
Set: lean::pp::implicit
|
||
Theorem Example1 (a b c d : N)
|
||
(H : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
|
||
N
|
||
(h a b)
|
||
(h c b) :=
|
||
DisjCases::explicit
|
||
(eq::explicit N a b ∧ eq::explicit N b c)
|
||
(eq::explicit N a d ∧ eq::explicit N d c)
|
||
(h a b == h c b)
|
||
H
|
||
(λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
|
||
CongrH::explicit
|
||
a
|
||
b
|
||
c
|
||
b
|
||
(Trans::explicit
|
||
N
|
||
a
|
||
b
|
||
c
|
||
(Conjunct1::explicit (eq::explicit N a b) (eq::explicit N b c) H1)
|
||
(Conjunct2::explicit (eq::explicit N a b) (eq::explicit N b c) H1))
|
||
(Refl::explicit N b))
|
||
(λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
|
||
CongrH::explicit
|
||
a
|
||
b
|
||
c
|
||
b
|
||
(Trans::explicit
|
||
N
|
||
a
|
||
d
|
||
c
|
||
(Conjunct1::explicit (eq::explicit N a d) (eq::explicit N d c) H1)
|
||
(Conjunct2::explicit (eq::explicit N a d) (eq::explicit N d c) H1))
|
||
(Refl::explicit N b))
|
||
Proved: Example2
|
||
Set: lean::pp::implicit
|
||
Theorem Example2 (a b c d : N)
|
||
(H : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
|
||
N
|
||
(h a b)
|
||
(h c b) :=
|
||
DisjCases::explicit
|
||
(eq::explicit N a b ∧ eq::explicit N b c)
|
||
(eq::explicit N a d ∧ eq::explicit N d c)
|
||
(eq::explicit N (h a b) (h c b))
|
||
H
|
||
(λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
|
||
CongrH::explicit
|
||
a
|
||
b
|
||
c
|
||
b
|
||
(Trans::explicit
|
||
N
|
||
a
|
||
b
|
||
c
|
||
(Conjunct1::explicit (a == b) (b == c) H1)
|
||
(Conjunct2::explicit (a == b) (b == c) H1))
|
||
(Refl::explicit N b))
|
||
(λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
|
||
CongrH::explicit
|
||
a
|
||
b
|
||
c
|
||
b
|
||
(Trans::explicit
|
||
N
|
||
a
|
||
d
|
||
c
|
||
(Conjunct1::explicit (a == d) (d == c) H1)
|
||
(Conjunct2::explicit (a == d) (d == c) H1))
|
||
(Refl::explicit N b))
|
||
Proved: Example3
|
||
Set: lean::pp::implicit
|
||
Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a b = h c b :=
|
||
DisjCases
|
||
H
|
||
(λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
|
||
(λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
|
||
Proved: Example4
|
||
Set: lean::pp::implicit
|
||
Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a c = h c a :=
|
||
DisjCases
|
||
H
|
||
(λ H1 : a = b ∧ b = e ∧ b = c,
|
||
let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
|
||
(λ H1 : a = d ∧ d = c, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))
|