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

refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-07 16:04:44 -08:00
parent 5454e2af32
commit 1ec01f5757
21 changed files with 102 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/builtin/CMakeLists.txt
View file

@ -95,8 +95,7 @@ add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
add_theory("subtype.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
add_theory("optional.lean" "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean")
add_theory("pair.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
add_theory("sum.lean" "${CMAKE_CURRENT_BINARY_DIR}/optional.olean" "${CMAKE_CURRENT_BINARY_DIR}/pair.olean")
add_theory("sum.lean" "${CMAKE_CURRENT_BINARY_DIR}/optional.olean")
update_interface("kernel.olean" "kernel" "-n")
update_interface("Nat.olean" "library/arith" "-n")

37
src/builtin/kernel.lean
View file

@ -766,6 +766,17 @@ theorem allext {A : (Type U)} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (
(assume Hl, take x, (H x) ◂ (Hl x))
(assume Hr, take x, (symm (H x)) ◂ (Hr x))
theorem proj1_congr {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b
:= subst (refl (proj1 a)) H
theorem proj2_congr {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2 b
:= subst (refl (proj2 a)) H
theorem hproj2_congr {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj2 a == proj2 b
:= subst (hrefl (proj2 a)) H
definition pair {A : (Type U)} {B : A → (Type U)} (a : A) (b : B a) := tuple (sig x : A, B x) : a, b
-- Up to this point, we proved all theorems using just reflexivity, substitution and case (proof by cases)
-- Function extensionality
@ -898,10 +909,34 @@ variable ind : Type
axiom infinity : ∃ f : ind → ind, injective f ∧ non_surjective f
-- Pair extensionality
axiom pairext {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x}
axiom pairext {A : (Type U)} {B : A → (Type U)} (a b : sig x, B x)
(H1 : proj1 a = proj1 b) (H2 : proj2 a == proj2 b)
: a = b
theorem pair_proj_eq {A : (Type U)} {B : A → (Type U)} (a : sig x, B x) : pair (proj1 a) (proj2 a) = a
:= have Heq1 : proj1 (pair (proj1 a) (proj2 a)) = proj1 a,
from refl (proj1 a),
have Heq2 : proj2 (pair (proj1 a) (proj2 a)) == proj2 a,
from hrefl (proj2 a),
show pair (proj1 a) (proj2 a) = a,
from pairext (pair (proj1 a) (proj2 a)) a Heq1 Heq2
theorem pair_congr {A : (Type U)} {B : A → (Type U)} {a a' : A} {b : B a} {b' : B a'} (Ha : a = a') (Hb : b == b')
: (pair a b) = (pair a' b')
:= have Heq1 : proj1 (pair a b) = proj1 (pair a' b'),
from Ha,
have Heq2 : proj2 (pair a b) == proj2 (pair a' b'),
from Hb,
show (pair a b) = (pair a' b'),
from pairext (pair a b) (pair a' b') Heq1 Heq2
theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b)
:= pairext p (pair a b) H1 (to_heq H2)
theorem hpairext_proj {A : (Type U)} {B : A → (Type U)} {p : sig x, B x} {a : A} {b : B a}
(H1 : proj1 p = a) (H2 : proj2 p == b) : p = (pair a b)
:= pairext p (pair a b) H1 H2
-- Heterogeneous equality axioms and theorems
-- We can "type-cast" an A expression into a B expression, if we can prove that A == B

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

BIN
src/builtin/obj/optional.olean
View file

Binary file not shown.

BIN
src/builtin/obj/pair.olean
View file

Binary file not shown.

BIN
src/builtin/obj/subtype.olean
View file

Binary file not shown.

BIN
src/builtin/obj/sum.olean
View file

Binary file not shown.

10
src/builtin/pair.lean
View file

@ -1,10 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
definition pair {A : (Type U)} {B : (Type U)} (a : A) (b : B) := tuple a, b
theorem pair_inj1 {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b
:= subst (refl (proj1 a)) H
theorem pair_inj2 {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2 b
:= subst (refl (proj2 a)) H
theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b)
:= @pairext A (λ x, B) p (pair a b) H1 (to_heq H2)

2
src/builtin/subtype.lean
View file

@ -20,7 +20,7 @@ theorem P_rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : P (rep a)
:= proj2 a
theorem rep_inj {A : (Type U)} {P : A → Bool} {a b : subtype A P} (H : rep a = rep b) : a = b
:= pairext H (hproof_irrel (proj2 a) (proj2 b))
:= pairext _ _ H (hproof_irrel (proj2 a) (proj2 b))
theorem ex_abst {A : (Type U)} {P : A → Bool} {r : A} (H : P r) : ∃ a, rep a = r
:= exists_intro (tuple (subtype A P) : r, H) (refl r)

8
src/builtin/sum.lean
View file

@ -2,11 +2,11 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros
import pair
import subtype
import optional
using subtype
using optional
-- We are encoding the (sum A B) as a subtype of (optional A) # (optional B), where
-- (proj1 n = none) ≠ (proj2 n = none)
definition sum_pred (A B : (Type U)) := λ p : (optional A) # (optional B), (proj1 p = none) ≠ (proj2 p = none)
@ -54,7 +54,7 @@ theorem inl_inj {A B : (Type U)} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2
show a1 = a2,
from optional::injectivity
(calc some a1 = proj1 (pair (some a1) (@none B)) : refl (some a1)
... = proj1 (pair (some a2) (@none B)) : pair_inj1 rep_eq
... = proj1 (pair (some a2) (@none B)) : proj1_congr rep_eq
... = some a2 : refl (some a2))
theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
@ -68,7 +68,7 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
show b1 = b2,
from optional::injectivity
(calc some b1 = proj2 (pair (@none A) (some b1)) : refl (some b1)
... = proj2 (pair (@none A) (some b2)) : pair_inj2 rep_eq
... = proj2 (pair (@none A) (some b2)) : @proj2_congr _ _ (pair (@none A) (some b1)) (pair (@none A) (some b2)) rep_eq
... = some b2 : refl (some b2))
theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
@ -80,7 +80,7 @@ theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
have rep_eq : (pair (some a) none) = (pair none (some b)),
from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
show false,
from absurd (pair_inj1 rep_eq) (optional::distinct a)
from absurd (proj1_congr rep_eq) (optional::distinct a)
theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
:= let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n

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

@ -482,7 +482,7 @@ class pp_fn {
return g_arrow_precedence;
} else if (is_cartesian(e)) {
return g_cartesian_product_precedence;
} else if (is_lambda(e) || is_pi(e) || is_let(e) || is_exists(e) || is_sigma(e) || is_pair(e)) {
} else if (is_lambda(e) || is_pi(e) || is_let(e) || is_exists(e) || is_sigma(e) || is_dep_pair(e)) {
return 0;
} else if (is_heq(e)) {
return g_heq_precedence;
@ -1125,7 +1125,7 @@ class pp_fn {
args.push_back(pair_first(a));
expr t = pair_type(a);
bool cartesian = is_cartesian(t);
while (is_pair(pair_second(a)) && !has_metavar(pair_second(a))) {
while (is_dep_pair(pair_second(a)) && !has_metavar(pair_second(a))) {
a = pair_second(a);
if (!is_cartesian(pair_type(a)))
cartesian = false;

6
src/kernel/expr.h
View file

@ -442,7 +442,7 @@ public:
inline bool is_var(expr_cell * e) { return e->kind() == expr_kind::Var; }
inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Constant; }
inline bool is_value(expr_cell * e) { return e->kind() == expr_kind::Value; }
inline bool is_pair(expr_cell * e) { return e->kind() == expr_kind::Pair; }
inline bool is_dep_pair(expr_cell * e) { return e->kind() == expr_kind::Pair; }
inline bool is_proj(expr_cell * e) { return e->kind() == expr_kind::Proj; }
inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; }
inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; }
@ -457,7 +457,7 @@ inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e) || i
inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; }
inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; }
inline bool is_value(expr const & e) { return e.kind() == expr_kind::Value; }
inline bool is_pair(expr const & e) { return e.kind() == expr_kind::Pair; }
inline bool is_dep_pair(expr const & e) { return e.kind() == expr_kind::Pair; }
inline bool is_proj(expr const & e) { return e.kind() == expr_kind::Proj; }
inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; }
inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; }
@ -526,7 +526,7 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3,
// Casting (these functions are only needed for low-level code)
inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); return static_cast<expr_var*>(e); }
inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast<expr_const*>(e); }
inline expr_dep_pair * to_pair(expr_cell * e) { lean_assert(is_pair(e)); return static_cast<expr_dep_pair*>(e); }
inline expr_dep_pair * to_pair(expr_cell * e) { lean_assert(is_dep_pair(e)); return static_cast<expr_dep_pair*>(e); }
inline expr_proj * to_proj(expr_cell * e) { lean_assert(is_proj(e)); return static_cast<expr_proj*>(e); }
inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast<expr_app*>(e); }
inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast<expr_abstraction*>(e); }

8
src/kernel/kernel_decls.cpp
View file

@ -163,6 +163,10 @@ MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel"));
MK_CONSTANT(exists_imp_distribute_fn, name("exists_imp_distribute"));
MK_CONSTANT(forall_uninhabited_fn, name("forall_uninhabited"));
MK_CONSTANT(allext_fn, name("allext"));
MK_CONSTANT(proj1_congr_fn, name("proj1_congr"));
MK_CONSTANT(proj2_congr_fn, name("proj2_congr"));
MK_CONSTANT(hproj2_congr_fn, name("hproj2_congr"));
MK_CONSTANT(pair_fn, name("pair"));
MK_CONSTANT(funext_fn, name("funext"));
MK_CONSTANT(eta_fn, name("eta"));
MK_CONSTANT(eps_fn, name("eps"));
@ -188,6 +192,10 @@ MK_CONSTANT(non_surjective_fn, name("non_surjective"));
MK_CONSTANT(ind, name("ind"));
MK_CONSTANT(infinity, name("infinity"));
MK_CONSTANT(pairext_fn, name("pairext"));
MK_CONSTANT(pair_proj_eq_fn, name("pair_proj_eq"));
MK_CONSTANT(pair_congr_fn, name("pair_congr"));
MK_CONSTANT(pairext_proj_fn, name("pairext_proj"));
MK_CONSTANT(hpairext_proj_fn, name("hpairext_proj"));
MK_CONSTANT(cast_fn, name("cast"));
MK_CONSTANT(cast_heq_fn, name("cast_heq"));
MK_CONSTANT(hsubst_fn, name("hsubst"));

25
src/kernel/kernel_decls.h
View file

@ -473,6 +473,19 @@ inline expr mk_forall_uninhabited_th(expr const & e1, expr const & e2, expr cons
expr mk_allext_fn();
bool is_allext_fn(expr const & e);
inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); }
expr mk_proj1_congr_fn();
bool is_proj1_congr_fn(expr const & e);
inline expr mk_proj1_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_proj1_congr_fn(), e1, e2, e3, e4, e5}); }
expr mk_proj2_congr_fn();
bool is_proj2_congr_fn(expr const & e);
inline expr mk_proj2_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_proj2_congr_fn(), e1, e2, e3, e4, e5}); }
expr mk_hproj2_congr_fn();
bool is_hproj2_congr_fn(expr const & e);
inline expr mk_hproj2_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hproj2_congr_fn(), e1, e2, e3, e4, e5}); }
expr mk_pair_fn();
bool is_pair_fn(expr const & e);
inline bool is_pair(expr const & e) { return is_app(e) && is_pair_fn(arg(e, 0)) && num_args(e) == 5; }
inline expr mk_pair(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_pair_fn(), e1, e2, e3, e4}); }
expr mk_funext_fn();
bool is_funext_fn(expr const & e);
inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); }
@ -550,6 +563,18 @@ bool is_infinity(expr const & e);
expr mk_pairext_fn();
bool is_pairext_fn(expr const & e);
inline expr mk_pairext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_pairext_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_pair_proj_eq_fn();
bool is_pair_proj_eq_fn(expr const & e);
inline expr mk_pair_proj_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_pair_proj_eq_fn(), e1, e2, e3}); }
expr mk_pair_congr_fn();
bool is_pair_congr_fn(expr const & e);
inline expr mk_pair_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_pair_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
expr mk_pairext_proj_fn();
bool is_pairext_proj_fn(expr const & e);
inline expr mk_pairext_proj_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_pairext_proj_fn(), e1, e2, e3, e4, e5, e6, e7}); }
expr mk_hpairext_proj_fn();
bool is_hpairext_proj_fn(expr const & e);
inline expr mk_hpairext_proj_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_hpairext_proj_fn(), e1, e2, e3, e4, e5, e6, e7}); }
expr mk_cast_fn();
bool is_cast_fn(expr const & e);
inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; }

2
src/kernel/normalizer.cpp
View file

@ -265,7 +265,7 @@ class normalizer::imp {
}
case expr_kind::Proj: {
expr new_arg = normalize(proj_arg(a), s, k);
if (is_pair(new_arg)) {
if (is_dep_pair(new_arg)) {
if (proj_first(a))
r = pair_first(new_arg);
else

2
src/kernel/replace_visitor.cpp
View file

@ -19,7 +19,7 @@ expr replace_visitor::visit_constant(expr const & e, context const & ctx) {
return update_const(e, visit(const_type(e), ctx));
}
expr replace_visitor::visit_pair(expr const & e, context const & ctx) {
lean_assert(is_pair(e));
lean_assert(is_dep_pair(e));
return update_pair(e, [&](expr const & f, expr const & s, expr const & t) {
return std::make_tuple(visit(f, ctx), visit(s, ctx), visit(t, ctx));
});

8
src/library/elaborator/elaborator.cpp
View file

@ -668,7 +668,7 @@ class elaborator::imp {
expr new_arg = arg;
if (m_use_normalizer)
new_arg = normalize(ctx, arg);
if (is_pair(new_arg)) {
if (is_dep_pair(new_arg)) {
if (proj_first(a))
a = pair_first(new_arg);
else
@ -1001,7 +1001,7 @@ class elaborator::imp {
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), heq_lhs(b), new_assumption);
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), heq_rhs(b), new_assumption);
imitation = mk_lambda(arg_types, mk_heq(mk_app_h_vars(h_1), mk_app_h_vars(h_2)));
} else if (is_pair(b)) {
} else if (is_dep_pair(b)) {
// Imitation for dependent pairs
expr h_f = new_state.m_menv->mk_metavar(ctx);
expr h_s = new_state.m_menv->mk_metavar(ctx);
@ -1261,7 +1261,7 @@ class elaborator::imp {
void imitate_pair(expr const & a, expr const & b, unification_constraint const & c) {
lean_assert(is_metavar(a));
lean_assert(is_pair(b));
lean_assert(is_dep_pair(b));
lean_assert(!is_assigned(a));
lean_assert(has_local_context(a));
// imitate
@ -1369,7 +1369,7 @@ class elaborator::imp {
} else if (is_heq(b)) {
imitate_heq(a, b, c);
return true;
} else if (is_pair(b)) {
} else if (is_dep_pair(b)) {
imitate_pair(a, b, c);
return true;
}

16
tests/lean/sum2.lean
View file

@ -2,11 +2,11 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros
import pair
import subtype
import optional
using subtype
using optional
-- We are encoding the (sum A B) as a subtype of (optional A) # (optional B), where
-- (proj1 n = none) ≠ (proj2 n = none)
definition sum_pred (A B : (Type U)) := λ p : (optional A) # (optional B), (proj1 p = none) ≠ (proj2 p = none)
@ -16,7 +16,7 @@ namespace sum
theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none)
:= not_intro
(assume N : (some a = none) = (none = (@none B)),
have eq : some a = none,
have eq : some a = none,
from (symm N) ◂ (refl (@none B)),
show false,
from absurd eq (distinct a))
@ -24,7 +24,7 @@ theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (som
theorem inr_pred (A : (Type U)) {B : (Type U)} (b : B) : sum_pred A B (pair none (some b))
:= not_intro
(assume N : (none = (@none A)) = (some b = none),
have eq : some b = none,
have eq : some b = none,
from N ◂ (refl (@none A)),
show false,
from absurd eq (distinct b))
@ -54,11 +54,11 @@ theorem inl_inj {A B : (Type U)} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2
show a1 = a2,
from optional::injectivity
(calc some a1 = proj1 (pair (some a1) (@none B)) : refl (some a1)
... = proj1 (pair (some a2) (@none B)) : pair_inj1 rep_eq
... = some a2 : refl (some a2))
... = proj1 (pair (some a2) (@none B)) : proj1_congr rep_eq
... = some a2 : refl (some a2))
theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
:= assume Heq : inr A b1 = inr A b2,
:= assume Heq : inr A b1 = inr A b2,
have eq1 : inr A b1 = abst (pair none (some b1)) (inhabr A (inhabited_intro b1)),
from refl (inr A b1),
have eq2 : inr A b2 = abst (pair none (some b2)) (inhabr A (inhabited_intro b1)),
@ -68,7 +68,7 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
show b1 = b2,
from optional::injectivity
(calc some b1 = proj2 (pair (@none A) (some b1)) : refl (some b1)
... = proj2 (pair (@none A) (some b2)) : pair_inj2 rep_eq
... = proj2 (pair (@none A) (some b2)) : @proj2_congr _ _ (pair (@none A) (some b1)) (pair (@none A) (some b2)) rep_eq
... = some b2 : refl (some b2))
theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
@ -80,7 +80,7 @@ theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
have rep_eq : (pair (some a) none) = (pair none (some b)),
from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
show false,
from absurd (pair_inj1 rep_eq) (optional::distinct a)
from absurd (proj1_congr rep_eq) (optional::distinct a)
theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
:= let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n

1
tests/lean/sum2.lean.expected.out
View file

@ -1,7 +1,6 @@
Set: pp::colors
Set: pp::unicode
Imported 'macros'
Imported 'pair'
Imported 'subtype'
Imported 'optional'
Using: subtype

16
tests/lean/sum3.lean
View file

@ -2,11 +2,11 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros
import pair
import subtype
import optional
using subtype
using optional
-- We are encoding the (sum A B) as a subtype of (optional A) # (optional B), where
-- (proj1 n = none) ≠ (proj2 n = none)
definition sum_pred (A B : (Type U)) := λ p : (optional A) # (optional B), (proj1 p = none) ≠ (proj2 p = none)
@ -16,7 +16,7 @@ namespace sum
theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none)
:= not_intro
(assume N : (some a = none) = (none = (@none B)),
have eq : some a = none,
have eq : some a = none,
from (symm N) ◂ (refl (@none B)),
show false,
from absurd eq (distinct a))
@ -24,7 +24,7 @@ theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (som
theorem inr_pred (A : (Type U)) {B : (Type U)} (b : B) : sum_pred A B (pair none (some b))
:= not_intro
(assume N : (none = (@none A)) = (some b = none),
have eq : some b = none,
have eq : some b = none,
from N ◂ (refl (@none A)),
show false,
from absurd eq (distinct b))
@ -54,11 +54,11 @@ theorem inl_inj {A B : (Type U)} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2
show a1 = a2,
from optional::injectivity
(calc some a1 = proj1 (pair (some a1) (@none B)) : refl (some a1)
... = proj1 (pair (some a2) (@none B)) : pair_inj1 rep_eq
... = some a2 : refl (some a2))
... = proj1 (pair (some a2) (@none B)) : proj1_congr rep_eq
... = some a2 : refl (some a2))
theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
:= assume Heq : inr A b1 = inr A b2,
:= assume Heq : inr A b1 = inr A b2,
have eq1 : inr A b1 = abst (pair none (some b1)) (inhabr A (inhabited_intro b1)),
from refl (inr A b1),
have eq2 : inr A b2 = abst (pair none (some b2)) (inhabr A (inhabited_intro b1)),
@ -68,7 +68,7 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
show b1 = b2,
from optional::injectivity
(calc some b1 = proj2 (pair (@none A) (some b1)) : refl (some b1)
... = proj2 (pair (@none A) (some b2)) : pair_inj2 rep_eq
... = proj2 (pair (@none A) (some b2)) : @proj2_congr _ _ (pair (@none A) (some b1)) (pair (@none A) (some b2)) rep_eq
... = some b2 : refl (some b2))
theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
@ -80,7 +80,7 @@ theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
have rep_eq : (pair (some a) none) = (pair none (some b)),
from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
show false,
from absurd (pair_inj1 rep_eq) (optional::distinct a)
from absurd (proj1_congr rep_eq) (optional::distinct a)
set_opaque optional false
set_opaque subtype false

1
tests/lean/sum3.lean.expected.out
View file

@ -1,7 +1,6 @@
Set: pp::colors
Set: pp::unicode
Imported 'macros'
Imported 'pair'
Imported 'subtype'
Imported 'optional'
Using: subtype