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>
Now, we are again using the following invariant for simplifier_fn::result
The type of in the equality of the result is definitionally equal to the
type of the resultant expression.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
For example, in the hpiext axiom, the resultant equality if for (Type M+1)
axiom hpiext {A A' : TypeM} {B : A -> TypeM} {B' : A' -> TypeM} :
A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x)
even if the actual arguments A, A’, B, B’ "live" in a much smaller universe (e.g., Type).
So, it would be great if we could move the resultant equality back to the right universe.
I don't see how to do it right now.
The other solution would require a major rewrite of the code base.
We would have to support universe level arguments like Agda, and write the axiom hpiext as:
axiom hpiext {l : level} {A A' : (Type l)} {B : A -> (Type l)} {B' : A' -> (Type l)} :
A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x)
This is the first instance I found where it is really handy to have this feature.
I think this would be a super clean solution, but it would require a big rewrite in the code base.
Another problem is that the actual semantics that Agda has for this kind of construction is not clear to me.
For instance, sometimes Agda reports that the type of an expression is (Set omega).
An easier to implement hack is to support "axiom templates".
We create instances of hipext "on-demand" for different universe levels.
This is essentially what Coq does, since the universe levels are implicit in Coq.
This is not as clean as the Agda approach, but it is much easier to implement.
A super dirty trick is to include some instances of hpiext for commonly used universes
(e.g., Type and (Type 1)).
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>
It is not incorrect to use size, but it can easily overflow due to sharing.
The following script demonstrates the problem:
local f = Const("f")
local a = Const("a")
function mk_shared(d)
if d == 0 then
return a
else
local c = mk_shared(d-1)
return f(c, c)
end
end
print(mk_shared(33):size())
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
