Merge remote-tracking branch 'upstream/main' into real

.github/workflows/ci.yml

@@ -13,6 +13,10 @@ jobs:
         - name: Linux
           os: ubuntu-latest
     steps:
+    - name: Install clang-15 (Linux)
+      if: matrix.os == 'ubuntu-latest'
+      run: |
+        sudo apt install clang-15 libc++-15-dev
     - name: Install Elan (Linux)
       if: matrix.os == 'ubuntu-latest'
       run: |

.gitignore

@@ -1,4 +1,2 @@
 /.vscode
-/build
-./lake-packages/*
-/lakefile.olean
+/.lake

Smt.lean

@@ -5,15 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.BitVec
-import Smt.Bool
-import Smt.Int
-import Smt.Nat
-import Smt.Prop
-import Smt.Rat
-import Smt.Solver
-import Smt.String
+import Smt.Reconstruct
 import Smt.Tactic
-import Smt.Term
-
-import Smt.Reconstruction.Certifying
+import Smt.Translate

Smt/Reconstruct.lean

@@ -0,0 +1,17 @@
+/-
+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: Abdalrhman Mohamed
+-/
+
+-- import Smt.Reconstruct.Arith
+import Smt.Reconstruct.Builtin
+import Smt.Reconstruct.Options
+import Smt.Reconstruct.Prop
+import Smt.Reconstruct.Quant
+import Smt.Reconstruct.Reconstruct
+import Smt.Reconstruct.Rewrite
+import Smt.Reconstruct.Timed
+import Smt.Reconstruct.UF
+import Smt.Reconstruct.Util

Smt/Reconstruct/Arith.lean

@@ -0,0 +1,17 @@
+/-
+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
+-/
+
+import Smt.Reconstruct.Arith.ArithMulSign
+import Smt.Reconstruct.Arith.MulPosNeg
+import Smt.Reconstruct.Arith.Rewrites
+import Smt.Reconstruct.Arith.SumBounds
+import Smt.Reconstruct.Arith.TangentPlane
+import Smt.Reconstruct.Arith.TightBounds
+import Smt.Reconstruct.Arith.Trichotomy
+
+-- Non-linear arithmetic is increasing compilation time too much
+-- import Smt.Reconstruct.Arith.TransFns

Smt/Reconstruction/Certifying/Arith/ArithMulSign.lean → Smt/Reconstruct/Arith/ArithMulSign.lean

@@ -8,6 +8,5 @@ Authors: Tomaz Gomes Mascarenhas
 -- implementation of:
 -- https://cvc5.github.io/docs/cvc5-1.0.2/proofs/proof_rules.html#_CPPv4N4cvc58internal6PfRule15ARITH_MULT_SIGNE
 
-import Smt.Reconstruction.Certifying.Arith.ArithMulSign.Lemmas
-import Smt.Reconstruction.Certifying.Arith.ArithMulSign.Tactic
-
+import Smt.Reconstruct.Arith.ArithMulSign.Lemmas
+import Smt.Reconstruct.Arith.ArithMulSign.Tactic

Smt/Reconstruction/Certifying/Arith/ArithMulSign/Lemmas.lean → Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean

@@ -1,18 +1,24 @@
-import Smt.Reconstruction.Certifying.Arith.MulPosNeg
-import Smt.Reconstruction.Certifying.Boolean
+/-
+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
+-/
 
 import Mathlib.Algebra.Parity
 import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Real.Basic
 
-open Smt.Reconstruction.Certifying
+import Smt.Reconstruct.Arith.MulPosNeg.Lemmas
+
+namespace Smt.Reconstruct.Arith
 
 variable {α : Type}
 
 variable [LinearOrderedRing α]
 
 variable {a b : α}
- 
+
 mutual
 
 theorem powNegEven : ∀ {k : Nat} {z : α}, z < 0 → Even k → z ^ k > 0 := by
@@ -35,7 +41,7 @@ theorem powNegOdd : ∀ {k : Nat} {z : α}, z < 0 → Odd k → z ^ k < 0 := by
   | zero    => simp at h₂
   | succ k' =>
     simp at h₂
-    have k'Even := notNotElim (mt Nat.even_add_one.mpr h₂)
+    have k'Even := of_not_not (mt Nat.even_add_one.mpr h₂)
     have rc := powNegEven h₁ k'Even
     simp [Int.pow]
     have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
@@ -101,3 +107,5 @@ instance : HMul ℤ ℝ ℝ where
 
 instance : HMul ℝ ℤ ℝ where
   hMul r z := r * Real.intCast.intCast z
+
+end Smt.Reconstruct.Arith