8214c7add4
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>
20 lines
671 B
Text
20 lines
671 B
Text
Set: pp::colors
|
|
Set: pp::unicode
|
|
Assumed: C
|
|
Assumed: D
|
|
Assumed: R
|
|
Proved: R2
|
|
Set: lean::pp::implicit
|
|
import "kernel"
|
|
import "Nat"
|
|
variable C {A B : Type} (H : @eq Type A B) (a : A) : B
|
|
variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (∀ x : A, B x) (∀ x : A', B' x)) :
|
|
@eq Type A A'
|
|
variable R {A A' : Type}
|
|
{B : A → Type}
|
|
{B' : A' → Type}
|
|
(H : @eq Type (∀ x : A, B x) (∀ x : A', B' x))
|
|
(a : A) :
|
|
@eq Type (B a) (B' (@C A A' (@D A A' B B' H) a))
|
|
theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
|
|
@R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
|