add more examples

DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S03_Negation.lean

@@ -0,0 +1,168 @@
+import Mathlib.Data.Real.Basic
+import Duper.Tactic
+
+namespace C03S03
+
+section
+variable (a b : ℝ)
+
+example (h : a < b) : ¬b < a := by
+  intro h'
+  have : a < a := lt_trans h h'
+  apply lt_irrefl a this
+
+example (h : a < b) : ¬b < a := by
+  duper [lt_trans, lt_irrefl, *]
+
+def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, f x ≤ a
+
+def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, a ≤ f x
+
+def FnHasUb (f : ℝ → ℝ) :=
+  ∃ a, FnUb f a
+
+def FnHasLb (f : ℝ → ℝ) :=
+  ∃ a, FnLb f a
+
+variable (f : ℝ → ℝ)
+
+example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
+  intro fnub
+  rcases fnub with ⟨a, fnuba⟩
+  rcases h a with ⟨x, hx⟩
+  have : f x ≤ a := fnuba x
+  linarith
+
+example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
+ duper [*, FnHasUb, FnUb, gt_iff_lt, not_le]
+
+example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f := by
+ duper [*, FnHasLb, FnLb, gt_iff_lt, not_le]
+
+example : ¬FnHasUb fun x ↦ x := by
+  have : ∀ x : ℝ, x < x + 1  := by simp
+  duper [*, FnHasUb, FnUb, gt_iff_lt, not_le, this]
+
+#check (not_le_of_gt : a > b → ¬a ≤ b)
+#check (not_lt_of_ge : a ≥ b → ¬a < b)
+#check (lt_of_not_ge : ¬a ≥ b → a < b)
+#check (le_of_not_gt : ¬a > b → a ≤ b)
+
+
+example (h : Monotone f) (h' : f a < f b) : a < b := by
+  apply lt_of_not_ge
+  intro h''
+  apply absurd h'
+  apply not_lt_of_ge (h h'')
+
+-- Nice!
+example (h : Monotone f) (h' : f a < f b) : a < b := by
+  duper [lt_of_not_ge, not_lt_of_ge, Monotone, *]
+
+example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
+  intro h''
+  apply absurd h'
+  apply not_lt_of_ge
+  apply h'' h
+
+example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
+  duper [Monotone, not_lt_of_ge, *]
+
+example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
+  intro h
+  let f := fun x : ℝ ↦ (0 : ℝ)
+  have monof : Monotone f := by
+    intro a b leab
+    rfl
+  have h' : f 1 ≤ f 0 := le_refl _
+  have : (1 : ℝ) ≤ 0 := h monof h'
+  linarith
+
+example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
+    set f := fun x : ℝ ↦ (0 : ℝ) with hf
+    have h' : f 1 ≤ f 0 := le_refl _
+    have : ¬ (1 : ℝ ) ≤ 0 := by linarith
+    duper [Monotone, *]
+
+example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
+  apply le_of_not_gt
+  intro h'
+  linarith [h _ h']
+
+example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
+  duper [*, le_of_not_gt, lt_irrefl]
+
+end
+
+section
+variable {α : Type*} (P : α → Prop) (Q : Prop)
+
+example (h : ¬∃ x, P x) : ∀ x, ¬P x := by
+  duper [h]
+
+example (h : ∀ x, ¬P x) : ¬∃ x, P x := by
+  duper [h]
+
+example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
+  duper [h]
+
+example (h : ∃ x, ¬P x) : ¬∀ x, P x := by
+  duper [h]
+
+example (h : ¬¬Q) : Q := by
+  duper [h]
+
+example (h : Q) : ¬¬Q := by
+  duper [h]
+
+end
+
+section
+variable (f : ℝ → ℝ)
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  intro a
+  by_contra h'
+  apply h
+  use a
+  intro x
+  apply le_of_not_gt
+  intro h''
+  apply h'
+  use x
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  duper [h, le_of_not_gt, FnHasUb, FnUb]
+
+example (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by
+  push_neg at h
+  exact h
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  dsimp only [FnHasUb, FnUb] at h
+  push_neg at h
+  exact h
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  duper [FnHasUb, FnUb, h, le_of_not_gt]
+
+example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
+  duper [Monotone, h, le_of_not_gt]
+
+
+example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by
+  contrapose! h
+  use x / 2
+  constructor <;> linarith
+
+end
+
+section
+variable (a : ℕ)
+
+example (h : 0 < 0) : a > 37 := by
+  duper [h, lt_irrefl]
+
+end

DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S04_Conjunction_and_Iff.lean

@@ -0,0 +1,167 @@
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Nat.Prime
+import Duper.Tactic
+
+namespace C03S04
+
+example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by
+  duper [*]
+
+example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
+  duper [*, le_antisymm]
+
+example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m := by
+  rcases h with ⟨h0, h1⟩
+  constructor
+  · exact h0
+  intro h2
+  apply h1
+  apply Nat.dvd_antisymm h0 h2
+
+example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m := by
+  duper [*, Nat.dvd_antisymm]
+
+example : ∃ x : ℝ, 2 < x ∧ x < 4 :=
+  ⟨5 / 2, by norm_num, by norm_num⟩
+
+example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
+  rintro ⟨z, xltz, zlty⟩
+  exact lt_trans xltz zlty
+
+example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
+  duper [*, lt_trans]
+
+example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
+  use 5
+  use 7
+  norm_num
+
+example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
+  have : 4 < 5 ∧ 5 < 7 ∧ 7 < 10 ∧ Nat.Prime 5 ∧ Nat.Prime 7 := by norm_num
+  duper [*]
+
+example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
+  rintro ⟨h₀, h₁⟩
+  use h₀
+  exact fun h' ↦ h₁ (le_antisymm h₀ h')
+
+example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
+  duper [le_antisymm]
+
+example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
+  constructor
+  · contrapose!
+    rintro rfl
+    rfl
+  contrapose!
+  exact le_antisymm h
+
+example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
+  duper [*, le_antisymm]
+
+example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y := by
+  constructor
+  · rintro ⟨h0, h1⟩
+    constructor
+    · exact h0
+    intro h2
+    apply h1
+    rw [h2]
+  rintro ⟨h0, h1⟩
+  constructor
+  · exact h0
+  intro h2
+  apply h1
+  apply le_antisymm h0 h2
+
+example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y := by
+  duper [le_antisymm]
+
+theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
+  have h' : x ^ 2 = 0 := by linarith [pow_two_nonneg x, pow_two_nonneg y]
+  pow_eq_zero h'
+
+example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
+  constructor
+  · intro h
+    constructor
+    · exact aux h
+    rw [add_comm] at h
+    exact aux h
+  rintro ⟨rfl, rfl⟩
+  norm_num
+
+example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
+  have : (0 : ℝ) ^ 2 = 0 := by norm_num
+  duper [*, aux, add_comm, add_zero]
+
+section
+
+-- Not good for Duper
+example (x : ℝ) : |x + 3| < 5 → -8 < x ∧ x < 2 := by
+  rw [abs_lt]
+  intro h
+  constructor <;> linarith
+
+example : 3 ∣ Nat.gcd 6 15 := by
+  rw [Nat.dvd_gcd_iff]
+  constructor <;> norm_num
+
+-- Interesting: this uses `decide` at the end
+example : 3 ∣ Nat.gcd 6 15 := by
+  duper [Nat.dvd_gcd_iff] {portfolioInstance := 7}
+
+end
+
+theorem not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
+  rw [Monotone]
+  push_neg
+  rfl
+
+example {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
+  duper [Monotone, not_le]
+
+example : ¬Monotone fun x : ℝ ↦ -x := by
+  rw [not_monotone_iff]
+  use 0, 1
+  norm_num
+
+example : ¬Monotone fun x : ℝ ↦ -x := by
+  duper [Monotone, not_lt, le_of_lt, neg_le_neg_iff, zero_lt_one]
+
+section
+variable {α : Type*} [PartialOrder α]
+variable (a b : α)
+
+example : a < b ↔ a ≤ b ∧ a ≠ b := by
+  rw [lt_iff_le_not_le]
+  constructor
+  · rintro ⟨h0, h1⟩
+    constructor
+    · exact h0
+    intro h2
+    apply h1
+    rw [h2]
+  rintro ⟨h0, h1⟩
+  constructor
+  · exact h0
+  intro h2
+  apply h1
+  apply le_antisymm h0 h2
+
+example : a < b ↔ a ≤ b ∧ a ≠ b := by
+  duper [lt_iff_le_not_le, le_antisymm]
+
+end
+
+section
+variable {α : Type*} [Preorder α]
+variable (a b c : α)
+
+example : ¬a < a := by
+  duper [lt_iff_le_not_le]
+
+example : a < b → b < c → a < c := by
+  duper [lt_iff_le_not_le, le_trans]
+
+end