812c1a2960
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics. For example, in one of the tests, the elaborator was producing the sub-expression (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤) After, this commit it produces (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1) The expressions above are definitionally equal, but the second is easier to work with. Question: do we really need hidden definitions? Perhaps, we can use only the opaque flag. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
118 lines
4.1 KiB
Text
118 lines
4.1 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) (eq::explicit N b c) H1)
|
||
(Conjunct2::explicit (eq::explicit N 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) (eq::explicit N d c) H1)
|
||
(Conjunct2::explicit (eq::explicit N 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))
|