refactor: move well-founded relations used by the iterators to init (#9095)
This PR moves the construction of the `Option.SomeLtNone.lt` (and `le`) relation, in which `some` is less than `none`, to `Init.Data.Option.Basic` and moves well-foundedness proofs for `Option.lt` and `Option.SomeLtNone.lt` into `Init.Data.Option.Lemmas`.
This commit is contained in:
Paul Reichert
GitHub
parent
c9dea51f7a
commit
c231b742ca
4 changed files with 84 additions and 79 deletions
|
|
@ -258,6 +258,55 @@ instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
|
|||
| some _, none => isFalse not_false
|
||||
| none, none => isFalse not_false
|
||||
|
||||
namespace SomeLtNone
|
||||
|
||||
/--
|
||||
Lifts an ordering relation to `Option` such that `none` is the *greatest* element.
|
||||
|
||||
It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
|
||||
and `β`.
|
||||
|
||||
Caution: Given `LT α`, `Option.SomeLtNone.lt LT.lt` differs from the `LT (Option α)` instance,
|
||||
which is implemented by `Option.lt Lt.lt`.
|
||||
|
||||
Examples:
|
||||
* `Option.lt (fun n k : Nat => n < k) none none = False`
|
||||
* `Option.lt (fun n k : Nat => n < k) none (some 3) = False`
|
||||
* `Option.lt (fun n k : Nat => n < k) (some 3) none = True`
|
||||
* `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
|
||||
* `Option.le (fun n k : Nat => n < k) (some 5) (some 4) = False`
|
||||
* `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
|
||||
-/
|
||||
def lt {α} (r : α → β → Prop) : Option α → Option β → Prop
|
||||
| none, _ => False
|
||||
| some _, none => True
|
||||
| some x, some y => r x y
|
||||
|
||||
/--
|
||||
Lifts an ordering relation to `Option` such that `none` is the *greatest* element.
|
||||
|
||||
It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
|
||||
and `β`.
|
||||
|
||||
Caution: Given `LE α`, `Option.SomeLtNone.le LE.le` differs from the `LE (Option α)` instance,
|
||||
which is implemented by `Option.le LE.le`.
|
||||
|
||||
Examples:
|
||||
* `Option.le (fun n k : Nat => n < k) none none = True`
|
||||
* `Option.le (fun n k : Nat => n < k) none (some 3) = False`
|
||||
* `Option.le (fun n k : Nat => n < k) (some 3) none = True`
|
||||
* `Option.le (fun n k : Nat => n < k) (some 4) (some 5) = True`
|
||||
* `Option.le (fun n k : Nat => n < k) (some 5) (some 4) = False`
|
||||
* `Option.le (fun n k : Nat => n < k) (some 4) (some 4) = True`
|
||||
-/
|
||||
def le {α} (r : α → β → Prop) : Option α → Option β → Prop
|
||||
| none, none => True
|
||||
| none, some _ => False
|
||||
| some _, none => True
|
||||
| some x, some y => r x y
|
||||
|
||||
end SomeLtNone
|
||||
|
||||
/--
|
||||
Applies a function to a two optional values if both are present. Otherwise, if one value is present,
|
||||
it is returned and the function is not used.
|
||||
|
|
|
|||
|
|
@ -1922,4 +1922,38 @@ theorem map_min [Min α] [Min β] {o o' : Option α} {f : α → β} (hf : ∀ x
|
|||
(min o o').map f = min (o.map f) (o'.map f) := by
|
||||
cases o <;> cases o' <;> simp [*]
|
||||
|
||||
theorem wellFounded_lt {α} {rel : α → α → Prop} (h : WellFounded rel) :
|
||||
WellFounded (Option.lt rel) := by
|
||||
refine ⟨fun x => ?_⟩
|
||||
have hn : Acc (Option.lt rel) none := by
|
||||
refine Acc.intro none ?_
|
||||
intro y hyx
|
||||
cases y <;> cases hyx
|
||||
cases x
|
||||
· exact hn
|
||||
· rename_i x
|
||||
induction h.apply x
|
||||
rename_i _ _ ih
|
||||
refine Acc.intro _ (fun y hy => ?_)
|
||||
cases y
|
||||
· exact hn
|
||||
· exact ih _ hy
|
||||
|
||||
theorem SomeLtNone.wellFounded_lt {α} {r : α → α → Prop} (h : WellFounded r) :
|
||||
WellFounded (SomeLtNone.lt r) := by
|
||||
refine ⟨?_⟩
|
||||
intro x
|
||||
constructor
|
||||
intro x' hlt
|
||||
match x' with
|
||||
| none => contradiction
|
||||
| some x' =>
|
||||
clear hlt
|
||||
induction h.apply x'
|
||||
rename_i ih
|
||||
refine Acc.intro _ (fun x'' hlt' => ?_)
|
||||
match x'' with
|
||||
| none => contradiction
|
||||
| some x'' => exact ih x'' hlt'
|
||||
|
||||
end Option
|
||||
|
|
|
|||
|
|
@ -18,73 +18,6 @@ This file provides an iterator combinator `IterM.zip` that combines two iterator
|
|||
of pairs.
|
||||
-/
|
||||
|
||||
namespace Std.Internal.Option
|
||||
|
||||
/- TODO: move this to Init.Data.Option -/
|
||||
namespace SomeLtNone
|
||||
|
||||
/--
|
||||
Lifts an ordering relation to `Option`, such that `none` is the greatest element.
|
||||
|
||||
It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
|
||||
and `β`.
|
||||
|
||||
Caution: Given `LT α`, `Option.SomeLtNone.lt LT.lt` differs from the `LT (Option α)` instance,
|
||||
which is implemented by `Option.lt Lt.lt`.
|
||||
|
||||
Examples:
|
||||
* `Option.lt (fun n k : Nat => n < k) none none = False`
|
||||
* `Option.lt (fun n k : Nat => n < k) none (some 3) = False`
|
||||
* `Option.lt (fun n k : Nat => n < k) (some 3) none = True`
|
||||
* `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
|
||||
* `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
|
||||
-/
|
||||
def lt {α} (r : α → α → Prop) : Option α → Option α → Prop
|
||||
| none, _ => false
|
||||
| some _, none => true
|
||||
| some a', some a => r a' a
|
||||
|
||||
end SomeLtNone
|
||||
|
||||
/- TODO: Move these to Init.Data.Option.Lemmas in a separate PR -/
|
||||
theorem wellFounded_lt {α} {rel : α → α → Prop} (h : WellFounded rel) :
|
||||
WellFounded (Option.lt rel) := by
|
||||
refine ⟨fun x => ?_⟩
|
||||
have hn : Acc (Option.lt rel) none := by
|
||||
refine Acc.intro none ?_
|
||||
intro y hyx
|
||||
cases y <;> cases hyx
|
||||
cases x
|
||||
· exact hn
|
||||
· rename_i x
|
||||
induction h.apply x
|
||||
rename_i x' h ih
|
||||
refine Acc.intro _ ?_
|
||||
intro y hyx'
|
||||
cases y
|
||||
· exact hn
|
||||
· exact ih _ hyx'
|
||||
|
||||
theorem SomeLtNone.wellFounded_lt {α} {r : α → α → Prop} (h : WellFounded r) :
|
||||
WellFounded (SomeLtNone.lt r) := by
|
||||
refine ⟨?_⟩
|
||||
intro x
|
||||
constructor
|
||||
intro x' hlt
|
||||
match x' with
|
||||
| none => contradiction
|
||||
| some x' =>
|
||||
clear hlt
|
||||
induction h.apply x'
|
||||
rename_i ih
|
||||
constructor
|
||||
intro x'' hlt'
|
||||
match x'' with
|
||||
| none => contradiction
|
||||
| some x'' => exact ih x'' hlt'
|
||||
|
||||
end Std.Internal.Option
|
||||
|
||||
namespace Std.Iterators
|
||||
open Std.Internal
|
||||
|
||||
|
|
|
|||
|
|
@ -131,23 +131,12 @@ theorem _root_.Array.toList_iterM [LawfulMonad m] {array : Array β} :
|
|||
(array.iterM m).toList = pure array.toList := by
|
||||
simp [Array.iterM_eq_iterFromIdxM, Array.toList_iterFromIdxM]
|
||||
|
||||
-- Move to Init.Data.Array.Lemmas in a separate PR afterwards
|
||||
private theorem drop_toArray' {l : List α} {k : Nat} :
|
||||
l.toArray.drop k = (l.drop k).toArray := by
|
||||
induction l generalizing k
|
||||
case nil => simp
|
||||
case cons l' ih =>
|
||||
match k with
|
||||
| 0 => simp
|
||||
| k' + 1 => simp [List.drop_succ_cons, ← ih]
|
||||
|
||||
@[simp]
|
||||
theorem _root_.Array.toArray_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} :
|
||||
(array.iterFromIdxM m pos).toArray = pure (array.extract pos) := by
|
||||
simp [← IterM.toArray_toList, Array.toList_iterFromIdxM]
|
||||
rw [← Array.drop_eq_extract]
|
||||
rw (occs := [2]) [← Array.toArray_toList (xs := array)]
|
||||
rw [drop_toArray']
|
||||
rw [← List.toArray_drop]
|
||||
|
||||
@[simp]
|
||||
theorem _root_.Array.toArray_toIterM [LawfulMonad m] {array : Array β} :
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue