Commit graph

286 commits

Author SHA1 Message Date
Leonardo de Moura
8f5c2b7d9f feat(library/basic_thms): add Refute theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 12:03:31 -08:00
Leonardo de Moura
8f9405c8b3 fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive
This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 09:39:02 -08:00
Leonardo de Moura
61bd27ff06 fix(library/elaborator): bug in simple_ho_match
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 21:48:55 -08:00
Leonardo de Moura
19ad39159e feat(library/basic_thms): add ForallIntro theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 17:35:31 -08:00
Leonardo de Moura
82dfb553d5 feat(library/basic_thms): add ExistsIntro theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 16:26:23 -08:00
Leonardo de Moura
993bea8206 refactor(library/elaborator): improve elaborator state data-structure
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>
2013-12-14 23:27:08 -08:00
Leonardo de Moura
bdbf85405a feat(library/elaborator): add extra occurs-check test
The idea is to catch the inconsistency in constraints such as:

    ctx |- ?m[inst:0 v] == fun x, ?m a x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 19:47:33 -08:00
Leonardo de Moura
160a8379ef feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed
The modifications started at commit 1852c86948 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:

[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a

After the changes, only very simple constraints are generated. The most complicated one is:

[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:59:35 -08:00
Leonardo de Moura
70b7e519f8 feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:54:49 -08:00
Leonardo de Moura
02ee31b786 feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:41:50 -08:00
Leonardo de Moura
4357c9196e feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm'
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>
2013-12-14 12:25:00 -08:00
Leonardo de Moura
51aee83b70 refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env
This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.

example showing that the approach for caching metavar_env is broken in the type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-13 18:59:15 -08:00
Leonardo de Moura
2e5e5e187f chore(util/rc): remove unnecessary argument from LEAN_COPY_REF and LEAN_MOVE_REF macros
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-13 15:01:24 -08:00
Leonardo de Moura
450d6a4b1e refactor(util/splay_tree): replace find with splay_find
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 17:27:30 -08:00
Leonardo de Moura
f97c260b0b refactor(kernel/environment): add ro_environment
The environment object is a "smart-pointer".
Before this commit, the use of "const &" for environment objects was broken.
For example, suppose we have a function f that should not modify the input environment.
Before this commit, its signature would be
       void f(environment const & env)
This is broken, f's implementation can easilty convert it to a read-write pointer by using
the copy constructor.
       environment rw_env(env);
Now, f can use rw_env to update env.

To fix this issue, we now have ro_environment. It is a shared *const* pointer.
We can convert an environment into a ro_environment, but not the other way around.

ro_environment can also be seen as a form of documentation.
For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:34 -08:00
Leonardo de Moura
3457fe5935 chore(kernel): rename read_only_environment and read_write_environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:33 -08:00
Leonardo de Moura
f728f80960 fix(library/elaborator): remove is_neutral_abstraction hack, and bug at process_metavar_lift_abstraction
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 19:41:24 -08:00
Leonardo de Moura
8f67348c05 fix(library/elaborator): remove nasty hack, this hack was throwing away the local context at process_meta_app_core
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 19:27:21 -08:00
Leonardo de Moura
c29b155fdd feat(library/elaborator): use improved has_free_vars in the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 16:15:20 -08:00
Leonardo de Moura
1d33d3b5db fix(library/elaborator): the context of auxiliary metavariables created in the imitation step was incorrect
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 12:35:32 -08:00
Leonardo de Moura
55389cf6e5 feat(kernel/context): add find, a version of lookup that does not throw an exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 09:54:54 -08:00
Leonardo de Moura
f8e87436a7 perf(library/elaborator): avoid exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 19:40:59 -08:00
Leonardo de Moura
4de5f06a97 fix(library/elaborator): bug in process_metavar_inst, and disable simplification that is negatively impacting the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 19:26:58 -08:00
Leonardo de Moura
5ae71e75bd perf(library/elaborator): avoid exception
Lean was spending 17% on the runtime "throwing exceptions" in the test tests/lean/implicit7.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 16:31:36 -08:00
Leonardo de Moura
1fb526a3d4 perf(library/type_inferer): improve is_proposition performance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 16:18:45 -08:00
Leonardo de Moura
b270fb0030 refactor(library/elaborator): remove synthesizer
Synthesizer is not part of the elaborator anymore.
The elaborator fills the "easy" holes.
The remaining holes are filled using different techniques (e.g., tactic framework) that are independent of the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 15:55:54 -08:00
Leonardo de Moura
c0b9c7ffc4 refactor(library/io_state): simplify regular/diagnostic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 13:09:35 -08:00
Leonardo de Moura
8f2fe273ea refactor(*): isolate std::thread dependency
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-09 15:20:26 -08:00
Leonardo de Moura
445d4f6793 refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 18:11:35 -08:00
Leonardo de Moura
2a80807fef refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 17:33:18 -08:00
Leonardo de Moura
340d643d89 fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 16:55:55 -08:00
Leonardo de Moura
8add5571f1 refactor(library/tactic): remove 'null' tactic, and operator bool tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 15:00:16 -08:00
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 14:37:38 -08:00
Leonardo de Moura
2f88d6710c feat(kernel/expr): add some_expr and none_expr for building values of type optional<expr>
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 10:34:38 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 23:21:10 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system
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>
2013-12-07 15:11:55 -08:00
Leonardo de Moura
195ea24d71 refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer
The idea is to make it an optional parameter independent of metavar_env.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 10:27:11 -08:00
Leonardo de Moura
5f3b9dbbbd fix(library/fo_unify): unify (?f ?x) with (g a b)
We flat applications. So, (g a b) is actually ((g a) b).
So, we must be able to unify (?f ?x) with (g a b).
Solution:
        ?g <- (g a)
        ?x <- b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 10:25:11 -08:00
Leonardo de Moura
015bff8283 fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term
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>
2013-12-06 16:14:25 -08:00
Leonardo de Moura
bd9df3b08f fix(library/tactic/goal): null hypothesis being added by to_goal
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 16:03:06 -08:00
Leonardo de Moura
0390f3c39b feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 15:01:54 -08:00
Leonardo de Moura
1df9d18891 feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 14:49:39 -08:00
Leonardo de Moura
d79a626523 fix(kernel/type_checker): Pi with metavariables case
The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 13:07:59 -08:00
Leonardo de Moura
fa03ae2a26 fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints
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>
2013-12-06 13:04:34 -08:00
Leonardo de Moura
c841763a05 feat(library/elaborator): add special treatment for constraints of the form ?m[inst:i v] << t, where t is a proposition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 04:51:07 -08:00
Leonardo de Moura
13f9454fe1 feat(library/tactic/proof_state): add option tactic::proof_state::goal_names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 21:18:22 -08:00
Leonardo de Moura
0c059a9917 feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 20:06:32 -08:00
Leonardo de Moura
c1afefb873 feat(library/fo_unify): unify heterogeneous - homogeneous equality
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 19:00:31 -08:00
Leonardo de Moura
a1b5a8e50f fix(frontends/lean): check wheter the synthesized proof term has metavars or not
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 14:22:19 -08:00
Leonardo de Moura
43ef8b9a4b refactor(library/tactic): rename boolean.* to boolean_tactics.*
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 05:03:18 -08:00