From dda0e388024a4d60c1673cdd67f12bc8a9051a24 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Jun 2019 12:40:21 -0700 Subject: [PATCH] chore(library/init): avoid local notation --- library/init/core.lean | 78 ++++++++----------- library/init/data/char/basic.lean | 16 ++-- library/init/data/list/basic.lean | 16 ++-- library/init/data/nat/basic.lean | 10 +-- library/init/lean/compiler/ir/basic.lean | 54 ++++++------- library/init/lean/compiler/ir/emitutil.lean | 7 +- .../lean/compiler/ir/expandresetreuse.lean | 5 +- library/init/lean/compiler/ir/livevars.lean | 30 ++++--- library/init/wf.lean | 19 ++--- 9 files changed, 101 insertions(+), 134 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 358822694e..14d6db6e4e 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -1140,31 +1140,30 @@ match h with section relation variables {α : Sort u} {β : Sort v} (r : β → β → Prop) -local infix `≺`:50 := r -def Reflexive := ∀ x, x ≺ x +def Reflexive := ∀ x, r x x -def Symmetric := ∀ {x y}, x ≺ y → y ≺ x +def Symmetric := ∀ {x y}, r x y → r y x -def Transitive := ∀ {x y z}, x ≺ y → y ≺ z → x ≺ z +def Transitive := ∀ {x y z}, r x y → r y z → r x z def Equivalence := Reflexive r ∧ Symmetric r ∧ Transitive r -def Total := ∀ x y, x ≺ y ∨ y ≺ x +def Total := ∀ x y, r x y ∨ r y x def mkEquivalence (rfl : Reflexive r) (symm : Symmetric r) (trans : Transitive r) : Equivalence r := ⟨rfl, @symm, @trans⟩ -def Irreflexive := ∀ x, ¬ x ≺ x +def Irreflexive := ∀ x, ¬ r x x -def AntiSymmetric := ∀ {x y}, x ≺ y → y ≺ x → x = y +def AntiSymmetric := ∀ {x y}, r x y → r y x → x = y def emptyRelation := λ a₁ a₂ : α, False def Subrelation (q r : β → β → Prop) := ∀ {x y}, q x y → r x y def InvImage (f : α → β) : α → α → Prop := -λ a₁ a₂, f a₁ ≺ f a₂ +λ a₁ a₂, r (f a₁) (f a₂) theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) := λ (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃), h h₁ h₂ @@ -1193,31 +1192,24 @@ theorem {u1 u2} TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α end relation -section binary +section Binary variables {α : Type u} {β : Type v} variable f : α → α → α -local infix * := f -def Commutative := ∀ a b, a * b = b * a -def Associative := ∀ a b c, (a * b) * c = a * (b * c) +def Commutative := ∀ a b, f a b = f b a +def Associative := ∀ a b c, f (f a b) c = f a (f b c) def RightCommutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁ def LeftCommutative (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b) -local infix `◾`:50 := Eq.trans - theorem leftComm : Commutative f → Associative f → LeftCommutative f := assume hcomm hassoc, assume a b c, - Eq.symm (hassoc a b c) -◾ (hcomm a b ▸ rfl : (a*b)*c = (b*a)*c) -◾ hassoc b a c +((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c) theorem rightComm : Commutative f → Associative f → RightCommutative f := assume hcomm hassoc, assume a b c, - hassoc a b c -◾ (hcomm b c ▸ rfl : a*(b*c) = a*(c*b)) -◾ Eq.symm (hassoc a c b) +((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b)) -end binary +end Binary /- Subtype -/ @@ -1409,44 +1401,42 @@ variable {α : Sort u} variable {r : α → α → Prop} variable {β : Quot r → Sort v} -local notation `⟦`:max a `⟧` := Quot.mk r a - @[reducible, macroInline] -protected def indep (f : Π a, β ⟦a⟧) (a : α) : PSigma β := -⟨⟦a⟧, f a⟩ +protected def indep (f : Π a, β (Quot.mk r a)) (a : α) : PSigma β := +⟨Quot.mk r a, f a⟩ -protected theorem indepCoherent (f : Π a, β ⟦a⟧) - (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) +protected theorem indepCoherent (f : Π a, β (Quot.mk r a)) + (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) : ∀ a b, r a b → Quot.indep f a = Quot.indep f b := λ a b e, PSigma.eq (sound e) (h a b e) protected theorem liftIndepPr1 - (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) + (f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) (q : Quot r) : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q := Quot.ind (λ (a : α), Eq.refl (Quot.indep f a).1) q @[reducible, elabAsEliminator, inline] protected def rec - (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) + (f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) (q : Quot r) : β 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, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : β q := + (q : Quot r) (f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) : β q := Quot.rec f h q @[reducible, elabAsEliminator, inline] protected def recOnSubsingleton - [h : ∀ a, Subsingleton (β ⟦a⟧)] (q : Quot r) (f : Π a, β ⟦a⟧) : β q := + [h : ∀ a, Subsingleton (β (Quot.mk r a))] (q : Quot r) (f : Π a, β (Quot.mk r a)) : β q := Quot.rec f (λ a b h, Subsingleton.elim _ (f b)) q @[reducible, elabAsEliminator, inline] protected def hrecOn - (q : Quot r) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q := + (q : Quot r) (f : Π a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q := Quot.recOn q f $ λ a b p, eqOfHeq $ - have p₁ : (Eq.rec (f a) (sound p) : β ⟦b⟧) ≅ f a, from eqRecHeq (sound p) (f a), + have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a, from eqRecHeq (sound p) (f a), Heq.trans p₁ (c a b p) end @@ -1556,7 +1546,7 @@ protected theorem inductionOn₃ Quotient.ind (λ a₁, Quotient.ind (λ a₂, Quotient.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁ end -section exact +section Exact variable {α : Sort u} variable [s : Setoid α] include s @@ -1569,17 +1559,15 @@ Quotient.liftOn₂ q₁ q₂ (λ a₁a₂, Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂)) (λ b₁b₂, Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂))))) -local infix `~` := rel - -private theorem rel.refl : ∀ q : Quotient s, q ~ q := +private theorem rel.refl : ∀ q : Quotient s, rel q q := λ q, Quot.inductionOn q (λ a, Setoid.refl a) -private theorem eqImpRel {q₁ q₂ : Quotient s} : q₁ = q₂ → q₁ ~ q₂ := +private theorem eqImpRel {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ := assume h, Eq.ndrecOn h (rel.refl q₁) theorem exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b := assume h, eqImpRel h -end exact +end Exact section universes uA uB uC @@ -1638,16 +1626,14 @@ instance {α : Sort u} {s : Setoid α} [d : ∀ a b : α, Decidable (a ≈ b)] : namespace Function variables {α : Sort u} {β : α → Sort v} -protected def Equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x +def Equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x -local infix `~` := Function.Equiv +protected theorem Equiv.refl (f : Π x : α, β x) : Equiv f f := assume x, rfl -protected theorem Equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl - -protected theorem Equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ := +protected theorem Equiv.symm {f₁ f₂ : Π x: α, β x} : Equiv f₁ f₂ → Equiv f₂ f₁ := λ h x, Eq.symm (h x) -protected theorem Equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ := +protected theorem Equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ := λ h₁ h₂ x, Eq.trans (h₁ x) (h₂ x) protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) := @@ -1673,8 +1659,6 @@ show extfunApp ⟦f₁⟧ = extfunApp ⟦f₂⟧, from congrArg extfunApp (sound h) end -local infix `~` := Function.Equiv - instance Pi.Subsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (Π a, β a) := ⟨λ f₁ f₂, funext (λ a, Subsingleton.elim (f₁ a) (f₂ a))⟩ diff --git a/library/init/data/char/basic.lean b/library/init/data/char/basic.lean index 8aa87ab9ce..6cbbfe5785 100644 --- a/library/init/data/char/basic.lean +++ b/library/init/data/char/basic.lean @@ -17,17 +17,15 @@ instance : HasSizeof Char := ⟨λ c, c.val.toNat⟩ namespace Char -local infix `&`:65 := UInt32.land - def utf8Size (c : Char) : UInt32 := let v := c.val in - if v & 0x80 = 0 then 1 -else if v & 0xE0 = 0xC0 then 2 -else if v & 0xF0 = 0xE0 then 3 -else if v & 0xF8 = 0xF0 then 4 -else if v & 0xFC = 0xF8 then 5 -else if v & 0xFE = 0xFC then 6 -else if v = 0xFF then 1 + if UInt32.land v 0x80 = 0 then 1 +else if UInt32.land v 0xE0 = 0xC0 then 2 +else if UInt32.land v 0xF0 = 0xE0 then 3 +else if UInt32.land v 0xF8 = 0xF0 then 4 +else if UInt32.land v 0xFC = 0xF8 then 5 +else if UInt32.land v 0xFE = 0xFC then 6 +else if v = 0xFF then 1 else 0 protected def Less (a b : Char) : Prop := a.val < b.val diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index d36aa813a6..55d2b3b0d6 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -35,8 +35,6 @@ def reverseAux : List α → List α → List α | [] r := r | (a::l) r := reverseAux l (a::r) -local infix `**`:66 := reverseAux - def reverse : List α → List α := λ l, reverseAux l [] @@ -46,7 +44,7 @@ reverseAux as.reverse bs instance : HasAppend (List α) := ⟨List.append⟩ -theorem reverseAuxReverseAuxNil : ∀ (as bs : List α), (as ** bs) ** [] = bs ** as +theorem reverseAuxReverseAuxNil : ∀ (as bs : List α), reverseAux (reverseAux as bs) [] = reverseAux bs as | [] bs := rfl | (a::as) bs := show reverseAux (reverseAux as (a::bs)) [] = reverseAux bs (a::as), from @@ -56,17 +54,15 @@ theorem nilAppend (as : List α) : [] ++ as = as := rfl theorem appendNil (as : List α) : as ++ [] = as := -show (as ** []) ** [] = as, from +show reverseAux (reverseAux as []) [] = as, from reverseAuxReverseAuxNil as [] -theorem reverseAuxReverseAux : ∀ (as bs cs : List α), (as ** bs) ** cs = bs ** ((as ** []) ** cs) +theorem reverseAuxReverseAux : ∀ (as bs cs : List α), reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as []) cs) | [] bs cs := rfl | (a::as) bs cs := - show (as ** a::bs) ** cs = bs ** ((as ** [a]) ** cs), from - have h₁ : (as ** a::bs) ** cs = bs ** a::((as ** []) ** cs), from reverseAuxReverseAux as (a::bs) cs, - have h₂ : ((as ** [a]) ** cs) = a::((as ** []) ** cs), from reverseAuxReverseAux as [a] cs, - have h₃ : bs ** a::((as ** []) ** cs) = bs ** ((as ** [a]) ** cs), from congrArg (λ b, bs ** b) h₂.symm, - Eq.trans h₁ h₃ + Eq.trans + (reverseAuxReverseAux as (a::bs) cs) + (congrArg (λ b, reverseAux bs b) (reverseAuxReverseAux as [a] cs).symm) theorem consAppend (a : α) (as bs : List α) : (a::as) ++ bs = a::(as ++ bs) := reverseAuxReverseAux as [a] bs diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index b8addeaa48..da1ea474dc 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -196,8 +196,6 @@ Nat.zeroAdd protected theorem oneMul (n : Nat) : 1 * n = n := Nat.mulComm n 1 ▸ Nat.mulOne n -local infix `◾`:50 := Eq.trans - protected theorem leftDistrib : ∀ (n m k : Nat), n * (m + k) = n * m + n * k | 0 m k := (Nat.zeroMul (m + k)).symm ▸ (Nat.zeroMul m).symm ▸ (Nat.zeroMul k).symm ▸ rfl | (succ n) m k := @@ -208,14 +206,14 @@ protected theorem leftDistrib : ∀ (n m k : Nat), n * (m + k) = n * m + n * k have h₅ : n * m + (m + (n * k + k)) = (n * m + m) + (n * k + k), from (Nat.addAssoc _ _ _).symm, have h₆ : (n * m + m) + (n * k + k) = (n * m + m) + succ n * k, from succMul n k ▸ rfl, have h₇ : (n * m + m) + succ n * k = succ n * m + succ n * k, from succMul n m ▸ rfl, - h₁ ◾ h₂ ◾ h₃ ◾ h₄ ◾ h₅ ◾ h₆ ◾ h₇ + (((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆).trans h₇ protected theorem rightDistrib (n m k : Nat) : (n + m) * k = n * k + m * k := have h₁ : (n + m) * k = k * (n + m), from Nat.mulComm _ _, have h₂ : k * (n + m) = k * n + k * m, from Nat.leftDistrib _ _ _, have h₃ : k * n + k * m = n * k + k * m, from Nat.mulComm n k ▸ rfl, have h₄ : n * k + k * m = n * k + m * k, from Nat.mulComm m k ▸ rfl, -h₁ ◾ h₂ ◾ h₃ ◾ h₄ +((h₁.trans h₂).trans h₃).trans h₄ protected theorem mulAssoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k) | n m 0 := rfl @@ -226,7 +224,7 @@ protected theorem mulAssoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k) have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m, from (mulAssoc n m k).symm ▸ rfl, have h₅ : (n * (m * k)) + n * m = n * (m * k + m), from (Nat.leftDistrib n (m*k) m).symm, have h₆ : n * (m * k + m) = n * (m * succ k), from Nat.mulSucc m k ▸ rfl, -h₁ ◾ h₂ ◾ h₃ ◾ h₄ ◾ h₅ ◾ h₆ +((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆ /- Inequalities -/ @@ -464,7 +462,7 @@ match le.dest h with | ⟨w, hw⟩ := have h₁ : k + n + w = k + (n + w), from Nat.addAssoc _ _ _, have h₂ : k + (n + w) = k + m, from congrArg _ hw, - le.intro $ h₁ ◾ h₂ + le.intro $ h₁.trans h₂ protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := have h₁ : n + k = k + n, from Nat.addComm _ _, diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean index 9c512dffcd..fae5cf1257 100644 --- a/library/init/lean/compiler/ir/basic.lean +++ b/library/init/lean/compiler/ir/basic.lean @@ -451,7 +451,7 @@ abbrev IndexRenaming := RBMap Index Index Index.lt class HasAlphaEqv (α : Type) := (aeqv : IndexRenaming → α → α → Bool) -local notation a `=[`:50 ρ `]=`:0 b:50 := HasAlphaEqv.aeqv ρ a b +export HasAlphaEqv (aeqv) def VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool := match ρ.find v₁.idx with @@ -461,32 +461,32 @@ match ρ.find v₁.idx with instance VarId.hasAeqv : HasAlphaEqv VarId := ⟨VarId.alphaEqv⟩ def Arg.alphaEqv (ρ : IndexRenaming) : Arg → Arg → Bool -| (Arg.var v₁) (Arg.var v₂) := v₁ =[ρ]= v₂ +| (Arg.var v₁) (Arg.var v₂) := aeqv ρ v₁ v₂ | Arg.irrelevant Arg.irrelevant := true | _ _ := false instance Arg.hasAeqv : HasAlphaEqv Arg := ⟨Arg.alphaEqv⟩ def args.alphaEqv (ρ : IndexRenaming) (args₁ args₂ : Array Arg) : Bool := -Array.isEqv args₁ args₂ (λ a b, a =[ρ]= b) +Array.isEqv args₁ args₂ (λ a b, aeqv ρ a b) instance args.hasAeqv : HasAlphaEqv (Array Arg) := ⟨args.alphaEqv⟩ def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool -| (Expr.ctor i₁ ys₁) (Expr.ctor i₂ ys₂) := i₁ == i₂ && ys₁ =[ρ]= ys₂ -| (Expr.reset n₁ x₁) (Expr.reset n₂ x₂) := n₁ == n₂ && x₁ =[ρ]= x₂ -| (Expr.reuse x₁ i₁ u₁ ys₁) (Expr.reuse x₂ i₂ u₂ ys₂) := x₁ =[ρ]= x₂ && i₁ == i₂ && u₁ == u₂ && ys₁ =[ρ]= ys₂ -| (Expr.proj i₁ x₁) (Expr.proj i₂ x₂) := i₁ == i₂ && x₁ =[ρ]= x₂ -| (Expr.uproj i₁ x₁) (Expr.uproj i₂ x₂) := i₁ == i₂ && x₁ =[ρ]= x₂ -| (Expr.sproj n₁ o₁ x₁) (Expr.sproj n₂ o₂ x₂) := n₁ == n₂ && o₁ == o₂ && x₁ =[ρ]= x₂ -| (Expr.fap c₁ ys₁) (Expr.fap c₂ ys₂) := c₁ == c₂ && ys₁ =[ρ]= ys₂ -| (Expr.pap c₁ ys₁) (Expr.pap c₂ ys₂) := c₁ == c₂ && ys₂ =[ρ]= ys₂ -| (Expr.ap x₁ ys₁) (Expr.ap x₂ ys₂) := x₁ =[ρ]= x₂ && ys₁ =[ρ]= ys₂ -| (Expr.box ty₁ x₁) (Expr.box ty₂ x₂) := ty₁ == ty₂ && x₁ =[ρ]= x₂ -| (Expr.unbox x₁) (Expr.unbox x₂) := x₁ =[ρ]= x₂ +| (Expr.ctor i₁ ys₁) (Expr.ctor i₂ ys₂) := i₁ == i₂ && aeqv ρ ys₁ ys₂ +| (Expr.reset n₁ x₁) (Expr.reset n₂ x₂) := n₁ == n₂ && aeqv ρ x₁ x₂ +| (Expr.reuse x₁ i₁ u₁ ys₁) (Expr.reuse x₂ i₂ u₂ ys₂) := aeqv ρ x₁ x₂ && i₁ == i₂ && u₁ == u₂ && aeqv ρ ys₁ ys₂ +| (Expr.proj i₁ x₁) (Expr.proj i₂ x₂) := i₁ == i₂ && aeqv ρ x₁ x₂ +| (Expr.uproj i₁ x₁) (Expr.uproj i₂ x₂) := i₁ == i₂ && aeqv ρ x₁ x₂ +| (Expr.sproj n₁ o₁ x₁) (Expr.sproj n₂ o₂ x₂) := n₁ == n₂ && o₁ == o₂ && aeqv ρ x₁ x₂ +| (Expr.fap c₁ ys₁) (Expr.fap c₂ ys₂) := c₁ == c₂ && aeqv ρ ys₁ ys₂ +| (Expr.pap c₁ ys₁) (Expr.pap c₂ ys₂) := c₁ == c₂ && aeqv ρ ys₂ ys₂ +| (Expr.ap x₁ ys₁) (Expr.ap x₂ ys₂) := aeqv ρ x₁ x₂ && aeqv ρ ys₁ ys₂ +| (Expr.box ty₁ x₁) (Expr.box ty₂ x₂) := ty₁ == ty₂ && aeqv ρ x₁ x₂ +| (Expr.unbox x₁) (Expr.unbox x₂) := aeqv ρ x₁ x₂ | (Expr.lit v₁) (Expr.lit v₂) := v₁ == v₂ -| (Expr.isShared x₁) (Expr.isShared x₂) := x₁ =[ρ]= x₂ -| (Expr.isTaggedPtr x₁) (Expr.isTaggedPtr x₂) := x₁ =[ρ]= x₂ +| (Expr.isShared x₁) (Expr.isShared x₂) := aeqv ρ x₁ x₂ +| (Expr.isTaggedPtr x₁) (Expr.isTaggedPtr x₂) := aeqv ρ x₁ x₂ | _ _ := false instance Expr.hasAeqv : HasAlphaEqv Expr:= ⟨Expr.alphaEqv⟩ @@ -503,26 +503,26 @@ if ps₁.size != ps₂.size then none else Array.foldl₂ (λ ρ p₁ p₂, do ρ ← ρ, addParamRename ρ p₁ p₂) (some ρ) ps₁ ps₂ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool -| ρ (FnBody.vdecl x₁ t₁ v₁ b₁) (FnBody.vdecl x₂ t₂ v₂ b₂) := t₁ == t₂ && v₁ =[ρ]= v₂ && FnBody.alphaEqv (addVarRename ρ x₁.idx x₂.idx) b₁ b₂ +| ρ (FnBody.vdecl x₁ t₁ v₁ b₁) (FnBody.vdecl x₂ t₂ v₂ b₂) := t₁ == t₂ && aeqv ρ v₁ v₂ && FnBody.alphaEqv (addVarRename ρ x₁.idx x₂.idx) b₁ b₂ | ρ (FnBody.jdecl j₁ ys₁ v₁ b₁) (FnBody.jdecl j₂ ys₂ v₂ b₂) := match addParamsRename ρ ys₁ ys₂ with | some ρ' := FnBody.alphaEqv ρ' v₁ v₂ && FnBody.alphaEqv (addVarRename ρ j₁.idx j₂.idx) b₁ b₂ | none := false -| ρ (FnBody.set x₁ i₁ y₁ b₁) (FnBody.set x₂ i₂ y₂ b₂) := x₁ =[ρ]= x₂ && i₁ == i₂ && y₁ =[ρ]= y₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ (FnBody.uset x₁ i₁ y₁ b₁) (FnBody.uset x₂ i₂ y₂ b₂) := x₁ =[ρ]= x₂ && i₁ == i₂ && y₁ =[ρ]= y₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ (FnBody.set x₁ i₁ y₁ b₁) (FnBody.set x₂ i₂ y₂ b₂) := aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ (FnBody.uset x₁ i₁ y₁ b₁) (FnBody.uset x₂ i₂ y₂ b₂) := aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && FnBody.alphaEqv ρ b₁ b₂ | ρ (FnBody.sset x₁ i₁ o₁ y₁ t₁ b₁) (FnBody.sset x₂ i₂ o₂ y₂ t₂ b₂) := - x₁ =[ρ]= x₂ && i₁ = i₂ && o₁ = o₂ && y₁ =[ρ]= y₂ && t₁ == t₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ (FnBody.setTag x₁ i₁ b₁) (FnBody.setTag x₂ i₂ b₂) := x₁ =[ρ]= x₂ && i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ (FnBody.inc x₁ n₁ c₁ b₁) (FnBody.inc x₂ n₂ c₂ b₂) := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ (FnBody.dec x₁ n₁ c₁ b₁) (FnBody.dec x₂ n₂ c₂ b₂) := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ (FnBody.del x₁ b₁) (FnBody.del x₂ b₂) := x₁ =[ρ]= x₂ && FnBody.alphaEqv ρ b₁ b₂ + aeqv ρ x₁ x₂ && i₁ = i₂ && o₁ = o₂ && aeqv ρ y₁ y₂ && t₁ == t₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ (FnBody.setTag x₁ i₁ b₁) (FnBody.setTag x₂ i₂ b₂) := aeqv ρ x₁ x₂ && i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ (FnBody.inc x₁ n₁ c₁ b₁) (FnBody.inc x₂ n₂ c₂ b₂) := aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ (FnBody.dec x₁ n₁ c₁ b₁) (FnBody.dec x₂ n₂ c₂ b₂) := aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ (FnBody.del x₁ b₁) (FnBody.del x₂ b₂) := aeqv ρ x₁ x₂ && FnBody.alphaEqv ρ b₁ b₂ | ρ (FnBody.mdata m₁ b₁) (FnBody.mdata m₂ b₂) := m₁ == m₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ (FnBody.case n₁ x₁ alts₁) (FnBody.case n₂ x₂ alts₂) := n₁ == n₂ && x₁ =[ρ]= x₂ && Array.isEqv alts₁ alts₂ (λ alt₁ alt₂, +| ρ (FnBody.case n₁ x₁ alts₁) (FnBody.case n₂ x₂ alts₂) := n₁ == n₂ && aeqv ρ x₁ x₂ && Array.isEqv alts₁ alts₂ (λ alt₁ alt₂, match alt₁, alt₂ with | Alt.ctor i₁ b₁, Alt.ctor i₂ b₂ := i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂ | Alt.default b₁, Alt.default b₂ := FnBody.alphaEqv ρ b₁ b₂ | _, _ := false) -| ρ (FnBody.jmp j₁ ys₁) (FnBody.jmp j₂ ys₂) := j₁ == j₂ && ys₁ =[ρ]= ys₂ -| ρ (FnBody.ret x₁) (FnBody.ret x₂) := x₁ =[ρ]= x₂ +| ρ (FnBody.jmp j₁ ys₁) (FnBody.jmp j₂ ys₂) := j₁ == j₂ && aeqv ρ ys₁ ys₂ +| ρ (FnBody.ret x₁) (FnBody.ret x₂) := aeqv ρ x₁ x₂ | _ FnBody.unreachable FnBody.unreachable := true | _ _ _ := false diff --git a/library/init/lean/compiler/ir/emitutil.lean b/library/init/lean/compiler/ir/emitutil.lean index db9239773f..386f92e245 100644 --- a/library/init/lean/compiler/ir/emitutil.lean +++ b/library/init/lean/compiler/ir/emitutil.lean @@ -99,17 +99,16 @@ def collectParams (ps : Array Param) : Collector := λ s, ps.foldl (λ s p, collectVar p.x p.ty s) s @[inline] def collectJP (j : JoinPointId) (xs : Array Param) : Collector | (vs, js) := (vs, js.insert j xs) -local infix ` >> `:50 := Function.comp /- `collectFnBody` assumes the variables in -/ partial def collectFnBody : FnBody → Collector -| (FnBody.vdecl x t _ b) := collectVar x t >> collectFnBody b -| (FnBody.jdecl j xs v b) := collectJP j xs >> collectParams xs >> collectFnBody v >> collectFnBody b +| (FnBody.vdecl x t _ b) := collectVar x t ∘ collectFnBody b +| (FnBody.jdecl j xs v b) := collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b | (FnBody.case _ _ alts) := λ s, alts.foldl (λ s alt, collectFnBody alt.body s) s | e := if e.isTerminal then id else collectFnBody e.body def collectDecl : Decl → Collector -| (Decl.fdecl _ xs _ b) := collectParams xs >> collectFnBody b +| (Decl.fdecl _ xs _ b) := collectParams xs ∘ collectFnBody b | _ := id end CollectMaps diff --git a/library/init/lean/compiler/ir/expandresetreuse.lean b/library/init/lean/compiler/ir/expandresetreuse.lean index 82c593b049..ea0c9225d0 100644 --- a/library/init/lean/compiler/ir/expandresetreuse.lean +++ b/library/init/lean/compiler/ir/expandresetreuse.lean @@ -23,11 +23,10 @@ abbrev Collector := ProjMap → ProjMap | Expr.sproj _ _ _ := m.insert x v | Expr.uproj _ _ := m.insert x v | _ := m -local infix ` >> `:50 := Function.comp partial def collectFnBody : FnBody → Collector -| (FnBody.vdecl x _ v b) := collectVDecl x v >> collectFnBody b -| (FnBody.jdecl _ _ v b) := collectFnBody v >> collectFnBody b +| (FnBody.vdecl x _ v b) := collectVDecl x v ∘ collectFnBody b +| (FnBody.jdecl _ _ v b) := collectFnBody v ∘ collectFnBody b | (FnBody.case _ _ alts) := λ s, alts.foldl (λ s alt, collectFnBody alt.body s) s | e := if e.isTerminal then id else collectFnBody e.body end CollectProjMap diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean index 3328cf8ec1..39043d2a33 100644 --- a/library/init/lean/compiler/ir/livevars.lean +++ b/library/init/lean/compiler/ir/livevars.lean @@ -112,18 +112,16 @@ private def bindVar (x : VarId) : Collector := private def bindParams (ps : Array Param) : Collector := λ s, ps.foldl (λ s p, s.erase p.x) s -local infix ` >> `:50 := Function.comp - def collectExpr : Expr → Collector | (Expr.ctor _ ys) := collectArgs ys | (Expr.reset _ x) := collectVar x -| (Expr.reuse x _ _ ys) := collectVar x >> collectArgs ys +| (Expr.reuse x _ _ ys) := collectVar x ∘ collectArgs ys | (Expr.proj _ x) := collectVar x | (Expr.uproj _ x) := collectVar x | (Expr.sproj _ _ x) := collectVar x | (Expr.fap _ ys) := collectArgs ys | (Expr.pap _ ys) := collectArgs ys -| (Expr.ap x ys) := collectVar x >> collectArgs ys +| (Expr.ap x ys) := collectVar x ∘ collectArgs ys | (Expr.box _ x) := collectVar x | (Expr.unbox x) := collectVar x | (Expr.lit v) := skip @@ -131,26 +129,26 @@ def collectExpr : Expr → Collector | (Expr.isTaggedPtr x) := collectVar x partial def collectFnBody : FnBody → JPLiveVarMap → Collector -| (FnBody.vdecl x _ v b) m := collectExpr v >> collectFnBody b m >> bindVar x +| (FnBody.vdecl x _ v b) m := collectExpr v ∘ collectFnBody b m ∘ bindVar x | (FnBody.jdecl j ys v b) m := - let jLiveVars := (collectFnBody v m >> bindParams ys) {} in + let jLiveVars := (collectFnBody v m ∘ bindParams ys) {} in let m := m.insert j jLiveVars in collectFnBody b m -| (FnBody.set x _ y b) m := collectVar x >> collectArg y >> collectFnBody b m -| (FnBody.setTag x _ b) m := collectVar x >> collectFnBody b m -| (FnBody.uset x _ y b) m := collectVar x >> collectVar y >> collectFnBody b m -| (FnBody.sset x _ _ y _ b) m := collectVar x >> collectVar y >> collectFnBody b m -| (FnBody.inc x _ _ b) m := collectVar x >> collectFnBody b m -| (FnBody.dec x _ _ b) m := collectVar x >> collectFnBody b m -| (FnBody.del x b) m := collectVar x >> collectFnBody b m +| (FnBody.set x _ y b) m := collectVar x ∘ collectArg y ∘ collectFnBody b m +| (FnBody.setTag x _ b) m := collectVar x ∘ collectFnBody b m +| (FnBody.uset x _ y b) m := collectVar x ∘ collectVar y ∘ collectFnBody b m +| (FnBody.sset x _ _ y _ b) m := collectVar x ∘ collectVar y ∘ collectFnBody b m +| (FnBody.inc x _ _ b) m := collectVar x ∘ collectFnBody b m +| (FnBody.dec x _ _ b) m := collectVar x ∘ collectFnBody b m +| (FnBody.del x b) m := collectVar x ∘ collectFnBody b m | (FnBody.mdata _ b) m := collectFnBody b m | (FnBody.ret x) m := collectArg x -| (FnBody.case _ x alts) m := collectVar x >> collectArray alts (λ alt, collectFnBody alt.body m) +| (FnBody.case _ x alts) m := collectVar x ∘ collectArray alts (λ alt, collectFnBody alt.body m) | (FnBody.unreachable) m := skip -| (FnBody.jmp j xs) m := collectJP m j >> collectArgs xs +| (FnBody.jmp j xs) m := collectJP m j ∘ collectArgs xs def updateJPLiveVarMap (j : JoinPointId) (ys : Array Param) (v : FnBody) (m : JPLiveVarMap) : JPLiveVarMap := -let jLiveVars := (collectFnBody v m >> bindParams ys) {} in +let jLiveVars := (collectFnBody v m ∘ bindParams ys) {} in m.insert j jLiveVars end LiveVars diff --git a/library/init/wf.lean b/library/init/wf.lean index c7cd75fef2..46842a7eac 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -46,22 +46,21 @@ assume a, WellFounded.recOn wf (λ p, p) a section variables {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) -local infix `≺`:50 := r -theorem recursion {C : α → Sort v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := +theorem recursion {C : α → Sort v} (a : α) (h : Π x, (Π y, r y x → C y) → C x) : C a := Acc.recOn (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih) -theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := +theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := recursion hwf a h variable {C : α → Sort v} -variable F : Π x, (Π y, y ≺ x → C y) → C x +variable F : Π x, (Π y, r y x → C y) → C x def fixF (x : α) (a : Acc r x) : C x := Acc.recOn a (λ x₁ ac₁ ih, F x₁ ih) theorem fixFEq (x : α) (acx : Acc r x) : - fixF F x acx = F x (λ (y : α) (p : y ≺ x), fixF F y (Acc.inv acx p)) := + fixF F x acx = F x (λ (y : α) (p : r y x), fixF F y (Acc.inv acx p)) := Acc.rec (λ x r ih, rfl) acx end @@ -115,7 +114,6 @@ end InvImage -- The transitive closure of a well-founded relation is well-founded namespace TC variables {α : Sort u} {r : α → α → Prop} -local notation `r⁺` := TC r def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := Acc.ndrecOn ac $ λ x acx ih, @@ -125,7 +123,7 @@ Acc.ndrecOn ac $ λ x acx ih, (λ a b c rab rbc ih₁ ih₂ acx ih, Acc.inv (ih₂ acx ih) rab) acx ih -def wf (h : WellFounded r) : WellFounded r⁺ := +def wf (h : WellFounded r) : WellFounded (TC r) := ⟨λ a, accessible (apply h a)⟩ end TC @@ -173,7 +171,6 @@ end section variables {α : Type u} {β : Type v} variables {ra : α → α → Prop} {rb : β → β → Prop} -local infix `≺`:50 := Lex ra rb def lexAccessible {a} (aca : Acc ra a) (acb : ∀ b, Acc rb b): ∀ b, Acc (Lex ra rb) (a, b) := Acc.ndrecOn aca $ λ xa aca iha b, @@ -219,12 +216,11 @@ end section variables {α : Sort u} {β : α → Sort v} variables {r : α → α → Prop} {s : Π a : α, β a → β a → Prop} -local infix `≺`:50 := Lex r s def lexAccessible {a} (aca : Acc r a) (acb : ∀ a, WellFounded (s a)) : ∀ (b : β a), Acc (Lex r s) ⟨a, b⟩ := Acc.ndrecOn aca $ λ xa aca (iha : ∀ y, r y xa → ∀ b : β y, Acc (Lex r s) ⟨y, b⟩) (b : β xa), Acc.ndrecOn (WellFounded.apply (acb xa) b) $ λ xb acb (ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩), - Acc.intro ⟨xa, xb⟩ $ λ p (lt : p ≺ ⟨xa, xb⟩), + Acc.intro ⟨xa, xb⟩ $ λ p (lt : Lex r s p ⟨xa, xb⟩), have aux : xa = xa → xb ≅ xb → Acc (Lex r s) p, from @PSigma.Lex.recOn α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 ≅ xb → Acc (Lex r s) p₁) p ⟨xa, xb⟩ lt @@ -275,12 +271,11 @@ section open WellFounded variables {α : Sort u} {β : Sort v} variables {r : α → α → Prop} {s : β → β → Prop} -local infix `≺`:50 := RevLex r s def revLexAccessible {b} (acb : Acc s b) (aca : ∀ a, Acc r a): ∀ a, Acc (RevLex r s) ⟨a, b⟩ := Acc.recOn acb $ λ xb acb (ihb : ∀ y, s y xb → ∀ a, Acc (RevLex r s) ⟨a, y⟩) a, Acc.recOn (aca a) $ λ xa aca (iha : ∀ y, r y xa → Acc (RevLex r s) (mk y xb)), - Acc.intro ⟨xa, xb⟩ $ λ p (lt : p ≺ ⟨xa, xb⟩), + Acc.intro ⟨xa, xb⟩ $ λ p (lt : RevLex r s p ⟨xa, xb⟩), have aux : xa = xa → xb = xb → Acc (RevLex r s) p, from @RevLex.recOn α β r s (λ p₁ p₂ _, fst p₂ = xa → snd p₂ = xb → Acc (RevLex r s) p₁) p ⟨xa, xb⟩ lt