feat(library/elaborator): only expand definitions that are not marked as hidden
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression
(λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)
After, this commit it produces
(λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)
The expressions above are definitionally equal, but the second is easier to work with.
Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 10:16:41 +00:00
|
|
|
(**
|
refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 20:47:36 +00:00
|
|
|
-- The elaborator does not expand definitions marked as 'opaque'.
|
feat(library/elaborator): only expand definitions that are not marked as hidden
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression
(λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)
After, this commit it produces
(λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)
The expressions above are definitionally equal, but the second is easier to work with.
Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 10:16:41 +00:00
|
|
|
-- To be able to prove the following theorem, we have to unmark the
|
|
|
|
|
-- 'forall'
|
|
|
|
|
local env = get_environment()
|
refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 20:47:36 +00:00
|
|
|
env:set_opaque("forall", false)
|
feat(library/elaborator): only expand definitions that are not marked as hidden
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression
(λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)
After, this commit it produces
(λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)
The expressions above are definitionally equal, but the second is easier to work with.
Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 10:16:41 +00:00
|
|
|
**)
|
|
|
|
|
Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
|
|
|
|
|
Abst (fun x, EqTIntro (H x))
|
