fix(library/elaborator): bug in process_lower
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
66f106da8c
commit
fddcdb8f40
4 changed files with 26 additions and 116 deletions
|
|
@ -145,6 +145,8 @@ class elaborator::imp {
|
|||
unsigned m_next_id;
|
||||
justification m_conflict;
|
||||
bool m_first;
|
||||
level m_U; // universe U used for builtin kernel axioms
|
||||
level m_M; // universe M
|
||||
|
||||
// options
|
||||
bool m_use_justifications;
|
||||
|
|
@ -1031,9 +1033,17 @@ class elaborator::imp {
|
|||
expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
|
||||
push_active(mk_choice_constraint(get_context(c), b, 5, choices, new_jst));
|
||||
return true;
|
||||
} else if (m_env->is_ge(ty_level(a), m_U)) {
|
||||
expr choices[2] = { a, Type(ty_level(a) + 1) };
|
||||
push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst));
|
||||
return true;
|
||||
} else if (m_env->is_ge(ty_level(a), m_M)) {
|
||||
expr choices[3] = { a, Type(ty_level(a) + 1), TypeU };
|
||||
push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
|
||||
return true;
|
||||
} else {
|
||||
expr choices[5] = { a, Type(ty_level(a) + 1), Type(ty_level(a) + 2), TypeM, TypeU };
|
||||
push_active(mk_choice_constraint(get_context(c), b, 5, choices, new_jst));
|
||||
expr choices[4] = { a, Type(ty_level(a) + 1), TypeM, TypeU };
|
||||
push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
|
||||
return true;
|
||||
}
|
||||
} else {
|
||||
|
|
@ -1534,6 +1544,8 @@ public:
|
|||
set_options(opts);
|
||||
m_next_id = 0;
|
||||
m_first = true;
|
||||
m_U = m_env->get_uvar("U");
|
||||
m_M = m_env->get_uvar("M");
|
||||
// display(std::cout);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -207,8 +207,7 @@ Failed to solve
|
|||
Bool
|
||||
Bool
|
||||
Failed to solve
|
||||
⊢
|
||||
(?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
|
||||
⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
|
||||
Destruct/Decompose
|
||||
⊢ Type ≺ ?M::0
|
||||
(line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
|
||||
|
|
@ -239,17 +238,6 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ?M::1 ≈ Type
|
||||
Assumption 0
|
||||
Failed to solve
|
||||
⊢ (Type 3) ≺ Type
|
||||
Substitution
|
||||
⊢ (Type 3) ≺ ?M::1
|
||||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ (Type 2)
|
||||
Assumption 3
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Type
|
||||
Assumption 0
|
||||
Failed to solve
|
||||
⊢ (Type M+1) ≺ Type
|
||||
Substitution
|
||||
|
|
@ -257,7 +245,7 @@ Failed to solve
|
|||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ (Type M)
|
||||
Assumption 4
|
||||
Assumption 3
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Type
|
||||
Assumption 0
|
||||
|
|
@ -268,13 +256,12 @@ Failed to solve
|
|||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ (Type U)
|
||||
Assumption 5
|
||||
Assumption 4
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Type
|
||||
Assumption 0
|
||||
Failed to solve
|
||||
⊢
|
||||
(?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
|
||||
⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
|
||||
Destruct/Decompose
|
||||
⊢ Type ≺ ?M::0
|
||||
(line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
|
||||
|
|
@ -290,10 +277,10 @@ Failed to solve
|
|||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ Type
|
||||
Assumption 7
|
||||
Assumption 6
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Bool
|
||||
Assumption 6
|
||||
Assumption 5
|
||||
Failed to solve
|
||||
⊢ (Type 2) ≺ Bool
|
||||
Substitution
|
||||
|
|
@ -301,21 +288,10 @@ Failed to solve
|
|||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ (Type 1)
|
||||
Assumption 8
|
||||
Assumption 7
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Bool
|
||||
Assumption 6
|
||||
Failed to solve
|
||||
⊢ (Type 3) ≺ Bool
|
||||
Substitution
|
||||
⊢ (Type 3) ≺ ?M::1
|
||||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ (Type 2)
|
||||
Assumption 9
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Bool
|
||||
Assumption 6
|
||||
Assumption 5
|
||||
Failed to solve
|
||||
⊢ (Type M+1) ≺ Bool
|
||||
Substitution
|
||||
|
|
@ -323,10 +299,10 @@ Failed to solve
|
|||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ (Type M)
|
||||
Assumption 10
|
||||
Assumption 8
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Bool
|
||||
Assumption 6
|
||||
Assumption 5
|
||||
Failed to solve
|
||||
⊢ (Type U+1) ≺ Bool
|
||||
Substitution
|
||||
|
|
@ -334,10 +310,10 @@ Failed to solve
|
|||
Propagate type, ?M::0 : ?M::1
|
||||
Assignment
|
||||
⊢ ?M::0 ≈ (Type U)
|
||||
Assumption 11
|
||||
Assumption 9
|
||||
Assignment
|
||||
⊢ ?M::1 ≈ Bool
|
||||
Assumption 6
|
||||
Assumption 5
|
||||
Failed to solve
|
||||
a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
|
||||
Substitution
|
||||
|
|
|
|||
|
|
@ -1,50 +0,0 @@
|
|||
Variable Eq {A : (Type U+1)} (a b : A) : Bool
|
||||
Infix 50 === : Eq
|
||||
Axiom EqSubst {A : (Type U+1)} {a b : A} (P : A -> Bool) (H1 : P a) (H2 : a === b) : P b
|
||||
Axiom EqRefl {A : (Type U+1)} (a : A) : a === a
|
||||
Theorem EqSymm {A : (Type U+1)} {a b : A} (H : a === b) : b === a :=
|
||||
EqSubst (fun x, x === a) (EqRefl a) H
|
||||
Theorem EqTrans {A : (Type U+1)} {a b c : A} (H1 : a === b) (H2 : b === c) : a === c :=
|
||||
EqSubst (fun x, a === x) H1 H2
|
||||
Theorem EqCongr {A B : (Type U+1)} (f : A -> B) {a b : A} (H : a === b) : (f a) === (f b) :=
|
||||
EqSubst (fun x, (f a) === (f x)) (EqRefl (f a)) H
|
||||
Theorem EqCongr1 {A : (Type U+1)} {B : A -> (Type U+1)} {f g : Pi x : A, B x} (a : A) (H : f === g) : (f a) === (g a) :=
|
||||
EqSubst (fun h : (Pi x : A, B x), (f a) === (h a)) (EqRefl (f a)) H
|
||||
Axiom ProofIrrelevance (P : Bool) (pr1 pr2 : P) : pr1 === pr2
|
||||
Axiom EqCast {A B : (Type U)} (H : A === B) (a : A) : B
|
||||
Axiom EqCastHom {A B : (Type U)} {a1 a2 : A} (HAB : A === B) (H : a1 === a2) : (EqCast HAB a1) === (EqCast HAB a2)
|
||||
Axiom EqCastRefl {A : (Type U)} (a : A) : (EqCast (EqRefl A) a) === a
|
||||
|
||||
Variable Vector : (Type U) -> Nat -> (Type U)
|
||||
Variable empty {A : (Type U)} : Vector A 0
|
||||
Variable append {A : (Type U)} {m n : Nat} (v1 : Vector A m) (v2 : Vector A n) : Vector A (m + n)
|
||||
Axiom Plus0 (n : Nat) : (n + 0) === n
|
||||
Theorem VectorPlus0 (A : (Type U)) (n : Nat) : (Vector A (n + 0)) === (Vector A n) :=
|
||||
EqSubst (fun x : Nat, (Vector A x) === (Vector A n))
|
||||
(EqRefl (Vector A n))
|
||||
(EqSymm (Plus0 n))
|
||||
SetOption pp::implicit true
|
||||
(* Check fun (A : Type) (n : Nat), VectorPlus0 A n *)
|
||||
Axiom AppendNil {A : Type} {n : Nat} (v : Vector A n) : (EqCast (VectorPlus0 A n) (append v empty)) === v
|
||||
|
||||
Variable List : (Type U) -> (Type U).
|
||||
Variables A B : (Type U)
|
||||
Axiom H1 : A === B.
|
||||
Theorem LAB : (List A) === (List B) :=
|
||||
EqCongr List H1
|
||||
Variable l1 : List A
|
||||
Variable l2 : List B
|
||||
Variable H2 : (EqCast LAB l1) == l2
|
||||
|
||||
|
||||
(*
|
||||
Theorem EqCastInv {A B : (Type U)} (H : A === B) (a : A) : (EqCast (EqSymm H) (EqCast H a)) === a :=
|
||||
*)
|
||||
|
||||
(*
|
||||
Variable ReflCast : Pi (A : (Type U)) (a : A) (H : Eq (Type U) A A), Eq A (Casting A A H a) a
|
||||
Theorem AppEq (A : (Type U)) (B : A -> (Type U)) (a b : A) (H : Eq A a b) : (Eq (Type U) (B b) (B a)) :=
|
||||
EqCongr A (Type U) B b a (EqSymm A a b H)
|
||||
Theorem EqCongr2 (A : (Type U)) (B : A -> (Type U)) (f : Pi x : A, B x) (a b : A) (H : Eq A a b) : Eq (B a) (f a) (Casting (B b) (B a) (AppEq A B a b H) (f a)) (f b) :=
|
||||
EqSubst (B a) a b (fun x : A, Eq (B a) (f a) (Casting (B x) (B a) (AppEq A B a b H) (f a)) (f x)
|
||||
*)
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Assumed: Eq
|
||||
Assumed: EqSubst
|
||||
Assumed: EqRefl
|
||||
Proved: EqSymm
|
||||
Proved: EqTrans
|
||||
Proved: EqCongr
|
||||
Proved: EqCongr1
|
||||
Assumed: ProofIrrelevance
|
||||
Assumed: EqCast
|
||||
Assumed: EqCastHom
|
||||
Assumed: EqCastRefl
|
||||
Assumed: Vector
|
||||
Assumed: empty
|
||||
Assumed: append
|
||||
Assumed: Plus0
|
||||
Proved: VectorPlus0
|
||||
Set: lean::pp::implicit
|
||||
Assumed: AppendNil
|
||||
Assumed: List
|
||||
Assumed: A
|
||||
Assumed: B
|
||||
Assumed: H1
|
||||
Proved: LAB
|
||||
Assumed: l1
|
||||
Assumed: l2
|
||||
Assumed: H2
|
||||
Loading…
Reference in a new issue