chore: remove obsolete attribute
This commit is contained in:
Leonardo de Moura
parent
072fb93cc2
commit
dfc346e76f
4 changed files with 59 additions and 120 deletions
|
|
@ -92,12 +92,10 @@ def Not (a : Prop) : Prop := a → False
|
|||
inductive Eq {α : Sort u} (a : α) : α → Prop
|
||||
| refl {} : Eq a a
|
||||
|
||||
@[elabAsEliminator, inline, reducible]
|
||||
def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
|
||||
abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
|
||||
Eq.rec (motive := fun α _ => motive α) m h
|
||||
|
||||
@[elabAsEliminator, inline, reducible]
|
||||
def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b :=
|
||||
abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b :=
|
||||
Eq.ndrec m h
|
||||
|
||||
/-
|
||||
|
|
@ -142,7 +140,6 @@ structure Iff (a b : Prop) : Prop :=
|
|||
|
||||
@[matchPattern] def rfl {α : Sort u} {a : α} : a = a := Eq.refl a
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
|
||||
Eq.ndrec h₂ h₁
|
||||
|
||||
|
|
@ -456,7 +453,7 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf
|
|||
|
||||
/-- Like `by applyInstance`, but not dependent on the tactic framework. -/
|
||||
@[reducible] def inferInstance {α : Type u} [i : α] : α := i
|
||||
@[reducible, elabSimple] def inferInstanceAs (α : Type u) [i : α] : α := i
|
||||
@[reducible] def inferInstanceAs (α : Type u) [i : α] : α := i
|
||||
|
||||
/- Boolean operators -/
|
||||
|
||||
|
|
@ -520,7 +517,6 @@ theorem id.def {α : Sort u} (a : α) : id a = a := rfl
|
|||
@[macroInline] def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α :=
|
||||
h ▸ b
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
|
||||
h₁ ▸ h₂
|
||||
|
||||
|
|
@ -601,11 +597,9 @@ theorem neTrueOfEqFalse : ∀ {b : Bool}, b = false → b ≠ true
|
|||
section
|
||||
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
|
||||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b :=
|
||||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||||
|
||||
|
|
@ -1130,14 +1124,12 @@ inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
|
|||
| base : ∀ a b, r a b → TC r a b
|
||||
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||||
(m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
|
||||
{a b : α} (h : TC r a b) : C a b :=
|
||||
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||||
{a b : α} (h : TC r a b)
|
||||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||||
|
|
@ -1341,8 +1333,6 @@ theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a)
|
|||
namespace Quot
|
||||
axiom sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
|
||||
|
||||
attribute [elabAsEliminator] lift ind
|
||||
|
||||
protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v}
|
||||
(f : α → β)
|
||||
(c : (a b : α) → r a b → f a = f b)
|
||||
|
|
@ -1356,11 +1346,9 @@ protected theorem indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot
|
|||
: (ind p (Quot.mk r a) : motive (Quot.mk r a)) = p a :=
|
||||
rfl
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : (a b : α) → r a b → f a = f b) : β :=
|
||||
protected abbrev liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : (a b : α) → r a b → f a = f b) : β :=
|
||||
lift f c q
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop}
|
||||
(q : Quot r)
|
||||
(h : (a : α) → motive (Quot.mk r a))
|
||||
|
|
@ -1393,23 +1381,20 @@ protected theorem liftIndepPr1
|
|||
induction q using Quot.ind
|
||||
exact rfl
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def rec
|
||||
protected abbrev rec
|
||||
(f : (a : α) → motive (Quot.mk r a))
|
||||
(h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
|
||||
(q : Quot r) : motive q :=
|
||||
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOn
|
||||
protected abbrev recOn
|
||||
(q : Quot r)
|
||||
(f : (a : α) → motive (Quot.mk r a))
|
||||
(h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
|
||||
: motive q :=
|
||||
Quot.rec f h q
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOnSubsingleton
|
||||
protected abbrev recOnSubsingleton
|
||||
[h : (a : α) → Subsingleton (motive (Quot.mk r a))]
|
||||
(q : Quot r)
|
||||
(f : (a : α) → motive (Quot.mk r a))
|
||||
|
|
@ -1418,8 +1403,7 @@ protected def recOnSubsingleton
|
|||
apply f
|
||||
apply Subsingleton.elim
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def hrecOn
|
||||
protected abbrev hrecOn
|
||||
(q : Quot r)
|
||||
(f : (a : α) → motive (Quot.mk r a))
|
||||
(c : (a b : α) → (p : r a b) → f a ≅ f b)
|
||||
|
|
@ -1443,19 +1427,15 @@ protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
|
|||
def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → Quotient.mk a = Quotient.mk b :=
|
||||
Quot.sound
|
||||
|
||||
@[reducible, elabAsEliminator]
|
||||
protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
|
||||
protected abbrev lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
|
||||
Quot.lift f
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem ind {α : Sort u} [s : Setoid α] {motive : Quotient s → Prop} : ((a : α) → motive (Quotient.mk a)) → (q : Quot Setoid.r) → motive q :=
|
||||
Quot.ind
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β :=
|
||||
protected abbrev liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β :=
|
||||
Quot.liftOn q f c
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn {α : Sort u} [s : Setoid α] {motive : Quotient s → Prop}
|
||||
(q : Quotient s)
|
||||
(h : (a : α) → motive (Quotient.mk a))
|
||||
|
|
@ -1478,24 +1458,21 @@ protected def rec
|
|||
: motive q :=
|
||||
Quot.rec f h q
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOn
|
||||
protected abbrev recOn
|
||||
(q : Quotient s)
|
||||
(f : (a : α) → motive (Quotient.mk a))
|
||||
(h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b)
|
||||
: motive q :=
|
||||
Quot.recOn q f h
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOnSubsingleton
|
||||
protected abbrev recOnSubsingleton
|
||||
[h : (a : α) → Subsingleton (motive (Quotient.mk a))]
|
||||
(q : Quotient s)
|
||||
(f : (a : α) → motive (Quotient.mk a))
|
||||
: motive q :=
|
||||
Quot.recOnSubsingleton (h := h) q f
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def hrecOn
|
||||
protected abbrev hrecOn
|
||||
(q : Quotient s)
|
||||
(f : (a : α) → motive (Quotient.mk a))
|
||||
(c : (a b : α) → (p : a ≈ b) → f a ≅ f b)
|
||||
|
|
@ -1508,8 +1485,7 @@ universes uA uB uC
|
|||
variables {α : Sort uA} {β : Sort uB} {φ : Sort uC}
|
||||
variables [s₁ : Setoid α] [s₂ : Setoid β]
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def lift₂
|
||||
protected abbrev lift₂
|
||||
(f : α → β → φ)
|
||||
(c : (a₁ : α) → (b₁ : β) → (a₂ : α) → (b₂ : β) → a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
|
||||
(q₁ : Quotient s₁) (q₂ : Quotient s₂)
|
||||
|
|
@ -1519,8 +1495,7 @@ protected def lift₂
|
|||
induction q₂ using Quotient.ind
|
||||
apply c; assumption; apply Setoid.refl
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def liftOn₂
|
||||
protected abbrev liftOn₂
|
||||
(q₁ : Quotient s₁)
|
||||
(q₂ : Quotient s₂)
|
||||
(f : α → β → φ)
|
||||
|
|
@ -1528,7 +1503,6 @@ protected def liftOn₂
|
|||
: φ :=
|
||||
Quotient.lift₂ f c q₁ q₂
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem ind₂
|
||||
{motive : Quotient s₁ → Quotient s₂ → Prop}
|
||||
(h : (a : α) → (b : β) → motive (Quotient.mk a) (Quotient.mk b))
|
||||
|
|
@ -1539,7 +1513,6 @@ protected theorem ind₂
|
|||
induction q₂ using Quotient.ind
|
||||
apply h
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn₂
|
||||
{motive : Quotient s₁ → Quotient s₂ → Prop}
|
||||
(q₁ : Quotient s₁)
|
||||
|
|
@ -1550,7 +1523,6 @@ protected theorem inductionOn₂
|
|||
induction q₂ using Quotient.ind
|
||||
apply h
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn₃
|
||||
[s₃ : Setoid φ]
|
||||
{motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop}
|
||||
|
|
@ -1594,8 +1566,7 @@ universes uA uB uC
|
|||
variables {α : Sort uA} {β : Sort uB}
|
||||
variables [s₁ : Setoid α] [s₂ : Setoid β]
|
||||
|
||||
@[reducible, elabAsEliminator]
|
||||
protected def recOnSubsingleton₂
|
||||
protected abbrev recOnSubsingleton₂
|
||||
{motive : Quotient s₁ → Quotient s₂ → Sort uC}
|
||||
[s : (a : α) → (b : β) → Subsingleton (motive (Quotient.mk a) (Quotient.mk b))]
|
||||
(q₁ : Quotient s₁)
|
||||
|
|
|
|||
|
|
@ -33,7 +33,6 @@ private theorem div.induction.F.{u}
|
|||
(x : Nat) (f : ∀ (x₁ : Nat), x₁ < x → ∀ (y : Nat), C x₁ y) (y : Nat) : C x y :=
|
||||
if h : 0 < y ∧ y ≤ x then h₁ x y h (f (x - y) (divRecLemma h) y) else h₂ x y h
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem div.inductionOn.{u}
|
||||
{motive : Nat → Nat → Sort u}
|
||||
(x y : Nat)
|
||||
|
|
@ -57,7 +56,6 @@ private theorem modDefAux (x y : Nat) : x % y = if h : 0 < y ∧ y ≤ x then (x
|
|||
theorem modDef (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
|
||||
difEqIf (0 < y ∧ y ≤ x) ((x - y) % y) x ▸ modDefAux x y
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem mod.inductionOn.{u}
|
||||
{motive : Nat → Nat → Sort u}
|
||||
(x y : Nat)
|
||||
|
|
|
|||
|
|
@ -13,14 +13,12 @@ set_option codegen false
|
|||
inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop
|
||||
| intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x
|
||||
|
||||
@[elabAsEliminator, inline, reducible]
|
||||
def Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
|
||||
abbrev Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
|
||||
(m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
|
||||
{a : α} (n : Acc r a) : C a :=
|
||||
Acc.rec (motive := fun α _ => C α) m n
|
||||
|
||||
@[elabAsEliminator, inline, reducible]
|
||||
def Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
|
||||
abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
|
||||
{a : α} (n : Acc r a)
|
||||
(m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
|
||||
: C a :=
|
||||
|
|
|
|||
|
|
@ -89,14 +89,13 @@ def Not (a : Prop) : Prop :=
|
|||
a → False
|
||||
|
||||
inductive Eq {α : Sort u} (a : α) : α → Prop
|
||||
| refl{} : Eq a a
|
||||
| refl{} : Eq a a
|
||||
|
||||
@[elabAsEliminator, inline, reducible]
|
||||
def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
|
||||
Eq.rec (motive := fun α _ => motive α) m h
|
||||
abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
|
||||
Eq.rec (motive := fun α _ => motive α) m h
|
||||
|
||||
@[elabAsEliminator, inline, reducible]
|
||||
def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b :=
|
||||
abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) :
|
||||
motive b :=
|
||||
Eq.ndrec m h
|
||||
|
||||
init_quot
|
||||
|
|
@ -131,9 +130,8 @@ structure Iff(a b : Prop) : Prop := intro ::
|
|||
|
||||
@[matchPattern]
|
||||
def rfl {α : Sort u} {a : α} : a = a :=
|
||||
Eq.refl a
|
||||
Eq.refl a
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
|
||||
Eq.ndrec h₂ h₁
|
||||
|
||||
|
|
@ -465,7 +463,7 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α :=
|
|||
def inferInstance {α : Type u} [i : α] : α :=
|
||||
i
|
||||
|
||||
@[reducible, elabSimple]
|
||||
@[reducible]
|
||||
def inferInstanceAs (α : Type u) [i : α] : α :=
|
||||
i
|
||||
|
||||
|
|
@ -545,9 +543,8 @@ def Eq.mp {α β : Sort u} (h : α = β) (a : α) : β :=
|
|||
|
||||
@[macroInline]
|
||||
def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α :=
|
||||
h ▸ b
|
||||
h ▸ b
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
|
||||
h₁ ▸ h₂
|
||||
|
||||
|
|
@ -636,12 +633,10 @@ section
|
|||
|
||||
variables{α β φ : Sort u}{a a' : α}{b b' : β}{c : φ}
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2}
|
||||
{b : β} (h : a ≅ b) : motive b :=
|
||||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β}
|
||||
(h : a ≅ b) (m : motive a) : motive b :=
|
||||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||||
|
|
@ -1143,14 +1138,12 @@ theorem InvImage.Irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (
|
|||
|
||||
inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
|
||||
| base : ∀ a b, r a b → TC r a b
|
||||
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
|
||||
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} (m₁ : ∀ (a b : α), r a b → C a b)
|
||||
(m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c) {a b : α} (h : TC r a b) : C a b :=
|
||||
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h
|
||||
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h
|
||||
|
||||
@[elabAsEliminator]
|
||||
theorem TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} {a b : α} (h : TC r a b)
|
||||
(m₁ : ∀ (a b : α), r a b → C a b) (m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c) : C a b :=
|
||||
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h
|
||||
|
|
@ -1339,22 +1332,18 @@ namespace Quot
|
|||
|
||||
axiom sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
|
||||
|
||||
attribute [elabAsEliminator] lift ind
|
||||
|
||||
protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : (a b : α) → r a b → f a = f b)
|
||||
(a : α) : lift f c (Quot.mk r a) = f a :=
|
||||
rfl
|
||||
|
||||
protected theorem indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (p : (a : α) → motive (Quot.mk r a))
|
||||
(a : α) : (ind p (Quot.mk r a) : motive (Quot.mk r a)) = p a :=
|
||||
rfl
|
||||
rfl
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β)
|
||||
protected abbrev liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β)
|
||||
(c : (a b : α) → r a b → f a = f b) : β :=
|
||||
lift f c q
|
||||
lift f c q
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r)
|
||||
(h : (a : α) → motive (Quot.mk r a)) : motive q :=
|
||||
ind h q
|
||||
|
|
@ -1384,28 +1373,24 @@ protected theorem liftIndepPr1 (f : (a : α) → motive (Quot.mk r a))
|
|||
(lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q :=
|
||||
by
|
||||
induction q using Quot.ind
|
||||
exact rfl
|
||||
exact rfl
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def rec (f : (a : α) → motive (Quot.mk r a)) (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
|
||||
protected abbrev rec (f : (a : α) → motive (Quot.mk r a)) (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
|
||||
(q : Quot r) : motive q :=
|
||||
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOn (q : Quot r) (f : (a : α) → motive (Quot.mk r a))
|
||||
protected abbrev recOn (q : Quot r) (f : (a : α) → motive (Quot.mk r a))
|
||||
(h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b) : motive q :=
|
||||
Quot.rec f h q
|
||||
Quot.rec f h q
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOnSubsingleton [h : (a : α) → Subsingleton (motive (Quot.mk r a))] (q : Quot r)
|
||||
protected abbrev recOnSubsingleton [h : (a : α) → Subsingleton (motive (Quot.mk r a))] (q : Quot r)
|
||||
(f : (a : α) → motive (Quot.mk r a)) : motive q :=
|
||||
by
|
||||
induction q using Quot.rec
|
||||
apply f
|
||||
apply Subsingleton.elim
|
||||
apply Subsingleton.elim
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def hrecOn (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (c : (a b : α) → (p : r a b) → f a ≅ f b) :
|
||||
protected abbrev hrecOn (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (c : (a b : α) → (p : r a b) → f a ≅ f b) :
|
||||
motive q :=
|
||||
Quot.recOn q f
|
||||
fun a b p =>
|
||||
|
|
@ -1427,24 +1412,20 @@ protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
|
|||
Quot.mk Setoid.r a
|
||||
|
||||
def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → Quotient.mk a = Quotient.mk b :=
|
||||
Quot.sound
|
||||
Quot.sound
|
||||
|
||||
@[reducible, elabAsEliminator]
|
||||
protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) :
|
||||
protected abbrev lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) :
|
||||
((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
|
||||
Quot.lift f
|
||||
Quot.lift f
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem ind {α : Sort u} [s : Setoid α] {motive : Quotient s → Prop} :
|
||||
((a : α) → motive (Quotient.mk a)) → (q : Quot Setoid.r) → motive q :=
|
||||
Quot.ind
|
||||
Quot.ind
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β)
|
||||
protected abbrev liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β)
|
||||
(c : (a b : α) → a ≈ b → f a = f b) : β :=
|
||||
Quot.liftOn q f c
|
||||
Quot.liftOn q f c
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn {α : Sort u} [s : Setoid α] {motive : Quotient s → Prop} (q : Quotient s)
|
||||
(h : (a : α) → motive (Quotient.mk a)) : motive q :=
|
||||
Quot.inductionOn q h
|
||||
|
|
@ -1463,21 +1444,18 @@ variable{motive : Quotient s → Sort v}
|
|||
@[inline]
|
||||
protected def rec (f : (a : α) → motive (Quotient.mk a))
|
||||
(h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b) (q : Quotient s) : motive q :=
|
||||
Quot.rec f h q
|
||||
Quot.rec f h q
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOn (q : Quotient s) (f : (a : α) → motive (Quotient.mk a))
|
||||
protected abbrev recOn (q : Quotient s) (f : (a : α) → motive (Quotient.mk a))
|
||||
(h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b) : motive q :=
|
||||
Quot.recOn q f h
|
||||
Quot.recOn q f h
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def recOnSubsingleton [h : (a : α) → Subsingleton (motive (Quotient.mk a))] (q : Quotient s)
|
||||
protected abbrev recOnSubsingleton [h : (a : α) → Subsingleton (motive (Quotient.mk a))] (q : Quotient s)
|
||||
(f : (a : α) → motive (Quotient.mk a)) : motive q :=
|
||||
Quot.recOnSubsingleton (h := h) q f
|
||||
Quot.recOnSubsingleton (h := h) q f
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def hrecOn (q : Quotient s) (f : (a : α) → motive (Quotient.mk a)) (c : (a b : α) → (p : a ≈ b) → f a ≅ f b) :
|
||||
motive q :=
|
||||
protected abbrev hrecOn (q : Quotient s) (f : (a : α) → motive (Quotient.mk a))
|
||||
(c : (a b : α) → (p : a ≈ b) → f a ≅ f b) : motive q :=
|
||||
Quot.hrecOn q f c
|
||||
|
||||
end
|
||||
|
|
@ -1490,8 +1468,7 @@ variables{α : Sort uA}{β : Sort uB}{φ : Sort uC}
|
|||
|
||||
variables[s₁ : Setoid α][s₂ : Setoid β]
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def lift₂ (f : α → β → φ)
|
||||
protected abbrev lift₂ (f : α → β → φ)
|
||||
(c : (a₁ : α) → (b₁ : β) → (a₂ : α) → (b₂ : β) → a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) (q₁ : Quotient s₁)
|
||||
(q₂ : Quotient s₂) : φ :=
|
||||
by
|
||||
|
|
@ -1500,31 +1477,27 @@ protected def lift₂ (f : α → β → φ)
|
|||
induction q₂ using Quotient.ind
|
||||
apply c;
|
||||
assumption;
|
||||
apply Setoid.refl
|
||||
apply Setoid.refl
|
||||
|
||||
@[reducible, elabAsEliminator, inline]
|
||||
protected def liftOn₂ (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ)
|
||||
protected abbrev liftOn₂ (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ)
|
||||
(c : (a₁ : α) → (b₁ : β) → (a₂ : α) → (b₂ : β) → a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) : φ :=
|
||||
Quotient.lift₂ f c q₁ q₂
|
||||
Quotient.lift₂ f c q₁ q₂
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem ind₂ {motive : Quotient s₁ → Quotient s₂ → Prop}
|
||||
(h : (a : α) → (b : β) → motive (Quotient.mk a) (Quotient.mk b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
|
||||
motive q₁ q₂ :=
|
||||
by
|
||||
induction q₁ using Quotient.ind
|
||||
induction q₂ using Quotient.ind
|
||||
apply h
|
||||
apply h
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn₂ {motive : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂)
|
||||
(h : (a : α) → (b : β) → motive (Quotient.mk a) (Quotient.mk b)) : motive q₁ q₂ :=
|
||||
by
|
||||
induction q₁ using Quotient.ind
|
||||
induction q₂ using Quotient.ind
|
||||
apply h
|
||||
apply h
|
||||
|
||||
@[elabAsEliminator]
|
||||
protected theorem inductionOn₃ [s₃ : Setoid φ] {motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop}
|
||||
(q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃)
|
||||
(h : (a : α) → (b : β) → (c : φ) → motive (Quotient.mk a) (Quotient.mk b) (Quotient.mk c)) : motive q₁ q₂ q₃ :=
|
||||
|
|
@ -1566,8 +1539,7 @@ variables{α : Sort uA}{β : Sort uB}
|
|||
|
||||
variables[s₁ : Setoid α][s₂ : Setoid β]
|
||||
|
||||
@[reducible, elabAsEliminator]
|
||||
protected def recOnSubsingleton₂ {motive : Quotient s₁ → Quotient s₂ → Sort uC}
|
||||
protected abbrev recOnSubsingleton₂ {motive : Quotient s₁ → Quotient s₂ → Sort uC}
|
||||
[s : (a : α) → (b : β) → Subsingleton (motive (Quotient.mk a) (Quotient.mk b))] (q₁ : Quotient s₁) (q₂ : Quotient s₂)
|
||||
(g : (a : α) → (b : β) → motive (Quotient.mk a) (Quotient.mk b)) : motive q₁ q₂ :=
|
||||
by
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue