michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/sum3.lean

96 lines
4.7 KiB
Text
Raw Normal View History

feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros
import subtype
import optional
using subtype
using optional
refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-08 00:04:44 +00:00
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
-- We are encoding the (sum A B) as a subtype of (optional A) # (optional B), where
-- (proj1 n = none) ≠ (proj2 n = none)
definition sum_pred (A B : (Type U)) := λ p : (optional A) # (optional B), (proj1 p = none) ≠ (proj2 p = none)
definition sum (A B : (Type U)) := subtype ((optional A) # (optional B)) (sum_pred A B)
namespace sum
theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none)
:= not_intro
(assume N : (some a = none) = (none = (@none B)),
refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-08 00:04:44 +00:00
have eq : some a = none,
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
from (symm N) ◂ (refl (@none B)),
show false,
from absurd eq (distinct a))
theorem inr_pred (A : (Type U)) {B : (Type U)} (b : B) : sum_pred A B (pair none (some b))
:= not_intro
(assume N : (none = (@none A)) = (some b = none),
refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-08 00:04:44 +00:00
have eq : some b = none,
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
from N ◂ (refl (@none A)),
show false,
from absurd eq (distinct b))
theorem inhabl {A : (Type U)} (H : inhabited A) (B : (Type U)) : inhabited (sum A B)
:= inhabited_elim H (take w : A,
subtype_inhabited (exists_intro (pair (some w) none) (inl_pred w B)))
theorem inhabr (A : (Type U)) {B : (Type U)} (H : inhabited B) : inhabited (sum A B)
:= inhabited_elim H (take w : B,
subtype_inhabited (exists_intro (pair none (some w)) (inr_pred A w)))
definition inl {A : (Type U)} (a : A) (B : (Type U)) : sum A B
:= abst (pair (some a) none) (inhabl (inhabited_intro a) B)
definition inr (A : (Type U)) {B : (Type U)} (b : B) : sum A B
:= abst (pair none (some b)) (inhabr A (inhabited_intro b))
theorem inl_inj {A B : (Type U)} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2
:= assume Heq : inl a1 B = inl a2 B,
have eq1 : inl a1 B = abst (pair (some a1) none) (inhabl (inhabited_intro a1) B),
from refl (inl a1 B),
have eq2 : inl a2 B = abst (pair (some a2) none) (inhabl (inhabited_intro a1) B),
from subst (refl (inl a2 B)) (proof_irrel (inhabl (inhabited_intro a2) B) (inhabl (inhabited_intro a1) B)),
have rep_eq : (pair (some a1) none) = (pair (some a2) none),
from abst_inj (inhabl (inhabited_intro a1) B) (inl_pred a1 B) (inl_pred a2 B) (trans (trans (symm eq1) Heq) eq2),
show a1 = a2,
from optional::injectivity
(calc some a1 = proj1 (pair (some a1) (@none B)) : refl (some a1)
refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-08 00:04:44 +00:00
... = proj1 (pair (some a2) (@none B)) : proj1_congr rep_eq
... = some a2 : refl (some a2))
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-08 00:04:44 +00:00
:= assume Heq : inr A b1 = inr A b2,
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
have eq1 : inr A b1 = abst (pair none (some b1)) (inhabr A (inhabited_intro b1)),
from refl (inr A b1),
have eq2 : inr A b2 = abst (pair none (some b2)) (inhabr A (inhabited_intro b1)),
from subst (refl (inr A b2)) (proof_irrel (inhabr A (inhabited_intro b2)) (inhabr A (inhabited_intro b1))),
have rep_eq : (pair none (some b1)) = (pair none (some b2)),
from abst_inj (inhabr A (inhabited_intro b1)) (inr_pred A b1) (inr_pred A b2) (trans (trans (symm eq1) Heq) eq2),
show b1 = b2,
from optional::injectivity
(calc some b1 = proj2 (pair (@none A) (some b1)) : refl (some b1)
refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-08 00:04:44 +00:00
... = proj2 (pair (@none A) (some b2)) : @proj2_congr _ _ (pair (@none A) (some b1)) (pair (@none A) (some b2)) rep_eq
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
... = some b2 : refl (some b2))
theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker We should not rely on this feature. It can be quite expensive. We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as is_convertible(num, Nat) If is_convertible starts unfolding opaque definitions, we would keep expanding num. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 19:30:49 +00:00
:= not_intro (assume N : inl a B = inr A b,
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
have eq1 : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B),
from refl (inl a B),
have eq2 : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B),
from subst (refl (inr A b)) (proof_irrel (inhabr A (inhabited_intro b)) (inhabl (inhabited_intro a) B)),
have rep_eq : (pair (some a) none) = (pair none (some b)),
from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
show false,
feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker We should not rely on this feature. It can be quite expensive. We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as is_convertible(num, Nat) If is_convertible starts unfolding opaque definitions, we would keep expanding num. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 19:30:49 +00:00
from absurd (proj1_congr rep_eq) (optional::distinct a))
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 05:07:26 +00:00
set_opaque optional false
set_opaque subtype false
set_opaque optional::some false
set_opaque optional::none false
set_opaque subtype::rep false
set_opaque subtype::abst false
set_opaque optional_pred false
theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
:= let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n
in _
Reference in a new issue Copy permalink