michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(equality): make homogeneous equality the default equality

Browse source 
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>
This commit is contained in:
Leonardo de Moura 2013-10-29 16:20:02 -07:00
parent d0009d0242
commit 4dd6cead83
22 changed files with 112 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/notation.cpp
View file

@ -15,10 +15,9 @@ namespace lean {
\brief Initialize builtin notation.
*/
void init_builtin_notation(frontend & f) {
f.add_infix("=", 50, mk_homo_eq_fn());
f.mark_implicit_arguments(mk_homo_eq_fn(), {true, false, false});
f.mark_implicit_arguments(mk_if_fn(), {true, false, false, false});
f.add_infix("==", 50, mk_homo_eq_fn());
f.add_infix("≃", 50, mk_homo_eq_fn());
f.add_prefix("\u00ac", 40, mk_not_fn()); // "¬"
f.add_infixr("&&", 35, mk_and_fn()); // "&&"

2
src/frontends/lean/pp.cpp
View file

@ -57,7 +57,7 @@ Author: Leonardo de Moura
namespace lean {
static format g_Type_fmt = highlight_builtin(format("Type"));
static format g_eq_fmt = format("=");
static format g_eq_fmt = format("==");
static format g_lambda_n_fmt = highlight_keyword(format("\u03BB"));
static format g_Pi_n_fmt = highlight_keyword(format("\u03A0"));
static format g_lambda_fmt = highlight_keyword(format("fun"));

4
src/frontends/lean/scanner.cpp
View file

@ -22,7 +22,7 @@ static name g_pi_name("Pi");
static name g_let_name("let");
static name g_in_name("in");
static name g_arrow_name("->");
static name g_eq_name("=");
static name g_eq_name("==");
static name g_forall_name("forall");
static name g_forall_unicode("\u2200");
static name g_exists_name("exists");
@ -393,7 +393,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
case scanner::token::NatVal: out << "Nat"; break;
case scanner::token::DecimalVal: out << "Dec"; break;
case scanner::token::StringVal: out << "String"; break;
case scanner::token::Eq: out << "="; break;
case scanner::token::Eq: out << "=="; break;
case scanner::token::Assign: out << ":="; break;
case scanner::token::Type: out << "Type"; break;
case scanner::token::Placeholder: out << "_"; break;

2
src/kernel/builtin.cpp
View file

@ -155,7 +155,7 @@ MK_CONSTANT(or_fn, name("or"));
MK_CONSTANT(not_fn, name("not"));
MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(homo_eq_fn, name("heq"));
MK_CONSTANT(homo_eq_fn, name("eq"));
// Axioms
MK_CONSTANT(mp_fn, name("MP"));

2
src/kernel/printer.cpp
View file

@ -56,7 +56,7 @@ struct print_expr_fn {
void print_eq(expr const & a, context const & c) {
print_child(eq_lhs(a), c);
out() << " = ";
out() << " == ";
print_child(eq_rhs(a), c);
}

8
src/tests/library/formatter.cpp
View file

@ -16,7 +16,7 @@ static void check(format const & f, char const * expected) {
std::ostringstream strm;
strm << f;
std::cout << strm.str() << "\n";
lean_assert(strm.str() == expected);
lean_assert_eq(strm.str(), expected);
}
static void tst1() {
@ -30,15 +30,15 @@ static void tst1() {
expr y = Const("y");
expr N = Const("N");
expr F = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a)))));
check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x = (f y a))))");
check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x == (f y a))))");
check(fmt(env.get_object("N")), "Variable N : Type");
context ctx;
ctx = extend(ctx, "x", f(a));
ctx = extend(ctx, "y", f(Var(0), N >> N));
ctx = extend(ctx, "z", N, Eq(Var(0), Var(1)));
check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y = x]");
check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y == x]");
check(fmt(ctx, f(Var(0), Var(2))), "f z x");
check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y = x] |- f z x");
check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y == x] |- f z x");
fmt.set_interrupt(true);
fmt.set_interrupt(false);
}

4
tests/lean/arith6.lean.expected.out
View file

