feat(frontends/lean): (Type u) can't be a proposition
(Type u) is the old (Type (u+1)) (PType u) is the old (Type u) Type* is the old (Type (_+1)) PType* is the old Type* The stdlib can be compiled, but we still have > 70 broken tests See discussion at #1341
This commit is contained in:
Leonardo de Moura
parent
0e3a8758dc
commit
bf9f7560f7
60 changed files with 438 additions and 303 deletions
|
|
@ -10,9 +10,7 @@ import init.category.monad init.data.list.basic
|
|||
universe variables u v w
|
||||
|
||||
namespace monad
|
||||
/- Remark: we use (u+1) to make sure β is not a proposition.
|
||||
That is, we are making sure that β and (list β) inhabit the same universe -/
|
||||
def mapm {m : Type (u+1) → Type v} [monad m] {α : Type w} {β : Type (u+1)} (f : α → m β) : list α → m (list β)
|
||||
def mapm {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β)
|
||||
| [] := return []
|
||||
| (h :: t) := do h' ← f h, t' ← mapm t, return (h' :: t')
|
||||
|
||||
|
|
@ -20,13 +18,13 @@ def mapm' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (f : α →
|
|||
| [] := return ()
|
||||
| (h :: t) := f h >> mapm' t
|
||||
|
||||
def for {m : Type (u+1) → Type v} [monad m] {α : Type w} {β : Type (u+1)} (l : list α) (f : α → m β) : m (list β) :=
|
||||
def for {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (l : list α) (f : α → m β) : m (list β) :=
|
||||
mapm f l
|
||||
|
||||
def for' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (l : list α) (f : α → m β) : m unit :=
|
||||
mapm' f l
|
||||
|
||||
def sequence {m : Type (u+1) → Type v} [monad m] {α : Type (u+1)} : list (m α) → m (list α)
|
||||
def sequence {m : Type u → Type v} [monad m] {α : Type u} : list (m α) → m (list α)
|
||||
| [] := return []
|
||||
| (h :: t) := do h' ← h, t' ← sequence t, return (h' :: t')
|
||||
|
||||
|
|
|
|||
|
|
@ -78,13 +78,13 @@ absurd (eq.mpr h this) this
|
|||
|
||||
universe variables u
|
||||
|
||||
lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = true) : (@ite c d α t e) = t :=
|
||||
lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : PType u} (t e : α) (h : c = true) : (@ite c d α t e) = t :=
|
||||
if_pos (of_eq_true h)
|
||||
|
||||
lemma if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = false) : (@ite c d α t e) = e :=
|
||||
lemma if_eq_of_eq_false {c : Prop} [d : decidable c] {α : PType u} (t e : α) (h : c = false) : (@ite c d α t e) = e :=
|
||||
if_neg (not_of_eq_false h)
|
||||
|
||||
lemma if_eq_of_eq (c : Prop) [d : decidable c] {α : Type u} {t e : α} (h : t = e) : (@ite c d α t e) = t :=
|
||||
lemma if_eq_of_eq (c : Prop) [d : decidable c] {α : PType u} {t e : α} (h : t = e) : (@ite c d α t e) = t :=
|
||||
match d with
|
||||
| (is_true hc) := rfl
|
||||
| (is_false hnc) := eq.symm h
|
||||
|
|
@ -110,8 +110,8 @@ eq_false_intro (λ ha, absurd ha (eq.mpr h trivial))
|
|||
lemma eq_true_of_not_eq_false {a : Prop} (h : (not a) = false) : a = true :=
|
||||
eq_true_intro (classical.by_contradiction (λ hna, eq.mp h hna))
|
||||
|
||||
lemma ne_of_eq_of_ne {α : Type u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c :=
|
||||
lemma ne_of_eq_of_ne {α : PType u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c :=
|
||||
h₁^.symm ▸ h₂
|
||||
|
||||
lemma ne_of_ne_of_eq {α : Type u} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c :=
|
||||
lemma ne_of_ne_of_eq {α : PType u} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c :=
|
||||
h₂ ▸ h₁
|
||||
|
|
|
|||
|
|
@ -175,7 +175,7 @@ local attribute [instance] prop_decidable
|
|||
noncomputable def type_decidable_eq (a : Type u) : decidable_eq a :=
|
||||
λ x y, prop_decidable (x = y)
|
||||
|
||||
noncomputable def type_decidable (a : Type u) : sum a (a → false) :=
|
||||
noncomputable def type_decidable (a : Type u) : sum a (a → empty) :=
|
||||
match (prop_decidable (nonempty a)) with
|
||||
| (is_true hp) := sum.inl (@inhabited.default _ (inhabited_of_nonempty hp))
|
||||
| (is_false hn) := sum.inr (λ a, absurd (nonempty.intro a) hn)
|
||||
|
|
|
|||
|
|
@ -27,50 +27,50 @@ prelude
|
|||
import init.data.list.basic init.data.subtype.basic init.data.prod
|
||||
universe variables u v
|
||||
|
||||
class has_lift (a : Type u) (b : Type v) :=
|
||||
class has_lift (a : PType u) (b : PType v) :=
|
||||
(lift : a → b)
|
||||
|
||||
/- auxiliary class that contains the transitive closure of has_lift. -/
|
||||
class has_lift_t (a : Type u) (b : Type v) :=
|
||||
class has_lift_t (a : PType u) (b : PType v) :=
|
||||
(lift : a → b)
|
||||
|
||||
class has_coe (a : Type u) (b : Type v) :=
|
||||
class has_coe (a : PType u) (b : PType v) :=
|
||||
(coe : a → b)
|
||||
|
||||
/- auxiliary class that contains the transitive closure of has_coe. -/
|
||||
class has_coe_t (a : Type u) (b : Type v) :=
|
||||
class has_coe_t (a : PType u) (b : PType v) :=
|
||||
(coe : a → b)
|
||||
|
||||
class has_coe_to_fun (a : Type u) : Type (max u (v+1)) :=
|
||||
(F : a → Type v) (coe : Π x, F x)
|
||||
class has_coe_to_fun (a : PType u) : PType (max u (v+1)) :=
|
||||
(F : a → PType v) (coe : Π x, F x)
|
||||
|
||||
class has_coe_to_sort (a : Type u) : Type (max u (v+1)) :=
|
||||
(S : Type v) (coe : a → S)
|
||||
class has_coe_to_sort (a : PType u) : Type (max u (v+1)) :=
|
||||
(S : PType v) (coe : a → S)
|
||||
|
||||
def lift {a : Type u} {b : Type v} [has_lift a b] : a → b :=
|
||||
def lift {a : PType u} {b : PType v} [has_lift a b] : a → b :=
|
||||
@has_lift.lift a b _
|
||||
|
||||
def lift_t {a : Type u} {b : Type v} [has_lift_t a b] : a → b :=
|
||||
def lift_t {a : PType u} {b : PType v} [has_lift_t a b] : a → b :=
|
||||
@has_lift_t.lift a b _
|
||||
|
||||
def coe_b {a : Type u} {b : Type v} [has_coe a b] : a → b :=
|
||||
def coe_b {a : PType u} {b : PType v} [has_coe a b] : a → b :=
|
||||
@has_coe.coe a b _
|
||||
|
||||
def coe_t {a : Type u} {b : Type v} [has_coe_t a b] : a → b :=
|
||||
def coe_t {a : PType u} {b : PType v} [has_coe_t a b] : a → b :=
|
||||
@has_coe_t.coe a b _
|
||||
|
||||
def coe_fn_b {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
|
||||
def coe_fn_b {a : PType u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
|
||||
has_coe_to_fun.coe
|
||||
|
||||
/- User level coercion operators -/
|
||||
|
||||
@[reducible] def coe {a : Type u} {b : Type v} [has_lift_t a b] : a → b :=
|
||||
@[reducible] def coe {a : PType u} {b : PType v} [has_lift_t a b] : a → b :=
|
||||
lift_t
|
||||
|
||||
@[reducible] def coe_fn {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
|
||||
@[reducible] def coe_fn {a : PType u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
|
||||
has_coe_to_fun.coe
|
||||
|
||||
@[reducible] def coe_sort {a : Type u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
|
||||
@[reducible] def coe_sort {a : PType u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
|
||||
has_coe_to_sort.coe
|
||||
|
||||
/- Notation -/
|
||||
|
|
@ -85,29 +85,29 @@ universe variables u₁ u₂ u₃
|
|||
|
||||
/- Transitive closure for has_lift, has_coe, has_coe_to_fun -/
|
||||
|
||||
instance lift_trans {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_lift a b] [has_lift_t b c] : has_lift_t a c :=
|
||||
instance lift_trans {a : PType u₁} {b : PType u₂} {c : PType u₃} [has_lift a b] [has_lift_t b c] : has_lift_t a c :=
|
||||
⟨λ x, lift_t (lift x : b)⟩
|
||||
|
||||
instance lift_base {a : Type u} {b : Type v} [has_lift a b] : has_lift_t a b :=
|
||||
instance lift_base {a : PType u} {b : PType v} [has_lift a b] : has_lift_t a b :=
|
||||
⟨lift⟩
|
||||
|
||||
instance coe_trans {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c :=
|
||||
instance coe_trans {a : PType u₁} {b : PType u₂} {c : PType u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c :=
|
||||
⟨λ x, coe_t (coe_b x : b)⟩
|
||||
|
||||
instance coe_base {a : Type u} {b : Type v} [has_coe a b] : has_coe_t a b :=
|
||||
instance coe_base {a : PType u} {b : PType v} [has_coe a b] : has_coe_t a b :=
|
||||
⟨coe_b⟩
|
||||
|
||||
instance coe_fn_trans {a : Type u₁} {b : Type u₂} [has_lift_t a b] [has_coe_to_fun.{u₂ u₃} b] : has_coe_to_fun.{u₁ u₃} a :=
|
||||
instance coe_fn_trans {a : PType u₁} {b : PType u₂} [has_lift_t a b] [has_coe_to_fun.{u₂ u₃} b] : has_coe_to_fun.{u₁ u₃} a :=
|
||||
{ F := λ x, @has_coe_to_fun.F.{u₂ u₃} b _ (coe x),
|
||||
coe := λ x, coe_fn (coe x) }
|
||||
|
||||
instance coe_sort_trans {a : Type u₁} {b : Type u₂} [has_lift_t a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a :=
|
||||
instance coe_sort_trans {a : PType u₁} {b : PType u₂} [has_lift_t a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a :=
|
||||
{ S := has_coe_to_sort.S.{u₂ u₃} b,
|
||||
coe := λ x, coe_sort (coe x) }
|
||||
|
||||
/- Every coercion is also a lift -/
|
||||
|
||||
instance coe_to_lift {a : Type u} {b : Type v} [has_coe_t a b] : has_lift_t a b :=
|
||||
instance coe_to_lift {a : PType u} {b : PType v} [has_coe_t a b] : has_lift_t a b :=
|
||||
⟨coe_t⟩
|
||||
|
||||
/- basic coercions -/
|
||||
|
|
@ -127,13 +127,13 @@ universe variables ua ua₁ ua₂ ub ub₁ ub₂
|
|||
|
||||
/- Remark: we cant use [has_lift_t a₂ a₁] since it will produce non-termination whenever a type class resolution
|
||||
problem does not have a solution. -/
|
||||
instance lift_fn {a₁ : Type ua₁} {a₂ : Type ua₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift a₂ a₁] [has_lift_t b₁ b₂] : has_lift (a₁ → b₁) (a₂ → b₂) :=
|
||||
instance lift_fn {a₁ : PType ua₁} {a₂ : PType ua₂} {b₁ : PType ub₁} {b₂ : PType ub₂} [has_lift a₂ a₁] [has_lift_t b₁ b₂] : has_lift (a₁ → b₁) (a₂ → b₂) :=
|
||||
⟨λ f x, ↑(f ↑x)⟩
|
||||
|
||||
instance lift_fn_range {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t b₁ b₂] : has_lift (a → b₁) (a → b₂) :=
|
||||
instance lift_fn_range {a : PType ua} {b₁ : PType ub₁} {b₂ : PType ub₂} [has_lift_t b₁ b₂] : has_lift (a → b₁) (a → b₂) :=
|
||||
⟨λ f x, ↑(f x)⟩
|
||||
|
||||
instance lift_fn_dom {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [has_lift a₂ a₁] : has_lift (a₁ → b) (a₂ → b) :=
|
||||
instance lift_fn_dom {a₁ : PType ua₁} {a₂ : PType ua₂} {b : PType ub} [has_lift a₂ a₁] : has_lift (a₁ → b) (a₂ → b) :=
|
||||
⟨λ f x, f ↑x⟩
|
||||
|
||||
instance lift_pair {a₁ : Type ua₁} {a₂ : Type ub₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t a₁ a₂] [has_lift_t b₁ b₂] : has_lift (a₁ × b₁) (a₂ × b₂) :=
|
||||
|
|
|
|||
|
|
@ -7,9 +7,9 @@ notation, basic datatypes and type classes
|
|||
-/
|
||||
prelude
|
||||
|
||||
notation `Prop` := Type 0
|
||||
notation `Type₂` := Type 2
|
||||
notation `Type₃` := Type 3
|
||||
notation `Prop` := PType 0
|
||||
notation `Type₂` := PType 2
|
||||
notation `Type₃` := PType 3
|
||||
|
||||
/- Logical operations and relations -/
|
||||
|
||||
|
|
@ -82,10 +82,10 @@ reserve infixl `; `:1
|
|||
universe variables u v
|
||||
|
||||
/- gadget for optional parameter support -/
|
||||
@[reducible] def opt_param (α : Type u) (default : α) : Type u :=
|
||||
@[reducible] def opt_param (α : PType u) (default : α) : PType u :=
|
||||
α
|
||||
|
||||
inductive poly_unit : Type u
|
||||
inductive poly_unit : PType u
|
||||
| star : poly_unit
|
||||
|
||||
inductive unit : Type
|
||||
|
|
@ -101,17 +101,22 @@ inductive empty : Type
|
|||
def not (a : Prop) := a → false
|
||||
prefix `¬` := not
|
||||
|
||||
inductive eq {α : Type u} (a : α) : α → Prop
|
||||
inductive eq {α : PType u} (a : α) : α → Prop
|
||||
| refl : eq a
|
||||
|
||||
init_quotient
|
||||
|
||||
inductive heq {α : Type u} (a : α) : Π {β : Type u}, β → Prop
|
||||
inductive heq {α : PType u} (a : α) : Π {β : PType u}, β → Prop
|
||||
| refl : heq a
|
||||
|
||||
structure prod (α : Type u) (β : Type v) :=
|
||||
(fst : α) (snd : β)
|
||||
|
||||
/- Similar to prod, but α and β can be propositions.
|
||||
We use this type internally to automatically generate the brec_on recursor. -/
|
||||
structure pprod (α : PType u) (β : PType v) :=
|
||||
(fst : α) (snd : β)
|
||||
|
||||
inductive and (a b : Prop) : Prop
|
||||
| intro : a → b → and
|
||||
|
||||
|
|
@ -129,6 +134,10 @@ inductive sum (α : Type u) (β : Type v)
|
|||
| inl {} : α → sum
|
||||
| inr {} : β → sum
|
||||
|
||||
inductive psum (α : PType u) (β : PType v)
|
||||
| inl {} : α → psum
|
||||
| inr {} : β → psum
|
||||
|
||||
inductive or (a b : Prop) : Prop
|
||||
| inl {} : a → or
|
||||
| inr {} : b → or
|
||||
|
|
@ -139,7 +148,10 @@ or.inl ha
|
|||
def or.intro_right (a : Prop) {b : Prop} (hb : b) : or a b :=
|
||||
or.inr hb
|
||||
|
||||
structure sigma {α : Type u} (β : α → Type v) :=
|
||||
structure sigma {α : Type u} (β : α → PType v) :=
|
||||
mk :: (fst : α) (snd : β fst)
|
||||
|
||||
structure psigma {α : PType u} (β : α → PType v) :=
|
||||
mk :: (fst : α) (snd : β fst)
|
||||
|
||||
inductive pos_num : Type
|
||||
|
|
@ -174,15 +186,15 @@ class inductive decidable (p : Prop)
|
|||
| is_true : p → decidable
|
||||
|
||||
@[reducible]
|
||||
def decidable_pred {α : Type u} (r : α → Prop) :=
|
||||
def decidable_pred {α : PType u} (r : α → Prop) :=
|
||||
Π (a : α), decidable (r a)
|
||||
|
||||
@[reducible]
|
||||
def decidable_rel {α : Type u} (r : α → α → Prop) :=
|
||||
def decidable_rel {α : PType u} (r : α → α → Prop) :=
|
||||
Π (a b : α), decidable (r a b)
|
||||
|
||||
@[reducible]
|
||||
def decidable_eq (α : Type u) :=
|
||||
def decidable_eq (α : PType u) :=
|
||||
decidable_rel (@eq α)
|
||||
|
||||
inductive option (α : Type u)
|
||||
|
|
@ -428,26 +440,26 @@ notation `(` h `, ` t:(foldr `, ` (e r, prod.mk e r)) `)` := prod.mk h t
|
|||
|
||||
attribute [refl] eq.refl
|
||||
|
||||
@[pattern] def rfl {α : Type u} {a : α} : a = a := eq.refl a
|
||||
@[pattern] def rfl {α : PType u} {a : α} : a = a := eq.refl a
|
||||
|
||||
@[elab_as_eliminator, subst]
|
||||
lemma eq.subst {α : Type u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
|
||||
lemma eq.subst {α : PType u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
|
||||
eq.rec h₂ h₁
|
||||
|
||||
notation h1 ▸ h2 := eq.subst h1 h2
|
||||
|
||||
@[trans] lemma eq.trans {α : Type u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
|
||||
@[trans] lemma eq.trans {α : PType u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
|
||||
h₂ ▸ h₁
|
||||
|
||||
@[symm] lemma eq.symm {α : Type u} {a b : α} (h : a = b) : b = a :=
|
||||
@[symm] lemma eq.symm {α : PType u} {a b : α} (h : a = b) : b = a :=
|
||||
h ▸ rfl
|
||||
|
||||
/- sizeof -/
|
||||
|
||||
class has_sizeof (α : Type u) :=
|
||||
class has_sizeof (α : PType u) :=
|
||||
(sizeof : α → nat)
|
||||
|
||||
def sizeof {α : Type u} [s : has_sizeof α] : α → nat :=
|
||||
def sizeof {α : PType u} [s : has_sizeof α] : α → nat :=
|
||||
has_sizeof.sizeof
|
||||
|
||||
/-
|
||||
|
|
@ -456,13 +468,13 @@ From now on, the inductive compiler will automatically generate sizeof instances
|
|||
-/
|
||||
|
||||
/- Every type `α` has a default has_sizeof instance that just returns 0 for every element of `α` -/
|
||||
instance default_has_sizeof (α : Type u) : has_sizeof α :=
|
||||
instance default_has_sizeof (α : PType u) : has_sizeof α :=
|
||||
⟨λ a, nat.zero⟩
|
||||
|
||||
/- TODO(Leo): the [simp.sizeof] annotations are not really necessary.
|
||||
What we need is a robust way of unfolding sizeof definitions. -/
|
||||
attribute [simp.sizeof]
|
||||
lemma default_has_sizeof_eq (α : Type u) (a : α) : @sizeof α (default_has_sizeof α) a = 0 :=
|
||||
lemma default_has_sizeof_eq (α : PType u) (a : α) : @sizeof α (default_has_sizeof α) a = 0 :=
|
||||
rfl
|
||||
|
||||
instance : has_sizeof nat :=
|
||||
|
|
|
|||
|
|
@ -259,10 +259,10 @@ protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
|
|||
end
|
||||
end
|
||||
|
||||
protected def {u} lt_ge_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C :=
|
||||
protected def {u} lt_ge_by_cases {a b : ℕ} {C : PType u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C :=
|
||||
decidable.by_cases h₁ (λ h, h₂ (or.elim (nat.lt_or_ge a b) (λ a, absurd a h) (λ a, a)))
|
||||
|
||||
protected def {u} lt_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a = b → C)
|
||||
protected def {u} lt_by_cases {a b : ℕ} {C : PType u} (h₁ : a < b → C) (h₂ : a = b → C)
|
||||
(h₃ : b < a → C) : C :=
|
||||
nat.lt_ge_by_cases h₁ (λ h₁,
|
||||
nat.lt_ge_by_cases h₃ (λ h, h₂ (nat.le_antisymm h h₁)))
|
||||
|
|
|
|||
|
|
@ -57,10 +57,10 @@ def option_orelse {α : Type u} : option α → option α → option α
|
|||
instance {α : Type u} : alternative option :=
|
||||
alternative.mk @option_fmap @some (@fapp _ _) @none @option_orelse
|
||||
|
||||
def option_t (m : Type (max 1 u) → Type v) [monad m] (α : Type u) : Type v :=
|
||||
def option_t (m : Type u → Type v) [monad m] (α : Type u) : Type v :=
|
||||
m (option α)
|
||||
|
||||
@[inline] def option_t_fmap {m : Type (max 1 u) → Type v} [monad m] {α β : Type u} (f : α → β) (e : option_t m α) : option_t m β :=
|
||||
@[inline] def option_t_fmap {m : Type u → Type v} [monad m] {α β : Type u} (f : α → β) (e : option_t m α) : option_t m β :=
|
||||
show m (option β), from
|
||||
do o ← e,
|
||||
match o with
|
||||
|
|
@ -68,7 +68,7 @@ do o ← e,
|
|||
| (some a) := return (some (f a))
|
||||
end
|
||||
|
||||
@[inline] def option_t_bind {m : Type (max 1 u) → Type v} [monad m] {α β : Type u} (a : option_t m α) (b : α → option_t m β)
|
||||
@[inline] def option_t_bind {m : Type u → Type v} [monad m] {α β : Type u} (a : option_t m α) (b : α → option_t m β)
|
||||
: option_t m β :=
|
||||
show m (option β), from
|
||||
do o ← a,
|
||||
|
|
@ -77,14 +77,14 @@ do o ← a,
|
|||
| (some a) := b a
|
||||
end
|
||||
|
||||
@[inline] def option_t_return {m : Type (max 1 u) → Type v} [monad m] {α : Type u} (a : α) : option_t m α :=
|
||||
@[inline] def option_t_return {m : Type u → Type v} [monad m] {α : Type u} (a : α) : option_t m α :=
|
||||
show m (option α), from
|
||||
return (some a)
|
||||
|
||||
instance {m : Type (max 1 u) → Type v} [monad m] : monad (option_t m) :=
|
||||
instance {m : Type u → Type v} [monad m] : monad (option_t m) :=
|
||||
{map := @option_t_fmap m _, ret := @option_t_return m _, bind := @option_t_bind m _}
|
||||
|
||||
def option_t_orelse {m : Type (max 1 u) → Type v} [monad m] {α : Type u} (a : option_t m α) (b : option_t m α) : option_t m α :=
|
||||
def option_t_orelse {m : Type u → Type v} [monad m] {α : Type u} (a : option_t m α) (b : option_t m α) : option_t m α :=
|
||||
show m (option α), from
|
||||
do o ← a,
|
||||
match o with
|
||||
|
|
@ -92,11 +92,11 @@ do o ← a,
|
|||
| (some v) := return (some v)
|
||||
end
|
||||
|
||||
def option_t_fail {m : Type (max 1 u) → Type v} [monad m] {α : Type u} : option_t m α :=
|
||||
def option_t_fail {m : Type u → Type v} [monad m] {α : Type u} : option_t m α :=
|
||||
show m (option α), from
|
||||
return none
|
||||
|
||||
instance {m : Type (max 1 u) → Type v} [monad m] : alternative (option_t m) :=
|
||||
instance {m : Type u → Type v} [monad m] : alternative (option_t m) :=
|
||||
{map := @option_t_fmap m _,
|
||||
pure := @option_t_return m _,
|
||||
seq := @fapp (option_t m) (@option_t.monad m _),
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ variables {α : Type u} {β : α → Type v}
|
|||
private def fun_setoid (α : Type u) (β : α → Type v) : setoid (Π x : α, β x) :=
|
||||
setoid.mk (@function.equiv α β) (function.equiv.is_equivalence α β)
|
||||
|
||||
private def extfun (α : Type u) (β : α → Type v) : Type (imax u v) :=
|
||||
private def extfun (α : Type u) (β : α → Type v) : Type (max u v) :=
|
||||
quotient (fun_setoid α β)
|
||||
|
||||
private def fun_to_extfun (f : Π x : α, β x) : extfun α β :=
|
||||
|
|
|
|||
|
|
@ -8,9 +8,9 @@ import init.core
|
|||
|
||||
universe variables u v w
|
||||
|
||||
@[reducible] def id {α : Type u} (a : α) : α := a
|
||||
@[reducible] def id {α : PType u} (a : α) : α := a
|
||||
|
||||
def flip {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ) : β → α → φ :=
|
||||
def flip {α : PType u} {β : PType v} {φ : PType w} (f : α → β → φ) : β → α → φ :=
|
||||
λ b a, f a b
|
||||
|
||||
/- implication -/
|
||||
|
|
@ -22,7 +22,7 @@ assume hp, h₂ (h₁ hp)
|
|||
|
||||
def trivial : true := ⟨⟩
|
||||
|
||||
@[inline] def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b :=
|
||||
@[inline] def absurd {a : Prop} {b : PType v} (h₁ : a) (h₂ : ¬a) : b :=
|
||||
false.rec b (h₂ h₁)
|
||||
|
||||
lemma not.intro {a : Prop} (h : a → false) : ¬ a :=
|
||||
|
|
@ -54,39 +54,39 @@ false.rec c h
|
|||
lemma proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ :=
|
||||
rfl
|
||||
|
||||
@[simp] lemma id.def {α : Type u} (a : α) : id a = a := rfl
|
||||
@[simp] lemma id.def {α : PType u} (a : α) : id a = a := rfl
|
||||
|
||||
-- Remark: we provide the universe levels explicitly to make sure `eq.drec` has the same type of `eq.rec` in the hoTT library
|
||||
attribute [elab_as_eliminator]
|
||||
protected lemma {u₁ u₂} eq.drec {α : Type u₂} {a : α} {φ : Π (x : α), a = x → Type u₁} (h₁ : φ a (eq.refl a)) {b : α} (h₂ : a = b) : φ b h₂ :=
|
||||
protected lemma {u₁ u₂} eq.drec {α : PType u₂} {a : α} {φ : Π (x : α), a = x → PType u₁} (h₁ : φ a (eq.refl a)) {b : α} (h₂ : a = b) : φ b h₂ :=
|
||||
eq.rec (λ h₂ : a = a, show φ a h₂, from h₁) h₂ h₂
|
||||
|
||||
attribute [elab_as_eliminator]
|
||||
protected lemma drec_on {α : Type u} {a : α} {φ : Π (x : α), a = x → Type v} {b : α} (h₂ : a = b) (h₁ : φ a (eq.refl a)) : φ b h₂ :=
|
||||
protected lemma drec_on {α : PType u} {a : α} {φ : Π (x : α), a = x → PType v} {b : α} (h₂ : a = b) (h₁ : φ a (eq.refl a)) : φ b h₂ :=
|
||||
eq.drec h₁ h₂
|
||||
|
||||
lemma eq.mp {α β : Type u} : (α = β) → α → β :=
|
||||
lemma eq.mp {α β : PType u} : (α = β) → α → β :=
|
||||
eq.rec_on
|
||||
|
||||
lemma eq.mpr {α β : Type u} : (α = β) → β → α :=
|
||||
lemma eq.mpr {α β : PType u} : (α = β) → β → α :=
|
||||
λ h₁ h₂, eq.rec_on (eq.symm h₁) h₂
|
||||
|
||||
lemma eq.substr {α : Type u} {p : α → Prop} {a b : α} (h₁ : b = a) : p a → p b :=
|
||||
lemma eq.substr {α : PType u} {p : α → Prop} {a b : α} (h₁ : b = a) : p a → p b :=
|
||||
eq.subst (eq.symm h₁)
|
||||
|
||||
lemma congr {α : Type u} {β : Type v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
|
||||
lemma congr {α : PType u} {β : PType v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
|
||||
eq.subst h₁ (eq.subst h₂ rfl)
|
||||
|
||||
lemma congr_fun {α : Type u} {β : α → Type v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
|
||||
lemma congr_fun {α : PType u} {β : α → PType v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
|
||||
eq.subst h (eq.refl (f a))
|
||||
|
||||
lemma congr_arg {α : Type u} {β : Type v} {a₁ a₂ : α} (f : α → β) : a₁ = a₂ → f a₁ = f a₂ :=
|
||||
lemma congr_arg {α : PType u} {β : PType v} {a₁ a₂ : α} (f : α → β) : a₁ = a₂ → f a₁ = f a₂ :=
|
||||
congr rfl
|
||||
|
||||
lemma trans_rel_left {α : Type u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
|
||||
lemma trans_rel_left {α : PType u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
|
||||
h₂ ▸ h₁
|
||||
|
||||
lemma trans_rel_right {α : Type u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
|
||||
lemma trans_rel_right {α : PType u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
|
||||
h₁^.symm ▸ h₂
|
||||
|
||||
lemma of_eq_true {p : Prop} (h : p = true) : p :=
|
||||
|
|
@ -95,25 +95,25 @@ h^.symm ▸ trivial
|
|||
lemma not_of_eq_false {p : Prop} (h : p = false) : ¬p :=
|
||||
assume hp, h ▸ hp
|
||||
|
||||
@[inline] def cast {α β : Type u} (h : α = β) (a : α) : β :=
|
||||
@[inline] def cast {α β : PType u} (h : α = β) (a : α) : β :=
|
||||
eq.rec a h
|
||||
|
||||
lemma cast_proof_irrel {α β : Type u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a :=
|
||||
lemma cast_proof_irrel {α β : PType u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a :=
|
||||
rfl
|
||||
|
||||
lemma cast_eq {α : Type u} (h : α = α) (a : α) : cast h a = a :=
|
||||
lemma cast_eq {α : PType u} (h : α = α) (a : α) : cast h a = a :=
|
||||
rfl
|
||||
|
||||
/- ne -/
|
||||
|
||||
@[reducible] def ne {α : Type u} (a b : α) := ¬(a = b)
|
||||
@[reducible] def ne {α : PType u} (a b : α) := ¬(a = b)
|
||||
notation a ≠ b := ne a b
|
||||
|
||||
@[simp] lemma ne.def {α : Type u} (a b : α) : a ≠ b = ¬ (a = b) :=
|
||||
@[simp] lemma ne.def {α : PType u} (a b : α) : a ≠ b = ¬ (a = b) :=
|
||||
rfl
|
||||
|
||||
namespace ne
|
||||
variable {α : Type u}
|
||||
variable {α : PType u}
|
||||
variables {a b : α}
|
||||
|
||||
lemma intro (h : a = b → false) : a ≠ b := h
|
||||
|
|
@ -126,7 +126,7 @@ namespace ne
|
|||
assume (h₁ : b = a), h (h₁^.symm)
|
||||
end ne
|
||||
|
||||
lemma false_of_ne {α : Type u} {a : α} : a ≠ a → false := ne.irrefl
|
||||
lemma false_of_ne {α : PType u} {a : α} : a ≠ a → false := ne.irrefl
|
||||
|
||||
section
|
||||
variables {p : Prop}
|
||||
|
|
@ -144,18 +144,18 @@ end
|
|||
attribute [refl] heq.refl
|
||||
|
||||
section
|
||||
variables {α β φ : Type u} {a a' : α} {b b' : β} {c : φ}
|
||||
variables {α β φ : PType u} {a a' : α} {b b' : β} {c : φ}
|
||||
|
||||
lemma eq_of_heq (h : a == a') : a = a' :=
|
||||
have ∀ (α' : Type u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from
|
||||
λ (α' : Type u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl),
|
||||
have ∀ (α' : PType u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from
|
||||
λ (α' : PType u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl),
|
||||
show (eq.rec_on (eq.refl α) a : α) = a', from
|
||||
this α a' h (eq.refl α)
|
||||
|
||||
lemma heq.elim {α : Type u} {a : α} {p : α → Type v} {b : α} (h₁ : a == b)
|
||||
lemma heq.elim {α : PType u} {a : α} {p : α → PType v} {b : α} (h₁ : a == b)
|
||||
: p a → p b := eq.rec_on (eq_of_heq h₁)
|
||||
|
||||
lemma heq.subst {p : ∀ T : Type u, T → Prop} : a == b → p α a → p β b :=
|
||||
lemma heq.subst {p : ∀ T : PType u, T → Prop} : a == b → p α a → p β b :=
|
||||
heq.rec_on
|
||||
|
||||
@[symm] lemma heq.symm (h : a == b) : b == a :=
|
||||
|
|
@ -177,13 +177,13 @@ def type_eq_of_heq (h : a == b) : α = β :=
|
|||
heq.rec_on h (eq.refl α)
|
||||
end
|
||||
|
||||
lemma eq_rec_heq {α : Type u} {φ : α → Type v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
|
||||
lemma eq_rec_heq {α : Type u} {φ : α → PType v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
|
||||
| a .a rfl p := heq.refl p
|
||||
|
||||
lemma heq_of_eq_rec_left {α : Type u} {φ : α → Type v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂
|
||||
lemma heq_of_eq_rec_left {α : PType u} {φ : α → PType v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂
|
||||
| a .a p₁ p₂ (eq.refl .a) h := eq.rec_on h (heq.refl p₁)
|
||||
|
||||
lemma heq_of_eq_rec_right {α : Type u} {φ : α → Type v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
|
||||
lemma heq_of_eq_rec_right {α : PType u} {φ : α → PType v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
|
||||
| a .a p₁ p₂ (eq.refl .a) h :=
|
||||
have p₁ = p₂, from h,
|
||||
this ▸ heq.refl p₁
|
||||
|
|
@ -191,19 +191,19 @@ lemma heq_of_eq_rec_right {α : Type u} {φ : α → Type v} : ∀ {a a' : α} {
|
|||
lemma of_heq_true {a : Prop} (h : a == true) : a :=
|
||||
of_eq_true (eq_of_heq h)
|
||||
|
||||
lemma eq_rec_compose : ∀ {α β φ : Type u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
|
||||
lemma eq_rec_compose : ∀ {α β φ : PType u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
|
||||
| α .α .α (eq.refl .α) (eq.refl .α) a := rfl
|
||||
|
||||
lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : Type u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂
|
||||
lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : PType u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂
|
||||
| α .α rfl a .a rfl := rfl
|
||||
|
||||
lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : Type u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂
|
||||
lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : PType u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂
|
||||
| α .α a .a (heq.refl .a) := rfl
|
||||
|
||||
lemma eq_rec_of_heq_right {α₁ α₂ : Type u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
|
||||
lemma eq_rec_of_heq_right {α₁ α₂ : PType u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
|
||||
eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
|
||||
|
||||
lemma cast_heq : ∀ {α β : Type u} (h : α = β) (a : α), cast h a == a
|
||||
lemma cast_heq : ∀ {α β : PType u} (h : α = β) (a : α), cast h a == a
|
||||
| α .α (eq.refl .α) a := heq.refl a
|
||||
|
||||
/- and -/
|
||||
|
|
@ -354,13 +354,13 @@ iff_true_intro not_false
|
|||
@[congr] lemma not_congr (h : a ↔ b) : ¬a ↔ ¬b :=
|
||||
iff.intro (λ h₁ h₂, h₁ (iff.mpr h h₂)) (λ h₁ h₂, h₁ (iff.mp h h₂))
|
||||
|
||||
@[simp] lemma ne_self_iff_false {α : Type u} (a : α) : (not (a = a)) ↔ false :=
|
||||
@[simp] lemma ne_self_iff_false {α : PType u} (a : α) : (not (a = a)) ↔ false :=
|
||||
iff.intro false_of_ne false.elim
|
||||
|
||||
@[simp] lemma eq_self_iff_true {α : Type u} (a : α) : (a = a) ↔ true :=
|
||||
@[simp] lemma eq_self_iff_true {α : PType u} (a : α) : (a = a) ↔ true :=
|
||||
iff_true_intro rfl
|
||||
|
||||
@[simp] lemma heq_self_iff_true {α : Type u} (a : α) : (a == a) ↔ true :=
|
||||
@[simp] lemma heq_self_iff_true {α : PType u} (a : α) : (a == a) ↔ true :=
|
||||
iff_true_intro (heq.refl a)
|
||||
|
||||
@[simp] lemma iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
|
||||
|
|
@ -537,7 +537,7 @@ iff.intro (λ h, trivial) (λ ha h, false.elim h)
|
|||
|
||||
/- exists -/
|
||||
|
||||
inductive Exists {α : Type u} (p : α → Prop) : Prop
|
||||
inductive Exists {α : PType u} (p : α → Prop) : Prop
|
||||
| intro : ∀ (a : α), p a → Exists
|
||||
|
||||
attribute [intro] Exists.intro
|
||||
|
|
@ -548,24 +548,24 @@ def exists.intro := @Exists.intro
|
|||
notation `exists` binders `, ` r:(scoped P, Exists P) := r
|
||||
notation `∃` binders `, ` r:(scoped P, Exists P) := r
|
||||
|
||||
lemma exists.elim {α : Type u} {p : α → Prop} {b : Prop}
|
||||
lemma exists.elim {α : PType u} {p : α → Prop} {b : Prop}
|
||||
(h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b :=
|
||||
Exists.rec h₂ h₁
|
||||
|
||||
/- exists unique -/
|
||||
|
||||
def exists_unique {α : Type u} (p : α → Prop) :=
|
||||
def exists_unique {α : PType u} (p : α → Prop) :=
|
||||
∃ x, p x ∧ ∀ y, p y → y = x
|
||||
|
||||
notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r
|
||||
|
||||
attribute [intro]
|
||||
lemma exists_unique.intro {α : Type u} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) :
|
||||
lemma exists_unique.intro {α : PType u} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) :
|
||||
∃! x, p x :=
|
||||
exists.intro w ⟨h₁, h₂⟩
|
||||
|
||||
attribute [recursor 4]
|
||||
lemma exists_unique.elim {α : Type u} {p : α → Prop} {b : Prop}
|
||||
lemma exists_unique.elim {α : PType u} {p : α → Prop} {b : Prop}
|
||||
(h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b :=
|
||||
exists.elim h₂ (λ w hw, h₁ w (and.left hw) (and.right hw))
|
||||
|
||||
|
|
@ -573,10 +573,10 @@ lemma exists_unique_of_exists_of_unique {α : Type u} {p : α → Prop}
|
|||
(hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x :=
|
||||
exists.elim hex (λ x px, exists_unique.intro x px (take y, suppose p y, hunique y x this px))
|
||||
|
||||
lemma exists_of_exists_unique {α : Type u} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x :=
|
||||
lemma exists_of_exists_unique {α : PType u} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x :=
|
||||
exists.elim h (λ x hx, ⟨x, and.left hx⟩)
|
||||
|
||||
lemma unique_of_exists_unique {α : Type u} {p : α → Prop}
|
||||
lemma unique_of_exists_unique {α : PType u} {p : α → Prop}
|
||||
(h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
|
||||
exists_unique.elim h
|
||||
(take x, suppose p x,
|
||||
|
|
@ -584,21 +584,21 @@ exists_unique.elim h
|
|||
show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂)))
|
||||
|
||||
/- exists, forall, exists unique congruences -/
|
||||
@[congr] lemma forall_congr {α : Type u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a :=
|
||||
@[congr] lemma forall_congr {α : PType u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a :=
|
||||
iff.intro (λ p a, iff.mp (h a) (p a)) (λ q a, iff.mpr (h a) (q a))
|
||||
|
||||
lemma exists_imp_exists {α : Type u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a :=
|
||||
lemma exists_imp_exists {α : PType u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a :=
|
||||
exists.elim p (λ a hp, ⟨a, h a hp⟩)
|
||||
|
||||
@[congr] lemma exists_congr {α : Type u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
|
||||
@[congr] lemma exists_congr {α : PType u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
|
||||
iff.intro
|
||||
(exists_imp_exists (λ a, iff.mp (h a)))
|
||||
(exists_imp_exists (λ a, iff.mpr (h a)))
|
||||
|
||||
@[congr] lemma exists_unique_congr {α : Type u} {p₁ p₂ : α → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := --
|
||||
@[congr] lemma exists_unique_congr {α : PType u} {p₁ p₂ : α → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := --
|
||||
exists_congr (λ x, and_congr (h x) (forall_congr (λ y, imp_congr (h y) iff.rfl)))
|
||||
|
||||
lemma forall_not_of_not_exists {α : Type u} {p : α → Prop} : ¬(∃ x, p x) → (∀ x, ¬p x) :=
|
||||
lemma forall_not_of_not_exists {α : PType u} {p : α → Prop} : ¬(∃ x, p x) → (∀ x, ¬p x) :=
|
||||
λ hne x hp, hne ⟨x, hp⟩
|
||||
|
||||
/- decidable -/
|
||||
|
|
@ -616,26 +616,26 @@ is_false not_false
|
|||
|
||||
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
|
||||
-- to the branches
|
||||
@[inline] def dite (c : Prop) [h : decidable c] {α : Type u} : (c → α) → (¬ c → α) → α :=
|
||||
@[inline] def dite (c : Prop) [h : decidable c] {α : PType u} : (c → α) → (¬ c → α) → α :=
|
||||
λ t e, decidable.rec_on h e t
|
||||
|
||||
/- if-then-else -/
|
||||
|
||||
@[inline] def ite (c : Prop) [h : decidable c] {α : Type u} (t e : α) : α :=
|
||||
@[inline] def ite (c : Prop) [h : decidable c] {α : PType u} (t e : α) : α :=
|
||||
decidable.rec_on h (λ hnc, e) (λ hc, t)
|
||||
|
||||
namespace decidable
|
||||
variables {p q : Prop}
|
||||
|
||||
def rec_on_true [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u} (h₃ : p) (h₄ : h₁ h₃)
|
||||
def rec_on_true [h : decidable p] {h₁ : p → PType u} {h₂ : ¬p → PType u} (h₃ : p) (h₄ : h₁ h₃)
|
||||
: decidable.rec_on h h₂ h₁ :=
|
||||
decidable.rec_on h (λ h, false.rec _ (h h₃)) (λ h, h₄)
|
||||
|
||||
def rec_on_false [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u} (h₃ : ¬p) (h₄ : h₂ h₃)
|
||||
def rec_on_false [h : decidable p] {h₁ : p → PType u} {h₂ : ¬p → PType u} (h₃ : ¬p) (h₄ : h₂ h₃)
|
||||
: decidable.rec_on h h₂ h₁ :=
|
||||
decidable.rec_on h (λ h, h₄) (λ h, false.rec _ (h₃ h))
|
||||
|
||||
def by_cases {q : Type u} [φ : decidable p] : (p → q) → (¬p → q) → q := dite _
|
||||
def by_cases {q : PType u} [φ : decidable p] : (p → q) → (¬p → q) → q := dite _
|
||||
|
||||
lemma em (p : Prop) [decidable p] : p ∨ ¬p := by_cases or.inl or.inr
|
||||
|
||||
|
|
@ -652,7 +652,7 @@ section
|
|||
def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q :=
|
||||
decidable_of_decidable_of_iff hp h^.to_iff
|
||||
|
||||
protected def or.by_cases [decidable p] [decidable q] {α : Type u}
|
||||
protected def or.by_cases [decidable p] [decidable q] {α : PType u}
|
||||
(h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
|
||||
if hp : p then h₁ hp else
|
||||
if hq : q then h₂ hq else
|
||||
|
|
@ -686,14 +686,14 @@ section
|
|||
decidable_of_decidable_of_iff and.decidable (iff_iff_implies_and_implies p q)^.symm
|
||||
end
|
||||
|
||||
instance {α : Type u} [decidable_eq α] (a b : α) : decidable (a ≠ b) :=
|
||||
instance {α : PType u} [decidable_eq α] (a b : α) : decidable (a ≠ b) :=
|
||||
implies.decidable
|
||||
|
||||
lemma bool.ff_ne_tt : ff = tt → false
|
||||
.
|
||||
|
||||
def is_dec_eq {α : Type u} (p : α → α → bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y
|
||||
def is_dec_refl {α : Type u} (p : α → α → bool) : Prop := ∀ x, p x x = tt
|
||||
def is_dec_eq {α : PType u} (p : α → α → bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y
|
||||
def is_dec_refl {α : PType u} (p : α → α → bool) : Prop := ∀ x, p x x = tt
|
||||
|
||||
open decidable
|
||||
instance : decidable_eq bool
|
||||
|
|
@ -702,18 +702,18 @@ instance : decidable_eq bool
|
|||
| tt ff := is_false (ne.symm bool.ff_ne_tt)
|
||||
| tt tt := is_true rfl
|
||||
|
||||
def decidable_eq_of_bool_pred {α : Type u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
|
||||
def decidable_eq_of_bool_pred {α : PType u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
|
||||
take x y : α,
|
||||
if hp : p x y = tt then is_true (h₁ hp)
|
||||
else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z, ¬p z y = tt) _ hxy hp))
|
||||
|
||||
lemma decidable_eq_inl_refl {α : Type u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) :=
|
||||
lemma decidable_eq_inl_refl {α : PType u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) :=
|
||||
match (h a a) with
|
||||
| (is_true e) := rfl
|
||||
| (is_false n) := absurd rfl n
|
||||
end
|
||||
|
||||
lemma decidable_eq_inr_neg {α : Type u} [h : decidable_eq α] {a b : α} : Π n : a ≠ b, h a b = is_false n :=
|
||||
lemma decidable_eq_inr_neg {α : PType u} [h : decidable_eq α] {a b : α} : Π n : a ≠ b, h a b = is_false n :=
|
||||
assume n,
|
||||
match (h a b) with
|
||||
| (is_true e) := absurd e n
|
||||
|
|
@ -722,22 +722,22 @@ end
|
|||
|
||||
/- inhabited -/
|
||||
|
||||
class inhabited (α : Type u) :=
|
||||
class inhabited (α : PType u) :=
|
||||
(default : α)
|
||||
|
||||
def default (α : Type u) [inhabited α] : α :=
|
||||
def default (α : PType u) [inhabited α] : α :=
|
||||
inhabited.default α
|
||||
|
||||
@[inline, irreducible] def arbitrary (α : Type u) [inhabited α] : α :=
|
||||
@[inline, irreducible] def arbitrary (α : PType u) [inhabited α] : α :=
|
||||
default α
|
||||
|
||||
instance prop.inhabited : inhabited Prop :=
|
||||
⟨true⟩
|
||||
|
||||
instance fun.inhabited (α : Type u) {β : Type v} [h : inhabited β] : inhabited (α → β) :=
|
||||
instance fun.inhabited (α : PType u) {β : PType v} [h : inhabited β] : inhabited (α → β) :=
|
||||
inhabited.rec_on h (λ b, ⟨λ a, b⟩)
|
||||
|
||||
instance pi.inhabited (α : Type u) {β : α → Type v} [Π x, inhabited (β x)] : inhabited (Π x, β x) :=
|
||||
instance pi.inhabited (α : PType u) {β : α → PType v} [Π x, inhabited (β x)] : inhabited (Π x, β x) :=
|
||||
⟨λ a, default (β a)⟩
|
||||
|
||||
instance : inhabited bool :=
|
||||
|
|
@ -749,27 +749,27 @@ instance : inhabited pos_num :=
|
|||
instance : inhabited num :=
|
||||
⟨num.zero⟩
|
||||
|
||||
class inductive nonempty (α : Type u) : Prop
|
||||
class inductive nonempty (α : PType u) : Prop
|
||||
| intro : α → nonempty
|
||||
|
||||
protected def nonempty.elim {α : Type u} {p : Prop} (h₁ : nonempty α) (h₂ : α → p) : p :=
|
||||
protected def nonempty.elim {α : PType u} {p : Prop} (h₁ : nonempty α) (h₂ : α → p) : p :=
|
||||
nonempty.rec h₂ h₁
|
||||
|
||||
instance nonempty_of_inhabited {α : Type u} [inhabited α] : nonempty α :=
|
||||
instance nonempty_of_inhabited {α : PType u} [inhabited α] : nonempty α :=
|
||||
⟨default α⟩
|
||||
|
||||
lemma nonempty_of_exists {α : Type u} {p : α → Prop} : (∃ x, p x) → nonempty α
|
||||
lemma nonempty_of_exists {α : PType u} {p : α → Prop} : (∃ x, p x) → nonempty α
|
||||
| ⟨w, h⟩ := ⟨w⟩
|
||||
|
||||
/- subsingleton -/
|
||||
|
||||
class inductive subsingleton (α : Type u) : Prop
|
||||
class inductive subsingleton (α : PType u) : Prop
|
||||
| intro : (∀ a b : α, a = b) → subsingleton
|
||||
|
||||
protected def subsingleton.elim {α : Type u} [h : subsingleton α] : ∀ (a b : α), a = b :=
|
||||
protected def subsingleton.elim {α : PType u} [h : subsingleton α] : ∀ (a b : α), a = b :=
|
||||
subsingleton.rec (λ p, p) h
|
||||
|
||||
protected def subsingleton.helim {α β : Type u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a == b :=
|
||||
protected def subsingleton.helim {α β : PType u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a == b :=
|
||||
eq.rec_on h (λ a b : α, heq_of_eq (subsingleton.elim a b))
|
||||
|
||||
instance subsingleton_prop (p : Prop) : subsingleton p :=
|
||||
|
|
@ -790,7 +790,7 @@ subsingleton.intro (λ d₁,
|
|||
end)
|
||||
end)
|
||||
|
||||
protected lemma rec_subsingleton {p : Prop} [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u}
|
||||
protected lemma rec_subsingleton {p : Prop} [h : decidable p] {h₁ : p → PType u} {h₂ : ¬p → PType u}
|
||||
[h₃ : Π (h : p), subsingleton (h₁ h)] [h₄ : Π (h : ¬p), subsingleton (h₂ h)]
|
||||
: subsingleton (decidable.rec_on h h₂ h₁) :=
|
||||
match h with
|
||||
|
|
@ -798,20 +798,20 @@ match h with
|
|||
| (is_false h) := h₄ h
|
||||
end
|
||||
|
||||
lemma if_pos {c : Prop} [h : decidable c] (hc : c) {α : Type u} {t e : α} : (ite c t e) = t :=
|
||||
lemma if_pos {c : Prop} [h : decidable c] (hc : c) {α : PType u} {t e : α} : (ite c t e) = t :=
|
||||
match h with
|
||||
| (is_true hc) := rfl
|
||||
| (is_false hnc) := absurd hc hnc
|
||||
end
|
||||
|
||||
lemma if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Type u} {t e : α} : (ite c t e) = e :=
|
||||
lemma if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : PType u} {t e : α} : (ite c t e) = e :=
|
||||
match h with
|
||||
| (is_true hc) := absurd hc hnc
|
||||
| (is_false hnc) := rfl
|
||||
end
|
||||
|
||||
attribute [simp]
|
||||
lemma if_t_t (c : Prop) [h : decidable c] {α : Type u} (t : α) : (ite c t t) = t :=
|
||||
lemma if_t_t (c : Prop) [h : decidable c] {α : PType u} (t : α) : (ite c t t) = t :=
|
||||
match h with
|
||||
| (is_true hc) := rfl
|
||||
| (is_false hnc) := rfl
|
||||
|
|
@ -823,7 +823,7 @@ assume hc, eq.rec_on (if_pos hc : ite c t e = t) h
|
|||
lemma implies_of_if_neg {c t e : Prop} [decidable c] (h : ite c t e) : ¬c → e :=
|
||||
assume hnc, eq.rec_on (if_neg hnc : ite c t e = e) h
|
||||
|
||||
lemma if_ctx_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
|
||||
lemma if_ctx_congr {α : PType u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
|
||||
{x y u v : α}
|
||||
(h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
|
||||
ite b x y = ite c u v :=
|
||||
|
|
@ -835,29 +835,29 @@ match dec_b, dec_c with
|
|||
end
|
||||
|
||||
@[congr]
|
||||
lemma if_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
|
||||
lemma if_congr {α : PType u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
|
||||
{x y u v : α}
|
||||
(h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
|
||||
ite b x y = ite c u v :=
|
||||
@if_ctx_congr α b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e)
|
||||
|
||||
lemma if_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
|
||||
lemma if_ctx_simp_congr {α : PType u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
|
||||
(h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
|
||||
ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
|
||||
@if_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e
|
||||
|
||||
@[congr]
|
||||
lemma if_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
|
||||
lemma if_simp_congr {α : PType u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
|
||||
(h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
|
||||
ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
|
||||
@if_ctx_simp_congr α b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
|
||||
|
||||
@[simp]
|
||||
lemma if_true {α : Type u} {h : decidable true} (t e : α) : (@ite true h α t e) = t :=
|
||||
lemma if_true {α : PType u} {h : decidable true} (t e : α) : (@ite true h α t e) = t :=
|
||||
if_pos trivial
|
||||
|
||||
@[simp]
|
||||
lemma if_false {α : Type u} {h : decidable false} (t e : α) : (@ite false h α t e) = e :=
|
||||
lemma if_false {α : PType u} {h : decidable false} (t e : α) : (@ite false h α t e) = e :=
|
||||
if_neg not_false
|
||||
|
||||
lemma if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
|
||||
|
|
@ -887,19 +887,19 @@ lemma if_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b]
|
|||
ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) :=
|
||||
@if_ctx_simp_congr_prop b c x y u v dec_b h_c (λ h, h_t) (λ h, h_e)
|
||||
|
||||
lemma dif_pos {c : Prop} [h : decidable c] (hc : c) {α : Type u} {t : c → α} {e : ¬ c → α} : dite c t e = t hc :=
|
||||
lemma dif_pos {c : Prop} [h : decidable c] (hc : c) {α : PType u} {t : c → α} {e : ¬ c → α} : dite c t e = t hc :=
|
||||
match h with
|
||||
| (is_true hc) := rfl
|
||||
| (is_false hnc) := absurd hc hnc
|
||||
end
|
||||
|
||||
lemma dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Type u} {t : c → α} {e : ¬ c → α} : dite c t e = e hnc :=
|
||||
lemma dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : PType u} {t : c → α} {e : ¬ c → α} : dite c t e = e hnc :=
|
||||
match h with
|
||||
| (is_true hc) := absurd hc hnc
|
||||
| (is_false hnc) := rfl
|
||||
end
|
||||
|
||||
lemma dif_ctx_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
|
||||
lemma dif_ctx_congr {α : PType u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
|
||||
{x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
|
||||
(h_c : b ↔ c)
|
||||
(h_t : ∀ (h : c), x (iff.mpr h_c h) = u h)
|
||||
|
|
@ -912,7 +912,7 @@ match dec_b, dec_c with
|
|||
| (is_true h₁), (is_false h₂) := absurd h₁ (iff.mpr (not_iff_not_of_iff h_c) h₂)
|
||||
end
|
||||
|
||||
lemma dif_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b]
|
||||
lemma dif_ctx_simp_congr {α : PType u} {b c : Prop} [dec_b : decidable b]
|
||||
{x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
|
||||
(h_c : b ↔ c)
|
||||
(h_t : ∀ (h : c), x (iff.mpr h_c h) = u h)
|
||||
|
|
@ -921,7 +921,7 @@ lemma dif_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b]
|
|||
@dif_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e
|
||||
|
||||
-- Remark: dite and ite are "defally equal" when we ignore the proofs.
|
||||
lemma dite_ite_eq (c : Prop) [h : decidable c] {α : Type u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e :=
|
||||
lemma dite_ite_eq (c : Prop) [h : decidable c] {α : PType u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e :=
|
||||
match h with
|
||||
| (is_true hc) := rfl
|
||||
| (is_false hnc) := rfl
|
||||
|
|
@ -952,7 +952,7 @@ match h₁, h₂ with
|
|||
end
|
||||
|
||||
/- Universe lifting operation -/
|
||||
structure {r s} ulift (α : Type s) : Type (max 1 s r) :=
|
||||
structure {r s} ulift (α : Type s) : Type (max s r) :=
|
||||
up :: (down : α)
|
||||
|
||||
namespace ulift
|
||||
|
|
@ -965,19 +965,19 @@ rfl
|
|||
end ulift
|
||||
|
||||
/- Equalities for rewriting let-expressions -/
|
||||
lemma let_value_eq {α : Type u} {β : Type v} {a₁ a₂ : α} (b : α → β) :
|
||||
lemma let_value_eq {α : PType u} {β : PType v} {a₁ a₂ : α} (b : α → β) :
|
||||
a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) :=
|
||||
λ h, eq.rec_on h rfl
|
||||
|
||||
lemma let_value_heq {α : Type v} {β : α → Type u} {a₁ a₂ : α} (b : Π x : α, β x) :
|
||||
lemma let_value_heq {α : PType v} {β : α → PType u} {a₁ a₂ : α} (b : Π x : α, β x) :
|
||||
a₁ = a₂ → (let x : α := a₁ in b x) == (let x : α := a₂ in b x) :=
|
||||
λ h, eq.rec_on h (heq.refl (b a₁))
|
||||
|
||||
lemma let_body_eq {α : Type v} {β : α → Type u} (a : α) {b₁ b₂ : Π x : α, β x} :
|
||||
lemma let_body_eq {α : PType v} {β : α → PType u} (a : α) {b₁ b₂ : Π x : α, β x} :
|
||||
(∀ x, b₁ x = b₂ x) → (let x : α := a in b₁ x) = (let x : α := a in b₂ x) :=
|
||||
λ h, h a
|
||||
|
||||
lemma let_eq {α : Type v} {β : Type u} {a₁ a₂ : α} {b₁ b₂ : α → β} :
|
||||
lemma let_eq {α : PType v} {β : PType u} {a₁ a₂ : α} {b₁ b₂ : α → β} :
|
||||
a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁ in b₁ x) = (let x : α := a₂ in b₂ x) :=
|
||||
λ h₁ h₂, eq.rec_on h₁ (h₂ a₁)
|
||||
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ universe variables u v
|
|||
inductive format.color
|
||||
| red | green | orange | blue | pink | cyan | grey
|
||||
|
||||
meta constant format : Type 1
|
||||
meta constant format : Type
|
||||
meta constant format.line : format
|
||||
meta constant format.space : format
|
||||
meta constant format.nil : format
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Authors: Leonardo de Moura
|
|||
prelude
|
||||
import init.meta.name
|
||||
universe variables u
|
||||
meta constant options : Type 1
|
||||
meta constant options : Type
|
||||
meta constant options.size : options → nat
|
||||
meta constant options.mk : options
|
||||
meta constant options.contains : options → name → bool
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
|
|||
prelude
|
||||
import init.data.ordering init.function init.meta.name init.meta.format
|
||||
|
||||
meta constant {u₁ u₂} rb_map : Type u₁ → Type u₂ → Type (max u₁ u₂ 1)
|
||||
meta constant {u₁ u₂} rb_map : Type u₁ → Type u₂ → Type (max u₁ u₂)
|
||||
|
||||
namespace rb_map
|
||||
meta constant mk_core {key : Type} (data : Type) : (key → key → ordering) → rb_map key data
|
||||
|
|
|
|||
|
|
@ -19,10 +19,10 @@ do t ← infer_type e,
|
|||
/- Auxiliary function for using brec_on "dictionary" -/
|
||||
private meta def mk_rec_inst_aux : expr → nat → tactic expr
|
||||
| F 0 := do
|
||||
P ← mk_app `prod.fst [F],
|
||||
mk_app `prod.fst [P]
|
||||
P ← mk_app `pprod.fst [F],
|
||||
mk_app `pprod.fst [P]
|
||||
| F (n+1) := do
|
||||
F' ← mk_app `prod.snd [F],
|
||||
F' ← mk_app `pprod.snd [F],
|
||||
mk_rec_inst_aux F' n
|
||||
|
||||
/- Construct brec_on "recursive value". F_name is the name of the brec_on "dictionary".
|
||||
|
|
|
|||
|
|
@ -137,7 +137,7 @@ meta def repeat_exactly : nat → tactic unit → tactic unit
|
|||
meta def repeat : tactic unit → tactic unit :=
|
||||
repeat_at_most 100000
|
||||
|
||||
meta def returnex {α : Type 1} (e : exceptional α) : tactic α :=
|
||||
meta def returnex {α : Type} (e : exceptional α) : tactic α :=
|
||||
λ s, match e with
|
||||
| (exceptional.success a) := tactic_result.success a s
|
||||
| (exceptional.exception .α f) := tactic_result.exception α (λ u, f options.mk) none s -- TODO(Leo): extract options from environment
|
||||
|
|
@ -282,8 +282,8 @@ meta constant get_unused_name : name → option nat → tactic name
|
|||
|
||||
Example, given
|
||||
rel.{l_1 l_2} : Pi (α : Type.{l_1}) (β : α -> Type.{l_2}), (Pi x : α, β x) -> (Pi x : α, β x) -> , Prop
|
||||
nat : Type 1
|
||||
real : Type 1
|
||||
nat : Type
|
||||
real : Type
|
||||
vec.{l} : Pi (α : Type l) (n : nat), Type.{l1}
|
||||
f g : Pi (n : nat), vec real n
|
||||
then
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
prelude
|
||||
import init.category
|
||||
|
||||
meta constant {u} task : Type u → Type (max u 1)
|
||||
meta constant {u} task : Type u → Type u
|
||||
|
||||
namespace task
|
||||
|
||||
|
|
|
|||
|
|
@ -75,7 +75,7 @@ meta constant vm_core.bind {α β : Type} : vm_core α → (α → vm_core β)
|
|||
meta instance : monad vm_core :=
|
||||
{map := @vm_core.map, ret := @vm_core.ret, bind := @vm_core.bind}
|
||||
|
||||
@[reducible] meta def vm (α : Type) : Type := option_t.{1 1} vm_core α
|
||||
@[reducible] meta def vm (α : Type) : Type := option_t vm_core α
|
||||
|
||||
namespace vm
|
||||
meta constant get_env : vm environment
|
||||
|
|
|
|||
|
|
@ -22,10 +22,9 @@ import init.native.config
|
|||
import init.native.result
|
||||
|
||||
namespace native
|
||||
|
||||
inductive error
|
||||
inductive error : Type
|
||||
| string : string → error
|
||||
| many : list error → error
|
||||
| many : list error → error
|
||||
|
||||
meta def error.to_string : error → string
|
||||
| (error.string s) := s
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ acc.rec_on h₁ (λ x₁ ac₁ ih h₂, ac₁ y h₂) h₂
|
|||
-- dependent elimination for acc
|
||||
attribute [recursor]
|
||||
protected def drec
|
||||
{C : Π (a : α), acc r a → Type v}
|
||||
{C : Π (a : α), acc r a → PType v}
|
||||
(h₁ : Π (x : α) (acx : Π (y : α), r y x → acc r y), (Π (y : α) (ryx : r y x), C y (acx y ryx)) → C x (acc.intro x acx))
|
||||
{a : α} (h₂ : acc r a) : C a h₂ :=
|
||||
acc.rec (λ x acx ih h₂, h₁ x acx (λ y ryx, ih y ryx (acx y ryx))) h₂ h₂
|
||||
|
|
@ -39,7 +39,7 @@ local infix `≺`:50 := r
|
|||
|
||||
hypothesis hwf : well_founded r
|
||||
|
||||
lemma recursion {C : α → Type v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a :=
|
||||
lemma recursion {C : α → PType v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a :=
|
||||
acc.rec_on (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih)
|
||||
|
||||
lemma induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a :=
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ Constructions with:
|
|||
|
||||
* an impredicative, proof-irrelevant type `Prop` of propositions
|
||||
* universe polymorphism
|
||||
* a non-cumulative hierarchy of universes, `Type 1`, `Type 2`, ... above `Prop`
|
||||
* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ... above `Prop`
|
||||
* inductively defined types
|
||||
* quotient types
|
||||
|
||||
|
|
|
|||
|
|
@ -155,7 +155,7 @@
|
|||
(,(rx word-start (group "example") ".") (1 'font-lock-keyword-face))
|
||||
(,(rx (or "∎")) . 'font-lock-keyword-face)
|
||||
;; Types
|
||||
(,(rx word-start (or "Prop" "Type" "Type*" "Type₀" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face)
|
||||
(,(rx word-start (or "Prop" "Type" "Type*" "PType" "PType*" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face)
|
||||
(,(rx word-start (group (or "Prop" "Type")) ".") (1 'font-lock-type-face))
|
||||
;; String
|
||||
("\"[^\"]*\"" . 'font-lock-string-face)
|
||||
|
|
|
|||
|
|
@ -48,18 +48,44 @@ bool get_parser_checkpoint_have(options const & opts) {
|
|||
|
||||
using namespace notation; // NOLINT
|
||||
|
||||
static name * g_no_universe_annotation = nullptr;
|
||||
|
||||
bool is_sort_wo_universe(expr const & e) {
|
||||
return is_annotation(e, *g_no_universe_annotation);
|
||||
}
|
||||
|
||||
expr mk_sort_wo_universe(parser & p, pos_info const & pos, bool is_type) {
|
||||
expr r = p.save_pos(mk_sort(is_type ? mk_level_one() : mk_level_zero()), pos);
|
||||
return p.save_pos(mk_annotation(*g_no_universe_annotation, r), pos);
|
||||
}
|
||||
|
||||
static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
if (p.curr_is_token(get_llevel_curly_tk())) {
|
||||
p.next();
|
||||
level l = p.parse_level();
|
||||
level l = mk_succ(p.parse_level());
|
||||
p.check_token_next(get_rcurly_tk(), "invalid Type expression, '}' expected");
|
||||
return p.save_pos(mk_sort(l), pos);
|
||||
} else {
|
||||
return p.save_pos(mk_sort(mk_level_one_placeholder()), pos);
|
||||
return mk_sort_wo_universe(p, pos, true);
|
||||
}
|
||||
}
|
||||
|
||||
static expr parse_PType(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
if (p.curr_is_token(get_llevel_curly_tk())) {
|
||||
p.next();
|
||||
level l = p.parse_level();
|
||||
p.check_token_next(get_rcurly_tk(), "invalid PType expression, '}' expected");
|
||||
return p.save_pos(mk_sort(l), pos);
|
||||
} else {
|
||||
return mk_sort_wo_universe(p, pos, false);
|
||||
}
|
||||
}
|
||||
|
||||
static expr parse_Type_star(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
return p.save_pos(mk_sort(mk_succ(mk_level_placeholder())), pos);
|
||||
}
|
||||
|
||||
static expr parse_PType_star(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
return p.save_pos(mk_sort(mk_level_placeholder()), pos);
|
||||
}
|
||||
|
||||
|
|
@ -743,6 +769,8 @@ parse_table init_nud_table() {
|
|||
r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
|
||||
r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
|
||||
r = r.add({transition("Type*", mk_ext_action(parse_Type_star))}, x0);
|
||||
r = r.add({transition("PType", mk_ext_action(parse_PType))}, x0);
|
||||
r = r.add({transition("PType*", mk_ext_action(parse_PType_star))}, x0);
|
||||
r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
|
||||
r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
|
||||
r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
|
||||
|
|
@ -902,6 +930,9 @@ parse_table get_builtin_led_table() {
|
|||
}
|
||||
|
||||
void initialize_builtin_exprs() {
|
||||
g_no_universe_annotation = new name("no_univ");
|
||||
register_annotation(*g_no_universe_annotation);
|
||||
|
||||
g_not = new expr(mk_constant(get_not_name()));
|
||||
g_nud_table = new parse_table();
|
||||
*g_nud_table = init_nud_table();
|
||||
|
|
@ -944,5 +975,6 @@ void finalize_builtin_exprs() {
|
|||
delete g_anonymous_constructor;
|
||||
delete g_field_notation_opcode;
|
||||
delete g_field_notation_name;
|
||||
delete g_no_universe_annotation;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,6 +7,8 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include "frontends/lean/parse_table.h"
|
||||
namespace lean {
|
||||
bool is_sort_wo_universe(expr const & e);
|
||||
|
||||
expr mk_anonymous_constructor(expr const & e);
|
||||
bool is_anonymous_constructor(expr const & e);
|
||||
expr const & get_anonymous_constructor_arg(expr const & e);
|
||||
|
|
|
|||
|
|
@ -675,6 +675,15 @@ expr elaborator::visit_typed_expr(expr const & e) {
|
|||
line() + format("but is expected to have type") + pp_indent(pp_fn, new_type));
|
||||
}
|
||||
|
||||
level elaborator::dec_level(level const & l, expr const & ref) {
|
||||
if (auto d = ::lean::dec_level(l))
|
||||
return *d;
|
||||
level r = m_ctx.mk_univ_metavar_decl();
|
||||
if (!m_ctx.is_def_eq(mk_succ(r), l))
|
||||
throw elaborator_exception(ref, "invalid pre-numeral, universe level must be > 0");
|
||||
return r;
|
||||
}
|
||||
|
||||
expr elaborator::visit_prenum(expr const & e, optional<expr> const & expected_type) {
|
||||
lean_assert(is_prenum(e));
|
||||
expr ref = e;
|
||||
|
|
@ -690,7 +699,7 @@ expr elaborator::visit_prenum(expr const & e, optional<expr> const & expected_ty
|
|||
m_numeral_types = cons(A, m_numeral_types);
|
||||
}
|
||||
level A_lvl = get_level(A, ref);
|
||||
levels ls(A_lvl);
|
||||
levels ls(dec_level(A_lvl, ref));
|
||||
if (v.is_neg())
|
||||
throw elaborator_exception(ref, "invalid pre-numeral, it must be a non-negative value");
|
||||
if (v.is_zero()) {
|
||||
|
|
@ -2449,6 +2458,8 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
|
|||
return visit(get_annotation_arg(e), expected_type);
|
||||
} else if (is_emptyc_or_emptys(e)) {
|
||||
return visit_emptyc_or_emptys(e, expected_type);
|
||||
} else if (is_sort_wo_universe(e)) {
|
||||
return visit(get_annotation_arg(e), expected_type);
|
||||
} else {
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Var: lean_unreachable(); // LCOV_EXCL_LINE
|
||||
|
|
|
|||
|
|
@ -158,6 +158,7 @@ private:
|
|||
|
||||
expr visit_scope_trace(expr const & e, optional<expr> const & expected_type);
|
||||
expr visit_typed_expr(expr const & e);
|
||||
level dec_level(level const & l, expr const & ref);
|
||||
expr visit_prenum_core(expr const & e, optional<expr> const & expected_type);
|
||||
expr visit_prenum(expr const & e, optional<expr> const & expected_type);
|
||||
expr visit_placeholder(expr const & e, optional<expr> const & expected_type);
|
||||
|
|
|
|||
|
|
@ -1950,9 +1950,13 @@ bool parser::curr_starts_expr() {
|
|||
}
|
||||
|
||||
expr parser::parse_led(expr left) {
|
||||
if (is_sort(left) && is_one_placeholder(sort_level(left)) &&
|
||||
if (is_sort_wo_universe(left) &&
|
||||
(curr_is_numeral() || curr_is_identifier() || curr_is_token(get_lparen_tk()) || curr_is_token(get_placeholder_tk()))) {
|
||||
left = get_annotation_arg(left);
|
||||
level l = parse_level(get_max_prec());
|
||||
lean_assert(sort_level(left) == mk_level_one() || sort_level(left) == mk_level_zero());
|
||||
if (sort_level(left) == mk_level_one())
|
||||
l = mk_succ(l);
|
||||
return copy_tag(left, update_sort(left, l));
|
||||
} else {
|
||||
switch (curr()) {
|
||||
|
|
|
|||
|
|
@ -604,8 +604,10 @@ auto pretty_fn::pp_sort(expr const & e) -> result {
|
|||
return result(format("Prop"));
|
||||
} else if (u == mk_level_one()) {
|
||||
return result(format("Type"));
|
||||
} else if (optional<level> u1 = dec_level(u)) {
|
||||
return result(group(format("Type") + space() + nest(5, pp_child(*u1))));
|
||||
} else {
|
||||
return result(group(format("Type") + space() + nest(5, pp_child(u))));
|
||||
return result(group(format("PType") + space() + nest(5, pp_child(u))));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -84,7 +84,8 @@ void init_token_table(token_table & t) {
|
|||
{"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec},
|
||||
{"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0},
|
||||
{"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
|
||||
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type*", g_max_prec},
|
||||
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
|
||||
{"Type", g_max_prec}, {"Type*", g_max_prec}, {"PType", g_max_prec}, {"PType*", g_max_prec},
|
||||
{"(:", g_max_prec}, {":)", 0},
|
||||
{"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
|
||||
{"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
|
|||
|
||||
virtual expr visit_app(expr const & e) {
|
||||
expr const & f = get_app_fn(e);
|
||||
if (is_constant(f) && const_name(f) == get_prod_fst_name()) {
|
||||
if (is_constant(f) && const_name(f) == get_pprod_fst_name()) {
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
if (args.size() >= 3 && is_rec_arg(args[2])) {
|
||||
|
|
@ -69,7 +69,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
|
|||
|
||||
optional<expr> simplify(expr const & e) {
|
||||
expr const & f = get_app_fn(e);
|
||||
if (!is_constant(f) || const_name(f) != get_prod_fst_name())
|
||||
if (!is_constant(f) || const_name(f) != get_pprod_fst_name())
|
||||
return none_expr();
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
|
|
@ -105,7 +105,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
|
|||
buffer<expr> typeformer_body_args;
|
||||
expr typeformer_body_fn = get_app_args(typeformer_body, typeformer_body_args);
|
||||
if (!is_constant(typeformer_body_fn) ||
|
||||
const_name(typeformer_body_fn) != get_prod_name() ||
|
||||
const_name(typeformer_body_fn) != get_pprod_name() ||
|
||||
typeformer_body_args.size() != 2) {
|
||||
return none_expr();
|
||||
}
|
||||
|
|
@ -143,7 +143,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
|
|||
}
|
||||
buffer<expr> type_args;
|
||||
expr type_fn = get_app_args(type, type_args);
|
||||
if (!is_constant(type_fn) || const_name(type_fn) != get_prod_name() || type_args.size() != 2) {
|
||||
if (!is_constant(type_fn) || const_name(type_fn) != get_pprod_name() || type_args.size() != 2) {
|
||||
return none_expr();
|
||||
}
|
||||
minor_ctx[k] = update_mlocal(minor_ctx[k], locals.mk_pi(type_args[0]));
|
||||
|
|
@ -154,7 +154,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
|
|||
buffer<expr> minor_body_args;
|
||||
expr minor_body_fn = get_app_args(minor_body, minor_body_args);
|
||||
if (!is_constant(minor_body_fn) ||
|
||||
const_name(minor_body_fn) != get_prod_mk_name() ||
|
||||
const_name(minor_body_fn) != get_pprod_mk_name() ||
|
||||
minor_body_args.size() != 4) {
|
||||
return none_expr();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -333,10 +333,11 @@ name const * g_pos_num = nullptr;
|
|||
name const * g_pos_num_bit0 = nullptr;
|
||||
name const * g_pos_num_bit1 = nullptr;
|
||||
name const * g_pos_num_one = nullptr;
|
||||
name const * g_prod = nullptr;
|
||||
name const * g_prod_mk = nullptr;
|
||||
name const * g_prod_fst = nullptr;
|
||||
name const * g_prod_snd = nullptr;
|
||||
name const * g_pprod = nullptr;
|
||||
name const * g_pprod_mk = nullptr;
|
||||
name const * g_pprod_fst = nullptr;
|
||||
name const * g_pprod_snd = nullptr;
|
||||
name const * g_propext = nullptr;
|
||||
name const * g_pexpr = nullptr;
|
||||
name const * g_pexpr_subst = nullptr;
|
||||
|
|
@ -377,6 +378,11 @@ name const * g_sigma_cases_on = nullptr;
|
|||
name const * g_sigma_mk = nullptr;
|
||||
name const * g_sigma_fst = nullptr;
|
||||
name const * g_sigma_snd = nullptr;
|
||||
name const * g_psigma = nullptr;
|
||||
name const * g_psigma_cases_on = nullptr;
|
||||
name const * g_psigma_mk = nullptr;
|
||||
name const * g_psigma_fst = nullptr;
|
||||
name const * g_psigma_snd = nullptr;
|
||||
name const * g_simp = nullptr;
|
||||
name const * g_simplifier_assoc_subst = nullptr;
|
||||
name const * g_simplifier_congr_bin_op = nullptr;
|
||||
|
|
@ -410,6 +416,10 @@ name const * g_sum = nullptr;
|
|||
name const * g_sum_cases_on = nullptr;
|
||||
name const * g_sum_inl = nullptr;
|
||||
name const * g_sum_inr = nullptr;
|
||||
name const * g_psum = nullptr;
|
||||
name const * g_psum_cases_on = nullptr;
|
||||
name const * g_psum_inl = nullptr;
|
||||
name const * g_psum_inr = nullptr;
|
||||
name const * g_default_smt_config = nullptr;
|
||||
name const * g_smt_state_mk = nullptr;
|
||||
name const * g_smt_tactic_execute = nullptr;
|
||||
|
|
@ -798,10 +808,11 @@ void initialize_constants() {
|
|||
g_pos_num_bit0 = new name{"pos_num", "bit0"};
|
||||
g_pos_num_bit1 = new name{"pos_num", "bit1"};
|
||||
g_pos_num_one = new name{"pos_num", "one"};
|
||||
g_prod = new name{"prod"};
|
||||
g_prod_mk = new name{"prod", "mk"};
|
||||
g_prod_fst = new name{"prod", "fst"};
|
||||
g_prod_snd = new name{"prod", "snd"};
|
||||
g_pprod = new name{"pprod"};
|
||||
g_pprod_mk = new name{"pprod", "mk"};
|
||||
g_pprod_fst = new name{"pprod", "fst"};
|
||||
g_pprod_snd = new name{"pprod", "snd"};
|
||||
g_propext = new name{"propext"};
|
||||
g_pexpr = new name{"pexpr"};
|
||||
g_pexpr_subst = new name{"pexpr", "subst"};
|
||||
|
|
@ -842,6 +853,11 @@ void initialize_constants() {
|
|||
g_sigma_mk = new name{"sigma", "mk"};
|
||||
g_sigma_fst = new name{"sigma", "fst"};
|
||||
g_sigma_snd = new name{"sigma", "snd"};
|
||||
g_psigma = new name{"psigma"};
|
||||
g_psigma_cases_on = new name{"psigma", "cases_on"};
|
||||
g_psigma_mk = new name{"psigma", "mk"};
|
||||
g_psigma_fst = new name{"psigma", "fst"};
|
||||
g_psigma_snd = new name{"psigma", "snd"};
|
||||
g_simp = new name{"simp"};
|
||||
g_simplifier_assoc_subst = new name{"simplifier", "assoc_subst"};
|
||||
g_simplifier_congr_bin_op = new name{"simplifier", "congr_bin_op"};
|
||||
|
|
@ -875,6 +891,10 @@ void initialize_constants() {
|
|||
g_sum_cases_on = new name{"sum", "cases_on"};
|
||||
g_sum_inl = new name{"sum", "inl"};
|
||||
g_sum_inr = new name{"sum", "inr"};
|
||||
g_psum = new name{"psum"};
|
||||
g_psum_cases_on = new name{"psum", "cases_on"};
|
||||
g_psum_inl = new name{"psum", "inl"};
|
||||
g_psum_inr = new name{"psum", "inr"};
|
||||
g_default_smt_config = new name{"default_smt_config"};
|
||||
g_smt_state_mk = new name{"smt_state", "mk"};
|
||||
g_smt_tactic_execute = new name{"smt_tactic", "execute"};
|
||||
|
|
@ -1264,10 +1284,11 @@ void finalize_constants() {
|
|||
delete g_pos_num_bit0;
|
||||
delete g_pos_num_bit1;
|
||||
delete g_pos_num_one;
|
||||
delete g_prod;
|
||||
delete g_prod_mk;
|
||||
delete g_prod_fst;
|
||||
delete g_prod_snd;
|
||||
delete g_pprod;
|
||||
delete g_pprod_mk;
|
||||
delete g_pprod_fst;
|
||||
delete g_pprod_snd;
|
||||
delete g_propext;
|
||||
delete g_pexpr;
|
||||
delete g_pexpr_subst;
|
||||
|
|
@ -1308,6 +1329,11 @@ void finalize_constants() {
|
|||
delete g_sigma_mk;
|
||||
delete g_sigma_fst;
|
||||
delete g_sigma_snd;
|
||||
delete g_psigma;
|
||||
delete g_psigma_cases_on;
|
||||
delete g_psigma_mk;
|
||||
delete g_psigma_fst;
|
||||
delete g_psigma_snd;
|
||||
delete g_simp;
|
||||
delete g_simplifier_assoc_subst;
|
||||
delete g_simplifier_congr_bin_op;
|
||||
|
|
@ -1341,6 +1367,10 @@ void finalize_constants() {
|
|||
delete g_sum_cases_on;
|
||||
delete g_sum_inl;
|
||||
delete g_sum_inr;
|
||||
delete g_psum;
|
||||
delete g_psum_cases_on;
|
||||
delete g_psum_inl;
|
||||
delete g_psum_inr;
|
||||
delete g_default_smt_config;
|
||||
delete g_smt_state_mk;
|
||||
delete g_smt_tactic_execute;
|
||||
|
|
@ -1729,10 +1759,11 @@ name const & get_pos_num_name() { return *g_pos_num; }
|
|||
name const & get_pos_num_bit0_name() { return *g_pos_num_bit0; }
|
||||
name const & get_pos_num_bit1_name() { return *g_pos_num_bit1; }
|
||||
name const & get_pos_num_one_name() { return *g_pos_num_one; }
|
||||
name const & get_prod_name() { return *g_prod; }
|
||||
name const & get_prod_mk_name() { return *g_prod_mk; }
|
||||
name const & get_prod_fst_name() { return *g_prod_fst; }
|
||||
name const & get_prod_snd_name() { return *g_prod_snd; }
|
||||
name const & get_pprod_name() { return *g_pprod; }
|
||||
name const & get_pprod_mk_name() { return *g_pprod_mk; }
|
||||
name const & get_pprod_fst_name() { return *g_pprod_fst; }
|
||||
name const & get_pprod_snd_name() { return *g_pprod_snd; }
|
||||
name const & get_propext_name() { return *g_propext; }
|
||||
name const & get_pexpr_name() { return *g_pexpr; }
|
||||
name const & get_pexpr_subst_name() { return *g_pexpr_subst; }
|
||||
|
|
@ -1773,6 +1804,11 @@ name const & get_sigma_cases_on_name() { return *g_sigma_cases_on; }
|
|||
name const & get_sigma_mk_name() { return *g_sigma_mk; }
|
||||
name const & get_sigma_fst_name() { return *g_sigma_fst; }
|
||||
name const & get_sigma_snd_name() { return *g_sigma_snd; }
|
||||
name const & get_psigma_name() { return *g_psigma; }
|
||||
name const & get_psigma_cases_on_name() { return *g_psigma_cases_on; }
|
||||
name const & get_psigma_mk_name() { return *g_psigma_mk; }
|
||||
name const & get_psigma_fst_name() { return *g_psigma_fst; }
|
||||
name const & get_psigma_snd_name() { return *g_psigma_snd; }
|
||||
name const & get_simp_name() { return *g_simp; }
|
||||
name const & get_simplifier_assoc_subst_name() { return *g_simplifier_assoc_subst; }
|
||||
name const & get_simplifier_congr_bin_op_name() { return *g_simplifier_congr_bin_op; }
|
||||
|
|
@ -1806,6 +1842,10 @@ name const & get_sum_name() { return *g_sum; }
|
|||
name const & get_sum_cases_on_name() { return *g_sum_cases_on; }
|
||||
name const & get_sum_inl_name() { return *g_sum_inl; }
|
||||
name const & get_sum_inr_name() { return *g_sum_inr; }
|
||||
name const & get_psum_name() { return *g_psum; }
|
||||
name const & get_psum_cases_on_name() { return *g_psum_cases_on; }
|
||||
name const & get_psum_inl_name() { return *g_psum_inl; }
|
||||
name const & get_psum_inr_name() { return *g_psum_inr; }
|
||||
name const & get_default_smt_config_name() { return *g_default_smt_config; }
|
||||
name const & get_smt_state_mk_name() { return *g_smt_state_mk; }
|
||||
name const & get_smt_tactic_execute_name() { return *g_smt_tactic_execute; }
|
||||
|
|
|
|||
|
|
@ -335,10 +335,11 @@ name const & get_pos_num_name();
|
|||
name const & get_pos_num_bit0_name();
|
||||
name const & get_pos_num_bit1_name();
|
||||
name const & get_pos_num_one_name();
|
||||
name const & get_prod_name();
|
||||
name const & get_prod_mk_name();
|
||||
name const & get_prod_fst_name();
|
||||
name const & get_prod_snd_name();
|
||||
name const & get_pprod_name();
|
||||
name const & get_pprod_mk_name();
|
||||
name const & get_pprod_fst_name();
|
||||
name const & get_pprod_snd_name();
|
||||
name const & get_propext_name();
|
||||
name const & get_pexpr_name();
|
||||
name const & get_pexpr_subst_name();
|
||||
|
|
@ -379,6 +380,11 @@ name const & get_sigma_cases_on_name();
|
|||
name const & get_sigma_mk_name();
|
||||
name const & get_sigma_fst_name();
|
||||
name const & get_sigma_snd_name();
|
||||
name const & get_psigma_name();
|
||||
name const & get_psigma_cases_on_name();
|
||||
name const & get_psigma_mk_name();
|
||||
name const & get_psigma_fst_name();
|
||||
name const & get_psigma_snd_name();
|
||||
name const & get_simp_name();
|
||||
name const & get_simplifier_assoc_subst_name();
|
||||
name const & get_simplifier_congr_bin_op_name();
|
||||
|
|
@ -412,6 +418,10 @@ name const & get_sum_name();
|
|||
name const & get_sum_cases_on_name();
|
||||
name const & get_sum_inl_name();
|
||||
name const & get_sum_inr_name();
|
||||
name const & get_psum_name();
|
||||
name const & get_psum_cases_on_name();
|
||||
name const & get_psum_inl_name();
|
||||
name const & get_psum_inr_name();
|
||||
name const & get_default_smt_config_name();
|
||||
name const & get_smt_state_mk_name();
|
||||
name const & get_smt_tactic_execute_name();
|
||||
|
|
|
|||
|
|
@ -328,10 +328,11 @@ pos_num
|
|||
pos_num.bit0
|
||||
pos_num.bit1
|
||||
pos_num.one
|
||||
prod
|
||||
prod.mk
|
||||
prod.fst
|
||||
prod.snd
|
||||
pprod
|
||||
pprod.mk
|
||||
pprod.fst
|
||||
pprod.snd
|
||||
propext
|
||||
pexpr
|
||||
pexpr.subst
|
||||
|
|
@ -372,6 +373,11 @@ sigma.cases_on
|
|||
sigma.mk
|
||||
sigma.fst
|
||||
sigma.snd
|
||||
psigma
|
||||
psigma.cases_on
|
||||
psigma.mk
|
||||
psigma.fst
|
||||
psigma.snd
|
||||
simp
|
||||
simplifier.assoc_subst
|
||||
simplifier.congr_bin_op
|
||||
|
|
@ -405,6 +411,10 @@ sum
|
|||
sum.cases_on
|
||||
sum.inl
|
||||
sum.inr
|
||||
psum
|
||||
psum.cases_on
|
||||
psum.inl
|
||||
psum.inr
|
||||
default_smt_config
|
||||
smt_state.mk
|
||||
smt_tactic.execute
|
||||
|
|
|
|||
|
|
@ -125,10 +125,10 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
|
|||
expr fst = mlocal_type(minor_arg);
|
||||
minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, Type_result));
|
||||
expr snd = Pi(minor_arg_args, mk_app(minor_arg, minor_arg_args));
|
||||
prod_pairs.push_back(mk_prod(tc, fst, snd, ibelow));
|
||||
prod_pairs.push_back(mk_pprod(tc, fst, snd, ibelow));
|
||||
}
|
||||
}
|
||||
expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_prod(tc, a, b, ibelow); },
|
||||
expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_pprod(tc, a, b, ibelow); },
|
||||
[&]() { return mk_unit(rlvl, ibelow); },
|
||||
prod_pairs.size(), prod_pairs.data());
|
||||
rec = mk_app(rec, Fun(minor_args, new_arg));
|
||||
|
|
@ -273,7 +273,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
|
|||
to_telescope(mlocal_type(C), C_args);
|
||||
expr C_t = mk_app(C, C_args);
|
||||
expr below_t = mk_app(belows[j], C_args);
|
||||
expr prod = mk_prod(tc, C_t, below_t, ind);
|
||||
expr prod = mk_pprod(tc, C_t, below_t, ind);
|
||||
rec = mk_app(rec, Fun(C_args, prod));
|
||||
}
|
||||
// add minor premises to rec
|
||||
|
|
@ -289,19 +289,19 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
|
|||
if (auto k = is_typeformer_app(typeformer_names, minor_arg_type)) {
|
||||
buffer<expr> C_args;
|
||||
get_app_args(minor_arg_type, C_args);
|
||||
expr new_minor_arg_type = mk_prod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind);
|
||||
expr new_minor_arg_type = mk_pprod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind);
|
||||
minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, new_minor_arg_type));
|
||||
if (minor_arg_args.empty()) {
|
||||
pairs.push_back(minor_arg);
|
||||
} else {
|
||||
expr r = mk_app(minor_arg, minor_arg_args);
|
||||
expr r_1 = Fun(minor_arg_args, mk_fst(tc, r, ind));
|
||||
expr r_2 = Fun(minor_arg_args, mk_snd(tc, r, ind));
|
||||
pairs.push_back(mk_pair(tc, r_1, r_2, ind));
|
||||
expr r_1 = Fun(minor_arg_args, mk_pprod_fst(tc, r, ind));
|
||||
expr r_2 = Fun(minor_arg_args, mk_pprod_snd(tc, r, ind));
|
||||
pairs.push_back(mk_pprod_mk(tc, r_1, r_2, ind));
|
||||
}
|
||||
}
|
||||
}
|
||||
expr b = foldr([&](expr const & a, expr const & b) { return mk_pair(tc, a, b, ind); },
|
||||
expr b = foldr([&](expr const & a, expr const & b) { return mk_pprod_mk(tc, a, b, ind); },
|
||||
[&]() { return mk_unit_mk(rlvl, ind); },
|
||||
pairs.size(), pairs.data());
|
||||
unsigned F_idx = *is_typeformer_app(typeformer_names, minor_type);
|
||||
|
|
@ -309,7 +309,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
|
|||
buffer<expr> F_args;
|
||||
get_app_args(minor_type, F_args);
|
||||
F_args.push_back(b);
|
||||
expr new_arg = mk_pair(tc, mk_app(F, F_args), b, ind);
|
||||
expr new_arg = mk_pprod_mk(tc, mk_app(F, F_args), b, ind);
|
||||
rec = mk_app(rec, Fun(minor_args, new_arg));
|
||||
}
|
||||
// add indices and major to rec
|
||||
|
|
@ -319,7 +319,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
|
|||
|
||||
name brec_on_name = name(n, ind ? "binduction_on" : "brec_on");
|
||||
expr brec_on_type = Pi(args, result_type);
|
||||
expr brec_on_value = Fun(args, mk_fst(tc, rec, ind));
|
||||
expr brec_on_value = Fun(args, mk_pprod_fst(tc, rec, ind));
|
||||
|
||||
declaration new_d = mk_definition_inferring_trusted(env, brec_on_name, blps, brec_on_type, brec_on_value,
|
||||
reducibility_hints::mk_abbreviation());
|
||||
|
|
|
|||
|
|
@ -414,13 +414,13 @@ struct structural_rec_fn {
|
|||
optional<expr> to_below(expr const & d, expr const & a, expr const & F) {
|
||||
expr const & fn = get_app_fn(d);
|
||||
trace_struct_aux(tout() << "d: " << d << ", a: " << a << ", F: " << F << "\n";);
|
||||
if (is_constant(fn, get_prod_name()) || is_constant(fn, get_and_name())) {
|
||||
if (is_constant(fn, get_pprod_name()) || is_constant(fn, get_and_name())) {
|
||||
bool prop = is_constant(fn, get_and_name());
|
||||
expr d_arg1 = m_ctx.whnf(app_arg(app_fn(d)));
|
||||
expr d_arg2 = m_ctx.whnf(app_arg(d));
|
||||
if (auto r = to_below(d_arg1, a, mk_fst(m_ctx, F, prop)))
|
||||
if (auto r = to_below(d_arg1, a, mk_pprod_fst(m_ctx, F, prop)))
|
||||
return r;
|
||||
else if (auto r = to_below(d_arg2, a, mk_snd(m_ctx, F, prop)))
|
||||
else if (auto r = to_below(d_arg2, a, mk_pprod_snd(m_ctx, F, prop)))
|
||||
return r;
|
||||
else
|
||||
return none_expr();
|
||||
|
|
@ -660,11 +660,11 @@ struct structural_rec_fn {
|
|||
buffer<expr> args;
|
||||
expr const & fn = get_app_args(e, args);
|
||||
if (args.size() == 3) {
|
||||
if (is_constant(fn, get_prod_fst_name())) {
|
||||
if (is_constant(fn, get_pprod_fst_name())) {
|
||||
bool r = is_F_instance(args[2], path);
|
||||
path.push_back(1);
|
||||
return r;
|
||||
} else if (is_constant(fn, get_prod_snd_name())) {
|
||||
} else if (is_constant(fn, get_pprod_snd_name())) {
|
||||
bool r = is_F_instance(args[2], path);
|
||||
path.push_back(2);
|
||||
return r;
|
||||
|
|
@ -788,7 +788,7 @@ struct structural_rec_fn {
|
|||
virtual expr visit_app(expr const & e) {
|
||||
buffer<expr> args;
|
||||
expr const & fn = get_app_args(e, args);
|
||||
if (is_constant(fn, get_prod_fst_name()) && args.size() >= 3) {
|
||||
if (is_constant(fn, get_pprod_fst_name()) && args.size() >= 3) {
|
||||
buffer<unsigned> path;
|
||||
if (is_F_instance(args[2], path)) {
|
||||
path.push_back(1);
|
||||
|
|
|
|||
|
|
@ -76,7 +76,7 @@ class add_basic_inductive_decl_fn {
|
|||
bool has_unit = has_poly_unit_decls(m_env);
|
||||
bool has_eq = has_eq_decls(m_env);
|
||||
bool has_heq = has_heq_decls(m_env);
|
||||
bool has_prod = has_prod_decls(m_env);
|
||||
bool has_prod = has_pprod_decls(m_env);
|
||||
|
||||
bool gen_rec_on = get_inductive_rec_on(m_opts);
|
||||
bool gen_brec_on = get_inductive_brec_on(m_opts);
|
||||
|
|
|
|||
|
|
@ -66,11 +66,11 @@ class add_mutual_inductive_decl_fn {
|
|||
expr l = mk_local_for(ty);
|
||||
expr dom = binding_domain(ty);
|
||||
expr rest = Fun(l, to_sigma_type(instantiate(binding_body(ty), l)));
|
||||
return mk_app(m_tctx, get_sigma_name(), {dom, rest});
|
||||
return mk_app(m_tctx, get_psigma_name(), {dom, rest});
|
||||
}
|
||||
|
||||
expr mk_sum(expr const & A, expr const & B) {
|
||||
return mk_app(m_tctx, get_sum_name(), A, B);
|
||||
return mk_app(m_tctx, get_psum_name(), A, B);
|
||||
}
|
||||
|
||||
expr mk_sum(unsigned num_args, expr const * args) {
|
||||
|
|
@ -108,8 +108,8 @@ class add_mutual_inductive_decl_fn {
|
|||
level l1 = get_level(m_tctx, A);
|
||||
level l2 = get_level(m_tctx, stype);
|
||||
stype = Fun(l, stype);
|
||||
maker = mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), A, stype, l, maker);
|
||||
stype = mk_app(m_tctx, get_sigma_name(), {A, stype});
|
||||
maker = mk_app(mk_constant(get_psigma_mk_name(), {l1, l2}), A, stype, l, maker);
|
||||
stype = mk_app(m_tctx, get_psigma_name(), {A, stype});
|
||||
}
|
||||
return mk_pair(Fun(locals, maker), stype);
|
||||
}
|
||||
|
|
@ -133,7 +133,7 @@ class add_mutual_inductive_decl_fn {
|
|||
expr l = mk_local_pp("rest", mk_sum(m_index_types.size() - i, m_index_types.data() + i));
|
||||
expr putter = l;
|
||||
for (unsigned j = i; j > 0; --j) {
|
||||
putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[j-1], mk_sum(m_index_types.size() - j, m_index_types.data() + j), putter);
|
||||
putter = mk_app(m_tctx, get_psum_inr_name(), m_index_types[j-1], mk_sum(m_index_types.size() - j, m_index_types.data() + j), putter);
|
||||
}
|
||||
return Fun(l, putter);
|
||||
}
|
||||
|
|
@ -144,13 +144,13 @@ class add_mutual_inductive_decl_fn {
|
|||
|
||||
expr putter;
|
||||
if (ind_idx == num_inds - 1) {
|
||||
putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[ind_idx - 1], m_index_types[ind_idx], l);
|
||||
putter = mk_app(m_tctx, get_psum_inr_name(), m_index_types[ind_idx - 1], m_index_types[ind_idx], l);
|
||||
ind_idx--;
|
||||
} else {
|
||||
putter = mk_app(m_tctx, get_sum_inl_name(), m_index_types[ind_idx], mk_sum(num_inds - ind_idx - 1, m_index_types.data() + ind_idx + 1), l);
|
||||
putter = mk_app(m_tctx, get_psum_inl_name(), m_index_types[ind_idx], mk_sum(num_inds - ind_idx - 1, m_index_types.data() + ind_idx + 1), l);
|
||||
}
|
||||
for (unsigned i = ind_idx; i > 0; --i) {
|
||||
putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[i - 1], mk_sum(num_inds - i, m_index_types.data() + i), putter);
|
||||
putter = mk_app(m_tctx, get_psum_inr_name(), m_index_types[i - 1], mk_sum(num_inds - i, m_index_types.data() + i), putter);
|
||||
}
|
||||
return Fun(l, putter);
|
||||
}
|
||||
|
|
@ -445,8 +445,8 @@ class add_mutual_inductive_decl_fn {
|
|||
level l1 = get_level(m_tctx, A);
|
||||
level l2 = get_level(m_tctx, stype);
|
||||
stype = Fun(sarg, stype);
|
||||
sigma = mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), A, stype, sarg, sigma);
|
||||
stype = mk_app(m_tctx, get_sigma_name(), {A, stype});
|
||||
sigma = mk_app(mk_constant(get_psigma_mk_name(), {l1, l2}), A, stype, sarg, sigma);
|
||||
stype = mk_app(m_tctx, get_psigma_name(), {A, stype});
|
||||
}
|
||||
return sigma;
|
||||
}
|
||||
|
|
@ -497,7 +497,7 @@ class add_mutual_inductive_decl_fn {
|
|||
minor_premise = Fun({a, b}, rest);
|
||||
}
|
||||
levels lvls = {motive_level, get_level(m_tctx, A), get_level(m_tctx, B)};
|
||||
return mk_app(mk_constant(get_sigma_cases_on_name(), lvls), {A, A_to_B, motive, major_premise, minor_premise});
|
||||
return mk_app(mk_constant(get_psigma_cases_on_name(), lvls), {A, A_to_B, motive, major_premise, minor_premise});
|
||||
}
|
||||
|
||||
expr unpack_sigma_and_apply_C(unsigned ind_idx, expr const & idx, expr const & C) {
|
||||
|
|
@ -551,7 +551,7 @@ class add_mutual_inductive_decl_fn {
|
|||
}
|
||||
level l1 = get_level(m_tctx, A);
|
||||
level l2 = get_level(m_tctx, B);
|
||||
return mk_app(mk_constant(get_sum_cases_on_name(), {motive_level, l1, l2}), {A, B, motive, index, case1, case2});
|
||||
return mk_app(mk_constant(get_psum_cases_on_name(), {motive_level, l1, l2}), {A, B, motive, index, case1, case2});
|
||||
}
|
||||
|
||||
expr construct_inner_C(expr const & C, unsigned ind_idx) {
|
||||
|
|
|
|||
|
|
@ -247,10 +247,16 @@ struct perm_ac_fn : public flat_assoc_fn {
|
|||
return mk_app(m_comm, a, b);
|
||||
}
|
||||
|
||||
level dec_level(level const & l) {
|
||||
if (auto r = ::lean::dec_level(l))
|
||||
return *r;
|
||||
throw_failed();
|
||||
}
|
||||
|
||||
expr mk_left_comm(expr const & a, expr const & b, expr const & c) {
|
||||
if (!m_left_comm) {
|
||||
expr A = m_ctx.infer(a);
|
||||
level lvl = get_level(m_ctx, A);
|
||||
level lvl = dec_level(get_level(m_ctx, A));
|
||||
m_left_comm = mk_app(mk_constant(get_left_comm_name(), {lvl}), A, m_op, m_comm, m_assoc);
|
||||
}
|
||||
return mk_app(*m_left_comm, a, b, c);
|
||||
|
|
|
|||
|
|
@ -1325,6 +1325,12 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part
|
|||
}
|
||||
}
|
||||
|
||||
if (l1.kind() != l2.kind() && (is_succ(l1) || is_succ(l2))) {
|
||||
if (optional<level> pred_l1 = dec_level(l1))
|
||||
if (optional<level> pred_l2 = dec_level(l2))
|
||||
return is_def_eq_core(*pred_l1, *pred_l2, partial);
|
||||
}
|
||||
|
||||
if (partial && (is_max_like(l1) || is_max_like(l2)))
|
||||
return l_undef;
|
||||
|
||||
|
|
@ -2341,7 +2347,7 @@ bool type_context::is_productive(expr const & e) {
|
|||
if (!is_constant(f))
|
||||
return true;
|
||||
name const & n = const_name(f);
|
||||
if (n == get_prod_fst_name()) {
|
||||
if (n == get_pprod_fst_name()) {
|
||||
/* We use prod.fst when compiling recursive equations and brec_on.
|
||||
So, we should check whether the main argument of the projection
|
||||
is productive */
|
||||
|
|
|
|||
|
|
@ -142,8 +142,8 @@ bool has_heq_decls(environment const & env) {
|
|||
return has_constructor(env, get_heq_refl_name(), get_heq_name(), 2);
|
||||
}
|
||||
|
||||
bool has_prod_decls(environment const & env) {
|
||||
return has_constructor(env, get_prod_mk_name(), get_prod_name(), 4);
|
||||
bool has_pprod_decls(environment const & env) {
|
||||
return has_constructor(env, get_pprod_mk_name(), get_pprod_name(), 4);
|
||||
}
|
||||
|
||||
bool has_lift_decls(environment const & env) {
|
||||
|
|
@ -441,32 +441,32 @@ expr mk_unit_mk(level const & l) {
|
|||
return mk_constant(get_poly_unit_star_name(), {l});
|
||||
}
|
||||
|
||||
expr mk_prod(abstract_type_context & ctx, expr const & A, expr const & B) {
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B) {
|
||||
level l1 = get_level(ctx, A);
|
||||
level l2 = get_level(ctx, B);
|
||||
return mk_app(mk_constant(get_prod_name(), {l1, l2}), A, B);
|
||||
return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B);
|
||||
}
|
||||
|
||||
expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b) {
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b) {
|
||||
expr A = ctx.infer(a);
|
||||
expr B = ctx.infer(b);
|
||||
level l1 = get_level(ctx, A);
|
||||
level l2 = get_level(ctx, B);
|
||||
return mk_app(mk_constant(get_prod_mk_name(), {l1, l2}), A, B, a, b);
|
||||
return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
|
||||
}
|
||||
|
||||
expr mk_fst(abstract_type_context & ctx, expr const & p) {
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p) {
|
||||
expr AxB = ctx.whnf(ctx.infer(p));
|
||||
expr const & A = app_arg(app_fn(AxB));
|
||||
expr const & B = app_arg(AxB);
|
||||
return mk_app(mk_constant(get_prod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p);
|
||||
return mk_app(mk_constant(get_pprod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p);
|
||||
}
|
||||
|
||||
expr mk_snd(abstract_type_context & ctx, expr const & p) {
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p) {
|
||||
expr AxB = ctx.whnf(ctx.infer(p));
|
||||
expr const & A = app_arg(app_fn(AxB));
|
||||
expr const & B = app_arg(AxB);
|
||||
return mk_app(mk_constant(get_prod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p);
|
||||
return mk_app(mk_constant(get_pprod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p);
|
||||
}
|
||||
|
||||
static expr * g_nat = nullptr;
|
||||
|
|
@ -478,11 +478,11 @@ static expr * g_nat_add_fn = nullptr;
|
|||
|
||||
static void initialize_nat() {
|
||||
g_nat = new expr(mk_constant(get_nat_name()));
|
||||
g_nat_zero = new expr(mk_app(mk_constant(get_zero_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_zero_name())}));
|
||||
g_nat_one = new expr(mk_app(mk_constant(get_one_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_one_name())}));
|
||||
g_nat_bit0_fn = new expr(mk_app(mk_constant(get_bit0_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_add_name())}));
|
||||
g_nat_bit1_fn = new expr(mk_app(mk_constant(get_bit1_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())}));
|
||||
g_nat_add_fn = new expr(mk_app(mk_constant(get_add_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_add_name())}));
|
||||
g_nat_zero = new expr(mk_app(mk_constant(get_zero_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_zero_name())}));
|
||||
g_nat_one = new expr(mk_app(mk_constant(get_one_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_one_name())}));
|
||||
g_nat_bit0_fn = new expr(mk_app(mk_constant(get_bit0_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_add_name())}));
|
||||
g_nat_bit1_fn = new expr(mk_app(mk_constant(get_bit1_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())}));
|
||||
g_nat_add_fn = new expr(mk_app(mk_constant(get_add_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_add_name())}));
|
||||
}
|
||||
|
||||
static void finalize_nat() {
|
||||
|
|
@ -529,17 +529,18 @@ static void finalize_char() {
|
|||
|
||||
expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); }
|
||||
expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); }
|
||||
expr mk_prod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
|
||||
return prop ? mk_and(a, b) : mk_prod(ctx, a, b);
|
||||
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
|
||||
return prop ? mk_and(a, b) : mk_pprod(ctx, a, b);
|
||||
}
|
||||
expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
|
||||
return prop ? mk_and_intro(ctx, a, b) : mk_pair(ctx, a, b);
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
|
||||
return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b);
|
||||
}
|
||||
expr mk_fst(abstract_type_context & ctx, expr const & p, bool prop) {
|
||||
return prop ? mk_and_elim_left(ctx, p) : mk_fst(ctx, p);
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop) {
|
||||
return prop ? mk_and_elim_left(ctx, p) : mk_pprod_fst(ctx, p);
|
||||
}
|
||||
expr mk_snd(abstract_type_context & ctx, expr const & p, bool prop) {
|
||||
return prop ? mk_and_elim_right(ctx, p) : mk_snd(ctx, p);
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop) {
|
||||
return prop ? mk_and_elim_right(ctx, p) : mk_pprod_snd(ctx, p);
|
||||
}
|
||||
|
||||
bool is_ite(expr const & e) {
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ optional<level> dec_level(level const & l);
|
|||
bool has_poly_unit_decls(environment const & env);
|
||||
bool has_eq_decls(environment const & env);
|
||||
bool has_heq_decls(environment const & env);
|
||||
bool has_prod_decls(environment const & env);
|
||||
bool has_pprod_decls(environment const & env);
|
||||
bool has_lift_decls(environment const & env);
|
||||
|
||||
/** \brief Return true iff \c n is the name of a recursive datatype in \c env.
|
||||
|
|
@ -167,18 +167,18 @@ expr mk_and_elim_right(abstract_type_context & ctx, expr const & H);
|
|||
expr mk_unit(level const & l);
|
||||
expr mk_unit_mk(level const & l);
|
||||
|
||||
expr mk_prod(abstract_type_context & ctx, expr const & A, expr const & B);
|
||||
expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b);
|
||||
expr mk_fst(abstract_type_context & ctx, expr const & p);
|
||||
expr mk_snd(abstract_type_context & ctx, expr const & p);
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B);
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b);
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p);
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p);
|
||||
|
||||
expr mk_unit(level const & l, bool prop);
|
||||
expr mk_unit_mk(level const & l, bool prop);
|
||||
|
||||
expr mk_prod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
||||
expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
||||
expr mk_fst(abstract_type_context & ctx, expr const & p, bool prop);
|
||||
expr mk_snd(abstract_type_context & ctx, expr const & p, bool prop);
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop);
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop);
|
||||
|
||||
expr mk_nat_type();
|
||||
bool is_nat_type(expr const & e);
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
inductive Foo : Type → Type*
|
||||
inductive {u} Foo : Type → Type (u+1)
|
||||
| mk : Π (X : Type), Foo X
|
||||
| wrap : Π (X : Type), Foo X → Foo X
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
open nat
|
||||
|
||||
inductive Vec (X : Type*) : ℕ → Type*
|
||||
inductive {u} Vec (X : Type u) : ℕ → Type u
|
||||
| nil {} : Vec 0
|
||||
| cons : X → Pi {n : nat}, Vec n → Vec (n + 1)
|
||||
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ constant foo {A : Type u} [inhabited A] (a b : A) : a = default A → a = b
|
|||
example (a b : nat) : a = 0 → a = b :=
|
||||
by do
|
||||
intro `H,
|
||||
apply (expr.const `foo [level.of_nat 1]),
|
||||
apply (expr.const `foo [level.of_nat 0]),
|
||||
trace_state,
|
||||
assumption
|
||||
|
||||
|
|
@ -20,7 +20,7 @@ set_option pp.all false
|
|||
example (a b : nat) : a = 0 → a = b :=
|
||||
by do
|
||||
intro `H,
|
||||
apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]),
|
||||
apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 0]),
|
||||
trace_state,
|
||||
a ← get_local `a,
|
||||
trace_state,
|
||||
|
|
@ -45,6 +45,6 @@ by do
|
|||
example (a b : nat) : a = 0 → a = b :=
|
||||
by do
|
||||
`[intro],
|
||||
apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]),
|
||||
apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 0]),
|
||||
`[exact inhabited.mk a],
|
||||
reflexivity
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
inductive vec (A : Type*) : nat → Type*
|
||||
inductive {u} vec (A : Type u) : nat → Type u
|
||||
| nil : vec 0
|
||||
| cons : ∀ {n}, A → vec n → vec (n+1)
|
||||
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ v + 1
|
|||
universe variable u
|
||||
|
||||
instance pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
|
||||
⟨Type (max 1 u), (λ p : A → Prop, subtype p)⟩
|
||||
⟨Type u, (λ p : A → Prop, subtype p)⟩
|
||||
|
||||
instance coesubtype {A : Type u} {p : A → Prop} : has_coe (@coe_sort _ pred2subtype p) A :=
|
||||
⟨λ s, subtype.elt_of s⟩
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
inductive tree (A : Type*)
|
||||
inductive {u} tree (A : Type u) : Type u
|
||||
| leaf : A -> tree
|
||||
| node : list tree -> tree
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
prelude
|
||||
definition Prop : Type.{1} := Type.{0}
|
||||
definition Prop : PType.{1} := PType.{0}
|
||||
constant eq : forall {A : Type}, A → A → Prop
|
||||
constant N : Type.{1}
|
||||
constant N : Type
|
||||
constants a b c : N
|
||||
infix `=`:50 := eq
|
||||
check a = b
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
prelude
|
||||
definition Prop := Type.{0}
|
||||
definition Prop := PType.{0}
|
||||
|
||||
definition false : Prop := ∀x : Prop, x
|
||||
definition false : Prop := ∀ x : Prop, x
|
||||
check false
|
||||
|
||||
theorem false.elim (C : Prop) (H : false) : C
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
set_option pp.binder_types true
|
||||
axiom Sorry {A : Type*} : A
|
||||
axiom Sorry {A : PType*} : A
|
||||
check (Sorry : ∀ a, a > 0)
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
check (λ {A : Type.{1}} (a : A), a) (10:num)
|
||||
check (λ {A : Type} (a : A), a) (10:num)
|
||||
set_option trace.app_builder true
|
||||
check (λ {A} (a : A), a) 10
|
||||
check (λ a, a) (10:num)
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ inductive nat : Type
|
|||
| succ : nat → nat
|
||||
namespace nat end nat open nat
|
||||
|
||||
inductive vector (A : Type*) : nat → Type*
|
||||
inductive {u} vector (A : Type u) : nat → Type u
|
||||
| vnil : vector zero
|
||||
| vcons : Π {n : nat}, A → vector n → vector (succ n)
|
||||
namespace vector end vector open vector
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
namespace list
|
||||
inductive list (A : Type*) : Type*
|
||||
inductive {u} list (A : Type u) : Type u
|
||||
| nil : list
|
||||
| cons : A → list → list
|
||||
|
||||
|
|
|
|||
|
|
@ -66,6 +66,6 @@ begin
|
|||
{intros, unfold size, apply nat.zero_lt_succ }
|
||||
end
|
||||
|
||||
inductive tree_list (α : Type u)
|
||||
inductive tree_list (α : Type u) : Type u
|
||||
| leaf : tree_list
|
||||
| node : list tree_list → α → tree_list
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
open tactic
|
||||
axiom Sorry : ∀ {A:Type*}, A
|
||||
axiom Sorry : ∀ {A:PType*}, A
|
||||
|
||||
example (a b c : nat) (h₀ : c > 0) (h₁ : a > 1) (h₂ : b > 0) : a + b + c = 0 :=
|
||||
by do
|
||||
|
|
|
|||
|
|
@ -1,34 +1,34 @@
|
|||
set_option trace.inductive_compiler.nested.define.failure true
|
||||
set_option max_memory 1000000
|
||||
|
||||
inductive vec (A : Type*) : nat -> Type*
|
||||
inductive {u} vec (A : Type u) : nat -> Type u
|
||||
| vnil : vec 0
|
||||
| vcons : Pi (n : nat), A -> vec n -> vec (n+1)
|
||||
|
||||
namespace X1
|
||||
print "simple"
|
||||
inductive foo
|
||||
inductive foo : Type
|
||||
| mk : list foo -> foo
|
||||
|
||||
end X1
|
||||
|
||||
namespace X2
|
||||
print "with param"
|
||||
inductive foo (A : Type*)
|
||||
inductive {u} foo (A : Type u) : Type u
|
||||
| mk : A -> list foo -> foo
|
||||
|
||||
end X2
|
||||
|
||||
namespace X3
|
||||
print "with indices"
|
||||
inductive foo (A B : Type*)
|
||||
inductive {u} foo (A B : Type u) : Type u
|
||||
| mk : A -> B -> vec foo 0 -> foo
|
||||
|
||||
end X3
|
||||
|
||||
namespace X4
|
||||
print "with locals in indices"
|
||||
inductive foo (A : Type*)
|
||||
inductive {u} foo (A : Type u) : Type u
|
||||
| mk : Pi (n : nat), A -> vec foo n -> foo
|
||||
|
||||
end X4
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
open classical sum
|
||||
|
||||
noncomputable example (A : Type _) (h : (A → false) → false) : A :=
|
||||
universe variable u
|
||||
noncomputable example (A : Type u) (h : (A → empty) → false) : A :=
|
||||
match type_decidable A with
|
||||
| (inl ha) := ha
|
||||
| (inr hna) := false.rec _ (h hna)
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
open nat
|
||||
|
||||
inductive vec (α : Type*) : ℕ → Type*
|
||||
inductive {u} vec (α : Type u) : ℕ → Type u
|
||||
| nil {} : vec 0
|
||||
| cons : α → Π {n : nat}, vec n → vec (n+1)
|
||||
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ universe variables u
|
|||
|
||||
attribute [instance]
|
||||
definition pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
|
||||
⟨Type (max 1 u), λ p : A → Prop, subtype p⟩
|
||||
⟨Type u, λ p : A → Prop, subtype p⟩
|
||||
|
||||
definition below (n : nat) : nat → Prop :=
|
||||
λ i, i < n
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
constant fibrant : Type* → Prop
|
||||
constant {u} fibrant : Type u → Prop
|
||||
|
||||
structure Fib : Type* :=
|
||||
{type : Type*} (pred : fibrant type)
|
||||
structure {u} Fib : Type (u+1) :=
|
||||
{type : Type u} (pred : fibrant type)
|
||||
|
||||
check Fib.mk
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
prelude
|
||||
definition Prop : Type.{1} := Type.{0}
|
||||
definition Prop : PType.{1} := PType.{0}
|
||||
section
|
||||
parameter A : Type*
|
||||
parameter A : PType*
|
||||
|
||||
definition Eq (a b : A) : Prop
|
||||
:= ∀P : A → Prop, P a → P b
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
prelude
|
||||
definition bool : Type.{1} := Type.{0}
|
||||
definition bool : PType 1 := PType 0
|
||||
definition and (p q : bool) : bool
|
||||
:= ∀ c : bool, (p → q → c) → c
|
||||
infixl `∧`:25 := and
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue