From 025d683ea43e37c2d86ec165a8e5bc0313d2d572 Mon Sep 17 00:00:00 2001 From: James Date: Thu, 7 Mar 2024 01:00:01 -0500 Subject: [PATCH 1/5] start a polymorphic range impl? --- LeanColls/Data/Range.lean | 81 ++++++++++++++++++++++----------------- 1 file changed, 45 insertions(+), 36 deletions(-) diff --git a/LeanColls/Data/Range.lean b/LeanColls/Data/Range.lean index d7f0dcd96..389a2ce68 100644 --- a/LeanColls/Data/Range.lean +++ b/LeanColls/Data/Range.lean @@ -12,48 +12,57 @@ import LeanColls.MathlibUpstream namespace LeanColls -structure Range extends Std.Range where - step_pos : step > 0 - start_le_stop : start ≤ stop +structure Range (ι : Type u) where + /-- The range's lower bound. -/ + start : ι + /-- Whether to include start. -/ + start_inclusive : Bool := true + /-- The range's upper bound. -/ + stop : ι + /-- Whether to include stop. -/ + stop_inclusive : Bool := false + /-- The amount to increment at each step. -/ + step : ι namespace Range -attribute [simp] step_pos start_le_stop - -@[simp] def ofStd : Std.Range → Range -| {start, stop, step} => - { start := start - , stop := max start stop - , step := max 1 step - , step_pos := by simp - , start_le_stop := by simp - } - -instance : Coe Std.Range Range where - coe := ofStd - -instance : CoeHead Range Std.Range where - coe r := r.toRange - - -def contains (r : Range) (i : Nat) := - r.start ≤ i && i < r.stop && r.step ∣ (i - r.start) - -instance : Membership Nat Range where +variable [LE ι] [LT ι] [DecidableRel (· < · : ι → ι → Prop)] [DecidableRel (· ≤ · : ι → ι → Prop)] + +#check LinearOrder +def contains + (r : Range ι) (i : ι) : Prop := + ( match r.start with + | none => true + | some (l, false) => l < i + | some (l, true) => l ≤ i + ) ∧ + ( match r.stop with + | none => true + | some (h, false) => i < h + | some (h, true) => i ≤ h + ) + +instance {r : Range ι} : DecidablePred (contains r) := fun _ => + @And.decidable _ _ + ( match r.start with + | none => inferInstance + | some (_, false) => inferInstance + | some (_, true) => inferInstance ) + ( match r.stop with + | none => inferInstance + | some (_, false) => inferInstance + | some (_, true) => inferInstance + ) + +def toSet (r : Range ι) : Set ι := contains r + +instance : Membership ι (Range ι) where mem i r := contains r i -theorem mem_def (r : Range) : x ∈ r ↔ r.start ≤ x ∧ x < r.stop ∧ (r.step ∣ x - r.start) := by - simp [Membership.mem, contains] - exact and_assoc - -def nth (r : Range) (i : Nat) : Nat := - r.start + i * r.step - -@[simp] theorem nth_ge_start (r : Range) (i : Nat) : nth r i ≥ r.start := by - simp [nth] +variable [Add ι] [One ι] -@[simp] theorem nth_sub_start (r : Range) (i : Nat) : r.step ∣ (nth r i - r.start) := by - simp [nth] +def foldl (f : β → ι → β) (acc : β) (r : Range ι) : β := + aux def ofNth (r : Range) (x : Nat) : Nat := (x - r.start) / r.step From 20ce29af42592b8233f12529ebf774e6628970ab Mon Sep 17 00:00:00 2001 From: James Gallicchio Date: Fri, 22 Mar 2024 21:01:39 -0400 Subject: [PATCH 2/5] so ummmmmm 9x everything --- LeanColls/Data/Range.lean | 144 ++++++++++++++++++++++----------- LeanColls/MathlibUpstream.lean | 72 +++++++++++++++++ 2 files changed, 167 insertions(+), 49 deletions(-) diff --git a/LeanColls/Data/Range.lean b/LeanColls/Data/Range.lean index 389a2ce68..cdd71545d 100644 --- a/LeanColls/Data/Range.lean +++ b/LeanColls/Data/Range.lean @@ -1,4 +1,4 @@ -/- Copyright (c) 2023 James Gallicchio +/- Copyright (c) 2023-2024 James Gallicchio Authors: James Gallicchio -/ @@ -12,56 +12,102 @@ import LeanColls.MathlibUpstream namespace LeanColls -structure Range (ι : Type u) where - /-- The range's lower bound. -/ - start : ι - /-- Whether to include start. -/ - start_inclusive : Bool := true - /-- The range's upper bound. -/ - stop : ι - /-- Whether to include stop. -/ - stop_inclusive : Bool := false - /-- The amount to increment at each step. -/ - step : ι - namespace Range -variable [LE ι] [LT ι] [DecidableRel (· < · : ι → ι → Prop)] [DecidableRel (· ≤ · : ι → ι → Prop)] - -#check LinearOrder -def contains - (r : Range ι) (i : ι) : Prop := - ( match r.start with - | none => true - | some (l, false) => l < i - | some (l, true) => l ≤ i - ) ∧ - ( match r.stop with - | none => true - | some (h, false) => i < h - | some (h, true) => i ≤ h - ) - -instance {r : Range ι} : DecidablePred (contains r) := fun _ => - @And.decidable _ _ - ( match r.start with - | none => inferInstance - | some (_, false) => inferInstance - | some (_, true) => inferInstance ) - ( match r.stop with - | none => inferInstance - | some (_, false) => inferInstance - | some (_, true) => inferInstance - ) - -def toSet (r : Range ι) : Set ι := contains r - -instance : Membership ι (Range ι) where - mem i r := contains r i - -variable [Add ι] [One ι] - -def foldl (f : β → ι → β) (acc : β) (r : Range ι) : β := +/-! ## Generalized Ranges + +Mathlib defines 9 common intervals over preorders, +based on whether the left and right bounds are +- closed (inclusive) +- open (exclusive) +- infinite (unbounded) + +These are denoted `Range.XX` here. +`X` is `C` for closed, `O` for open, and `I` for infinite. +-/ + +structure II (ι : Type u) +structure IC {ι : Type u} ( R : ι) +structure IO {ι : Type u} ( R : ι) +structure CI {ι : Type u} (L : ι) +structure OI {ι : Type u} (L : ι) +structure OO {ι : Type u} (L R : ι) +structure CO {ι : Type u} (L R : ι) +structure OC {ι : Type u} (L R : ι) +structure CC {ι : Type u} (L R : ι) + +/-! ## Range Notation + +- Ranges are denoted by `a..b` +- By default the endpoints are included +- Write `a<..b` or `a.. II +notation ".." r => IC r +notation "..<" r => IO r +notation l ".." => CI l +notation l "<.." => OI l +notation l ".." r => OO l r +notation l "..<" r => CO l r +notation l "<.." r => OC l r +notation l "<..<" r => CC l r + +/-! ## Range Membership -/ + +section +variable [LE ι] [DecidableRel (· ≤ · : ι → ι → Prop)] [LT ι] [DecidableRel (· < · : ι → ι → Prop)] + +@[inline] def II.contains (_self : II (ι := ι) ) : ι → Prop := fun _i => true +@[inline] def IC.contains (_self : IC (ι := ι) r ) : ι → Prop := fun i => r ≤ i +@[inline] def IO.contains (_self : IO (ι := ι) r ) : ι → Prop := fun i => r < i +@[inline] def CI.contains (_self : CI (ι := ι) l ) : ι → Prop := fun i => l ≤ i +@[inline] def OI.contains (_self : OI (ι := ι) l ) : ι → Prop := fun i => l < i +@[inline] def OO.contains (_self : OO (ι := ι) l r) : ι → Prop := fun i => l < i && i < r +@[inline] def CO.contains (_self : CO (ι := ι) l r) : ι → Prop := fun i => l ≤ i && i < r +@[inline] def OC.contains (_self : OC (ι := ι) l r) : ι → Prop := fun i => l < i && i ≤ r +@[inline] def CC.contains (_self : CC (ι := ι) l r) : ι → Prop := fun i => l ≤ i && i ≤ r + +@[inline] instance : Membership ι (II (ι := ι) ) := ⟨Function.swap II.contains⟩ +@[inline] instance : Membership ι (IC (ι := ι) r ) := ⟨Function.swap IC.contains⟩ +@[inline] instance : Membership ι (IO (ι := ι) r ) := ⟨Function.swap IO.contains⟩ +@[inline] instance : Membership ι (CI (ι := ι) l ) := ⟨Function.swap CI.contains⟩ +@[inline] instance : Membership ι (OI (ι := ι) l ) := ⟨Function.swap OI.contains⟩ +@[inline] instance : Membership ι (OO (ι := ι) l r) := ⟨Function.swap OO.contains⟩ +@[inline] instance : Membership ι (CO (ι := ι) l r) := ⟨Function.swap CO.contains⟩ +@[inline] instance : Membership ι (OC (ι := ι) l r) := ⟨Function.swap OC.contains⟩ +@[inline] instance : Membership ι (CC (ι := ι) l r) := ⟨Function.swap CC.contains⟩ + +instance : DecidablePred (II.contains (self : II (ι := ι) )) := by unfold II.contains; infer_instance +instance : DecidablePred (IC.contains (self : IC (ι := ι) r )) := by unfold IC.contains; infer_instance +instance : DecidablePred (IO.contains (self : IO (ι := ι) r )) := by unfold IO.contains; infer_instance +instance : DecidablePred (CI.contains (self : CI (ι := ι) l )) := by unfold CI.contains; infer_instance +instance : DecidablePred (OI.contains (self : OI (ι := ι) l )) := by unfold OI.contains; infer_instance +instance : DecidablePred (OO.contains (self : OO (ι := ι) l r)) := by unfold OO.contains; infer_instance +instance : DecidablePred (CO.contains (self : CO (ι := ι) l r)) := by unfold CO.contains; infer_instance +instance : DecidablePred (OC.contains (self : OC (ι := ι) l r)) := by unfold OC.contains; infer_instance +instance : DecidablePred (CC.contains (self : CC (ι := ι) l r)) := by unfold CC.contains; infer_instance + +instance II.instDecidableMem : Decidable (i ∈ (self : II (ι := ι) )) := by simp [Membership.mem]; infer_instance +instance IC.instDecidableMem : Decidable (i ∈ (self : IC (ι := ι) r )) := by simp [Membership.mem]; infer_instance +instance IO.instDecidableMem : Decidable (i ∈ (self : IO (ι := ι) r )) := by simp [Membership.mem]; infer_instance +instance CI.instDecidableMem : Decidable (i ∈ (self : CI (ι := ι) l )) := by simp [Membership.mem]; infer_instance +instance OI.instDecidableMem : Decidable (i ∈ (self : OI (ι := ι) l )) := by simp [Membership.mem]; infer_instance +instance OO.instDecidableMem : Decidable (i ∈ (self : OO (ι := ι) l r)) := by simp [Membership.mem]; infer_instance +instance CO.instDecidableMem : Decidable (i ∈ (self : CO (ι := ι) l r)) := by simp [Membership.mem]; infer_instance +instance OC.instDecidableMem : Decidable (i ∈ (self : OC (ι := ι) l r)) := by simp [Membership.mem]; infer_instance +instance CC.instDecidableMem : Decidable (i ∈ (self : CC (ι := ι) l r)) := by simp [Membership.mem]; infer_instance + +end + +/-! ## Range Folds -/ + +section +variable [LE ι] [DecidableRel (· ≤ · : ι → ι → Prop)] [LT ι] [DecidableRel (· < · : ι → ι → Prop)] + [Add ι] [One ι] + +def foldlAux (f : β → ι → β) (acc : β) (start stop : ι) : β := aux def ofNth (r : Range) (x : Nat) : Nat := diff --git a/LeanColls/MathlibUpstream.lean b/LeanColls/MathlibUpstream.lean index 2f1f6effb..be8167254 100644 --- a/LeanColls/MathlibUpstream.lean +++ b/LeanColls/MathlibUpstream.lean @@ -236,3 +236,75 @@ theorem List.foldl_product (f : γ → α × β → γ) (init : γ) induction L1 generalizing init <;> simp case cons hd tl ih => rw [ih]; simp [foldl_map] +section LinearOrders + +instance : LinearOrder UInt8 where + decidableLE := inferInstance + le_refl := by + simp [LE.le]; unfold UInt8.le; simp + le_trans := by + simp [LE.le]; unfold UInt8.le + intro a b c; apply Preorder.le_trans + le_antisymm := by + simp [LE.le]; unfold UInt8.le + intro a b hab hba; apply UInt8.ext; apply PartialOrder.le_antisymm <;> assumption + le_total := by + simp [LE.le]; unfold UInt8.le + intro a b; apply LinearOrder.le_total + lt_iff_le_not_le := by + simp [LE.le, LT.lt]; unfold UInt8.le UInt8.lt + intro a b; apply Preorder.lt_iff_le_not_le + +instance : LinearOrder UInt16 where + decidableLE := inferInstance + le_refl := by + simp [LE.le]; unfold UInt16.le + simp + le_trans := by + simp [LE.le]; unfold UInt16.le + intro a b c; apply Preorder.le_trans + le_antisymm := by + simp [LE.le]; unfold UInt16.le + intro a b hab hba; apply UInt16.ext; apply PartialOrder.le_antisymm <;> assumption + le_total := by + simp [LE.le]; unfold UInt16.le + intro a b; apply LinearOrder.le_total + lt_iff_le_not_le := by + simp [LE.le, LT.lt]; unfold UInt16.le UInt16.lt + intro a b; apply Preorder.lt_iff_le_not_le + +instance : LinearOrder UInt32 where + decidableLE := inferInstance + le_refl := by + unfold LE.le; simp [instLEUInt32] + le_trans := by + unfold LE.le; simp [instLEUInt32] + intro a b c; apply Preorder.le_trans + le_antisymm := by + unfold LE.le; simp [instLEUInt32] + intro a b hab hba; apply UInt32.ext; apply PartialOrder.le_antisymm <;> assumption + le_total := by + unfold LE.le; simp [instLEUInt32] + intro a b; apply LinearOrder.le_total + lt_iff_le_not_le := by + unfold LE.le LT.lt; simp only [instLEUInt32, instLTUInt32] + intro a b; apply Preorder.lt_iff_le_not_le + +instance : LinearOrder UInt64 where + decidableLE := inferInstance + le_refl := by + simp [LE.le]; unfold UInt64.le; simp + le_trans := by + simp [LE.le]; unfold UInt64.le + intro a b c; apply Preorder.le_trans + le_antisymm := by + simp [LE.le]; unfold UInt64.le + intro a b hab hba; apply UInt64.ext; apply PartialOrder.le_antisymm <;> assumption + le_total := by + simp [LE.le]; unfold UInt64.le + intro a b; apply LinearOrder.le_total + lt_iff_le_not_le := by + simp [LE.le, LT.lt]; unfold UInt64.le UInt64.lt + intro a b; apply Preorder.lt_iff_le_not_le + +end LinearOrders From 9a2a7b0e909b2b1153a2361178ad75787fe14f1b Mon Sep 17 00:00:00 2001 From: James Date: Mon, 25 Mar 2024 03:10:56 -0400 Subject: [PATCH 3/5] screaming --- LeanColls/Data/Range.lean | 304 ++++++++++++++++++++------------------ 1 file changed, 160 insertions(+), 144 deletions(-) diff --git a/LeanColls/Data/Range.lean b/LeanColls/Data/Range.lean index cdd71545d..e8267e1d0 100644 --- a/LeanColls/Data/Range.lean +++ b/LeanColls/Data/Range.lean @@ -101,151 +101,167 @@ instance CC.instDecidableMem : Decidable (i ∈ (self : CC (ι := ι) l r)) := b end +/-! ## Range Stepping -/ + +/-- Step function for range types. +`step i = i'` should be the smallest `i'` s.t. `i < i'`. +-/ +class Step (ι : Type u) where + step : ι → ι + +class LawfulStep (ι) [Step ι] [LT ι] [LE ι] where + step_minimal : ∀ i : ι, (∃ i', i < i') → ∀ i', i < i' → Step.step i ≤ i' + +instance : Step Nat where + step := Nat.succ + +instance : LawfulStep Nat where + step_minimal := by + rintro i - i'' hi'' + exact hi'' + +instance : Step (Fin n) where + step := fun i => + have : n > 0 := Nat.lt_of_le_of_lt (Nat.zero_le _) i.isLt + ⟨(i+1) % n, Nat.mod_lt _ this⟩ + +instance : LawfulStep (Fin n) where + step_minimal := by + rintro i - i'' hi'' + cases i; cases i'' + simp_all [Step.step] + rw [Nat.mod_eq_of_lt] + · assumption + · omega + /-! ## Range Folds -/ -section -variable [LE ι] [DecidableRel (· ≤ · : ι → ι → Prop)] [LT ι] [DecidableRel (· < · : ι → ι → Prop)] - [Add ι] [One ι] - -def foldlAux (f : β → ι → β) (acc : β) (start stop : ι) : β := - aux - -def ofNth (r : Range) (x : Nat) : Nat := - (x - r.start) / r.step - -theorem ofNth_nth (r : Range) (i : Nat) - : ofNth r (nth r i) = i := by - simp [nth, ofNth] - -theorem nth_ofNth {r : Range} {x : Nat} (h : x ∈ r) - : nth r (ofNth r x) = x := by - simp [mem_def] at h - simp [nth, ofNth] - rw [Nat.div_mul_cancel h.2.2] - simp only [*, ge_iff_le, add_tsub_cancel_of_le] - -def size (r : Range) : Nat := - (r.stop - r.start + r.step - 1) / r.step - -instance : Size Range where - size := size - -theorem nth_lt_stop_iff_lt_size (r : Range) (i : Nat) - : nth r i < r.stop ↔ i < size r := by - simp [nth, size, Nat.lt_iff_add_one_le, - Nat.le_div_iff_mul_le r.step_pos] - zify; simp - constructor <;> intro h <;> linarith - -@[simp] theorem nth_mem_iff_lt_size (r : Range) (i : Nat) - : nth r i ∈ r ↔ i < size r := by - simp [mem_def, nth_lt_stop_iff_lt_size] - -theorem nth_size_eq_stop (r : Range) (h : r.step = 1) - : r.nth r.size = r.stop := by - simp [nth, size, h] - -theorem nth_size_lt (r : Range) - : r.nth r.size < r.stop + r.step := by - simp [nth, size] - rw [Nat.add_comm, Nat.lt_iff_add_one_le, Nat.add_assoc] - apply Nat.add_le_of_le_sub - · apply Nat.add_le_add; simp; apply r.step_pos - convert Nat.div_mul_le_self _ _ using 1 - rw [Nat.add_comm, Nat.sub_add_eq, - Nat.add_sub_assoc r.start_le_stop, - Nat.add_comm, - Nat.add_sub_assoc r.step_pos] - - -def empty (start := 0) : Range where - start := start - stop := start - step_pos := by simp - start_le_stop := by simp - -@[inline] def isEmpty (r : Range) : Bool := - r.start = r.stop - -theorem size_eq_zero_iff_isEmpty (r : Range) - : r.size = 0 ↔ r.isEmpty := by - simp [size, isEmpty] - rw [Nat.div_eq_zero_iff r.step_pos, - Nat.lt_iff_add_one_le, - Nat.sub_add_cancel] - · simp - constructor <;> intro h - · apply Nat.le_antisymm - exact r.start_le_stop - have := (Nat.sub_eq_iff_eq_add r.start_le_stop).mp h - simp [this] - · simp [h] - · exact le_add_left r.step_pos - - -def get (r : Range) (i : Fin (size r)) : Nat := nth r i - -theorem get_mem (r : Range) (i) : get r i ∈ r := by - rcases i with ⟨i,hi⟩ - simp [get, mem_def, nth_lt_stop_iff_lt_size] - simp [nth, hi] - -theorem mem_iff_exists_get (r : Range) : x ∈ r ↔ ∃ i, x = get r i := by - constructor - · intro h - have := nth_ofNth h - rw [← this] at h ⊢; clear this - simp at h - use ⟨_,h⟩ - rfl - · rintro ⟨⟨i,hi⟩,rfl⟩ - simp [get, hi] - - -def foldl (r : Range) (f : α → Nat → α) (init : α) : α := - aux r.start (fun h => by simp_all [mem_def]) init -where - aux i (hi : i < r.stop → i ∈ r) (acc : α) := - if h : i < r.stop then - have := r.step_pos - have : r.stop - (i + r.step) < r.stop - i := by - rw [Nat.sub_add_eq]; apply Nat.sub_lt - repeat simp [*] - aux (i + r.step) (fun h => by - simp_all [mem_def]; rcases hi with ⟨left,right⟩ - constructor - · apply le_add_right; assumption - · rw [Nat.sub_add_comm left]; simp [*] - ) (f acc i) +class WellFoundedStepLE (ι) [Step ι] [LE ι] where + wf_step_le : ∀ stop, WellFounded (fun (x y : ι) => x ≤ stop ∧ Step.step y = x) + +class WellFoundedStepLT (ι) [Step ι] [LT ι] where + wf_step_lt : ∀ stop, WellFounded (fun (x y : ι) => x < stop ∧ Step.step y = x) + +instance : WellFoundedStepLE Nat where + wf_step_le stop := by + constructor + intro x + simp [Step.step] + if hx : ¬(x ≤ stop) then + constructor + intro y ⟨h,rfl⟩ + exfalso; apply hx (Nat.le_of_succ_le h) else - acc -termination_by r.stop - i - -instance : Fold Range Nat where - fold := foldl - -def foldl' (r : Range) (f : α → (i : Nat) → i ∈ r → α) (init : α) : α := - aux r.start (fun h => by simp_all [mem_def]) init -where - aux i (hi : i < r.stop → i ∈ r) (acc : α) := - if h : i < r.stop then - have := r.step_pos - have : r.stop - (i + r.step) < r.stop - i := by - rw [Nat.sub_add_eq]; apply Nat.sub_lt - repeat simp [*] - aux (i + r.step) (fun h => by - simp_all [mem_def]; rcases hi with ⟨left,right⟩ - constructor - · apply le_add_right; assumption - · rw [Nat.sub_add_comm left]; simp [*] - ) (f acc i (hi h)) + simp at hx + let diff := stop - x + have : x = stop - diff := by + simp only; rw [Nat.sub_sub_self hx] + rw [this]; clear hx this + have : diff ≤ stop := by omega + clear_value diff + induction diff with + | zero => + constructor + rintro - ⟨h,rfl⟩ + exfalso + simp at h; exact Nat.not_succ_le_self _ h + | succ i ih => + constructor + rintro - ⟨-,rfl⟩ + have : (stop - i.succ).succ = (stop - i) := by omega + rw [this]; clear this + apply ih + omega + +instance : WellFoundedStepLT Nat where + wf_step_lt stop := by + constructor + intro x + simp [Step.step] + if hx : ¬(x < stop) then + constructor + intro y ⟨h,rfl⟩ + exfalso; apply hx (Nat.le_of_succ_le h) else - acc -termination_by r.stop - i - -theorem fold_def (r : Range) (f : β → Nat → β) - : fold r f init = - Fin.foldl (r.size) (fun acc i => f acc (r.get i)) init - := by - simp [fold, foldl, Fin.foldl] - sorry -- TODO + simp at hx + let diff := stop - x + have : x = stop - diff := by + rw [Nat.sub_sub_self]; exact Nat.le_of_lt hx + rw [this]; clear hx this + have : diff ≤ stop := by omega + clear_value diff + induction diff with + | zero => + constructor + rintro - ⟨h,rfl⟩ + exfalso + simp at h; exact Nat.not_succ_le_self _ (Nat.le_of_lt h) + | succ i ih => + constructor + rintro - ⟨-,rfl⟩ + have : (stop - i.succ).succ = (stop - i) := by omega + rw [this]; clear this + apply ih + omega + +structure StepToLE (ι : Type u) where + (start stop : ι) + +instance [Step ι] [LE ι] [WellFoundedStepLE ι] : WellFoundedRelation (StepToLE ι) where + rel := fun ⟨start,stop⟩ ⟨start',stop'⟩ => + stop = stop' ∧ Step.step start' = start ∧ start ≤ stop + wf := by + constructor + rintro ⟨start,stop⟩ + simp + have ⟨this⟩ := WellFoundedStepLE.wf_step_le stop + specialize this start + induction this with + | intro start _h ih => + constructor + rintro ⟨start', stop'⟩ + simp_all + +structure StepToLT (ι : Type u) where + (start stop : ι) + +instance [Step ι] [LT ι] [WellFoundedStepLT ι] : WellFoundedRelation (StepToLT ι) where + rel := fun ⟨start,stop⟩ ⟨start',stop'⟩ => + stop = stop' ∧ Step.step start' = start ∧ start < stop + wf := by + constructor + rintro ⟨start,stop⟩ + simp + have ⟨this⟩ := WellFoundedStepLT.wf_step_lt stop + specialize this start + induction this with + | intro start _h ih => + constructor + rintro ⟨start', stop'⟩ + simp_all + +section +variable [DecidableEq ι] + [LE ι] [DecidableRel (· ≤ · : ι → ι → Prop)] + [LT ι] [DecidableRel (· < · : ι → ι → Prop)] + [Step ι] + +attribute [-instance] instSizeOf + +def foldAuxIncl [LawfulStep ι] [WellFoundedStepLE ι] (stop : ι) (f : β → ι → β) (i : ι) (acc : β) : β := + if h : i < stop then + have := (LawfulStep.step_minimal i) ⟨stop,h⟩ _ h + foldAuxIncl stop f (Step.step i) (f acc i) + else + f acc i +termination_by StepToLE.mk i stop + +def foldAuxExcl [LawfulStep ι] [WellFoundedStepLE ι] (stop : ι) (f : β → ι → β) (i : ι) (acc : β) : β := + if h : i < stop then + have := (LawfulStep.step_minimal i) ⟨stop,h⟩ _ h + foldAuxExcl stop f (Step.step i) (f acc i) + else + acc +termination_by StepToLE.mk i stop + +end From 27d63c86c9d8a72a52eb6a84d5bc532130858c9a Mon Sep 17 00:00:00 2001 From: James Gallicchio Date: Wed, 27 Mar 2024 15:59:48 -0400 Subject: [PATCH 4/5] almost have range fold! --- LeanColls/Data/Range.lean | 212 ++++++++++++++++++++------------- LeanColls/MathlibUpstream.lean | 12 ++ 2 files changed, 138 insertions(+), 86 deletions(-) diff --git a/LeanColls/Data/Range.lean b/LeanColls/Data/Range.lean index e8267e1d0..6e5e408f4 100644 --- a/LeanColls/Data/Range.lean +++ b/LeanColls/Data/Range.lean @@ -109,50 +109,62 @@ end class Step (ι : Type u) where step : ι → ι +instance [One ι] [Add ι] : Step ι where + step x := x + 1 + class LawfulStep (ι) [Step ι] [LT ι] [LE ι] where step_minimal : ∀ i : ι, (∃ i', i < i') → ∀ i', i < i' → Step.step i ≤ i' -instance : Step Nat where - step := Nat.succ - instance : LawfulStep Nat where - step_minimal := by +step_minimal := by rintro i - i'' hi'' exact hi'' -instance : Step (Fin n) where - step := fun i => - have : n > 0 := Nat.lt_of_le_of_lt (Nat.zero_le _) i.isLt - ⟨(i+1) % n, Nat.mod_lt _ this⟩ - -instance : LawfulStep (Fin n) where +instance [NeZero n] : LawfulStep (Fin n) where step_minimal := by rintro i - i'' hi'' cases i; cases i'' - simp_all [Step.step] + simp_all [Step.step, Fin.add_def] rw [Nat.mod_eq_of_lt] · assumption · omega -/-! ## Range Folds -/ - -class WellFoundedStepLE (ι) [Step ι] [LE ι] where - wf_step_le : ∀ stop, WellFounded (fun (x y : ι) => x ≤ stop ∧ Step.step y = x) - -class WellFoundedStepLT (ι) [Step ι] [LT ι] where - wf_step_lt : ∀ stop, WellFounded (fun (x y : ι) => x < stop ∧ Step.step y = x) - -instance : WellFoundedStepLE Nat where +instance : LawfulStep UInt8 where + step_minimal := by + rintro ⟨⟨i,hi⟩⟩ - ⟨⟨i',hi'1⟩⟩ hi'2 + simp [ + Step.step, Nat.lt_iff_add_one_le, + instLEUInt8, UInt8.le, + instLTUInt8, UInt8.lt, + UInt8.add_def, Fin.add_def + ] at hi'2 ⊢ + rw [Nat.mod_eq_of_lt] + · exact hi'2 + · calc _ ≤ i' := hi'2 + _ < UInt8.size := hi'1 + +/-- Defines well-founded stepping in terms of accessibility. + +The relation used is `x R y ↔ x = step y ∧ y < stop`. +This way, when `y = stop`, there is no `x` such that `x R y`, +which serves as the base case for the `Acc` predicate. +But when `y < stop`, `step y R y`, +which forms a chain of accessibility to any `x ≤ stop`. + -/ +class WellFoundedStep (ι) [Step ι] extends LinearOrder ι where + wf_step_le : ∀ stop, ∀ x, Acc (fun (x y : ι) => y < stop ∧ Step.step y = x) x + +instance : WellFoundedStep Nat where wf_step_le stop := by - constructor intro x - simp [Step.step] - if hx : ¬(x ≤ stop) then + by_cases hx : x ≤ stop + case neg => constructor - intro y ⟨h,rfl⟩ - exfalso; apply hx (Nat.le_of_succ_le h) - else - simp at hx + rintro - ⟨h,rfl⟩ + exfalso + rw [Preorder.lt_iff_le_not_le] at h + exact hx h.1 + case pos => let diff := stop - x have : x = stop - diff := by simp only; rw [Nat.sub_sub_self hx] @@ -164,104 +176,132 @@ instance : WellFoundedStepLE Nat where constructor rintro - ⟨h,rfl⟩ exfalso - simp at h; exact Nat.not_succ_le_self _ h + simp at h | succ i ih => constructor rintro - ⟨-,rfl⟩ - have : (stop - i.succ).succ = (stop - i) := by omega - rw [this]; clear this + have : (stop - i.succ) + 1 = (stop - i) := by omega + conv => arg 2; simp [Step.step]; rw [this] + clear this apply ih omega -instance : WellFoundedStepLT Nat where - wf_step_lt stop := by - constructor - intro x - simp [Step.step] - if hx : ¬(x < stop) then +instance [NeZero n] : WellFoundedStep (Fin n) where + wf_step_le := by + intro ⟨stop,hstop⟩ ⟨x,hxstop⟩ + by_cases hx : x ≤ stop + case neg => constructor - intro y ⟨h,rfl⟩ - exfalso; apply hx (Nat.le_of_succ_le h) - else + rintro - ⟨h,rfl⟩ + exfalso + rw [Preorder.lt_iff_le_not_le] at h + exact hx h.1 + case pos => simp at hx let diff := stop - x have : x = stop - diff := by - rw [Nat.sub_sub_self]; exact Nat.le_of_lt hx - rw [this]; clear hx this - have : diff ≤ stop := by omega - clear_value diff + rw [Nat.sub_sub_self]; exact hx + have hdiff : diff ≤ stop := by omega + clear_value diff; clear hx + cases this induction diff with | zero => constructor rintro - ⟨h,rfl⟩ exfalso - simp at h; exact Nat.not_succ_le_self _ (Nat.le_of_lt h) + simp_all [Step.step] | succ i ih => constructor rintro - ⟨-,rfl⟩ - have : (stop - i.succ).succ = (stop - i) := by omega - rw [this]; clear this - apply ih - omega - -structure StepToLE (ι : Type u) where - (start stop : ι) - -instance [Step ι] [LE ι] [WellFoundedStepLE ι] : WellFoundedRelation (StepToLE ι) where - rel := fun ⟨start,stop⟩ ⟨start',stop'⟩ => - stop = stop' ∧ Step.step start' = start ∧ start ≤ stop - wf := by - constructor - rintro ⟨start,stop⟩ - simp - have ⟨this⟩ := WellFoundedStepLE.wf_step_le stop - specialize this start - induction this with - | intro start _h ih => + have : stop - i.succ + 1 = (stop - i) := by omega + have : (stop - i.succ + 1) % n = stop - i := by + rw [this]; apply Nat.mod_eq_of_lt + apply Nat.lt_of_le_of_lt; apply Nat.sub_le; exact hstop + convert ih ?_ ?_ + · simp [Step.step, Fin.add_def, this] + · omega + · omega + +instance : WellFoundedStep UInt8 where + wf_step_le := by + intro ⟨stop,hstop⟩ ⟨x,hxstop⟩ + by_cases hx : x ≤ stop + case neg => constructor - rintro ⟨start', stop'⟩ - simp_all - -structure StepToLT (ι : Type u) where + rintro - ⟨h,rfl⟩ + exfalso + rw [Preorder.lt_iff_le_not_le] at h + exact hx h.1 + case pos => + simp at hx + let diff := stop - x + have : x = stop - diff := by + rw [Nat.sub_sub_self]; exact hx + have hdiff : diff ≤ stop := by omega + clear_value diff; clear hx + cases this + induction diff with + | zero => + constructor + rintro - ⟨h,rfl⟩ + exfalso + simp_all [Step.step] + | succ i ih => + constructor + rintro - ⟨-,rfl⟩ + have : stop - i.succ + 1 = (stop - i) := by omega + have : (stop - i.succ + 1) % UInt8.size = stop - i := by + rw [this]; apply Nat.mod_eq_of_lt + apply Nat.lt_of_le_of_lt; apply Nat.sub_le; exact hstop + convert ih ?_ ?_ + · simp [Step.step, UInt8.add_def, Fin.add_def, ← Fin.val_inj]; exact this + · omega + · omega + +structure StepToRel (ι : Type u) where (start stop : ι) -instance [Step ι] [LT ι] [WellFoundedStepLT ι] : WellFoundedRelation (StepToLT ι) where +instance [Step ι] [WellFoundedStep ι] : WellFoundedRelation (StepToRel ι) where rel := fun ⟨start,stop⟩ ⟨start',stop'⟩ => - stop = stop' ∧ Step.step start' = start ∧ start < stop + stop = stop' ∧ Step.step start' = start ∧ start' < stop wf := by constructor rintro ⟨start,stop⟩ simp - have ⟨this⟩ := WellFoundedStepLT.wf_step_lt stop - specialize this start + have := WellFoundedStep.wf_step_le stop start induction this with | intro start _h ih => constructor rintro ⟨start', stop'⟩ + simp + rintro rfl rfl h simp_all +/-! ## Range Folds -/ + section -variable [DecidableEq ι] - [LE ι] [DecidableRel (· ≤ · : ι → ι → Prop)] - [LT ι] [DecidableRel (· < · : ι → ι → Prop)] - [Step ι] +variable [DecidableEq ι] [Step ι] [WellFoundedStep ι] [LawfulStep ι] attribute [-instance] instSizeOf -def foldAuxIncl [LawfulStep ι] [WellFoundedStepLE ι] (stop : ι) (f : β → ι → β) (i : ι) (acc : β) : β := - if h : i < stop then - have := (LawfulStep.step_minimal i) ⟨stop,h⟩ _ h - foldAuxIncl stop f (Step.step i) (f acc i) +def foldIncl (stop : ι) (f : β → ι → β) (i : ι) (acc : β) : β := + if i ≤ stop then + aux i acc else - f acc i -termination_by StepToLE.mk i stop + acc +where + aux (i acc) := + if i < stop then + aux (Step.step i) (f acc i) + else + f acc i + termination_by StepToRel.mk i stop -def foldAuxExcl [LawfulStep ι] [WellFoundedStepLE ι] (stop : ι) (f : β → ι → β) (i : ι) (acc : β) : β := - if h : i < stop then - have := (LawfulStep.step_minimal i) ⟨stop,h⟩ _ h - foldAuxExcl stop f (Step.step i) (f acc i) +def foldExcl (stop : ι) (f : β → ι → β) (i : ι) (acc : β) : β := + if i < stop then + foldExcl stop f (Step.step i) (f acc i) else acc -termination_by StepToLE.mk i stop +termination_by StepToRel.mk i stop end diff --git a/LeanColls/MathlibUpstream.lean b/LeanColls/MathlibUpstream.lean index be8167254..af67ac8de 100644 --- a/LeanColls/MathlibUpstream.lean +++ b/LeanColls/MathlibUpstream.lean @@ -236,6 +236,18 @@ theorem List.foldl_product (f : γ → α × β → γ) (init : γ) induction L1 generalizing init <;> simp case cons hd tl ih => rw [ih]; simp [foldl_map] + +section UIntFacts + +theorem UInt8.add_def (i j : UInt8) : i + j = ⟨i.val + j.val⟩ := rfl +theorem UInt16.add_def (i j : UInt16) : i + j = ⟨i.val + j.val⟩ := rfl +theorem UInt32.add_def (i j : UInt32) : i + j = ⟨i.val + j.val⟩ := rfl +theorem UInt64.add_def (i j : UInt64) : i + j = ⟨i.val + j.val⟩ := rfl + +theorem UInt8.toNat_ofNat (n : Nat) : (OfNat.ofNat n : UInt8).toNat = n % UInt8.size := rfl + +end UIntFacts + section LinearOrders instance : LinearOrder UInt8 where From b5599df313b856e59316421504681997e2b63e66 Mon Sep 17 00:00:00 2001 From: James Gallicchio Date: Wed, 27 Mar 2024 16:19:47 -0400 Subject: [PATCH 5/5] implement all the range folds --- LeanColls/Data/Range.lean | 27 +++++++++++++++++++++++++++ LeanColls/MathlibUpstream.lean | 24 ++++++++++++++++++++++++ 2 files changed, 51 insertions(+) diff --git a/LeanColls/Data/Range.lean b/LeanColls/Data/Range.lean index 6e5e408f4..4b4914246 100644 --- a/LeanColls/Data/Range.lean +++ b/LeanColls/Data/Range.lean @@ -304,4 +304,31 @@ def foldExcl (stop : ι) (f : β → ι → β) (i : ι) (acc : β) : β := acc termination_by StepToRel.mk i stop +@[inline] def CC.foldl (_self : CC (ι := ι) l r) (f : β → ι → β) (acc : β) : β := + foldIncl r f l acc + +@[inline] def OC.foldl (_self : OC (ι := ι) l r) (f : β → ι → β) (acc : β) : β := + foldIncl r f (Step.step l) acc + +@[inline] def CO.foldl (_self : CO (ι := ι) l r) (f : β → ι → β) (acc : β) : β := + foldExcl r f l acc + +@[inline] def OO.foldl (_self : OO (ι := ι) l r) (f : β → ι → β) (acc : β) : β := + foldExcl r f (Step.step l) acc + +@[inline] def CI.foldl [Top ι] (_self : CI (ι := ι) l ) (f : β → ι → β) (acc : β) : β := + foldIncl ⊤ f l acc + +@[inline] def OI.foldl [Top ι] (_self : OI (ι := ι) l ) (f : β → ι → β) (acc : β) : β := + foldIncl ⊤ f (Step.step l) acc + +@[inline] def IC.foldl [Bot ι] (_self : IC (ι := ι) r ) (f : β → ι → β) (acc : β) : β := + foldIncl r f ⊥ acc + +@[inline] def IO.foldl [Bot ι] (_self : IO (ι := ι) r ) (f : β → ι → β) (acc : β) : β := + foldExcl r f ⊥ acc + +@[inline] def II.foldl [Top ι] [Bot ι] (_self : II (ι := ι) ) (f : β → ι → β) (acc : β) : β := + foldIncl ⊤ f ⊥ acc + end diff --git a/LeanColls/MathlibUpstream.lean b/LeanColls/MathlibUpstream.lean index af67ac8de..340d2274c 100644 --- a/LeanColls/MathlibUpstream.lean +++ b/LeanColls/MathlibUpstream.lean @@ -319,4 +319,28 @@ instance : LinearOrder UInt64 where simp [LE.le, LT.lt]; unfold UInt64.le UInt64.lt intro a b; apply Preorder.lt_iff_le_not_le +instance : BoundedOrder UInt8 where + top := ⟨⊤⟩ + le_top := by rintro ⟨x⟩; simp [instLEUInt8, UInt8.le] + bot := ⟨⊥⟩ + bot_le := by rintro ⟨x⟩; simp [instLEUInt8, UInt8.le] + +instance : BoundedOrder UInt16 where + top := ⟨⊤⟩ + le_top := by rintro ⟨x⟩; simp [instLEUInt16, UInt16.le] + bot := ⟨⊥⟩ + bot_le := by rintro ⟨x⟩; simp [instLEUInt16, UInt16.le] + +instance : BoundedOrder UInt32 where + top := ⟨⊤⟩ + le_top := by rintro ⟨x⟩; simp [instLEUInt32] + bot := ⟨⊥⟩ + bot_le := by rintro ⟨x⟩; simp [instLEUInt32] + +instance : BoundedOrder UInt64 where + top := ⟨⊤⟩ + le_top := by rintro ⟨x⟩; simp [instLEUInt64, UInt64.le] + bot := ⟨⊥⟩ + bot_le := by rintro ⟨x⟩; simp [instLEUInt64, UInt64.le] + end LinearOrders