@ -7,8 +7,8 @@ false
true
true
Assumed: x
3 + -1 * (x * (3 div x)) = 0
x + -1 * (3 * (x div 3)) = 0
3 + -1 * (x * (3 div x)) == 0
x + -1 * (3 * (x div 3)) == 0
false
Set: lean::pp::notation
Int::divides 3 x

2
tests/lean/cast2.lean.expected.out
View file

@ -6,7 +6,7 @@
Assumed: B'
Assumed: H
Assumed: a
DomInj H : A = A'
DomInj H : A == A'
Proved: BeqB'
Set: lean::pp::implicit
DomInj::explicit A A' (λ x : A, B) (λ x : A', B') H

2
tests/lean/cast3.lean.expected.out
View file

@ -6,7 +6,7 @@
Assumed: B'
Assumed: x
x
x = x
x == x
Assumed: b
Defined: f
Assumed: H

4
tests/lean/elab1.lean
View file

@ -10,9 +10,9 @@ Variable h : Pi (A : Type), A -> A.
Check fun x, fun A : Type, h A x
Variable eq : Pi A : Type, A -> A -> Bool.
Variable my_eq : Pi A : Type, A -> A -> Bool.
Check fun (A B : Type) (a : _) (b : _) (C : Type), eq C a b.
Check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b.
Variable a : Bool
Variable b : Bool

16
tests/lean/elab1.lean.expected.out
View file

@ -123,11 +123,11 @@ x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A
with arguments:
A
x
Assumed: eq
Assumed: my_eq
Failed to solve
A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C
(line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
eq
my_eq
with arguments:
C
a
@ -139,29 +139,29 @@ Error (line: 20, pos: 28) unexpected metavariable occurrence
Failed to solve
⊢ b ≈ a
Substitution
⊢ b ≈ ?M3::2
⊢ b ≈ ?M3::3
Destruct/Decompose
⊢ b = b ≺ ?M3::2 = ?M3::3
⊢ b == b ≺ ?M3::3 == ?M3::4
(line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
Trans::explicit
with arguments:
?M3::0
?M3::1
?M3::2
?M3::3
?M3::4
Refl a
Refl b
Assignment
⊢ a ≈ ?M3::2
⊢ a ≈ ?M3::3
Destruct/Decompose
⊢ a = a ≺ ?M3::1 = ?M3::2
⊢ a == a ≺ ?M3::2 == ?M3::3
(line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of
Trans::explicit
with arguments:
?M3::0
?M3::1
?M3::2
?M3::3
?M3::4
Refl a
Refl b
Failed to solve

15
tests/lean/elab4.lean.expected.out
View file

@ -5,19 +5,24 @@
Assumed: R
Proved: R2
Set: lean::pp::implicit
Variable C {A B : Type} (H : A = B) (a : A) : B
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 : (Π x : A, B x) = (Π x : A', B' x)) : A = 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 : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
(B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
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 : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
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

15
tests/lean/elab5.lean.expected.out
View file

@ -5,19 +5,24 @@
Assumed: R
Proved: R2
Set: lean::pp::implicit
Variable C {A B : Type} (H : A = B) (a : A) : B
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 : (Π x : A, B x) = (Π x : A', B' x)) : A = 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 : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
(B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
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 : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
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

5
tests/lean/eq1.lean Normal file
View file

@ -0,0 +1,5 @@
Variable i : Int
Check i = 0
Set pp::coercion true
Check i = 0

6
tests/lean/eq1.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
Set: pp::colors
Set: pp::unicode
Assumed: i
i = 0 : Bool
Set: lean::pp::coercion
i = (nat_to_int 0) : Bool

4
tests/lean/tst1.lean.expected.out
View file

@ -26,7 +26,7 @@ Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2
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) ⊤ ⊥
if (two == two) ⊤ ⊥
update (const three ⊥) two ⊤ : vector Bool three
--------
@ -46,4 +46,4 @@ map normal form -->
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)
λ (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)

2
tests/lean/tst11.lean.expected.out
View file

@ -6,7 +6,7 @@
⊤
Assumed: a
a ⊕ a ⊕ a
Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a = b) → (P b)
Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a == b) → (P b)
Proved: EM2
EM2 : Π a : Bool, a ∨ ¬ a
EM2 a : a ∨ ¬ a

