Skip to content

Commit

Permalink
24 to go
Browse files Browse the repository at this point in the history
  • Loading branch information
@tomaz1502
tomaz1502 committed Dec 27, 2024
1 parent d8b8c05 commit 295bbb1
Showing 1 changed file with 129 additions and 46 deletions.
175 changes: 129 additions & 46 deletions Smt/Reconstruct/Rat/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,10 +43,10 @@ theorem Rat.le_antisymm {a b : Rat} (hab : a ≤ b) (hba : b ≤ a) : a = b := b
rw [Rat.add_zero] at this
exact this

theorem Rat.le_antisymm_iff (a b : Rat) : a = b ↔ a ≤ b ∧ b ≤ a :=
⟨fun h ↦ ⟨by rw [h]; exact Rat.le_refl, by rw [h]; exact Rat.le_refl⟩, fun ⟨ab, ba⟩ ↦ le_antisymm ab ba⟩
theorem le_antisymm_iff (a b : Rat) : a = b ↔ a ≤ b ∧ b ≤ a :=
⟨fun h ↦ ⟨by rw [h]; exact Rat.le_refl, by rw [h]; exact Rat.le_refl⟩, fun ⟨ab, ba⟩ ↦ Rat.le_antisymm ab ba⟩

theorem Rat.le_iff_eq_or_lt (a b : Rat) : a ≤ b ↔ a = b ∨ a < b := by
theorem le_iff_eq_or_lt (a b : Rat) : a ≤ b ↔ a = b ∨ a < b := by
rw [Rat.le_antisymm_iff, Rat.lt_iff_le_not_le, ← and_or_left]; simp [Classical.em]

theorem lt_iff_sub_pos (a b : Rat) : a < b ↔ 0 < b - a := by
Expand Down Expand Up @@ -466,7 +466,7 @@ theorem eq_eq_sub_eq_zero : (a = b) = (a - b = 0) := by
constructor
· intro h; rw [h]; simp
· intro h
have h' := congrArg (fun z => z + b) h
have h' := congrArg (fun z => z + b) h
simp at h'
rw [Rat.zero_add] at h'
rw [Rat.sub_eq_add_neg] at h'
Expand All @@ -488,16 +488,110 @@ theorem lt_of_sub_eq_pos {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0)
rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, Rat.mul_lt_mul_left hc]
rw [lt_eq_sub_lt_zero, @lt_eq_sub_lt_zero b₁, ← this hc₁, ← this hc₂, h]

theorem mul_sign₁ : a < 0 → b < 0 → a * b > 0 :=
Rat.numDenCasesOn' a fun a_num a_den a_den_nz ha =>
Rat.numDenCasesOn' b fun b_num b_den b_den_nz hb => by
have : 0 < a_den := Nat.zero_lt_of_ne_zero a_den_nz
have a_den_pos : (0 : Int) < a_den := Int.ofNat_pos.mpr this
have a_num_neg : a_num < 0 := (Rat.divInt_neg_iff_of_neg_right a_den_pos).mp ha
have : 0 < b_den := Nat.zero_lt_of_ne_zero b_den_nz
have b_den_pos : (0 : Int) < b_den := Int.ofNat_pos.mpr this
have b_num_neg : b_num < 0 := (Rat.divInt_neg_iff_of_neg_right b_den_pos).mp hb
have bar : (a_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr a_den_nz
have bar' : (b_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr b_den_nz
rw [Rat.divInt_mul_divInt _ _ bar bar']
have : 0 < (a_den : Int) * b_den := Int.mul_pos a_den_pos b_den_pos
apply (Rat.divInt_pos_iff_of_pos_right this).mpr
exact Int.mul_pos_of_neg_of_neg a_num_neg b_num_neg

theorem mul_sign₃ : a < 0 → b > 0 → a * b < 0 :=
Rat.numDenCasesOn' a fun a_num a_den a_den_nz ha =>
Rat.numDenCasesOn' b fun b_num b_den b_den_nz hb => by
have : 0 < a_den := Nat.zero_lt_of_ne_zero a_den_nz
have a_den_pos : (0 : Int) < a_den := Int.ofNat_pos.mpr this
have a_num_neg : a_num < 0 := (Rat.divInt_neg_iff_of_neg_right a_den_pos).mp ha
have : 0 < b_den := Nat.zero_lt_of_ne_zero b_den_nz
have b_den_pos : (0 : Int) < b_den := Int.ofNat_pos.mpr this
have b_num_neg : 0 < b_num := (Rat.divInt_pos_iff_of_pos_right b_den_pos).mp hb
have bar : (a_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr a_den_nz
have bar' : (b_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr b_den_nz
rw [Rat.divInt_mul_divInt _ _ bar bar']
have : 0 < (a_den : Int) * b_den := Int.mul_pos a_den_pos b_den_pos
apply (Rat.divInt_neg_iff_of_neg_right this).mpr
exact Int.mul_neg_of_neg_of_pos a_num_neg b_num_neg

theorem mul_sign₄ (ha : a > 0) (hb : b < 0) : a * b < 0 := by
rw [Rat.mul_comm]
exact mul_sign₃ hb ha

theorem le_mul_of_lt_of_le (a b : Rat) : a < 0 → b ≤ 0 → 0 ≤ a * b := by
intros h1 h2
cases (Rat.le_iff_eq_or_lt b 0).mp h2 with
| inl heq => rw [heq, Rat.mul_zero]; exact rfl
| inr hlt => have := mul_sign₁ h1 hlt; exact le_of_lt this

theorem foo (a b : Rat) : a < 0 → 0 ≤ a * b → b ≤ 0 := by
intros h1 h2
apply Classical.byContradiction
intro h3
have : 0 < b := Rat.not_nonpos.mp h3
have : a * b < 0 := mul_sign₃ h1 this
have := Rat.lt_of_lt_of_le this h2
exact Rat.lt_irrefl this

theorem bar (a b : Rat) : a < 0 → 0 < a * b → b < 0 := by
intros h1 h2
apply Classical.byContradiction
intro h3
have : 0 ≤ b := Rat.not_lt.mp h3
cases (Rat.le_iff_eq_or_lt 0 b).mp this with
| inl heq => rw [<-heq, Rat.mul_zero] at h2; exact Rat.lt_irrefl h2
| inr hlt => have := mul_sign₃ h1 hlt; have := Rat.lt_trans h2 this; exact Rat.lt_irrefl this

theorem le_iff_sub_nonneg' (x y : Rat) : y ≤ x ↔ y - x ≤ 0 := by
rw [Rat.le_iff_sub_nonneg]
rw [Rat.nonneg_iff_sub_nonpos]
rw [Rat.neg_sub]

theorem lt_iff_sub_pos' (x y : Rat) : y < x ↔ y - x < 0 := by
rw [Rat.lt_iff_sub_pos]
rw [Rat.pos_iff_neg_nonpos]
rw [Rat.neg_sub]

theorem lt_of_sub_eq_neg' {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) → (b₁ < b₂) := by
intro h2
have := (Rat.lt_iff_sub_pos' a₂ a₁).mp h2
have : 0 < c₁ * (a₁ - a₂) := mul_sign₁ hc₁ this
rw [h] at this
have := bar c₂ (b₁ - b₂) hc₂ this
exact (lt_iff_sub_pos' b₂ b₁).mpr this

theorem lt_of_sub_eq_neg {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) := by
sorry
apply propext
constructor
· exact lt_of_sub_eq_neg' hc₁ hc₂ h
· intro h2
exact lt_of_sub_eq_neg' (c₁ := c₂) (c₂ := c₁) (a₁ := b₁) (a₂ := b₂) (b₁ := a₁) (b₂ := a₂) hc₂ hc₁ (Eq.symm h) h2

theorem le_of_sub_eq_pos {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≤ a₂) = (b₁ ≤ b₂) := by
have {c x y : Rat} (hc : c > 0) : (c * (x - y) ≤ 0) = (x - y ≤ 0) := by
rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, Rat.mul_le_mul_left hc]
rw [le_eq_sub_le_zero, @le_eq_sub_le_zero b₁, ← this hc₁, ← this hc₂, h]

theorem le_of_sub_eq_neg' {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≤ a₂) → (b₁ ≤ b₂) := by
intro h2
have := (Rat.le_iff_sub_nonneg' a₂ a₁).mp h2
have : 0 ≤ c₁ * (a₁ - a₂) := le_mul_of_lt_of_le c₁ (a₁ - a₂) hc₁ this
rw [h] at this
have := foo c₂ (b₁ - b₂) hc₂ this
exact (Rat.le_iff_sub_nonneg' b₂ b₁).mpr this

theorem le_of_sub_eq_neg {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≤ a₂) = (b₁ ≤ b₂) := by
sorry
apply propext
constructor
· exact le_of_sub_eq_neg' hc₁ hc₂ h
· intro h2
exact le_of_sub_eq_neg' (c₁ := c₂) (c₂ := c₁) (a₁ := b₁) (a₂ := b₂) (b₁ := a₁) (b₂ := a₂) hc₂ hc₁ (Eq.symm h) h2

theorem eq_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ ≠ 0) (hc₂ : c₂ ≠ 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ = a₂) = (b₁ = b₂) := by
apply propext
Expand All @@ -520,18 +614,43 @@ theorem ge_of_sub_eq_pos {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0)
rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, ge_iff_le, Rat.mul_le_mul_left hc]
rw [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero b₁, ← this hc₁, ← this hc₂, h]

theorem mul_neg (a b : Rat) : a * (-b) = - (a * b) :=
Rat.numDenCasesOn' a fun a_num a_den a_den_nz =>
Rat.numDenCasesOn' b fun b_num b_den b_den_nz => by
rw [Rat.divInt_mul_divInt _ _ (Int.ofNat_ne_zero.mpr a_den_nz) (Int.ofNat_ne_zero.mpr b_den_nz)]
rw [Rat.neg_divInt]
rw [Rat.divInt_mul_divInt _ _ (Int.ofNat_ne_zero.mpr a_den_nz) (Int.ofNat_ne_zero.mpr b_den_nz)]
rw [Int.mul_neg, Rat.neg_divInt]

theorem neg_eq {a b : Rat} : -a = -b → a = b := by
intro h
have h' := congrArg (fun z => -z) h
simp only [Rat.neg_neg] at h'
exact h'

theorem ge_of_sub_eq_neg {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≥ a₂) = (b₁ ≥ b₂) := by
sorry
show (a₂ ≤ a₁) = (b₂ ≤ b₁)
rw [<- Rat.neg_sub, <- Rat.neg_sub (x := b₂) (y := b₁), mul_neg, mul_neg] at h
have h' := neg_eq h
exact le_of_sub_eq_neg hc₁ hc₂ h'

theorem gt_of_sub_eq_pos {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ > a₂) = (b₁ > b₂) := by
have {c x y : Rat} (hc : c > 0) : (c * (x - y) > 0) = (x - y > 0) := by
rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, gt_iff_lt, Rat.mul_lt_mul_left hc]
rw [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h]

theorem gt_of_sub_eq_neg {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ > a₂) = (b₁ > b₂) := by
sorry
show (a₂ < a₁) = (b₂ < b₁)
rw [<- Rat.neg_sub, <- Rat.neg_sub (x := b₂) (y := b₁), mul_neg, mul_neg] at h
have h' := neg_eq h
exact lt_of_sub_eq_neg hc₁ hc₂ h'

theorem lt_of_sub_eq_pos_int_left {a₁ a₂ : Int} {b₁ b₂ c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * ↑(a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) :=
instance foobar : IntCast (R := Rat) := by infer_instance

#print foobar

theorem lt_of_sub_eq_pos_int_left {a₁ a₂ : Int} {b₁ b₂ c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * ↑(a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) := by
-- have := lt_of_sub_eq_pos hc₁ hc₂ h
sorry

theorem lt_of_sub_eq_neg_int_left {a₁ a₂ : Int} {b₁ b₂ c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * ↑(a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) := by
Expand Down Expand Up @@ -559,6 +678,7 @@ theorem gt_of_sub_eq_neg_int_left {a₁ a₂ : Int} {b₁ b₂ c₁ c₂ : Rat}
sorry

theorem lt_of_sub_eq_pos_int_right {a₁ a₂ : Rat} {b₁ b₂ : Int} {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * ↑(b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) :=
--have := lt_of_sub_eq_pos hc₁ hc₂ h
sorry

theorem lt_of_sub_eq_neg_int_right {a₁ a₂ : Rat} {b₁ b₂ : Int} {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * ↑(b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) := by
Expand All @@ -585,42 +705,6 @@ theorem gt_of_sub_eq_pos_int_right {a₁ a₂ : Rat} {b₁ b₂ : Int} {c₁ c
theorem gt_of_sub_eq_neg_int_right {a₁ a₂ : Rat} {b₁ b₂ : Int} {c₁ c₂ : Rat} (hc₁ : c₁ < 0) (hc₂ : c₂ < 0) (h : c₁ * (a₁ - a₂) = c₂ * ↑(b₁ - b₂)) : (a₁ > a₂) = (b₁ > b₂) := by
sorry

theorem mul_sign₁ : a < 0 → b < 0 → a * b > 0 :=
Rat.numDenCasesOn' a fun a_num a_den a_den_nz ha =>
Rat.numDenCasesOn' b fun b_num b_den b_den_nz hb => by
have : 0 < a_den := Nat.zero_lt_of_ne_zero a_den_nz
have a_den_pos : (0 : Int) < a_den := Int.ofNat_pos.mpr this
have a_num_neg : a_num < 0 := (Rat.divInt_neg_iff_of_neg_right a_den_pos).mp ha
have : 0 < b_den := Nat.zero_lt_of_ne_zero b_den_nz
have b_den_pos : (0 : Int) < b_den := Int.ofNat_pos.mpr this
have b_num_neg : b_num < 0 := (Rat.divInt_neg_iff_of_neg_right b_den_pos).mp hb
have bar : (a_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr a_den_nz
have bar' : (b_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr b_den_nz
rw [Rat.divInt_mul_divInt _ _ bar bar']
have : 0 < (a_den : Int) * b_den := Int.mul_pos a_den_pos b_den_pos
apply (Rat.divInt_pos_iff_of_pos_right this).mpr
exact Int.mul_pos_of_neg_of_neg a_num_neg b_num_neg

theorem mul_sign₃ : a < 0 → b > 0 → a * b < 0 :=
Rat.numDenCasesOn' a fun a_num a_den a_den_nz ha =>
Rat.numDenCasesOn' b fun b_num b_den b_den_nz hb => by
have : 0 < a_den := Nat.zero_lt_of_ne_zero a_den_nz
have a_den_pos : (0 : Int) < a_den := Int.ofNat_pos.mpr this
have a_num_neg : a_num < 0 := (Rat.divInt_neg_iff_of_neg_right a_den_pos).mp ha
have : 0 < b_den := Nat.zero_lt_of_ne_zero b_den_nz
have b_den_pos : (0 : Int) < b_den := Int.ofNat_pos.mpr this
have b_num_neg : 0 < b_num := (Rat.divInt_pos_iff_of_pos_right b_den_pos).mp hb
have bar : (a_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr a_den_nz
have bar' : (b_den : Int) ≠ (0 : Int) := Int.ofNat_ne_zero.mpr b_den_nz
rw [Rat.divInt_mul_divInt _ _ bar bar']
have : 0 < (a_den : Int) * b_den := Int.mul_pos a_den_pos b_den_pos
apply (Rat.divInt_neg_iff_of_neg_right this).mpr
exact Int.mul_neg_of_neg_of_pos a_num_neg b_num_neg

theorem mul_sign₄ (ha : a > 0) (hb : b < 0) : a * b < 0 := by
rw [Rat.mul_comm]
exact mul_sign₃ hb ha

theorem mul_sign₆ : a > 0 → b > 0 → a * b > 0 :=
Rat.numDenCasesOn' a fun a_num a_den a_den_nz ha =>
Rat.numDenCasesOn' b fun b_num b_den b_den_nz hb => by
Expand Down Expand Up @@ -704,7 +788,6 @@ theorem mul_neg_lt : (c < 0 ∧ a < b) → c * a > c * b :=
rw [Int.mul_comm, Int.mul_comm a_den b_num]
exact h3


theorem Int.mul_le_mul_of_neg_left {a b c : Int} (h : b ≤ a) (hc : c < 0) : c * a ≤ c * b :=
match Int.le_iff_eq_or_lt.mp h with
| Or.inl heq => by rw [heq]; exact Int.le_refl (c * a)
Expand Down

0 comments on commit 295bbb1

Please sign in to comment.