Retreat demo changes.

Author: abdoo8080

Smt/Preprocess.lean

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed, Tomaz Gomes Mascarenhas
 -/
 
+import Smt.Preprocess.Decidable
 import Smt.Preprocess.Iff
 import Smt.Preprocess.Mono
 import Smt.Preprocess.PushHintsToCtx

Smt/Preprocess/Basic.lean

@@ -27,8 +27,9 @@ def getPropHyps : MetaM (Array FVarId) := do
   return result
 where
   isNonEmpty (e : Expr) : Bool :=
-  match_expr e with
-  | Nonempty _ => true
+  match e with
+  | .app (.const ``Nonempty _) _ => true
+  | .forallE _ _ b _ => isNonEmpty b
   | _ => false
 
 end Smt.Preprocess

Smt/Preprocess/Decidable.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2021-2024 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 Lean
+import Smt.Preprocess.Basic
+
+namespace Smt.Preprocess
+
+theorem classical_ite_congr {α : Sort u} {c₁ c₂ : Prop} {h₁ : Decidable c₁} {t₁ t₂ e₁ e₂ : α}
+    (hc : c₁ = c₂) (ht : t₁ = t₂) (he : e₁ = e₂) :
+    @ite α c₁ h₁ t₁ e₁ = @ite α c₂ (Classical.propDecidable c₂) t₂ e₂ := by
+  grind
+
+open Lean
+
+def replaceIteDecidableInst (e : Expr) : MetaM Expr := do
+  go #[] e
+where
+  go (xs : Array Expr) (e : Expr) : MetaM Expr := do
+  match e with
+  | mkApp3 (.const ``ite us) α c (.app (.const ``Classical.propDecidable []) _) =>
+    let α ← go xs α
+    let c ← go xs c
+    match ← Meta.synthInstance? (.app (.const ``Decidable []) (c.instantiateRev xs)) with
+    | some h => return mkApp3 (.const ``ite us) α c h
+    | none    => return e
+  | .app f a         =>
+    let f ← go xs f
+    let a ← go xs a
+    return e.updateApp! f a
+  | .lam n t b bi     =>
+    let t ← go xs t
+    Meta.withLocalDecl n bi (t.instantiateRev xs) fun x => do
+      Meta.mkLambdaFVars #[x] (← go (xs.push x) b) false false false false
+  | .forallE n t b bi =>
+    let t ← go xs t
+    Meta.withLocalDecl n bi (t.instantiateRev xs) fun x => do
+      Meta.mkForallFVars #[x] (← go (xs.push x) b)  false false false
+  | .letE n t v b nd  =>
+    let t ← go xs t
+    let v ← go xs v
+    Meta.withLetDecl n t v (nondep := nd) fun x => do
+      Meta.mkLetFVars #[x] (← go (xs.push x) b) false false
+  | .proj _ _ b      =>
+    return e.updateProj! (← go xs b)
+  | .mdata _ a       =>
+    return e.updateMData! (← go xs a)
+  | _                =>
+    return e
+
+def mkEqIteDecidableInst (e : Expr) : MetaM Expr := do
+  let e' ← replaceIteDecidableInst e
+  Meta.mkAppM ``Eq #[e, e']
+
+def containsClassicalPropDecidable (e : Expr) : Bool :=
+  (Expr.const ``Classical.propDecidable []).occurs e
+
+def replaceIteInst (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.withContext do
+  let t ← instantiateMVars (← mv.getType)
+  let ts ← hs.mapM (Meta.inferType · >>= instantiateMVars)
+  if !(containsClassicalPropDecidable t || ts.any containsClassicalPropDecidable) then
+    return { map := Std.HashMap.insertMany ∅ (hs.zip (hs.map .singleton)), hs, mv }
+  let simpTheorems ← #[``eq_self, ``classical_ite_congr].foldlM (·.addConst ·) {}
+  let simpTheorems := #[simpTheorems]
+  let congrTheorems := {}
+  let ctx ← Meta.Simp.mkContext {} simpTheorems congrTheorems
+  let (hs', mv') ← replaceIteInstLocalDecls mv hs.toList ctx #[]
+  let mv' ← replaceIteInstTarget mv' ctx
+  return { map := Std.HashMap.insertMany ∅ (hs'.zip (hs.map .singleton)), hs := hs', mv := mv' }
+where
+  replaceIteInstLocalDecls mv hs ctx hs' := do match hs with
+    | [] => return (hs', mv)
+    | h :: hs =>
+      let type ← Meta.inferType h
+      let eq ← mkEqIteDecidableInst (← instantiateMVars type)
+      let (_, l, r) := eq.eq?.get!
+      if l == r then
+        replaceIteInstLocalDecls mv hs ctx (hs'.push h)
+      else
+        let (res, _) ← Meta.simp eq ctx
+        let h' := mkApp4 (.const ``Eq.mp [0]) l r (mkOfEqTrue eq (← res.getProof)) h
+        if let .some fv := h.fvarId? then
+          let res ← mv.replace fv h' (.some r)
+          let hs' := hs'.map res.subst.apply
+          let hs := hs.map res.subst.apply
+          res.mvarId.withContext (replaceIteInstLocalDecls res.mvarId hs ctx (hs'.push (.fvar res.fvarId)))
+        else
+          replaceIteInstLocalDecls mv hs ctx (hs'.push h')
+      termination_by hs.length
+  replaceIteInstTarget mv ctx := mv.withContext do
+    let eq ← mkEqIteDecidableInst (← instantiateMVars (← mv.getType))
+    let (res, _) ← Meta.simp eq ctx
+    if res.expr.isTrue then
+      mv.replaceTargetEq eq.appArg! (mkOfEqTrue eq (← res.getProof))
+    else
+      return mv
+  mkOfEqTrue p hpt :=
+    mkApp2 (.const ``of_eq_true []) p hpt
+
+end Smt.Preprocess

Smt/Reconstruct/UF.lean

@@ -24,7 +24,13 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
 
 @[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with
   | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol!
-  | _ => return none
+  | _ =>
+    if s.isInstantiated then
+      let base ← reconstructSort s.getUninterpretedSortConstructor!
+      let params ← s.getInstantiatedParameters!.mapM reconstructSort
+      return some (mkAppN base params)
+    else
+      return none
 
 @[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
   | .APPLY_UF =>

Smt/Tactic/Smt.lean

@@ -32,6 +32,8 @@ structure Config where
   mono : Bool := false
   /-- Whether to eliminate `↔` in the Lean goal before sending it to the SMT solver. -/
   elimIff : Bool := true
+  /-- Whether to replace `ite` instances in the Lean goal before sending it to the SMT solver. -/
+  replaceIteInst : Bool := true
   /-- Whether to trust the result of the SMT solver. Closes the current goal with a `sorry` if the
       SMT solver returns `unsat`. **Warning**: use with caution, as this may lead to unsoundness.
       Additionally adds the translation from Lean to SMT to the trusted code base, which is not
@@ -71,11 +73,12 @@ def smt (cfg : Config) (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.with
   let ⟨map₁, hs₁, mv₂⟩ ← (if cfg.mono then Preprocess.mono else Preprocess.pushHintsToCtx) mv₁ hs
   -- 2. Preprocess the hypotheses and goal.
   let ⟨map₂, hs₂, mv₂⟩ ← if cfg.elimIff then Preprocess.elimIff mv₂ hs₁ else pure ⟨map₁, hs₁, mv₂⟩
-  mv₂.withContext do
-  let goalType : Q(Prop) ← mv₂.getType
+  let ⟨map₃, hs₃, mv₃⟩ ← if cfg.replaceIteInst then Preprocess.replaceIteInst mv₂ hs₂ else pure ⟨map₂, hs₂, mv₂⟩
+  mv₃.withContext do
+  let goalType : Q(Prop) ← mv₃.getType
   -- 3. Generate the SMT query.
   let (fvNames₁, fvNames₂) ← genUniqueFVarNames
-  let cmds ← prepareSmtQuery hs₂.toList (← mv₂.getType) fvNames₁
+  let cmds ← prepareSmtQuery hs₃.toList (← mv₃.getType) fvNames₁
   let cmds := .setLogic "ALL" :: cmds
   if cfg.showQuery then
     logInfo m!"goal: {goalType}\n\nquery:\n{Command.cmdsAsQuery (cmds ++ [.checkSat])}"
@@ -85,6 +88,7 @@ def smt (cfg : Config) (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.with
     trace[smt] "goal: {goalType}"
     trace[smt] "\nquery:\n{Command.cmdsAsQuery (cmds ++ [.checkSat])}"
   -- 4. Run the solver.
+  -- throwError "here1"
   let res ← solve (Command.cmdsAsQuery cmds) cfg.timeout (defaultSolverOptions ++ cfg.extraSolverOptions)
   -- trace[smt] "\nresult: {res}"
   match res with
@@ -101,9 +105,12 @@ def smt (cfg : Config) (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.with
     let ctx := { userNames := fvNames₂, native := cfg.native }
     let (uc, _) ← (uc.mapM Reconstruct.reconstructTerm).run ctx {}
     trace[smt] "unsat core: {uc}"
-    let ts₂ ← hs₂.mapM Meta.inferType
-    let uc := uc.filterMap fun p => ts₂.findIdx? (· == p) >>= (hs₂[·]?)
-    let uc := uc.filterMap (map₂[·]?)
+    trace[smt] "unsat core: {mv₃}"
+    -- throwError "here2"
+    let ts₃ ← hs₃.mapM Meta.inferType
+    let uc := uc.filterMap fun p => ts₃.findIdx? (· == p) >>= (hs₃[·]?)
+    let uc := uc.filterMap (map₃[·]?)
+    let uc := uc.flatten.filterMap (map₂[·]?)
     let uc := uc.flatten.filterMap (map₁[·]?)
     let uc := hs.filter uc.flatten.contains
     if cfg.trust then
@@ -112,10 +119,10 @@ def smt (cfg : Config) (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.with
       return .unsat [] uc
     -- 7. Reconstruct proof.
     let (_, ps, p, hp, mvs) ← reconstructProof pf ctx
-    let mv₂ ← mv₂.assert (← mkFreshId) p hp
-    let ⟨_, mv₂⟩ ← mv₂.intro1
-    let mut gs ← mv₂.apply (← Meta.mkAppOptM ``Prop.implies_of_not_and #[listExpr ps.dropLast q(Prop), goalType])
-    mv₂.withContext (gs.forM (·.assumption))
+    let mv₃ ← mv₃.assert (← mkFreshId) p hp
+    let ⟨_, mv₃⟩ ← mv₃.intro1
+    let mut gs ← mv₃.apply (← Meta.mkAppOptM ``Prop.implies_of_not_and #[listExpr ps.dropLast q(Prop), goalType])
+    mv₃.withContext (gs.forM (·.assumption))
     mv.assign (.mvar mv₁)
     return .unsat mvs uc
   | .ok (.sat model) =>
@@ -242,11 +249,29 @@ def elabHints : TSyntax ``smtHints → TacticM (Std.HashMap Expr (TSyntax ``smtH
   | `(smtHints| ) => return ({}, #[])
   | _ => throwUnsupportedSyntax
 
+/-- Returns `true` if `fv` corresponds to a proposition in the local context. -/
+def isPropHyp (fv : FVarId) : MetaM Bool := do
+  let localDecl ← fv.getDecl
+  unless localDecl.isImplementationDetail do
+    if ← pure !(isNonEmpty localDecl.type) <&&> Meta.isProp localDecl.type then
+      return true
+  return false
+where
+  isNonEmpty (e : Expr) : Bool :=
+  match e with
+  | .app (.const ``Nonempty _) _ => true
+  | .forallE _ _ b _ => isNonEmpty b
+  | _ => false
+
 def evalSmtCore (cfg : TSyntax ``Parser.Tactic.optConfig) (hs : TSyntax ``smtHints) := withMainContext do
   let cfg ← elabConfig cfg
-  let mv ← Tactic.getMainGoal
   let (map, hs) ← elabHints hs
-  let res ← Smt.smt cfg mv hs
+  let mv ← Tactic.getMainGoal
+  let (fvs, mv) ← mv.intros
+  Tactic.replaceMainGoal [mv]
+  let fvs ← liftM (mv.withContext (fvs.filterM isPropHyp))
+  let hs' := fvs.map Expr.fvar
+  let res ← Smt.smt cfg mv (hs ++ hs')
   match res with
     | .sat none =>
       throwError "unable to prove goal, either it is false or you need to provide more facts. Try adding '+model' config option to display a potential counter-example (experimental)."
@@ -260,6 +285,7 @@ def evalSmtCore (cfg : TSyntax ``Parser.Tactic.optConfig) (hs : TSyntax ``smtHin
         throwError "unable to prove goal, either it is false or you need to provide more facts. Here is a potential counter-example:\n{md}"
     | .unsat mvs uc =>
       Tactic.replaceMainGoal mvs
+      let uc := uc.filter (!hs'.contains ·)
       let uc := uc.filterMap map.get?
       let uc := uc.toList.eraseDups.toArray
       return uc

lake-manifest.json

@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "77f45ae314d657466853138a61cba8fca00094c8",
+   "rev": "5d96f48fbcee46a5bc35c49121ed3d81fd54af4b",
    "name": "cvc5",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "77f45ae314d657466853138a61cba8fca00094c8",
+   "inputRev": "5d96f48fbcee46a5bc35c49121ed3d81fd54af4b",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",

lakefile.lean

@@ -6,7 +6,7 @@ require auto from
   git "https://github.com/leanprover-community/lean-auto.git" @ "2c088e7617d6e2018386de23b5df3b127fae4634"
 
 require cvc5 from
-  git "https://github.com/abdoo8080/lean-cvc5.git" @ "77f45ae"
+  git "https://github.com/abdoo8080/lean-cvc5.git" @ "5d96f48fbcee46a5bc35c49121ed3d81fd54af4b"
 
 require mathlib from
   git "https://github.com/leanprover-community/mathlib4.git" @ "v4.23.0"