The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition
definition a := 1
it will match 'a' with '1' since they are definitionally equal.
Then, if we have a theorem
theorem a_eq_1 : a = 1
as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"
a --> 1 --> 1 --> 1 ...
The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.
To avoid this loop, we test if the new expression is not equal to the previous one.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
In the new test elab8.lean, the parameter B is in (Type U+1).
Before, this commit, the type checker was forcing all metavariables that must be types to be <= (Type U). This restriction was preventing the elaborator from succeeding in reasonable cases.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This example produces a stackoverflow on Valgrind.
We don't execute Valgrind on tests in the slow subdirectory.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.
For example, if we had
variable f {A : Type} : A -> Bool
Then, the definition of @f was
definition @f (A : Type) (a : A) : Bool := f A a
This definition is equivalent to
fun A a, f A a
which is not definitionally equal to
f
since definitionally equality in Lean ignores Eta conversion.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The optimization was incorrect if the term indirectly contained a metavariable.
It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable.
This commit also adds a new test that exposes the problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Before this commit, the elaborator was solving constraints of the form
ctx |- (?m x) == (f x)
as
?m <- (fun x : A, f x) where A is the domain of f.
In our kernel, the terms f and (fun x, f x) are not definitionally equal.
So, the solution above is not the only one. Another possible solution is
?m <- f
Depending of the circumstances we want ?m <- (fun x : A, f x) OR ?m <- f.
For example, when Lean is elaborating the eta-theorem in kernel.lean, the first solution should be used:
?m <- (fun x : A, f x)
When we are elaborating the axiom_of_choice theorem, we need to use the second one:
?m <- f
Of course, we can always provide the parameters explicitly and bypass the elaborator.
However, this goes against the idea that the elaborator can do mechanical steps for us.
This commit addresses this issue by creating a case-split
?m <- (fun x : A, f x)
OR
?m <- f
Another solution is to implement eta-expanded normal forms in the Kernel.
With this change, we were able to cleanup the following "hacks" in kernel.lean:
@eps_ax A (nonempty_ex_intro H) P w Hw
@axiom_of_choice A B P H
where we had to explicitly provided the implicit arguments
This commit also improves the imitation step for Pi-terms that are actually arrows.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
