The "quota" hack used before this commit was inefficient, and too hackish.
This commit uses two lists of constraints: active and delayed.
The delayed constraints are only processed when there are no active constraints.
We use a simple index to quickly find which delayed constraints have assigned metavariables.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle
ctx |- Type << ?f b
as
ctx |- Type =:= ?f b
This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit fixes a problem exposed by t13.lean.
It has a theorem of the form:
Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 := (show A by auto),
lemma2 := (show B by auto)
in (show B /\ A by auto)
When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form
[ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A
The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type).
Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions.
Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created
A : Bool, B : Bool, assumption : A /\ B |- B /\ A
That is, the lemmas are not available when solving B /\ A.
Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used.
Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
let lemma1 := Conjunct1 assumption,
lemma2 := Conjunct2 assumption
in Conj (Conjunct2 assumption) (Conjunct1 assumption)
This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal
A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A
After this commit, the proof for theorem T1 is
Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
let lemma1 := Conjunct1 assumption,
lemma2 := Conjunct2 assumption
in Conj lemma2 lemma1
as expected.
Finally, this example suggests that the encoding
Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := (by auto),
lemma2 : B := (by auto)
in (show B /\ A by auto)
is more efficient than
Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 := (show A by auto),
lemma2 := (show B by auto)
in (show B /\ A by auto)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remark: on Windows, Ctrl-D does not seem to work.
So, this commit also changes the Lean startup message.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
When using tactics for proving theorems, a common pattern is
Theorem T : <proposition> := _.
apply <tactic>.
...
done.
This commit allows the user to write the simplified form:
Theorem T : <proposition>.
apply <tactic>.
...
done.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
In expression code blocks, we do not have to write a "return".
After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write
apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
instead of
apply (** return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
For example, after this commit, we can write
simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic
instead of
simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>
