4dd6cead83
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.
- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
l = nil
will not propagate the type (List Int) to nil.
- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.
Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
38 lines
985 B
Text
38 lines
985 B
Text
Set: pp::colors
|
|
Set: pp::unicode
|
|
Assumed: f
|
|
Assumed: N
|
|
Assumed: n1
|
|
Assumed: n2
|
|
Set: lean::pp::implicit
|
|
f::explicit N n1 n2
|
|
f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
|
|
Assumed: EqNice
|
|
EqNice::explicit N n1 n2
|
|
f::explicit N n1 n2 : N
|
|
Congr::explicit :
|
|
Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), (f == g) → (a == b) → ((f a) == (g b))
|
|
f::explicit N n1 n2
|
|
Assumed: a
|
|
Assumed: b
|
|
Assumed: c
|
|
Assumed: g
|
|
Assumed: H1
|
|
Proved: Pr
|
|
Axiom H1 : eq::explicit N a b ∧ eq::explicit N b c
|
|
Theorem Pr : eq::explicit N (g a) (g c) :=
|
|
Congr::explicit
|
|
N
|
|
(λ x : N, N)
|
|
g
|
|
g
|
|
a
|
|
c
|
|
(Refl::explicit (N → N) g)
|
|
(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))
|