20a36e98ec
Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P.
For example, consider the constraint
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b))
Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet.
So, the elaborator would continue to process the constraint, and convert it into:
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true
Now, ?M::1 is assigned to the term
if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true
This is bad, since the original structure was lost.
This commit also contains an example that only works after the commit is applied.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
118 lines
4.2 KiB
Text
118 lines
4.2 KiB
Text
Set: pp::colors
|
||
Set: pp::unicode
|
||
Assumed: N
|
||
Assumed: h
|
||
Proved: CongrH
|
||
Set: lean::pp::implicit
|
||
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
|
||
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
|
||
Set: lean::pp::implicit
|
||
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
|
||
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH 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))
|