From 748aed9fd7b4b810ff8d6882b67d976402e6257e Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Fri, 25 Sep 2026 09:43:10 +0200 Subject: [PATCH] add stuff --- src/Init/Data/Ord/Basic.lean | 45 +++++++++++++++++++++++++++++++++++- src/Init/Prelude.lean | 14 +++++++++++ src/Init/PropLemmas.lean | 17 +++++++++++++- src/Init/SimpLemmas.lean | 24 +++++++++++++++++++ 4 files changed, 98 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Ord/Basic.lean b/src/Init/Data/Ord/Basic.lean index 44ce5fe00b9c..06367b73da37 100644 --- a/src/Init/Data/Ord/Basic.lean +++ b/src/Init/Data/Ord/Basic.lean @@ -96,6 +96,15 @@ Ordering.lt | .eq => b | a => a +/-- +Dependent version of `Ordering.then`. +-/ +@[macro_inline, expose, implicit_reducible] +def dthen (a : Ordering) (b : a = .eq → Ordering) : Ordering := + match a with + | .eq => b rfl + | a => a + /-- Version of `Ordering.then'` for proof by reflection. -/ @[expose] noncomputable def then' (a b : Ordering) : Ordering := Ordering.rec a b a a @@ -252,6 +261,7 @@ theorem isGE_eq_isGT_or_isEq : ∀ {o : Ordering}, o.isGE = (o.isGT || o.isEq) : theorem isEq_eq_beq_eq : ∀ {o : Ordering}, o.isEq = (o == .eq) := by decide theorem isNe_eq_not_beq_eq : ∀ {o : Ordering}, o.isNe = (!o == .eq) := by decide theorem isNe_eq_isLT_or_isGT : ∀ {o : Ordering}, o.isNe = (o.isLT || o.isGT) := by decide +theorem isLE_and_isGE_eq : ∀ {o : Ordering}, (o.isLE && o.isGE) = o.isEq := by decide @[simp] theorem not_isLT_eq_isGE : ∀ {o : Ordering}, (!o.isLT) = o.isGE := by decide @[simp] theorem not_isLE_eq_isGT : ∀ {o : Ordering}, (!o.isLE) = o.isGT := by decide @@ -271,6 +281,9 @@ theorem swap_then : ∀ (o₁ o₂ : Ordering), (o₁.then o₂).swap = o₁.swa theorem then_eq_lt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by decide theorem then_eq_gt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by decide @[simp] theorem then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by decide +theorem then_eq_eq_of_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁ = eq → o₂ = eq → o₁.then o₂ = eq := by decide +theorem left_eq_eq_of_then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq → o₁ = eq := by decide +theorem right_eq_eq_of_then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq → o₂ = eq := by decide theorem isLT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLT = (o₁.isLT || o₁.isEq && o₂.isLT) := by decide theorem isEq_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isEq = (o₁.isEq && o₂.isEq) := by decide @@ -290,7 +303,37 @@ theorem isLE_then_iff_and : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE theorem isLE_left_of_isLE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE → o₁.isLE := by decide theorem isGE_left_of_isGE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGE → o₁.isGE := by decide -theorem isLE_and_isGE_eq : ∀ {o : Ordering}, (o.isLE && o.isGE) = o.isEq := by decide +theorem then_eq_left_iff : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = o₁ ↔ (o₁ = .eq → o₂ = o₁) := by decide +theorem then_eq_right_iff : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = o₂ ↔ (o₁ ≠ .eq → o₂ = o₁) := by decide + +@[congr] theorem dthen_congr {x x' : Ordering} + {y : x = eq → Ordering} {y' : x' = eq → Ordering} + (hx : x = x') (hy : ∀ h, y (hx ▸ h) = y' h) : + x.dthen y = x'.dthen y' := by cases hx; cases funext hy; rfl + +@[simp] theorem dthen_eq_then : ∀ {o₁ o₂ : Ordering}, o₁.dthen (fun _ => o₂) = o₁.then o₂ := by decide + +theorem swap_dthen : ∀ (o₁ : Ordering) (o₂), (o₁.dthen o₂).swap = o₁.swap.dthen (fun h => (o₂ (swap_eq_eq.mp h)).swap) := by decide + +theorem dthen_eq_lt : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = lt ↔ o₁ = lt ∨ ∃ h : o₁ = eq, o₂ h = lt := by decide +theorem dthen_eq_gt : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = gt ↔ o₁ = gt ∨ ∃ h : o₁ = eq, o₂ h = gt := by decide +@[simp] theorem dthen_eq_eq : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = eq ↔ ∃ h : o₁ = eq, o₂ h = eq := by decide +theorem dthen_eq_eq_of_eq_eq : ∀ {o₁ : Ordering} {o₂}, (h₁ : o₁ = .eq) → o₂ h₁ = .eq → o₁.dthen o₂ = .eq := by decide +theorem left_eq_eq_of_dthen_eq_eq : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = .eq → o₁ = .eq := by decide +theorem right_eq_eq_of_dthen_eq_eq : ∀ {o₁ : Ordering} {o₂}, (h : o₁.dthen o₂ = .eq) → o₂ (left_eq_eq_of_dthen_eq_eq h) = .eq := by decide + +@[simp] theorem lt_dthen {o} : lt.dthen o = lt := rfl +@[simp] theorem gt_dthen {o} : gt.dthen o = gt := rfl +@[simp] theorem eq_dthen {o} : eq.dthen o = o rfl := rfl + +theorem dthen_assoc : ∀ (o₁ : Ordering) (o₂ o₃), (o₁.dthen o₂).dthen o₃ = + o₁.dthen (fun h => (o₂ h).dthen fun h' => o₃ (dthen_eq_eq_of_eq_eq h h')) := by decide + +theorem isLE_dthen_iff_or : ∀ {o₁ : Ordering} {o₂}, (o₁.dthen o₂).isLE ↔ o₁ = lt ∨ (∃ h, (o₂ h).isLE) := by decide +theorem isLE_left_of_isLE_dthen : ∀ {o₁ : Ordering} {o₂}, (o₁.dthen o₂).isLE → o₁.isLE := by decide +theorem isGE_left_of_isGE_dthen : ∀ {o₁ : Ordering} {o₂}, (o₁.dthen o₂).isGE → o₁.isGE := by decide + +theorem dthen_eq_left_iff : ∀ {o₁ : Ordering} {o₂}, o₁.dthen o₂ = o₁ ↔ (∀ h, o₂ h = o₁) := by decide instance : Std.Associative Ordering.then := ⟨then_assoc⟩ instance : Std.IdempotentOp Ordering.then := ⟨fun _ => then_self⟩ diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index a2c96336af28..5675ec266312 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1076,6 +1076,14 @@ noncomputable def Bool.and (x y : Bool) : Bool := | false => false | true => y +/-- +The dependent version of `a && b`. +-/ +@[macro_inline, implicit_reducible] def Bool.dand (a : Bool) (b : Eq a true → Bool) : Bool := + match a with + | false => false + | true => b rfl + /-- Boolean negation, also known as Boolean complement. `not x` can be written `!x`. @@ -1264,6 +1272,12 @@ instance [dp : Decidable p] : Decidable (Not p) where | isTrue hp => absurd hp | isFalse hp => hp +theorem Bool.Reflects.of_imp {x : Bool} {p : Prop} (h₁ : Eq x true → p) (h₂ : p → Eq x true) : + x.Reflects p := + match x with + | false => fun hp => Bool.noConfusion (h₂ hp) + | true => h₁ rfl + /-- Decides whether two Booleans are equal. diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 2c7d94dd4d29..4880e30593e0 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -542,6 +542,22 @@ instance forall_prop_decidable {p} (P : p → Prop) | isFalse h2 => fun al => absurd (al h) h2 | isFalse h => fun h2 => absurd h2 h +@[inline] +instance forall_forall_prop_decidable {p} {α : Sort u} (P : (p → α) → Prop) + [hp : Decidable p] [hP : ∀ f, Decidable (P f)] + [hα : ∀ Q : α → Bool, Decidable (∀ x, Q x = true)] : Decidable (∀ f, P f) where + decide := if h : p then decide (∀ a, decide <| P fun _ => a) else decide (P h.elim) + reflects_decide := + match hp with + | isTrue h => + match hα (fun a => decide <| P fun _ => a) with + | isTrue h2 => fun f => of_decide_eq_true (h2 (f h)) + | isFalse h2 => fun h' => h2 fun _ => decide_eq_true (h' _) + | isFalse h => show (decide (P h.elim)).Reflects (∀ h, P h) from + match hP h.elim with + | isTrue h2 => fun f => (funext (fun h' => absurd h' h) : f = h.elim) ▸ h2 + | isFalse h2 => fun h' => absurd (h' _) h2 + @[bool_to_prop] theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) ↔ p := by simp @[simp, bool_to_prop] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} : @@ -942,4 +958,3 @@ theorem Bool.dite_else_true {p : Prop} [Decidable p] {x : p → Bool} : (if h : @[deprecated Bool.dite_false_right_eq_false (since := "2026-07-21")] theorem Bool.dite_else_false_eq_false {p : Prop} [Decidable p] {x : p → Bool} : (if h : p then x h else Bool.false) = Bool.false ↔ ∀ (h : p), x h = Bool.false := Bool.dite_false_right_eq_false - diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 1e6f11fb1dcd..c29e49a77016 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -377,6 +377,30 @@ instance : Std.LawfulIdentity (· && ·) true where instance : Std.IdempotentOp (· && ·) := ⟨Bool.and_self⟩ @[simp] theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true) := by cases a <;> cases b <;> decide +theorem Bool.and_eq_true_of_eq_true {x y : Bool} (hx : x = true) (hy : y = true) : + (x && y) = true := and_eq_true x y ▸ ⟨hx, hy⟩ +theorem Bool.left_eq_true_of_and_eq_true {x y : Bool} (h : (x && y) = true) : + x = true := (and_eq_true x y ▸ h).1 +theorem Bool.right_eq_true_of_and_eq_true {x y : Bool} (h : (x && y) = true) : + y = true := (and_eq_true x y ▸ h).2 + +@[congr] theorem Bool.dand_congr {x x' : Bool} {y : x = true → Bool} {y' : x' = true → Bool} + (hx : x = x') (hy : ∀ h, y (hx ▸ h) = y' h) : + x.dand y = x'.dand y' := by cases hx; cases funext hy; rfl +@[simp] theorem Bool.false_dand {y : false = true → Bool} : false.dand y = false := rfl +@[simp] theorem Bool.true_dand {y : true = true → Bool} : true.dand y = y rfl := rfl +@[simp] theorem Bool.dand_eq_and {x y : Bool} : x.dand (fun _ => y) = (x && y) := by cases x <;> rfl +@[simp] theorem Bool.dand_eq_true_iff {x : Bool} {y : x = true → Bool} : + x.dand y = true ↔ Exists fun h : x = true => y h = true := + match x with + | false => iff_of_false nofun nofun + | true => ⟨fun hy => ⟨rfl, hy⟩, fun ⟨_, hy⟩ => hy⟩ +theorem Bool.dand_eq_true_of_eq_true {x : Bool} {y : x = true → Bool} + (hx : x = true) (hy : y hx = true) : x.dand y = true := dand_eq_true_iff.mpr ⟨hx, hy⟩ +theorem Bool.left_eq_true_of_dand_eq_true {x : Bool} {y : x = true → Bool} (h : x.dand y = true) : + x = true := (dand_eq_true_iff.mp h).1 +theorem Bool.right_eq_true_of_dand_eq_true {x : Bool} {y : x = true → Bool} (h : x.dand y = true) : + y (left_eq_true_of_dand_eq_true h) = true := (dand_eq_true_iff.mp h).2 theorem Bool.and_assoc (a b c : Bool) : (a && b && c) = (a && (b && c)) := by cases a <;> cases b <;> cases c <;> decide