fb135b8cfe
Currently this will fail in two tests, because of changes in #3965. * Sometimes we need to add an additional universe annotation, or we get a `stuck at solving universe constraint max u ?u =?= u`. * Sometimes we need to specify arguments that could previously be found by unification. --------- Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
206 lines
4.9 KiB
Text
206 lines
4.9 KiB
Text
section Mathlib.Logic.Function.Iterate
|
||
|
||
universe u v
|
||
|
||
variable {α : Type u}
|
||
|
||
/-- Iterate a function. -/
|
||
def Nat.iterate {α : Sort u} (op : α → α) : Nat → α → α := sorry
|
||
|
||
notation:max f "^["n"]" => Nat.iterate f n
|
||
|
||
theorem Function.iterate_succ' (f : α → α) (n : Nat) : f^[n.succ] = f ∘ f^[n] := sorry
|
||
|
||
end Mathlib.Logic.Function.Iterate
|
||
|
||
section Mathlib.Data.Quot
|
||
|
||
variable {α : Sort _}
|
||
|
||
noncomputable def Quot.out {r : α → α → Prop} (q : Quot r) : α := sorry
|
||
|
||
end Mathlib.Data.Quot
|
||
|
||
section Mathlib.Init.Order.Defs
|
||
|
||
universe u
|
||
variable {α : Type u}
|
||
|
||
section Preorder
|
||
|
||
class Preorder (α : Type u) extends LE α, LT α where
|
||
|
||
variable [Preorder α]
|
||
|
||
theorem lt_of_lt_of_le : ∀ {a b c : α}, a < b → b ≤ c → a < c := sorry
|
||
|
||
end Preorder
|
||
|
||
variable [LE α]
|
||
|
||
theorem le_total : ∀ a b : α, a ≤ b ∨ b ≤ a := sorry
|
||
|
||
end Mathlib.Init.Order.Defs
|
||
|
||
section Mathlib.Order.RelClasses
|
||
|
||
universe u
|
||
|
||
class IsWellOrder (α : Type u) (r : α → α → Prop) : Prop
|
||
|
||
end Mathlib.Order.RelClasses
|
||
|
||
section Mathlib.Order.SetNotation
|
||
|
||
universe u v
|
||
variable {α : Type u} {ι : Sort v}
|
||
|
||
class SupSet (α : Type _) where
|
||
|
||
def iSup [SupSet α] (s : ι → α) : α := sorry
|
||
|
||
end Mathlib.Order.SetNotation
|
||
|
||
section Mathlib.SetTheory.Ordinal.Basic
|
||
|
||
noncomputable section
|
||
|
||
universe u v w
|
||
|
||
variable {α : Type u}
|
||
|
||
structure WellOrder : Type (u + 1) where
|
||
α : Type u
|
||
|
||
instance Ordinal.isEquivalent : Setoid WellOrder := sorry
|
||
|
||
def Ordinal : Type (u + 1) := Quotient Ordinal.isEquivalent
|
||
|
||
instance (o : Ordinal) : LT o.out.α := sorry
|
||
|
||
namespace Ordinal
|
||
|
||
def typein (r : α → α → Prop) [IsWellOrder α r] (a : α) : Ordinal := sorry
|
||
|
||
instance partialOrder : Preorder Ordinal := sorry
|
||
|
||
theorem typein_lt_self {o : Ordinal} (i : o.out.α) :
|
||
@typein _ (· < ·) sorry i < o := sorry
|
||
|
||
instance : SupSet Ordinal := sorry
|
||
|
||
end Ordinal
|
||
|
||
end
|
||
|
||
end Mathlib.SetTheory.Ordinal.Basic
|
||
|
||
section Mathlib.SetTheory.Ordinal.Arithmetic
|
||
|
||
noncomputable section
|
||
|
||
universe u v w
|
||
|
||
namespace Ordinal
|
||
|
||
def sup {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v} :=
|
||
iSup f
|
||
|
||
def lsub {ι} (f : ι → Ordinal) : Ordinal :=
|
||
sup f
|
||
|
||
def blsub₂ (o₁ o₂ : Ordinal) (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) :
|
||
Ordinal :=
|
||
lsub (fun x : o₁.out.α × o₂.out.α => op (typein_lt_self x.1) (typein_lt_self x.2))
|
||
|
||
theorem lt_blsub₂ {o₁ o₂ : Ordinal}
|
||
(op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal}
|
||
(ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op := sorry
|
||
|
||
|
||
end Ordinal
|
||
|
||
end
|
||
|
||
end Mathlib.SetTheory.Ordinal.Arithmetic
|
||
|
||
section Mathlib.SetTheory.Ordinal.FixedPoint
|
||
|
||
noncomputable section
|
||
|
||
universe u v
|
||
|
||
namespace Ordinal
|
||
|
||
section
|
||
|
||
variable {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}}
|
||
|
||
def nfpFamily (f : ι → Ordinal → Ordinal) (a : Ordinal) : Ordinal :=
|
||
sup (List.foldr f a)
|
||
|
||
end
|
||
|
||
section
|
||
|
||
variable {f : Ordinal.{u} → Ordinal.{u}}
|
||
|
||
def nfp (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
|
||
nfpFamily fun _ : Unit => f
|
||
|
||
theorem lt_nfp {a b} : a < nfp f b ↔ ∃ n, a < f^[n] b := sorry
|
||
|
||
end
|
||
|
||
end Ordinal
|
||
|
||
end
|
||
|
||
end Mathlib.SetTheory.Ordinal.FixedPoint
|
||
|
||
section Mathlib.SetTheory.Ordinal.Principal
|
||
|
||
universe u v w
|
||
|
||
namespace Ordinal
|
||
|
||
def Principal (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) : Prop :=
|
||
∀ ⦃a b⦄, a < o → b < o → op a b < o
|
||
|
||
theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
|
||
Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
|
||
fun a b ha hb => by
|
||
rw [lt_nfp] at *
|
||
rcases ha with ⟨m, hm⟩
|
||
rcases hb with ⟨n, hn⟩
|
||
rcases le_total
|
||
((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
|
||
((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
|
||
· refine ⟨n+1, ?_⟩
|
||
rw [Function.iterate_succ']
|
||
-- after https://github.com/leanprover/lean4/pull/3965 this requires `lt_blsub₂.{u}` or we get
|
||
-- `stuck at solving universe constraint max u ?u =?= u`
|
||
-- Note that there are two solutions: 0 and u. Both of them work.
|
||
exact lt_blsub₂.{u} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
|
||
· sorry
|
||
|
||
-- Trying again with 0
|
||
theorem principal_nfp_blsub₂' (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
|
||
Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
|
||
fun a b ha hb => by
|
||
rw [lt_nfp] at *
|
||
rcases ha with ⟨m, hm⟩
|
||
rcases hb with ⟨n, hn⟩
|
||
rcases le_total
|
||
((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
|
||
((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
|
||
· refine ⟨n+1, ?_⟩
|
||
rw [Function.iterate_succ']
|
||
-- universe 0 also works here
|
||
exact lt_blsub₂.{0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
|
||
· sorry
|
||
|
||
|
||
end Ordinal
|
||
|
||
end Mathlib.SetTheory.Ordinal.Principal
|