3
tests/lean/tst17.lean.expected.out
View file

@ -5,5 +5,6 @@
∀ a b : Type, ∃ c : Type, (g a b) = (f c)
∀ a b : Type, ∃ c : Type, (g a b) = (f c) : Bool
(λ a : Type,
(λ b : Type, if ((λ x : Type, if ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) = (λ x : Type, ⊤)) =
(λ b : Type, if ((λ x : Type, if ((g a b) == (f x)) ⊥ ⊤) == (λ x : Type, ⊤)) ⊥ ⊤) ==
(λ x : Type, ⊤)) ==
(λ x : Type, ⊤)

14
tests/lean/tst4.lean.expected.out
View file

@ -11,7 +11,7 @@ f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
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))
Π (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
@ -19,8 +19,8 @@ f::explicit N n1 n2
Assumed: g
Assumed: H1
Proved: Pr
Axiom H1 : a = b ∧ b = c
Theorem Pr : (g a) = (g c) :=
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)
@ -29,4 +29,10 @@ Theorem Pr : (g a) = (g c) :=
a
c
(Refl::explicit (N → N) g)
(Trans::explicit N a b c (Conjunct1::explicit (a = b) (b = c) H1) (Conjunct2::explicit (a = b) (b = c) H1))
(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))

10
tests/lean/tst5.lean
View file

@ -1,9 +1,9 @@
Variable N : Type
Variable a : N
Variable b : N
Show a ≃ b
Check a ≃ b
Show a = b
Check a = b
Set lean::pp::implicit true
Show a ≃ b
Show (Type 1) ≃ (Type 1)
Show true ≃ false
Show a = b
Show (Type 1) = (Type 1)
Show true = false

10
tests/lean/tst5.lean.expected.out
View file

@ -3,9 +3,9 @@
Assumed: N
Assumed: a
Assumed: b
a ≃ b
a ≃ b : Bool
a = b
a = b : Bool
Set: lean::pp::implicit
heq::explicit N a b
heq::explicit (Type 2) (Type 1) (Type 1)
heq::explicit Bool ⊤ ⊥
eq::explicit N a b
eq::explicit (Type 2) (Type 1) (Type 1)
eq::explicit Bool ⊤ ⊥

53
tests/lean/tst6.lean.expected.out
View file

@ -4,7 +4,10 @@
Assumed: h
Proved: CongrH
Set: lean::pp::implicit
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
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)
@ -20,13 +23,17 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h
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 : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
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
(a = b ∧ b = c)
(a = d ∧ d = c)
((h a b) = (h c b))
(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 : a = b ∧ b = c,
(λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
CongrH::explicit
a
b
@ -37,10 +44,10 @@ Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
a
b
c
(Conjunct1::explicit (a = b) (b = c) H1)
(Conjunct2::explicit (a = b) (b = c) H1))
(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 : a = d ∧ d = c,
(λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
CongrH::explicit
a
b
@ -51,18 +58,22 @@ Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
a
d
c
(Conjunct1::explicit (a = d) (d = c) H1)
(Conjunct2::explicit (a = d) (d = c) H1))
(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 : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
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
(a = b ∧ b = c)
(a = d ∧ d = c)
((h a b) = (h c b))
(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 : a = b ∧ b = c,
(λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
CongrH::explicit
a
b
@ -73,10 +84,10 @@ Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
a
b
c
(Conjunct1::explicit (a = b) (b = c) H1)
(Conjunct2::explicit (a = b) (b = c) H1))
(Conjunct1::explicit (a == b) (b == c) H1)
(Conjunct2::explicit (a == b) (b == c) H1))
(Refl::explicit N b))
(λ H1 : a = d ∧ d = c,
(λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
CongrH::explicit
a
b
@ -87,8 +98,8 @@ Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
a
d
c
(Conjunct1::explicit (a = d) (d = c) H1)
(Conjunct2::explicit (a = d) (d = c) H1))
(Conjunct1::explicit (a == d) (d == c) H1)
(Conjunct2::explicit (a == d) (d == c) H1))
(Refl::explicit N b))
Proved: Example3
Set: lean::pp::implicit