lean2/tests/lean/elab5.lean.expected.out
Leonardo de Moura 4dd6cead83 refactor(equality): make homogeneous equality the default equality
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>
2013-10-29 16:20:06 -07:00

28 lines
1.1 KiB
Text

Set: pp::colors
Set: pp::unicode
Assumed: C
Assumed: D
Assumed: R
Proved: R2
Set: lean::pp::implicit
Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B
Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a
Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) :
eq::explicit Type A A'
Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A =
A' :=
D H
Variable R {A A' : Type}
{B : A → Type}
{B' : A' → Type}
(H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x))
(a : A) :
eq::explicit Type (B a) (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
Definition R::explicit (A A' : Type)
(B : A → Type)
(B' : A' → Type)
(H : (Π x : A, B x) = (Π x : A', B' x))
(a : A) : (B a) = (B' (C (D H) a)) :=
R H a
Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 :=
R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a