Syncing Proof Reconstruction (#67)

* change interface of factor * generalize smtCong * andElim, true/false elim/intro * fix order of output or-chain in R2 * fix inferring of smtCong to use * completing flipped resolution thms * fixed flipped lengths in resolution * fix: instantiateMVars in smtCong * fix: infer which resolution_thm to use * feat: resolution don't need the goal in the context anymore * added script for building only Reconstruction/Certifying * new tactic: notOrElim * rename doubleNeg to notNotElim * iteElim * cnfOrNeg * cnfOrNeg * missing only one rule * fix warnings * finished all rules from boolean * update lakefile * update lakefile * fix bug in andElim * comment profiling logs * added rule for neg_symm * new tactic: LiftOrNToNeg * adding liftOrNToNeg to Certifying.lean * small fix on resolution * fix bug in pull * new parameter for resolution - adapted Pull to use this new parameter instead of backtrack; - resolution will group the correct suffix in the resulting expression. Example: h1 := A \/ B \/ C \/ D h2 := E \/ (Not B) \/ F \/ G R1 h1, h2, B, [2, -1] := A \/ (C \/ D) \/ E \/ F \/ G * added new parameter for factor and fix it's ambiguity * changing Iff to Eq * removing unnecessary pullTail * fix on permutateOr (big example is now working) * arithmetic tactic for naturals * Int arith rules * added all rules for arithmetic reasoning * added tactic for trichotomy * tighting bounds (unfinished) * update on tight bounds * bump lean version * complete first theorem * almost finished last lemma * finished bounds lemmas (refactor needed) * some refactors in TightBounds * fix on liftOrNToImp * refactor tight bounds * added macro for flipped version of notAnd and congrIte * remove unused theorems in Boolean * added import to tightbounds * removed nat arith * fix on permutateOr * fix on liftorntoneg * using builtin modus tollens * change parameters to implicit in cnf rules * bump lean version, update examples and enabling benchmark of tactics * new trace option for profiler * using trace[smt.profile] instead of loginfo * exposing instances of LinearOrder * Generalizing sumBounds to work with n arguments * sumBounds: more examples * ...I guess? * updating #elab * fix: trichotomy for LE.le and GE.ge * new rule: mulPosNeg * neg version of mulPosNeg * fixed lemmas about ceil and floor * castLT * [quant] Changing to equality conclusions, adding Skolemization example * [quant] Have instForall require body, instantiation Also adds a macro to pass premise first and an example with two instantiated variables. * tactic for tight bounds * change flip inst macro to finish it with endline probably there is a better solution than to use brackets, but this one was simple enough to do * tactic for intTightLb * fix on groupOrPrefix * erase code on Options.lean * macro for flipping congrArg * improving andElim and notOrElim * moving from boolean.lean to util.lean * expanding macros at andElim * hiding Rat from Lean * Unpolished changes useful for demo. * Slight changes to demo. * macro for decidable ite * fixing new let declaration in liftOrNToImp expanding types in liftOrNImp * removing unnecessary * removing examples * removing old example * bumping lean version * update .gitignore * new implementation for groupOrPrefix using only MetaM * ported liftorntoimp * fixing order of arguments congOrLeft * removing bench script * removing git mark * fixing build * pullToMiddle working up to step 2 * pull working up to step 3 * pullToMiddle working! * pull complete * liftOrNToNeg done * rename pullCore' -> pullCore * rename groupPrefixCore' -> groupPrefixCore * PermutateOr ported * resolution and boolean * moving timed theorems * factor done * timed factor * adding copyright notice * adding namespaces * revert gitignore * remove profile script from lakefile * revert Smt/Int.lean * moving examples * removing abbrev Implies to avoid ambiguity * using just the namespace Smt.Reconstruction.Certifying for all reconstruction files * skipping examples and reconstruction in tests * Update lakefile.lean Co-authored-by: Abdalrhman Mohamed <[email protected]> * fix on resolution * stop using panic in mulposneg * new util function * fix on permutateor * remove unnecessary do * changing interface for all tactics, automatically close goal * getting rid of panic! * fix on liftorntoimp * added tests for reconstruction * adding tests for each tactic * removing benchmark tests * changing interface for arithMulPosNeg * metaM for mulPosNeg * ported sumBounds to metaM * porting tightBounds to MetaM * porting trichotomy to MetaM * fix: mulPosNeg can receive arbitrary expressions * remove commentary * added lemmas required for arithMulSign * half arithMulSign * remove bench * arithMulSign done * fix on arithMulSign * arithMulSign works with mixed types * fix on notOrElim * congruence over addition * patch on mulPosNeg to support literals as parameters * arithMulPos/Neg supports equality * arithMulSign supports arbitrary expressions * arithMulSign refactor and supports NZ * cleanup arithMulSign * more cleanup arithMulSign * more cleanup arithMulSign * patch on getOp * testing update on process_lean_smt * revert testing log * added theorems for tangent plane * bump mathlib and lean version new mathlib version contains transcendental functions * bump mathlib * tracing profile for resolution * testing log * adding profile traces * changing milliseconds to nanoseconds * iteIntro * iteIntro not just for props * iteIntro with explicit parameters * fixes on mulPosNeg and sumBounds and iteIntro * timed tactic * fix tests for associativity on arith * fix on factor, pullToMiddle and createOrChain * exporting TimedBoolean * fix test on mulposneg * groupClausePrefix * fix on permutateOr * test * using tactics without setting the goal * fix on factor * timed supports macros and theorems without parameters * typo * props example * add README on certified * support for sharing in boolean tactics * typo on factor * more tests * fix on mulPosNeg * expanding lets on arith tactics * fixing propsExample * erase certified * adding examples of proof scripts * improvement on propsExample * deleting tightbounds/castlt * fix on tight bounds * removing TimedTheorems * remove test and rename timed * rolling back Certified/ (not part of this PR) * rolling back Certified/ (not part of this PR) * removing stuff from PR * TimedBoolean -> Timed * moving tests to the tests folder * removing support for nat in sumbounds * added universe parameter for congrIte * added universe parameter for iteIntro * new tactic for congruence * fix on expandLet * remove blank line * simplification * update * removing library search * removing expand let (fix tests) * lake manifest * changing unique identifiers on test --------- Co-authored-by: Tomaz Gomes Mascarenhas <[email protected]> Co-authored-by: Haniel Barbosa <[email protected]> Co-authored-by: Abdalrhman M Mohamed <[email protected]>
ufmg-smite · Nov 8, 2023 · 666dbd8 · 666dbd8
1 parent 7b461ed
commit 666dbd8
Show file tree

Hide file tree

Showing 37 changed files with 1,310 additions and 594 deletions.
diff --git a/Smt/Reconstruction/Certifying.lean b/Smt/Reconstruction/Certifying.lean
@@ -1,11 +1,13 @@
 import Smt.Reconstruction.Certifying.Boolean
+import Smt.Reconstruction.Certifying.Congruence
 import Smt.Reconstruction.Certifying.Factor
 import Smt.Reconstruction.Certifying.LiftOrNToImp
 import Smt.Reconstruction.Certifying.LiftOrNToNeg
 import Smt.Reconstruction.Certifying.PermutateOr
 import Smt.Reconstruction.Certifying.Pull
 import Smt.Reconstruction.Certifying.Quant
 import Smt.Reconstruction.Certifying.Resolution
+import Smt.Reconstruction.Certifying.Timed
 import Smt.Reconstruction.Certifying.Util
 import Smt.Reconstruction.Certifying.Arith
 import Smt.Reconstruction.Rewrites.Arith

diff --git a/Smt/Reconstruction/Certifying/Arith.lean b/Smt/Reconstruction/Certifying/Arith.lean
@@ -5,7 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomaz Gomes Mascarenhas
 -/
 
+import Smt.Reconstruction.Certifying.Arith.ArithMulSign
 import Smt.Reconstruction.Certifying.Arith.MulPosNeg
 import Smt.Reconstruction.Certifying.Arith.SumBounds
-import Smt.Reconstruction.Certifying.Arith.Trichotomy
+import Smt.Reconstruction.Certifying.Arith.TangentPlane
 import Smt.Reconstruction.Certifying.Arith.TightBounds
+import Smt.Reconstruction.Certifying.Arith.Trichotomy
diff --git a/Smt/Reconstruction/Certifying/Arith/ArithMulSign.lean b/Smt/Reconstruction/Certifying/Arith/ArithMulSign.lean
@@ -0,0 +1,13 @@
+/-
+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
+-/
+
+-- 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
+
diff --git a/Smt/Reconstruction/Certifying/Arith/ArithMulSign/Lemmas.lean b/Smt/Reconstruction/Certifying/Arith/ArithMulSign/Lemmas.lean
@@ -0,0 +1,102 @@
+import Smt.Reconstruction.Certifying.Arith.MulPosNeg
+import Smt.Reconstruction.Certifying.Boolean
+
+import Mathlib.Algebra.Parity
+import Mathlib.Data.Nat.Parity
+
+open Smt.Reconstruction.Certifying
+
+variable {α : Type}
+
+variable [LinearOrderedRing α]
+
+variable {a b : α}
+
+mutual
+
+theorem powNegEven : ∀ {k : Nat} {z : α}, z < 0 → Even k → z ^ k > 0 := by
+  intros k z h₁ h₂
+  cases k with
+  | zero    => simp
+  | succ k' =>
+    have k'NotEven := Nat.even_add_one.mp h₂
+    have k'Odd := Nat.odd_iff_not_even.mpr k'NotEven
+    have rc := powNegOdd h₁ k'Odd
+    simp [Pow.pow]
+    have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
+    simp at mulZ
+    rw [pow_succ]
+    exact mulZ
+
+theorem powNegOdd : ∀ {k : Nat} {z : α}, z < 0 → Odd k → z ^ k < 0 := by
+  intros k z h₁ h₂
+  cases k with
+  | zero    => simp at h₂
+  | succ k' =>
+    simp at h₂
+    have k'Even := notNotElim (mt Nat.even_add_one.mpr h₂)
+    have rc := powNegEven h₁ k'Even
+    simp [Int.pow]
+    have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
+    simp at mulZ
+    rw [pow_succ]
+    exact mulZ
+
+end
+
+theorem powPos : ∀ {k : Nat} {z : α}, z > 0 → z ^ k > 0 := by
+  intro k z h
+  cases k with
+  | zero    => simp
+  | succ k' =>
+    have ih := @powPos k' z h
+    rw [pow_succ]
+    have h₂ := arith_mul_pos_lt ⟨h, ih⟩
+    simp at h₂
+    exact h₂
+
+theorem nonZeroEvenPow : ∀ {k : Nat} {z : α},
+    z ≠ 0 → Even k → z ^ k > 0 := by
+  intros k z h₁ h₂
+  match lt_trichotomy z 0 with
+  | Or.inl zNeg => exact powNegEven zNeg h₂
+  | Or.inr (Or.inl zZero) => rw [zZero] at h₁; simp at h₁
+  | Or.inr (Or.inr zPos)  => exact powPos zPos
+
+theorem combineSigns₁ : a > 0 → b > 0 → b * a > 0 := by
+  intros h₁ h₂
+  have h := mul_lt_mul_of_pos_left h₁ h₂
+  simp at h
+  exact h
+
+theorem combineSigns₂ : a > 0 → b < 0 → b * a < 0 := by
+  intros h₁ h₂
+  have h := mul_lt_mul_of_pos_right h₂ h₁
+  simp at h
+  exact h
+
+theorem combineSigns₃ : a < 0 → b > 0 → b * a < 0 := by
+  intros h₁ h₂
+  have h := mul_lt_mul_of_pos_left h₁ h₂
+  simp at h
+  exact h
+
+theorem combineSigns₄ : a < 0 → b < 0 → b * a > 0 := by
+  intros h₁ h₂
+  have h := mul_lt_mul_of_neg_left h₁ h₂
+  simp at h
+  exact h
+
+theorem castPos : ∀ (a : Int), a > 0 → Rat.ofInt a > 0 := by
+  intros a h
+  simp [h]
+
+theorem castNeg : ∀ (a : Int), a < 0 → Rat.ofInt a < 0 := by
+  intros a h
+  simp [h]
+
+instance : HMul ℤ ℚ ℚ where
+  hMul z q := Rat.ofInt z * q
+
+instance : HMul ℚ ℤ ℚ where
+  hMul q z := q * Rat.ofInt z
diff --git a/Smt/Reconstruction/Certifying/Arith/ArithMulSign/Tactic.lean b/Smt/Reconstruction/Certifying/Arith/ArithMulSign/Tactic.lean
@@ -0,0 +1,149 @@
+import Lean
+
+import Mathlib.Data.Nat.Parity
+
+import Smt.Reconstruction.Certifying.Util
+import Smt.Reconstruction.Certifying.Arith.ArithMulSign.Lemmas
+import Smt.Reconstruction.Certifying.Arith.MulPosNeg.Instances
+
+open Lean Elab Tactic Meta Expr
+open Smt.Reconstruction.Certifying
+
+inductive Pol where
+ | Neg : Pol
+ | NZ  : Pol
+ | Pos : Pol
+ deriving BEq
+
+--              var names/neg or pos/ exponents
+-- arithMulSign [a, b, c] [1, -1, 1], [2, 3, 1]
+syntax (name := arithMulSign) "arithMulSign" ("[" term,* "]")? "," ("[" term,* "]") "," ("[" term,* "]")? : tactic
+
+def parseArithMulSign : Syntax → TacticM (List (Expr × Pol × Nat))
+  | `(tactic| arithMulSign [ $[$ns],* ], [ $[$bs],* ], [ $[$es],* ]) => do
+    let exprs: List Expr ←
+      ns.toList.mapM (fun h: Term => elabTerm h none)
+    let bools: List Pol ←
+      bs.toList.mapM (fun h: Term => do
+                      let hExpr ← elabTerm h none
+                      match getNatLit? hExpr with
+                      | none   => pure Pol.Neg
+                      | some 0 => pure Pol.NZ
+                      | some 1 => pure Pol.Pos
+                      | _      => throwError "[arithMulSign]: invalid polarity"
+                    )
+    let exps : List Nat ← es.toList.mapM stxToNat
+    pure (exprs.zip (bools.zip exps))
+  | _ => throwError "[ArithMulSign]: wrong syntax"
+
+@[tactic arithMulSign] def evalArithMulSign : Tactic := fun stx => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+    trace[smt.profile] m!"[arithMulSign] start time: {← IO.monoNanosNow}ns"
+    let data ← parseArithMulSign stx
+    let answer ← go true data (mkConst `empty) (mkConst `empty)
+    let answerType ← inferType answer
+    let fname ← mkFreshId
+    let (_, mvar') ← MVarId.intro1P $ ← mvar.assert fname answerType answer
+    replaceMainGoal [mvar']
+    evalTactic (← `(tactic| exact $(mkIdent fname)))
+    trace[smt.profile] m!"[arithMulSign] end time: {← IO.monoNanosNow}ns"
+where
+-- acc is a partial proof corresponding to the sign of the prefix of the multiplication
+  go (first : Bool) (xs : (List (Expr × Pol × Nat))) (prodSignPf : Expr) (prod : Expr) : MetaM Expr :=
+    match xs with
+    | [] => return prodSignPf
+    | (expr, pol, exp) :: t => do
+      let exprType ← inferType expr
+      let exprIsInt ←
+        match exprType with
+        | .const `Rat .. => pure false
+        | .const `Int .. => pure true
+        | _ => throwError "[arithMulSign]: unexpected type for expression"
+      let lorInst := mkConst $
+        if exprIsInt then ``lorInt else ``lorRat
+      let zeroI := mkApp (mkConst ``Int.ofNat) (mkNatLit 0)
+      let zeroR := mkApp (mkConst ``Rat.ofInt) zeroI
+      -- zero with the same type as the current argument
+      let currZero := if exprIsInt then zeroI else zeroR
+      let bindedType: Expr ←
+        match pol with
+        | Pol.Neg => mkAppM ``LT.lt #[expr, currZero]
+        | Pol.NZ  => mkAppM ``Ne    #[expr, currZero]
+        | Pol.Pos => mkAppM ``GT.gt #[expr, currZero]
+      let expParityPf ← do
+        if exp % 2 == 0 then
+          let rflExpr ← mkAppOptM ``rfl #[(mkConst ``Nat), (mkNatLit 0)]
+          let iffExp := mkApp (mkConst ``Nat.even_iff) (mkNatLit exp)
+          mkAppM ``Iff.mpr #[iffExp, rflExpr]
+        else
+          let rflExpr ← mkAppOptM ``rfl #[(mkConst ``Nat), (mkNatLit 1)]
+          let iffExp := mkApp (mkConst ``Nat.odd_iff) (mkNatLit exp)
+          mkAppM ``Iff.mpr #[iffExp, rflExpr]
+      withLocalDeclD (← mkFreshId) bindedType $ fun bv => do
+        let exprPowSignPf ←
+          if exp == 1 then
+            pure bv
+          else
+            match pol with
+            | Pol.NZ =>
+              pure $ mkApp6 (mkConst ``nonZeroEvenPow) exprType lorInst (mkNatLit exp) expr bv expParityPf
+            | Pol.Pos =>
+              pure $ mkApp5 (mkConst ``powPos) exprType lorInst (mkNatLit exp) expr bv
+            | Pol.Neg =>
+              if exp % 2 == 0 then
+                mkAppM ``powNegEven #[bv, expParityPf]
+              else
+                mkAppM ``powNegOdd #[bv, expParityPf]
+        let exprPow ←
+          if exp == 1 then
+            pure expr
+          else mkAppM ``Pow.pow #[expr, mkNatLit exp]
+        let prodType ←
+          if first then
+            pure exprType
+          else inferType prod
+        let prodIsInt ←
+          match prodType with
+          | .const `Int .. => pure true
+          | .const `Rat .. => pure false
+          | _ => throwError "[arithMulSign]: unexpected type for accumulated product"
+        let prodSignPfType ←
+          if first then
+            inferType exprPowSignPf
+          else inferType prodSignPf
+        let prodPos := (← getOp prodSignPfType) == `GT.gt
+        -- normalize types in case one is rat and the other is int
+        let (exprPow', prod', exprPowSignPf', prodSignPf') :=
+          match exprIsInt, prodIsInt with
+          | false, true  =>
+            let prodSignPf' :=
+              if prodPos then
+                mkApp2 (mkConst ``castPos) prod prodSignPf
+              else mkApp2 (mkConst ``castNeg) prod prodSignPf
+            (exprPow, mkApp (mkConst ``Rat.ofInt) prod, exprPowSignPf, prodSignPf')
+          | true, false  =>
+            let exprPowSignPf' :=
+              if pol == Pol.Pos || pol == Pol.NZ || exp % 2 == 0 then
+                mkApp2 (mkConst ``castPos) exprPow exprPowSignPf
+              else mkApp2 (mkConst ``castNeg) exprPow exprPowSignPf
+            (mkApp (mkConst ``Rat.ofInt) exprPow, prod, exprPowSignPf', prodSignPf)
+          | _, _   => (exprPow, prod, exprPowSignPf, prodSignPf)
+        let answer ←
+          if first then pure exprPowSignPf
+          else
+            if pol == Pol.Pos || pol == Pol.NZ || exp % 2 == 0 then
+              if prodPos then
+                mkAppOptM ``combineSigns₁ #[none, none, exprPow', prod', exprPowSignPf', prodSignPf']
+              else mkAppOptM ``combineSigns₂ #[none, none, exprPow', prod', exprPowSignPf', prodSignPf']
+            else
+              if prodPos then
+                mkAppOptM ``combineSigns₃ #[none, none, exprPow', prod', exprPowSignPf', prodSignPf']
+              else mkAppOptM ``combineSigns₄ #[none, none, exprPow', prod', exprPowSignPf', prodSignPf']
+        let prod' ←
+          if first then
+            pure exprPow
+          else mkAppM ``Mul.mul #[prod', exprPow']
+        let rc ← go false t answer prod'
+        mkLambdaFVars #[bv] rc
+
diff --git a/Smt/Reconstruction/Certifying/Arith/MulPosNeg.lean b/Smt/Reconstruction/Certifying/Arith/MulPosNeg.lean
@@ -10,5 +10,6 @@ Authors: Tomaz Gomes Mascarenhas
 -- and
 -- https://cvc5.github.io/docs/cvc5-1.0.2/proofs/proof_rules.html#_CPPv4N4cvc58internal6PfRule14ARITH_MULT_NEGE
 
+import Smt.Reconstruction.Certifying.Arith.MulPosNeg.Instances
 import Smt.Reconstruction.Certifying.Arith.MulPosNeg.Lemmas
 import Smt.Reconstruction.Certifying.Arith.MulPosNeg.Tactic
diff --git a/Smt/Reconstruction/Certifying/Arith/MulPosNeg/Instances.lean b/Smt/Reconstruction/Certifying/Arith/MulPosNeg/Instances.lean
@@ -0,0 +1,6 @@
+import Mathlib.Data.Rat.Basic
+import Mathlib.Data.Rat.Order
+import Mathlib.Algebra.Order.Ring.Lemmas
+
+instance lorInt : LinearOrderedRing Int := inferInstance
+instance lorRat : LinearOrderedRing Rat := inferInstance