feat: remove unnecessary decidability requirements (#9096)
This PR removes some unnecessary `Decidable*` instance arguments by using lemmas in the `Classical` namespace instead of the `Decidable` namespace. This might lead to some additional dependency on classical axioms, but large parts of the standard library are relying on them either way.
This commit is contained in:
Paul Reichert
GitHub
parent
561f347f5a
commit
84cd2c49eb
4 changed files with 61 additions and 57 deletions
|
|
@ -26,9 +26,9 @@ namespace Array
|
|||
@[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
|
||||
|
||||
protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
|
||||
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
|
||||
protected theorem not_le_iff_gt [LT α] {xs ys : Array α} :
|
||||
¬ xs ≤ ys ↔ ys < xs :=
|
||||
Decidable.not_not
|
||||
Classical.not_not
|
||||
|
||||
@[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
|
||||
simp [lex]
|
||||
|
|
@ -94,7 +94,7 @@ instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
|
|||
Trans (· < · : Array α → Array α → Prop) (· < ·) (· < ·) where
|
||||
trans h₁ h₂ := Array.lt_trans h₁ h₂
|
||||
|
||||
protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem lt_of_le_of_lt [LT α]
|
||||
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
|
||||
[i₁ : Std.Asymm (· < · : α → α → Prop)]
|
||||
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -102,7 +102,7 @@ protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
|||
{xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
|
||||
List.lt_of_le_of_lt h₁ h₂
|
||||
|
||||
protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_trans [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -110,7 +110,7 @@ protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
|
|||
{xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
|
||||
fun h₃ => h₁ (Array.lt_of_le_of_lt h₂ h₃)
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -122,34 +122,34 @@ protected theorem lt_asymm [LT α]
|
|||
[i : Std.Asymm (· < · : α → α → Prop)]
|
||||
{xs ys : Array α} (h : xs < ys) : ¬ ys < xs := List.lt_asymm h
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Asymm (· < · : α → α → Prop)] :
|
||||
Std.Asymm (· < · : Array α → Array α → Prop) where
|
||||
asymm _ _ := Array.lt_asymm
|
||||
|
||||
protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_total [LT α]
|
||||
[i : Std.Total (¬ · < · : α → α → Prop)] (xs ys : Array α) : xs ≤ ys ∨ ys ≤ xs :=
|
||||
List.le_total xs.toList ys.toList
|
||||
|
||||
@[simp] protected theorem not_lt [LT α]
|
||||
{xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
|
||||
|
||||
@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
|
||||
{xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Decidable.not_not
|
||||
@[simp] protected theorem not_le [LT α]
|
||||
{xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
|
||||
|
||||
protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_of_lt [LT α]
|
||||
[i : Std.Total (¬ · < · : α → α → Prop)]
|
||||
{xs ys : Array α} (h : xs < ys) : xs ≤ ys :=
|
||||
List.le_of_lt h
|
||||
|
||||
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_iff_lt_or_eq [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
[Std.Total (¬ · < · : α → α → Prop)]
|
||||
{xs ys : Array α} : xs ≤ ys ↔ xs < ys ∨ xs = ys := by
|
||||
simpa using List.le_iff_lt_or_eq (l₁ := xs.toList) (l₂ := ys.toList)
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Total (¬ · < · : α → α → Prop)] :
|
||||
Std.Total (· ≤ · : Array α → Array α → Prop) where
|
||||
total := Array.le_total
|
||||
|
|
@ -218,7 +218,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
|
|||
cases l₂
|
||||
simp_all [List.lex_eq_false_iff_exists]
|
||||
|
||||
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
|
||||
protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
|
||||
xs < ys ↔
|
||||
(xs = ys.take xs.size ∧ xs.size < ys.size) ∨
|
||||
(∃ (i : Nat) (h₁ : i < xs.size) (h₂ : i < ys.size),
|
||||
|
|
@ -228,7 +228,7 @@ protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {xs ys
|
|||
cases ys
|
||||
simp [List.lt_iff_exists]
|
||||
|
||||
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_iff_exists [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Array α} :
|
||||
|
|
@ -248,7 +248,7 @@ theorem append_left_lt [LT α] {xs ys zs : Array α} (h : ys < zs) :
|
|||
cases zs
|
||||
simpa using List.append_left_lt h
|
||||
|
||||
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
|
||||
theorem append_left_le [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -272,7 +272,7 @@ protected theorem map_lt [LT α] [LT β]
|
|||
cases ys
|
||||
simpa using List.map_lt w h
|
||||
|
||||
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
|
||||
protected theorem map_le [LT α] [LT β]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
|
|||
|
|
@ -362,12 +362,13 @@ theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel
|
|||
· exact h₁ (Lex.rel hba)
|
||||
· exact eq (antisymm _ _ hab hba)
|
||||
|
||||
protected theorem le_antisymm [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_antisymm [LT α]
|
||||
[i : Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
{as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
|
||||
open Classical in
|
||||
not_lex_antisymm i.antisymm h₁ h₂
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[s : Std.Antisymm (¬ · < · : α → α → Prop)] :
|
||||
Std.Antisymm (· ≤ · : List α → List α → Prop) where
|
||||
antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂
|
||||
|
|
|
|||
|
|
@ -22,9 +22,9 @@ namespace List
|
|||
@[simp] theorem not_lex_lt [LT α] {l₁ l₂ : List α} : ¬ Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁ := Iff.rfl
|
||||
|
||||
protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
|
||||
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
|
||||
protected theorem not_le_iff_gt [LT α] {l₁ l₂ : List α} :
|
||||
¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
|
||||
Decidable.not_not
|
||||
Classical.not_not
|
||||
|
||||
theorem lex_irrefl {r : α → α → Prop} (irrefl : ∀ x, ¬r x x) (l : List α) : ¬Lex r l l := by
|
||||
induction l with
|
||||
|
|
@ -78,13 +78,14 @@ theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂
|
|||
¬ Lex r (a :: l₁) (b :: l₂) ↔ (¬ r a b ∧ a ≠ b) ∨ (¬ r a b ∧ ¬ Lex r l₁ l₂) := by
|
||||
rw [cons_lex_cons_iff, not_or, Decidable.not_and_iff_or_not, and_or_left]
|
||||
|
||||
theorem cons_le_cons_iff [DecidableEq α] [LT α] [DecidableLT α]
|
||||
theorem cons_le_cons_iff [LT α]
|
||||
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
|
||||
[i₁ : Std.Asymm (· < · : α → α → Prop)]
|
||||
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
{a b} {l₁ l₂ : List α} :
|
||||
(a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂ := by
|
||||
dsimp only [instLE, instLT, List.le, List.lt]
|
||||
open Classical in
|
||||
simp only [not_cons_lex_cons_iff, ne_eq]
|
||||
constructor
|
||||
· rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
|
||||
|
|
@ -104,7 +105,7 @@ theorem cons_le_cons_iff [DecidableEq α] [LT α] [DecidableLT α]
|
|||
· right
|
||||
exact ⟨fun w => i₀.irrefl _ (h₁ ▸ w), h₂⟩
|
||||
|
||||
theorem not_lt_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
|
||||
theorem not_lt_of_cons_le_cons [LT α]
|
||||
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
|
||||
[i₁ : Std.Asymm (· < · : α → α → Prop)]
|
||||
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -114,7 +115,7 @@ theorem not_lt_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
|
|||
· exact i₁.asymm _ _ h
|
||||
· exact i₀.irrefl _
|
||||
|
||||
theorem le_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
|
||||
theorem le_of_cons_le_cons [LT α]
|
||||
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
|
||||
[i₁ : Std.Asymm (· < · : α → α → Prop)]
|
||||
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -165,7 +166,7 @@ instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
|
|||
@[deprecated List.le_antisymm (since := "2024-12-13")]
|
||||
protected abbrev lt_antisymm := @List.le_antisymm
|
||||
|
||||
protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem lt_of_le_of_lt [LT α]
|
||||
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
|
||||
[i₁ : Std.Asymm (· < · : α → α → Prop)]
|
||||
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -180,7 +181,7 @@ protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
|||
| cons c l₁ =>
|
||||
apply Lex.rel
|
||||
replace h₁ := not_lt_of_cons_le_cons h₁
|
||||
apply Decidable.byContradiction
|
||||
apply Classical.byContradiction
|
||||
intro h₂
|
||||
have := i₃.trans h₁ h₂
|
||||
contradiction
|
||||
|
|
@ -193,9 +194,9 @@ protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
|||
by_cases w₅ : a = c
|
||||
· subst w₅
|
||||
exact Lex.cons (ih (le_of_cons_le_cons h₁))
|
||||
· exact Lex.rel (Decidable.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))
|
||||
· exact Lex.rel (Classical.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))
|
||||
|
||||
protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_trans [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -203,7 +204,7 @@ protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
|
|||
{l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
|
||||
fun h₃ => h₁ (List.lt_of_le_of_lt h₂ h₃)
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -231,9 +232,9 @@ instance [LT α] [Std.Asymm (· < · : α → α → Prop)] :
|
|||
Std.Asymm (· < · : List α → List α → Prop) where
|
||||
asymm _ _ := List.lt_asymm
|
||||
|
||||
theorem not_lex_total [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
|
||||
theorem not_lex_total {r : α → α → Prop}
|
||||
(h : ∀ x y : α, ¬ r x y ∨ ¬ r y x) (l₁ l₂ : List α) : ¬ Lex r l₁ l₂ ∨ ¬ Lex r l₂ l₁ := by
|
||||
rw [Decidable.or_iff_not_imp_left, Decidable.not_not]
|
||||
rw [Classical.or_iff_not_imp_left, Classical.not_not]
|
||||
intro w₁ w₂
|
||||
match l₁, l₂, w₁, w₂ with
|
||||
| nil, _ :: _, .nil, w₂ => simp at w₂
|
||||
|
|
@ -246,11 +247,11 @@ theorem not_lex_total [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
|
|||
| _ :: l₁, _ :: l₂, .cons _, .cons _ =>
|
||||
obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradiction
|
||||
|
||||
protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_total [LT α]
|
||||
[i : Std.Total (¬ · < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
|
||||
not_lex_total i.total l₂ l₁
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Total (¬ · < · : α → α → Prop)] :
|
||||
Std.Total (· ≤ · : List α → List α → Prop) where
|
||||
total := List.le_total
|
||||
|
|
@ -258,10 +259,10 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
|
|||
@[simp] protected theorem not_lt [LT α]
|
||||
{l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
|
||||
|
||||
@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
|
||||
{l₁ l₂ : List α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Decidable.not_not
|
||||
@[simp] protected theorem not_le [LT α]
|
||||
{l₁ l₂ : List α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Classical.not_not
|
||||
|
||||
protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_of_lt [LT α]
|
||||
[i : Std.Total (¬ · < · : α → α → Prop)]
|
||||
{l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂ := by
|
||||
obtain (h' | h') := List.le_total l₁ l₂
|
||||
|
|
@ -269,7 +270,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
|||
· exfalso
|
||||
exact h' h
|
||||
|
||||
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_iff_lt_or_eq [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
[Std.Total (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -280,7 +281,7 @@ protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
|
|||
· right
|
||||
apply List.le_antisymm h h'
|
||||
· left
|
||||
exact Decidable.not_not.mp h'
|
||||
exact Classical.not_not.mp h'
|
||||
· rintro (h | rfl)
|
||||
· exact List.le_of_lt h
|
||||
· exact List.le_refl l₁
|
||||
|
|
@ -445,16 +446,17 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
|
|||
simpa using w₁ (j + 1) (by simpa)
|
||||
· simpa using w₂
|
||||
|
||||
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
|
||||
protected theorem lt_iff_exists [LT α] {l₁ l₂ : List α} :
|
||||
l₁ < l₂ ↔
|
||||
(l₁ = l₂.take l₁.length ∧ l₁.length < l₂.length) ∨
|
||||
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
|
||||
(∀ j, (hj : j < i) →
|
||||
l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
|
||||
open Classical in
|
||||
rw [← lex_eq_true_iff_lt, lex_eq_true_iff_exists]
|
||||
simp
|
||||
|
||||
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_iff_exists [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
|
||||
|
|
@ -463,6 +465,7 @@ protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
|
|||
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
|
||||
(∀ j, (hj : j < i) →
|
||||
l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
|
||||
open Classical in
|
||||
rw [← lex_eq_false_iff_ge, lex_eq_false_iff_exists]
|
||||
· simp only [isEqv_eq, beq_iff_eq, decide_eq_true_eq]
|
||||
simp only [eq_comm]
|
||||
|
|
@ -477,7 +480,7 @@ theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
|
|||
| nil => simp [h]
|
||||
| cons a l₁ ih => simp [cons_lt_cons_iff, ih]
|
||||
|
||||
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
|
||||
theorem append_left_le [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -511,7 +514,7 @@ protected theorem map_lt [LT α] [LT β]
|
|||
| cons a l₁, cons b l₂, .rel h =>
|
||||
simp [cons_lt_cons_iff, w, h]
|
||||
|
||||
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
|
||||
protected theorem map_le [LT α] [LT β]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
|
|||
|
|
@ -28,9 +28,9 @@ namespace Vector
|
|||
@[simp] theorem le_toList [LT α] {xs ys : Vector α n} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
|
||||
|
||||
protected theorem not_lt_iff_ge [LT α] {xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
|
||||
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Vector α n} :
|
||||
protected theorem not_le_iff_gt [LT α] {xs ys : Vector α n} :
|
||||
¬ xs ≤ ys ↔ ys < xs :=
|
||||
Decidable.not_not
|
||||
Classical.not_not
|
||||
|
||||
@[simp] theorem mk_lt_mk [LT α] :
|
||||
Vector.mk (α := α) (n := n) data₁ size₁ < Vector.mk data₂ size₂ ↔ data₁ < data₂ := Iff.rfl
|
||||
|
|
@ -92,7 +92,7 @@ instance [LT α]
|
|||
Trans (· < · : Vector α n → Vector α n → Prop) (· < ·) (· < ·) where
|
||||
trans h₁ h₂ := Vector.lt_trans h₁ h₂
|
||||
|
||||
protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem lt_of_le_of_lt [LT α]
|
||||
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
|
||||
[i₁ : Std.Asymm (· < · : α → α → Prop)]
|
||||
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -100,7 +100,7 @@ protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
|||
{xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
|
||||
Array.lt_of_le_of_lt h₁ h₂
|
||||
|
||||
protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_trans [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -108,7 +108,7 @@ protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
|
|||
{xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
|
||||
fun h₃ => h₁ (Vector.lt_of_le_of_lt h₂ h₃)
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -120,16 +120,16 @@ protected theorem lt_asymm [LT α]
|
|||
[i : Std.Asymm (· < · : α → α → Prop)]
|
||||
{xs ys : Vector α n} (h : xs < ys) : ¬ ys < xs := Array.lt_asymm h
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Asymm (· < · : α → α → Prop)] :
|
||||
Std.Asymm (· < · : Vector α n → Vector α n → Prop) where
|
||||
asymm _ _ := Vector.lt_asymm
|
||||
|
||||
protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_total [LT α]
|
||||
[i : Std.Total (¬ · < · : α → α → Prop)] (xs ys : Vector α n) : xs ≤ ys ∨ ys ≤ xs :=
|
||||
Array.le_total _ _
|
||||
|
||||
instance [DecidableEq α] [LT α] [DecidableLT α]
|
||||
instance [LT α]
|
||||
[Std.Total (¬ · < · : α → α → Prop)] :
|
||||
Std.Total (· ≤ · : Vector α n → Vector α n → Prop) where
|
||||
total := Vector.le_total
|
||||
|
|
@ -137,15 +137,15 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
|
|||
@[simp] protected theorem not_lt [LT α]
|
||||
{xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
|
||||
|
||||
@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
|
||||
{xs ys : Vector α n} : ¬ ys ≤ xs ↔ xs < ys := Decidable.not_not
|
||||
@[simp] protected theorem not_le [LT α]
|
||||
{xs ys : Vector α n} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
|
||||
|
||||
protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_of_lt [LT α]
|
||||
[i : Std.Total (¬ · < · : α → α → Prop)]
|
||||
{xs ys : Vector α n} (h : xs < ys) : xs ≤ ys :=
|
||||
Array.le_of_lt h
|
||||
|
||||
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_iff_lt_or_eq [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
[Std.Total (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -210,14 +210,14 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
|
|||
rcases ys with ⟨ys, n₂⟩
|
||||
simp_all [Array.lex_eq_false_iff_exists]
|
||||
|
||||
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Vector α n} :
|
||||
protected theorem lt_iff_exists [LT α] {xs ys : Vector α n} :
|
||||
xs < ys ↔
|
||||
(∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → xs[j] = ys[j]) ∧ xs[i] < ys[i]) := by
|
||||
cases xs
|
||||
cases ys
|
||||
simp_all [Array.lt_iff_exists]
|
||||
|
||||
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
|
||||
protected theorem le_iff_exists [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Vector α n} :
|
||||
|
|
@ -232,7 +232,7 @@ theorem append_left_lt [LT α] {xs : Vector α n} {ys ys' : Vector α m} (h : ys
|
|||
xs ++ ys < xs ++ ys' := by
|
||||
simpa using Array.append_left_lt h
|
||||
|
||||
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
|
||||
theorem append_left_le [LT α]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
@ -245,7 +245,7 @@ protected theorem map_lt [LT α] [LT β]
|
|||
map f xs < map f ys := by
|
||||
simpa using Array.map_lt w h
|
||||
|
||||
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
|
||||
protected theorem map_le [LT α] [LT β]
|
||||
[Std.Irrefl (· < · : α → α → Prop)]
|
||||
[Std.Asymm (· < · : α → α → Prop)]
|
||||
[Std.Antisymm (¬ · < · : α → α → Prop)]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue