From 3903be34a432e327ef8e53d1a4b038b44df685d5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Aug 2014 21:26:17 -0700 Subject: [PATCH] feat(frontends/lean): process theorem statement independently of proof, thus we have the same behavior in sequential and parallel compilation modes, closes #84 Signed-off-by: Leonardo de Moura --- library/data/sum.lean | 4 ++-- library/logic/connectives/instances.lean | 13 ++++++------- src/frontends/lean/decl_cmds.cpp | 11 +++++++---- 3 files changed, 15 insertions(+), 13 deletions(-) diff --git a/library/data/sum.lean b/library/data/sum.lean index feec304d0..e2f6bf107 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -63,8 +63,8 @@ theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabite inhabited_mk (inr A (default B)) theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A ⊎ B) - (H1 : ∀a1 a2, decidable (inl B a1 = inl B a2)) - (H2 : ∀b1 b2, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) := + (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2)) + (H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) := rec_on s1 (take a1, show decidable (inl B a1 = s2), from rec_on s2 diff --git a/library/logic/connectives/instances.lean b/library/logic/connectives/instances.lean index 69fb01a58..9184cd28c 100644 --- a/library/logic/connectives/instances.lean +++ b/library/logic/connectives/instances.lean @@ -51,12 +51,11 @@ congr2_mk (assume H3 : b1 ↔ b2, iff_trans H1 (iff_trans H3 (iff_symm H2)))) -- theorem congr_const_iff [instance] := congr.const iff iff_refl -theorem congr_not_compose [instance] := congr.compose congr_not -theorem congr_and_compose [instance] := congr.compose21 congr_and -theorem congr_or_compose [instance] := congr.compose21 congr_or -theorem congr_implies_compose [instance] := congr.compose21 congr_imp -theorem congr_iff_compose [instance] := congr.compose21 congr_iff - +definition congr_not_compose [instance] := congr.compose congr_not +definition congr_and_compose [instance] := congr.compose21 congr_and +definition congr_or_compose [instance] := congr.compose21 congr_or +definition congr_implies_compose [instance] := congr.compose21 congr_imp +definition congr_iff_compose [instance] := congr.compose21 congr_iff -- Generalized substitution -- ------------------------ @@ -104,7 +103,7 @@ relation.is_transitive_mk (@iff_trans) -- Mp-like for iff -- --------------- -theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : relation.mp_like H := +theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : @relation.mp_like iff a b H := relation.mp_like_mk (iff_elim_left H) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 1d44cda43..882974cff 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -310,13 +310,16 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { if (!found_cached) { if (is_theorem) { + auto type_pos = p.pos_of(type); + std::tie(type, new_ls) = p.elaborate_type(type); + ls = append(ls, new_ls); + expr type_as_is = p.save_pos(mk_as_is(type), type_pos); if (!p.collecting_info() && p.num_threads() > 1) { // add as axiom, and create a task to prove the theorem - p.add_delayed_theorem(env, real_n, ls, type, value); - std::tie(type, new_ls) = p.elaborate_type(type); - env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type))); + p.add_delayed_theorem(env, real_n, ls, type_as_is, value); + env = module::add(env, check(env, mk_axiom(real_n, ls, type))); } else { - std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque); + std::tie(type, value, new_ls) = p.elaborate_definition(n, type_as_is, value, modifiers.m_is_opaque); new_ls = append(ls, new_ls); env = module::add(env, check(env, mk_theorem(real_n, new_ls, type, value))); p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);