Update proofs with newer version of lean

Smt/Reconstruct/Int/Core.lean

@@ -2,7 +2,7 @@
 Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
 institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed
+Authors: Adrien Champion
 -/
 
 namespace Int
@@ -112,11 +112,11 @@ theorem neg_neg_iff_pos : -a < 0 ↔ 0 < a := ⟨Int.pos_of_neg_neg, Int.neg_neg
 theorem neg_nonpos_iff_nonneg : -a ≤ 0 ↔ 0 ≤ a :=
   ⟨Int.nonneg_of_neg_nonpos, Int.neg_nonpos_of_nonneg⟩
 
-@[simp] protected
-theorem sub_pos : 0 < a - b ↔ b < a := ⟨Int.lt_of_sub_pos, Int.sub_pos_of_lt⟩
+@[simp]
+protected theorem sub_pos : 0 < a - b ↔ b < a := ⟨Int.lt_of_sub_pos, Int.sub_pos_of_lt⟩
 
-@[simp] protected
-theorem sub_nonneg : 0 ≤ a - b ↔ b ≤ a := ⟨Int.le_of_sub_nonneg, Int.sub_nonneg_of_le⟩
+@[simp]
+protected theorem sub_nonneg : 0 ≤ a - b ↔ b ≤ a := ⟨Int.le_of_sub_nonneg, Int.sub_nonneg_of_le⟩
 
 protected theorem le_rfl : a ≤ a := a.le_refl
 protected theorem lt_or_lt_of_ne : a ≠ b → a < b ∨ b < a := Int.lt_or_gt_of_ne
@@ -134,8 +134,6 @@ protected theorem le_iff_eq_or_lt {a b : Int} : a ≤ b ↔ a = b ∨ a < b := b
   simp [Decidable.em]
 protected theorem le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by rw [Int.le_iff_eq_or_lt, or_comm]
 
-
-
 protected theorem div_gcd_nonneg_iff_of_pos
   {b : Nat} (b_pos : 0 < b)
 : 0 ≤ a / (a.gcd b) ↔ 0 ≤ a := by
@@ -145,12 +143,9 @@ protected theorem div_gcd_nonneg_iff_of_pos
     apply Nat.gcd_pos_of_pos_right _ b_pos
   exact Int.div_nonneg_iff_of_pos nz_den
 
-protected theorem div_gcd_nonneg_iff_of_nz
-  {b : Nat} (nz_b : b ≠ 0)
-: 0 ≤ a / (a.gcd b) ↔ 0 ≤ a :=
+protected theorem div_gcd_nonneg_iff_of_nz {b : Nat} (nz_b : b ≠ 0) : 0 ≤ a / (a.gcd b) ↔ 0 ≤ a :=
   Nat.pos_of_ne_zero nz_b |> Int.div_gcd_nonneg_iff_of_pos
 
-
 @[simp]
 theorem mul_nonneg_iff_of_pos_right (c_pos : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b := ⟨
   by

Smt/Reconstruct/Rat/Core.lean

@@ -8,8 +8,9 @@ Authors: Abdalrhman Mohamed
 import Batteries.Logic
 import Batteries.Data.Rat
 
-namespace Rat
+import Smt.Reconstruct.Int.Core
 
+namespace Rat
 
 section basics
 
@@ -22,23 +23,273 @@ protected def pow (m : Rat) : Nat → Rat
 instance : NatPow Rat where
   pow := Rat.pow
 
-protected theorem add_zero : ∀ a : Rat, a + 0 = a := by
-  sorry
+theorem num_divInt_den (q : Rat) : q.num /. q.den = q :=
+  divInt_self _
+
+theorem mk'_eq_divInt {n d h c} : (⟨n, d, h, c⟩ : Rat) = n /. d :=
+  (num_divInt_den _).symm
+
+theorem divInt_num (q : Rat) : (q.num /. q.den).num = q.num := by
+  simp [mkRat, q.den_nz, normalize, Rat.reduced]
+
+theorem divInt_num'
+  {n : Int} {d : Nat}
+  (nz_d : d ≠ 0 := by omega)
+  (reduced : n.natAbs.Coprime d := by assumption)
+: (n /. d).num = n := by
+  simp [mkRat, nz_d, normalize, reduced]
+
+theorem divInt_den (q : Rat) : (q.num /. q.den).den = q.den := by
+  simp [mkRat, q.den_nz, normalize, Rat.reduced]
+
+theorem divInt_den'
+  {n : Int} {d : Nat}
+  (nz_d : d ≠ 0 := by omega)
+  (reduced : n.natAbs.Coprime d := by assumption)
+: (n /. d).den = d := by
+  simp [mkRat, nz_d, normalize, reduced]
+
+@[elab_as_elim]
+def numDenCasesOn.{u} {C : Rat → Sort u}
+: ∀ (a : Rat) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a
+| ⟨n, d, h, c⟩, H => by rw [mk'_eq_divInt]; exact H n d (Nat.pos_of_ne_zero h) c
+
+@[elab_as_elim]
+def numDenCasesOn'.{u} {C : Rat → Sort u} (a : Rat)
+  (H : ∀ (n : Int) (d : Nat), d ≠ 0 → C (n /. d))
+: C a :=
+  numDenCasesOn a fun n d h _ => H n d (Nat.pos_iff_ne_zero.mp h)
+
+@[elab_as_elim]
+def numDenCasesOn''.{u} {C : Rat → Sort u} (a : Rat)
+  (H : ∀ (n : Int) (d : Nat) (nz red), C (mk' n d nz red))
+: C a :=
+  numDenCasesOn a fun n d h h' ↦ by
+    let h_pos := Nat.pos_iff_ne_zero.mp h
+    rw [← mk_eq_divInt _ _ h_pos h']
+    exact H n d h_pos _
+
+theorem normalize_eq_mk'
+  (n : Int) (d : Nat) (h : d ≠ 0) (c : Nat.gcd (Int.natAbs n) d = 1)
+: normalize n d h = mk' n d h c :=
+  (mk_eq_normalize ..).symm
+
+protected theorem normalize_den_ne_zero
+: ∀ {d : Int} {n : Nat}, (h : n ≠ 0) → (normalize d n h).den ≠ 0 := by
+  intro d n nz
+  simp only [Rat.normalize_eq, ne_eq]
+  intro h
+  apply nz
+  rw [← Nat.zero_mul (d.natAbs.gcd n)]
+  apply Nat.div_eq_iff_eq_mul_left _ _ |>.mp
+  · assumption
+  · exact Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero nz)
+  · exact Nat.gcd_dvd_right _ _
+
+protected theorem eq_mkRat : ∀ a : Rat, a = mkRat a.num a.den := fun a => by
+  simp [Rat.mkRat_def, a.den_nz, Rat.normalize_eq, a.reduced]
+
+@[simp]
+theorem mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by
+  congr
+  apply Nat.coprime_zero_left d |>.mp w
+
+theorem eq_iff_mul_eq_mul {p q : Rat} : p = q ↔ p.num * q.den = q.num * p.den := by
+  conv =>
+    lhs
+    rw [← num_divInt_den p, ← num_divInt_den q]
+  apply Rat.divInt_eq_iff <;>
+    · rw [← Int.natCast_zero, Ne, Int.ofNat_inj]
+      apply den_nz
+
+end basics
+
+section le_lt_basics
+
+protected theorem not_le {q' : Rat} : ¬q ≤ q' ↔ q' < q := by
+  exact (Bool.not_eq_false _).to_iff
+
+protected theorem not_lt {q' : Rat} : ¬q < q' ↔ q' ≤ q := by
+  rw [not_congr (Rat.not_le (q := q') (q' := q)) |>.symm]
+  simp only [Decidable.not_not]
 
-protected theorem add_assoc : ∀ a b c : Rat, a + b + c = a + (b + c) := by
-  sorry
+protected theorem lt_iff_blt {x y : Rat} : x < y ↔ x.blt y := by
+  simp only [LT.lt]
+
+protected theorem le_iff_blt {x y : Rat} : x ≤ y ↔ ¬ y.blt x := by
+  simp [LE.le]
+
+protected theorem lt_asymm {x y : Rat} : x < y → ¬ y < x := by
+  simp [Rat.lt_iff_blt]
+  simp [Rat.blt]
+  intro h
+  cases h with
+  | inl h =>
+    simp [Int.not_lt_of_lt_rev h.1, Int.not_le.mpr h.1, Int.le_of_lt h.1]
+    intro nz_ynum ynum_neg _
+    apply ynum_neg
+    apply Int.lt_of_le_of_ne h.2
+    intro h
+    apply nz_ynum
+    rw [h]
+  | inr h =>
+    split at h
+    case isTrue xnum_0 =>
+      simp [Int.not_lt_of_lt_rev h, xnum_0, h]
+    case inr xnum_ne_0 =>
+      let ⟨h, h'⟩ := h
+      simp [Int.not_lt_of_lt_rev h']
+      cases h
+      case inl h =>
+        simp [h]
+        intro _ xnum_pos
+        apply h
+        apply Int.lt_of_le_of_ne xnum_pos
+        intro eq ; apply xnum_ne_0 ; rw [eq]
+      case inr h =>
+        simp [Int.not_le.mp h |> Int.not_lt_of_lt_rev]
+        intro eq
+        rw [eq] at h
+        contradiction
+
+end le_lt_basics
+
+section add_basics
+
+variable (a b c : Rat)
+
+protected theorem add_comm : a + b = b + a := by
+  simp [add_def, Int.add_comm, Int.mul_comm, Nat.mul_comm]
+
+protected theorem add_zero : ∀ a : Rat, a + 0 = a
+| ⟨num, den, _h, _h'⟩ => by
+  simp [Rat.add_def]
+  simp only [Rat.normalize_eq_mkRat, Rat.mk_eq_normalize]
+
+protected theorem zero_add : 0 + a = a :=
+  Rat.add_comm a 0 ▸ Rat.add_zero a
+
+protected theorem add_assoc : a + b + c = a + (b + c) :=
+  numDenCasesOn' a fun n₁ d₁ h₁ =>
+  numDenCasesOn' b fun n₂ d₂ h₂ =>
+  numDenCasesOn' c fun n₃ d₃ h₃ => by
+    simp only [
+      ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂,
+      Rat.divInt_add_divInt, Int.mul_eq_zero, or_self, h₃
+    ]
+    rw [Int.mul_assoc, Int.add_mul, Int.add_mul, Int.mul_assoc, Int.add_assoc]
+    congr 2
+    ac_rfl
+
+end add_basics
+
+section mul_basics
+
+variable {a b : Rat}
+
+protected theorem mul_eq_zero_iff : a * b = 0 ↔ a = 0 ∨ b = 0 := by
+  constructor
+  · simp only [Rat.mul_def, Rat.normalize_eq_zero]
+    intro h
+    cases Int.mul_eq_zero.mp h
+    · apply Or.inl
+      rw [Rat.eq_mkRat a, Rat.mkRat_eq_zero]
+      assumption
+      exact a.den_nz
+    · apply Or.inr
+      rw [Rat.eq_mkRat b, Rat.mkRat_eq_zero]
+      assumption
+      exact b.den_nz
+  · intro
+    | .inl h => simp only [h, Rat.zero_mul]
+    | .inr h => simp only [h, Rat.mul_zero]
+
+protected theorem mul_ne_zero_iff : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by
+  simp only [not_congr (@Rat.mul_eq_zero_iff a b), not_or, ne_eq]
+
+protected theorem mul_assoc (a b c : Rat) : a + b + c = a + (b + c) :=
+  numDenCasesOn' a fun n₁ d₁ _h₁ =>
+  numDenCasesOn' b fun n₂ d₂ _h₂ =>
+  numDenCasesOn' c fun n₃ d₃ _h₃ => by
+    simp only [Rat.divInt_ofNat]
+    exact Rat.add_assoc _ _ _
+
+end mul_basics
+
+section num_related
+
+variable {q : Rat}
+
+@[simp]
+theorem neg_neg : - -q = q := by
+  rw [← Rat.mkRat_self q]
+  simp [Rat.neg_mkRat]
+
+@[simp]
+theorem num_eq_zero : q.num = 0 ↔ q = 0 := by
+  induction q
+  constructor
+  · rintro rfl
+    exact mk'_zero _ _ _
+  · exact congr_arg num
 
-protected theorem mul_assoc (a b c : Rat) : a * b * c = a * (b * c) := by
-  sorry
+theorem num_ne_zero : q.num ≠ 0 ↔ q ≠ 0 := not_congr num_eq_zero
+
+@[simp]
+theorem num_nonneg : 0 ≤ q.num ↔ 0 ≤ q := by
+  simp [Int.le_iff_lt_or_eq, instLE, Rat.blt, Int.not_lt]
+  omega
+
+theorem nonneg_iff_sub_nonpos : 0 ≤ q ↔ -q ≤ 0 := by
+  rw [← num_nonneg]
+  conv => rhs ; simp [LE.le, Rat.blt]
+  omega
+
+theorem nonneg_sub_iff_nonpos : 0 ≤ -q ↔ q ≤ 0 := by
+  simp [nonneg_iff_sub_nonpos, Rat.neg_neg]
+
+@[simp]
+theorem num_nonpos : q.num ≤ 0 ↔ q ≤ 0 := by
+  conv => lhs ; rw [← Int.neg_nonneg]
+  simp [Rat.neg_num q ▸ @num_nonneg (-q)]
+  conv => rhs ; rw [← nonneg_sub_iff_nonpos]
+
+theorem not_nonpos : ¬ q ≤ 0 ↔ 0 < q := by
+  simp [Rat.lt_iff_blt, Rat.blt]
+  rw [← num_nonpos]
+  exact Int.not_le
+
+@[simp]
+theorem num_pos : 0 < q.num ↔ 0 < q := by
+  let tmp := not_congr (num_nonpos (q := q))
+  rw [Int.not_le] at tmp
+  simp [tmp, Rat.not_nonpos]
+
+theorem pos_iff_neg_nonpos : 0 < q ↔ -q < 0 := by
+  rw [← num_pos]
+  conv => rhs ; simp [Rat.lt_iff_blt] ; unfold Rat.blt ; simp
+  constructor <;> intro h
+  · apply Or.inl
+    exact num_pos.mp h
+  · let h : 0 < q := by
+      cases h
+      case inl h => exact h
+      case inr h => exact h.2.2
+    apply num_pos.mpr h
+
+@[simp]
+theorem num_neg : q.num < 0 ↔ q < 0 := by
+  let tmp := @num_pos (-q)
+  simp [Rat.neg_num q, Int.lt_neg_of_lt_neg] at tmp
+  rw [tmp]
+  apply Rat.neg_neg ▸ Rat.pos_iff_neg_nonpos (q := -q)
 
 @[simp]
 theorem num_neg_eq_neg_num (q : Rat) : (-q).num = -q.num :=
   rfl
 
 end num_related
 
-
-
 section le_lt_extra
 
 variable {x y : Rat}
@@ -71,8 +322,6 @@ protected theorem ne_of_lt : x < y → x ≠ y := by
 
 end le_lt_extra
 
-
-
 section nonneg
 
 variable (x : Rat)
@@ -90,8 +339,6 @@ protected theorem nonneg_antisymm : 0 ≤ x → 0 ≤ -x → x = 0 := by
 
 end nonneg
 
-
-
 section neg_sub
 
 variable {x y : Rat}
@@ -104,13 +351,13 @@ protected theorem neg_sub : -(x - y) = y - x := by
   rw [Nat.mul_comm dx dy]
   constructor
   · rw [← Int.neg_ediv_of_dvd]
-    rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.neg_sub]
-    rw [Int.neg_mul, ← Int.sub_eq_add_neg]
+    rw [← Int.sub_eq_add_neg, Int.neg_sub]
+    rw [← Int.sub_eq_add_neg]
     rw [← Int.natAbs_neg, Int.neg_sub]
     · conv => lhs ; arg 1 ; arg 2 ; rw [← Int.natAbs_ofNat (dy * dx)]
       exact Int.gcd_dvd_left
-  · rw [Int.neg_mul, ← Int.sub_eq_add_neg]
-    rw [Int.neg_mul, ← Int.sub_eq_add_neg]
+  · rw [← Int.sub_eq_add_neg]
+    rw [← Int.sub_eq_add_neg]
     rw [← Int.natAbs_neg, Int.neg_sub]
 
 @[simp]
@@ -197,8 +444,6 @@ protected theorem sub_nonneg {a b : Rat} : 0 ≤ a - b ↔ b ≤ a := by
 
 end neg_sub
 
-
-
 section divInt
 
 @[simp]
@@ -218,7 +463,7 @@ protected theorem divInt_le_divInt
   rw [Rat.divInt_add_divInt]
   simp [Rat.divInt_nonneg_iff_of_pos_right (Int.mul_pos d0 b0)]
   rw [← Int.sub_nonneg (a := c * b)]
-  rw [Int.neg_mul, ← Int.sub_eq_add_neg]
+  rw [← Int.sub_eq_add_neg]
   · apply Int.lt_iff_le_and_ne.mp d0 |>.2 |>.symm
   · apply Int.lt_iff_le_and_ne.mp b0 |>.2 |>.symm