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