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>
49 lines
1.9 KiB
Text
49 lines
1.9 KiB
Text
Set: pp::colors
|
||
Set: pp::unicode
|
||
Assumed: N
|
||
Assumed: lt
|
||
Assumed: zero
|
||
Assumed: one
|
||
Assumed: two
|
||
Assumed: three
|
||
Assumed: two_lt_three
|
||
Defined: vector
|
||
Defined: const
|
||
Defined: update
|
||
Defined: select
|
||
Defined: map
|
||
Axiom two_lt_three : two < three
|
||
Definition vector (A : Type) (n : N) : Type := Π (i : N), (i < n) → A
|
||
Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d
|
||
Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d
|
||
Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n :=
|
||
λ (j : N) (H : j < n), if (j = i) d (v j H)
|
||
Definition update::explicit (A : Type) (n : N) (v : vector A n) (i : N) (d : A) : vector A n := update v i d
|
||
Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H
|
||
Definition select::explicit (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n) : A := select v i H
|
||
Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
|
||
λ (i : N) (H : i < n), f (v1 i H) (v2 i H)
|
||
Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
|
||
map f v1 v2
|
||
select (update (const three ⊥) two ⊤) two two_lt_three : Bool
|
||
if (two == two) ⊤ ⊥
|
||
update (const three ⊥) two ⊤ : vector Bool three
|
||
|
||
--------
|
||
select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), (i < n) → A
|
||
|
||
map type --->
|
||
map::explicit : Π (A B C : Type) (n : N), (A → B → C) → (vector A n) → (vector B n) → (vector C n)
|
||
|
||
map normal form -->
|
||
λ (A B C : Type)
|
||
(n : N)
|
||
(f : A → B → C)
|
||
(v1 : Π (i : N), (i < n) → A)
|
||
(v2 : Π (i : N), (i < n) → B)
|
||
(i : N)
|
||
(H : i < n),
|
||
f (v1 i H) (v2 i H)
|
||
|
||
update normal form -->
|
||
λ (A : Type) (n : N) (v : Π (i : N), (i < n) → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)
|