feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition.
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
066dacea31
commit
20a36e98ec
5 changed files with 117 additions and 89 deletions
|
|
@ -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 <tt>(?m ...)</tt> 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; }
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
9
tests/lean/tactic4.lean
Normal file
9
tests/lean/tactic4.lean
Normal file
|
|
@ -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.
|
||||
4
tests/lean/tactic4.lean.expected.out
Normal file
4
tests/lean/tactic4.lean.expected.out
Normal file
|
|
@ -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))
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue