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>
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++
The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.
Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
We need support for recursive locks. The main user of this class is
the environment object. This commit adds a test that demonstrates that
the shared_lock of the environment object may be recursively requested.
Before this fix, the Lean was deadlocking in this example.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The token }} is a bad delimiter for blocks of Lua script code nested in Lean files.
The problem is that the sequence }} occurs very often in Lua code because Lua uses { and } to build tables/lists/arrays.
Here is an example of Lua code that contains the sequence }}
t = {{1, 2}, {2, 3}, {3, 4}}
In Lean, (* ... *) is used to create comments. Thus, (** ... **) code blocks will not affect
valid Lean files. It also looks reasonably good.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The problem is that unique names depend on the order compilation units are initialized. The order of initialization is not specified by the C++ standard. Then, different compilers (or even the same compiler) may produce different initialization orders, and consequently the metavariable prefix is going to be different for different builds. This is not a bug, but it makes unit tests to fail since the output produced by different builds is different for the same input file.
Avoiding unique name feature in the default metavariable prefix avoids this problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.
- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
l = nil
will not propagate the type (List Int) to nil.
- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.
Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
