From 20a36e98ecf03b60a65956fb52a97560b084be58 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Nov 2013 09:14:54 -0800 Subject: [PATCH] feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 23 +++- tests/lean/elab1.lean.expected.out | 168 +++++++++++++------------- tests/lean/tactic4.lean | 9 ++ tests/lean/tactic4.lean.expected.out | 4 + tests/lean/tst6.lean.expected.out | 2 +- 5 files changed, 117 insertions(+), 89 deletions(-) create mode 100644 tests/lean/tactic4.lean create mode 100644 tests/lean/tactic4.lean.expected.out diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index c1f062f78..18b718376 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -236,6 +236,15 @@ class elaborator::imp { return is_meta_app(a) && has_local_context(arg(a, 0)); } + /** \brief Return true iff \c a is a proposition */ + bool is_proposition(expr const & a, context const & ctx) { + try { + return m_type_inferer.is_proposition(a, ctx); + } catch (...) { + return false; + } + } + static expr mk_lambda(name const & n, expr const & d, expr const & b) { return ::lean::mk_lambda(n, d, b); } @@ -388,7 +397,7 @@ class elaborator::imp { 4- \c a is an application of the form (?m ...) where ?m is an assigned metavariable. */ enum status { Processed, Failed, Continue }; - status process_metavar(unification_constraint const & c, expr const & a, expr const & b, bool is_lhs, bool allow_assignment) { + status process_metavar(unification_constraint const & c, expr const & a, expr const & b, bool is_lhs) { if (is_metavar(a)) { if (is_assigned(a)) { // Case 1 @@ -401,7 +410,11 @@ class elaborator::imp { if (has_metavar(b, a)) { m_conflict = justification(new unification_failure_justification(c)); return Failed; - } else if (allow_assignment) { + } else if (is_eq(c) || is_proposition(b, get_context(c))) { + // At this point, we only assign metavariables if the constraint is an equational constraint, + // or b is a proposition. + // It is important to handle propositions since we don't want to normalize them. + // The normalization process destroys the structure of the proposition. assign(a, b, c); return Processed; } @@ -1078,11 +1091,9 @@ class elaborator::imp { } status r; - // At this point, we only assign metavariables if the constraint is an equational constraint. - bool allow_assignment = eq; - r = process_metavar(c, a, b, true, allow_assignment); + r = process_metavar(c, a, b, true); if (r != Continue) { return r == Processed; } - r = process_metavar(c, b, a, false, allow_assignment); + r = process_metavar(c, b, a, false); if (r != Continue) { return r == Processed; } if (normalize_head(a, b, c)) { return true; } diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index aa9ec15a7..1df6b1aff 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -543,100 +543,104 @@ Failed to solve Assumption 29 Failed to solve a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ if (if a b ⊤) a ⊤ - Substitution - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ ?M::5[lift:0:1] + Normalize + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ (a ⇒ b) ⇒ a Substitution - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ?M::8 ≺ ?M::5[lift:0:1] - Destruct/Decompose - a : Bool, b : Bool, H : ?M::2 ⊢ Π H_na : ?M::7, ?M::8 ≺ Π _ : ?M::4, ?M::5[lift:0:1] - (line: 27: pos: 21) Type of argument 6 must be convertible to the expected type in the application of - DisjCases::explicit - with arguments: - ?M::3 - ?M::4 - ?M::5 - EM a - λ H_a : ?M::6, H - λ H_na : ?M::7, NotImp1 (MT H H_na) - Assignment - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≈ ?M::8 + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ ?M::5[lift:0:1] + Substitution + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ?M::8 ≺ ?M::5[lift:0:1] Destruct/Decompose - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ if ?M::8 ?M::9 ⊤ - Normalize - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::8 ⇒ ?M::9 - Substitution - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::10 - Destruct/Decompose - a : Bool, - b : Bool, - H : ?M::2, - H_na : ?M::7 ⊢ - if (if a b ⊤) a ⊤ ≺ if ?M::10 ?M::11 ⊤ - Normalize - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ (a ⇒ b) ⇒ a ≺ if ?M::10 ?M::11 ⊤ - Substitution + a : Bool, b : Bool, H : ?M::2 ⊢ Π H_na : ?M::7, ?M::8 ≺ Π _ : ?M::4, ?M::5[lift:0:1] + (line: 27: pos: 21) Type of argument 6 must be convertible to the expected type in the application of + DisjCases::explicit + with arguments: + ?M::3 + ?M::4 + ?M::5 + EM a + λ H_a : ?M::6, H + λ H_na : ?M::7, NotImp1 (MT H H_na) + Assignment + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≈ ?M::8 + Destruct/Decompose + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ if ?M::8 ?M::9 ⊤ + Normalize + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::8 ⇒ ?M::9 + Substitution + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::10 + Destruct/Decompose + a : Bool, + b : Bool, + H : ?M::2, + H_na : ?M::7 ⊢ + if (if a b ⊤) a ⊤ ≺ if ?M::10 ?M::11 ⊤ + Normalize a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ - ?M::2[lift:0:2] ≺ if ?M::10 ?M::11 ⊤ - Normalize + (a ⇒ b) ⇒ a ≺ if ?M::10 ?M::11 ⊤ + Substitution a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ - ?M::2[lift:0:2] ≺ ?M::10 ⇒ ?M::11 - (line: 29: pos: 48) Type of argument 3 must be convertible to the expected type in the application of - MT::explicit - with arguments: - ?M::10 - ?M::11 - H - H_na - Normalize assignment - ?M::0 - Assignment - a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0 - Destruct/Decompose - a : Bool, - b : Bool ⊢ - Π H : ?M::2, ?M::5 ≺ Π _ : ?M::0, ?M::1[lift:0:1] - (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of - Discharge::explicit - with arguments: - ?M::0 - ?M::1 - λ H : ?M::2, - DisjCases - (EM a) - (λ H_a : ?M::6, H) - (λ H_na : ?M::7, NotImp1 (MT H H_na)) - Assignment - a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a - Destruct/Decompose - a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a + ?M::2[lift:0:2] ≺ if ?M::10 ?M::11 ⊤ + Normalize + a : Bool, + b : Bool, + H : ?M::2, + H_na : ?M::7 ⊢ + ?M::2[lift:0:2] ≺ ?M::10 ⇒ ?M::11 + (line: 29: pos: 48) Type of argument 3 must be convertible to the expected type in the application of + MT::explicit + with arguments: + ?M::10 + ?M::11 + H + H_na + Normalize assignment + ?M::0 + Assignment + a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0 Destruct/Decompose - a : Bool ⊢ - Π b : Bool, ?M::0 ⇒ ?M::1 ≺ - Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + a : Bool, + b : Bool ⊢ + Π H : ?M::2, ?M::5 ≺ Π _ : ?M::0, ?M::1[lift:0:1] + (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of + Discharge::explicit + with arguments: + ?M::0 + ?M::1 + λ H : ?M::2, + DisjCases + (EM a) + (λ H_a : ?M::6, H) + (λ H_na : ?M::7, NotImp1 (MT H H_na)) + Assignment + a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a + Destruct/Decompose + a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a Destruct/Decompose - ⊢ - Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ - Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. - Assignment - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ?M::10 ≈ ?M::8 ⇒ ?M::9 - Destruct/Decompose - a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ¬ ?M::10 ≺ ¬ (?M::8 ⇒ ?M::9) - (line: 29: pos: 40) Type of argument 3 must be convertible to the expected type in the application of - NotImp1::explicit - with arguments: - ?M::8 - ?M::9 - MT H H_na - Assignment - a : Bool, b : Bool, H : ?M::2 ⊢ if (if a b ⊤) a ⊤ ≺ ?M::5 - Normalize + a : Bool ⊢ + Π b : Bool, ?M::0 ⇒ ?M::1 ≺ + Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + Destruct/Decompose + ⊢ + Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ + Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. + Assignment + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ?M::10 ≈ ?M::8 ⇒ ?M::9 + Destruct/Decompose + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ¬ ?M::10 ≺ ¬ (?M::8 ⇒ ?M::9) + (line: 29: pos: 40) Type of argument 3 must be convertible to the expected type in the application of + NotImp1::explicit + with arguments: + ?M::8 + ?M::9 + MT H H_na + Assignment a : Bool, b : Bool, H : ?M::2 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5 Normalize a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1] diff --git a/tests/lean/tactic4.lean b/tests/lean/tactic4.lean new file mode 100644 index 000000000..d897cf33c --- /dev/null +++ b/tests/lean/tactic4.lean @@ -0,0 +1,9 @@ +(** +simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic() +**) + +Theorem T4 (a b : Bool) : a => b => a /\ b := _. + apply simple_tac + done + +Show Environment 1. \ No newline at end of file diff --git a/tests/lean/tactic4.lean.expected.out b/tests/lean/tactic4.lean.expected.out new file mode 100644 index 000000000..49bf244cc --- /dev/null +++ b/tests/lean/tactic4.lean.expected.out @@ -0,0 +1,4 @@ + Set: pp::colors + Set: pp::unicode + Proved: T4 +Theorem T4 (a b : Bool) : a ⇒ b ⇒ a ∧ b := Discharge (λ H : a, Discharge (λ H::1 : b, Conj H H::1)) diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index 2356f95d5..5416ebbf8 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -71,7 +71,7 @@ Theorem Example2 (a b c d : N) DisjCases::explicit (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)) + (eq::explicit N (h a b) (h c b)) H (λ H1 : eq::explicit N a b ∧ eq::explicit N b c, CongrH::explicit