chore: simplify Prelude.lean and Core.lean using elabAsElim
This commit is contained in:
Leonardo de Moura
parent
485406cc55
commit
eafd2a88ce
5 changed files with 43 additions and 31 deletions
|
|
@ -292,10 +292,10 @@ section
|
|||
variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
|
||||
|
||||
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
|
||||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||||
h.rec m
|
||||
|
||||
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
|
||||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||||
h.rec m
|
||||
|
||||
theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
|
||||
eq_of_heq h₁ ▸ h₂
|
||||
|
|
@ -304,7 +304,7 @@ theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p
|
|||
HEq.ndrecOn h₁ h₂
|
||||
|
||||
theorem HEq.symm (h : HEq a b) : HEq b a :=
|
||||
HEq.ndrecOn (motive := fun x => HEq x a) h (HEq.refl a)
|
||||
h.rec (HEq.refl a)
|
||||
|
||||
theorem heq_of_eq (h : a = a') : HEq a a' :=
|
||||
Eq.subst h (HEq.refl a)
|
||||
|
|
@ -319,7 +319,7 @@ theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : HEq a' b) : HEq a b :=
|
|||
HEq.trans (heq_of_eq h₁) h₂
|
||||
|
||||
def type_eq_of_heq (h : HEq a b) : α = β :=
|
||||
HEq.ndrecOn (motive := @fun (x : Sort u) _ => α = x) h (Eq.refl α)
|
||||
h.rec (Eq.refl α)
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -497,7 +497,7 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
|
|||
|
||||
/-- Auxiliary definitions for generating compact `noConfusion` for enumeration types -/
|
||||
abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
|
||||
Decidable.casesOn (motive := fun _ => Sort w) (inst (f x) (f y))
|
||||
(inst (f x) (f y)).casesOn
|
||||
(fun _ => P)
|
||||
(fun _ => P → P)
|
||||
|
||||
|
|
@ -549,7 +549,7 @@ theorem recSubsingleton
|
|||
{h₂ : ¬p → Sort u}
|
||||
[h₃ : ∀ (h : p), Subsingleton (h₁ h)]
|
||||
[h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)]
|
||||
: Subsingleton (Decidable.casesOn (motive := fun _ => Sort u) h h₂ h₁) :=
|
||||
: Subsingleton (h.casesOn h₂ h₁) :=
|
||||
match h with
|
||||
| isTrue h => h₃ h
|
||||
| isFalse h => h₄ h
|
||||
|
|
@ -767,6 +767,7 @@ protected theorem indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot
|
|||
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
|
||||
|
||||
@[elabAsElim]
|
||||
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop}
|
||||
(q : Quot r)
|
||||
(h : (a : α) → motive (Quot.mk r a))
|
||||
|
|
@ -774,7 +775,7 @@ protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Q
|
|||
ind h q
|
||||
|
||||
theorem exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (fun a => (Quot.mk r a) = q) :=
|
||||
Quot.inductionOn (motive := fun q => Exists (fun a => (Quot.mk r a) = q)) q (fun a => ⟨a, rfl⟩)
|
||||
q.inductionOn (fun a => ⟨a, rfl⟩)
|
||||
|
||||
section
|
||||
variable {α : Sort u}
|
||||
|
|
@ -810,7 +811,7 @@ protected abbrev recOn
|
|||
(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
|
||||
q.rec f h
|
||||
|
||||
protected abbrev recOnSubsingleton
|
||||
[h : (a : α) → Subsingleton (motive (Quot.mk r a))]
|
||||
|
|
@ -858,6 +859,7 @@ protected theorem ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Pro
|
|||
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
|
||||
|
||||
@[elabAsElim]
|
||||
protected theorem inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop}
|
||||
(q : Quotient s)
|
||||
(h : (a : α) → motive (Quotient.mk s a))
|
||||
|
|
@ -872,7 +874,7 @@ variable {α : Sort u}
|
|||
variable {s : Setoid α}
|
||||
variable {motive : Quotient s → Sort v}
|
||||
|
||||
@[inline]
|
||||
@[inline, elabAsElim]
|
||||
protected def rec
|
||||
(f : (a : α) → motive (Quotient.mk s a))
|
||||
(h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b)
|
||||
|
|
@ -880,6 +882,7 @@ protected def rec
|
|||
: motive q :=
|
||||
Quot.rec f h q
|
||||
|
||||
@[elabAsElim]
|
||||
protected abbrev recOn
|
||||
(q : Quotient s)
|
||||
(f : (a : α) → motive (Quotient.mk s a))
|
||||
|
|
@ -887,6 +890,7 @@ protected abbrev recOn
|
|||
: motive q :=
|
||||
Quot.recOn q f h
|
||||
|
||||
@[elabAsElim]
|
||||
protected abbrev recOnSubsingleton
|
||||
[h : (a : α) → Subsingleton (motive (Quotient.mk s a))]
|
||||
(q : Quotient s)
|
||||
|
|
@ -894,6 +898,7 @@ protected abbrev recOnSubsingleton
|
|||
: motive q :=
|
||||
Quot.recOnSubsingleton (h := h) q f
|
||||
|
||||
@[elabAsElim]
|
||||
protected abbrev hrecOn
|
||||
(q : Quotient s)
|
||||
(f : (a : α) → motive (Quotient.mk s a))
|
||||
|
|
@ -925,6 +930,7 @@ protected abbrev liftOn₂
|
|||
: φ :=
|
||||
Quotient.lift₂ f c q₁ q₂
|
||||
|
||||
@[elabAsElim]
|
||||
protected theorem ind₂
|
||||
{motive : Quotient s₁ → Quotient s₂ → Prop}
|
||||
(h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))
|
||||
|
|
@ -935,6 +941,7 @@ protected theorem ind₂
|
|||
induction q₂ using Quotient.ind
|
||||
apply h
|
||||
|
||||
@[elabAsElim]
|
||||
protected theorem inductionOn₂
|
||||
{motive : Quotient s₁ → Quotient s₂ → Prop}
|
||||
(q₁ : Quotient s₁)
|
||||
|
|
@ -945,6 +952,7 @@ protected theorem inductionOn₂
|
|||
induction q₂ using Quotient.ind
|
||||
apply h
|
||||
|
||||
@[elabAsElim]
|
||||
protected theorem inductionOn₃
|
||||
{s₃ : Setoid φ}
|
||||
{motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop}
|
||||
|
|
@ -973,7 +981,7 @@ private def rel {s : Setoid α} (q₁ q₂ : Quotient s) : Prop :=
|
|||
(fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
|
||||
|
||||
private theorem rel.refl {s : Setoid α} (q : Quotient s) : rel q q :=
|
||||
Quot.inductionOn (motive := fun q => rel q q) q (fun a => Setoid.refl a)
|
||||
q.inductionOn Setoid.refl
|
||||
|
||||
private theorem rel_of_eq {s : Setoid α} {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
|
||||
fun h => Eq.ndrecOn h (rel.refl q₁)
|
||||
|
|
@ -988,6 +996,7 @@ universe uA uB uC
|
|||
variable {α : Sort uA} {β : Sort uB}
|
||||
variable {s₁ : Setoid α} {s₂ : Setoid β}
|
||||
|
||||
@[elabAsElim]
|
||||
protected abbrev recOnSubsingleton₂
|
||||
{motive : Quotient s₁ → Quotient s₂ → Sort uC}
|
||||
[s : (a : α) → (b : β) → Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))]
|
||||
|
|
@ -1012,7 +1021,7 @@ variable (r : α → α → Prop)
|
|||
|
||||
instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
|
||||
fun (q₁ q₂ : Quotient s) =>
|
||||
Quotient.recOnSubsingleton₂ (motive := fun a b => Decidable (a = b)) q₁ q₂
|
||||
Quotient.recOnSubsingleton₂ q₁ q₂
|
||||
fun a₁ a₂ =>
|
||||
match d a₁ a₂ with
|
||||
| isTrue h₁ => isTrue (Quotient.sound h₁)
|
||||
|
|
|
|||
|
|
@ -74,9 +74,9 @@ namespace Iterator
|
|||
else find it.next p
|
||||
|
||||
@[specialize] def foldUntil (it : Iterator) (init : α) (f : α → Char → Option α) : α × Iterator :=
|
||||
if it.atEnd then
|
||||
if it.atEnd then
|
||||
(init, it)
|
||||
else if let some a := f init it.curr then
|
||||
else if let some a := f init it.curr then
|
||||
foldUntil it.next a f
|
||||
else
|
||||
(init, it)
|
||||
|
|
|
|||
|
|
@ -50,16 +50,16 @@ inductive PEmpty : Sort u where
|
|||
def Not (a : Prop) : Prop := a → False
|
||||
|
||||
@[macroInline] def False.elim {C : Sort u} (h : False) : C :=
|
||||
@False.rec (fun _ => C) h
|
||||
h.rec
|
||||
|
||||
@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=
|
||||
False.elim (h₂ h₁)
|
||||
(h₂ h₁).rec
|
||||
|
||||
inductive Eq : α → α → Prop where
|
||||
| refl (a : α) : Eq a a
|
||||
|
||||
@[simp] 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
|
||||
h.rec m
|
||||
|
||||
@[matchPattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
|
||||
|
||||
|
|
@ -75,7 +75,7 @@ theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq
|
|||
h₂ ▸ h₁
|
||||
|
||||
@[macroInline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
|
||||
Eq.rec (motive := fun α _ => α) a h
|
||||
h.rec a
|
||||
|
||||
theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
|
||||
h ▸ rfl
|
||||
|
|
@ -142,7 +142,6 @@ In fact, the computation principle is declared as a reduction rule.
|
|||
-/
|
||||
add_decl_doc Quot.lift
|
||||
|
||||
|
||||
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
|
||||
| refl (a : α) : HEq a a
|
||||
|
||||
|
|
@ -151,10 +150,8 @@ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
|
|||
|
||||
theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
|
||||
have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
|
||||
fun α _ a _ h₁ =>
|
||||
HEq.rec (motive := fun {β} (b : β) (_ : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
|
||||
(fun (_ : Eq α α) => rfl)
|
||||
h₁
|
||||
fun _ _ _ _ h₁ =>
|
||||
h₁.rec (fun _ => rfl)
|
||||
this α α a a' h rfl
|
||||
|
||||
structure Prod (α : Type u) (β : Type v) where
|
||||
|
|
@ -310,7 +307,7 @@ class inductive Decidable (p : Prop) where
|
|||
| isTrue (h : p) : Decidable p
|
||||
|
||||
@[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
|
||||
Decidable.casesOn (motive := fun _ => Bool) h (fun _ => false) (fun _ => true)
|
||||
h.casesOn (fun _ => false) (fun _ => true)
|
||||
|
||||
export Decidable (isTrue isFalse decide)
|
||||
|
||||
|
|
@ -369,12 +366,12 @@ instance [DecidableEq α] : BEq α where
|
|||
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
|
||||
-- to the branches
|
||||
@[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
|
||||
Decidable.casesOn (motive := fun _ => α) h e t
|
||||
h.casesOn e t
|
||||
|
||||
/-! # if-then-else -/
|
||||
|
||||
@[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
|
||||
Decidable.casesOn (motive := fun _ => α) h (fun _ => e) (fun _ => t)
|
||||
h.casesOn (fun _ => e) (fun _ => t)
|
||||
|
||||
@[macroInline] instance {p q} [dp : Decidable p] [dq : Decidable q] : Decidable (And p q) :=
|
||||
match dp with
|
||||
|
|
|
|||
|
|
@ -15,20 +15,19 @@ inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
|
|||
noncomputable 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
|
||||
n.rec m
|
||||
|
||||
noncomputable 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 :=
|
||||
Acc.rec (motive := fun α _ => C α) m n
|
||||
n.rec m
|
||||
|
||||
namespace Acc
|
||||
variable {α : Sort u} {r : α → α → Prop}
|
||||
|
||||
def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
|
||||
Acc.recOn (motive := fun (x : α) _ => r y x → Acc r y)
|
||||
h₁ (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
|
||||
h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
|
||||
|
||||
end Acc
|
||||
|
||||
|
|
@ -41,8 +40,7 @@ class WellFoundedRelation (α : Sort u) where
|
|||
|
||||
namespace WellFounded
|
||||
def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
|
||||
WellFounded.recOn (motive := fun _ => (y : α) → Acc r y)
|
||||
wf (fun p => p) a
|
||||
wf.rec (fun p => p) a
|
||||
|
||||
section
|
||||
variable {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
|
||||
|
|
|
|||
|
|
@ -75,3 +75,11 @@ protected def znum.bit1 : znum → znum
|
|||
| zero => pos .one
|
||||
| pos n => pos (pos_num.bit1 n)
|
||||
| neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1)
|
||||
|
||||
example (h : False) : a = c :=
|
||||
h.rec
|
||||
|
||||
example (h : False) : a = c :=
|
||||
h.elim
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue