Run intros and contra automatically on goal.

Co-Authored-By: Qiyuan Zhao <[email protected]>

Author: abdoo8080

Smt/Preprocess.lean

@@ -6,6 +6,8 @@ Authors: Abdalrhman Mohamed, Tomaz Gomes Mascarenhas
 -/
 
 import Smt.Preprocess.Embedding
+import Smt.Preprocess.Intros
 import Smt.Preprocess.Mono
 import Smt.Preprocess.Normalize
+import Smt.Preprocess.NegateGoal
 import Smt.Preprocess.PushHintsToCtx

Smt/Preprocess/Embedding.lean

@@ -56,7 +56,7 @@ def embedding (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.withContext d
   let (fvs, mv) ← mv.revert fvs true
   -- Simplify the goal using the embedding theorems.
   let congrTheorems ← Meta.getSimpCongrTheorems
-  let ctx ← Meta.Simp.mkContext {} simpTheorems congrTheorems
+  let ctx ← Meta.Simp.mkContext { zeta := false } simpTheorems congrTheorems
   let (some mv, _) ← Meta.simpTarget mv ctx simpProcs (mayCloseGoal := false) | throwError "[embedding] simplification failed"
   -- Extend `fvs` to account for `nonneg` assumptions.
   let bts := bts.pop -- Do not consider `Bool` for assumptions.

Smt/Preprocess/Embedding/Nat.lean

@@ -17,6 +17,7 @@ attribute [embedding ↓] Int.cast_ofNat_Int
 attribute [embedding ↓] Int.natCast_add
 attribute [embedding ↓] Int.natCast_mul
 attribute [embedding ↓] Int.natCast_ediv
+attribute [embedding ↓] Int.natCast_emod
 attribute [embedding ↓ ←] Int.ofNat_inj
 attribute [embedding ↓ ←] Int.ofNat_le
 attribute [embedding ↓ ←] Int.ofNat_lt

Smt/Preprocess/Intros.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2021-2026 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.Preprocess.Basic
+import Lean.Meta.Tactic.Assert
+
+namespace Smt.Preprocess
+
+open Lean
+
+/-- 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 intros (mv : MVarId) (hs : Array Expr) : MetaM Result := do
+  let (fvs, mv) ← mv.intros
+  let hfvs := fvs.map Expr.fvar
+  return { map := Std.HashMap.insertMany {} (hfvs.zip (hfvs.map (#[·]))), hs := hs ++ hfvs, mv }
+
+end Smt.Preprocess

Smt/Preprocess/NegateGoal.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2021-2026 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.Preprocess.Basic
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Intro
+
+namespace Smt.Preprocess
+
+open Lean
+
+def negateGoal (mv : MVarId) (hs : Array Expr) : MetaM Result := do
+  let target ← mv.getType
+  if target.isFalse then return { map := {}, hs, mv }
+  let [mv] ← mv.applyConst ``Classical.byContradiction
+    | throwError "[negateGoal] Unexpected result after applying {``Classical.byContradiction}"
+  let (fv, mv) ← mv.intro1
+  return { map := Std.HashMap.insert {} (.fvar fv) #[.fvar fv], hs := hs.push (.fvar fv), mv }
+
+end Smt.Preprocess

Smt/Preprocess/Normalize.lean

@@ -34,7 +34,7 @@ def normalize (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.withContext d
   let (fvs', mv) ← mv.revert fvs true
   -- Simplify the goal using the smt_normalize theorems.
   let congrTheorems ← Meta.getSimpCongrTheorems
-  let ctx ← Meta.Simp.mkContext {} simpTheorems congrTheorems
+  let ctx ← Meta.Simp.mkContext { zeta := false } simpTheorems congrTheorems
   let (some mv, _) ← Meta.simpTarget mv ctx simpProcs (mayCloseGoal := false) | throwError "[smt_normalize] simplification failed"
   -- Re-introduce all free vars.
   let (fvs'', mv) ← mv.introNP fvs'.size

Smt/Preprocess/Normalize/Int.lean

@@ -25,5 +25,7 @@ theorem Int.lt_def : Int.lt a b = (a < b) := rfl
 @[smt_normalize ↓]
 theorem Int.le_def' : Int.le a b = (a ≤ b) := rfl
 
-attribute [smt_normalize ↓] Int.add_def Int.mul_def Int.div_def
+attribute [smt_normalize ↓] Int.add_def Int.mul_def
   Int.ofNat_eq_natCast Int.negSucc_eq Int.cast_ofNat_Int
+
+attribute [smt_normalize ↓ ←] Int.div_def

Smt/Reconstruct/Prop/Lemmas.lean

@@ -705,6 +705,9 @@ theorem implies_of_not_and : ¬(andN (ps ++ [¬q])) → impliesN ps q := by
         | .inl hnp => contradiction
         | .inr hnps => exact ih hnps
 
+theorem implies_false_of_not_and : ¬(andN ps) → impliesN ps False := by
+  simp_all [implies_of_not_and]
+
 syntax "flipCongrArg " term ("[" term "]")? : term
 macro_rules
 | `(flipCongrArg $premiss:term [$arg:term]) => `(congrArg $arg $premiss)

Smt/Reconstruct/UF.lean

@@ -42,9 +42,9 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
     let some n := (← read).sortCard[t.getSort]? | throwError "unknown sort {t.getSort}"
     let s := t.toString
     let endPos := (s.rawEndPos - t.getSort.toString).decreaseBy 2
-    let endPos := if endPos.dec.get? s == some '|' then endPos.dec else endPos
-    let startPos := (s.revFindAux (· != '_') endPos).get!
-    let i : Nat := (String.Pos.Raw.extract s startPos endPos).toNat!
+    let endPos := s.pos! (if endPos.dec.get? s == some '|' then endPos.dec else endPos)
+    let startPos := (endPos.revFind? (· != '_')).get!
+    let i : Nat := (s.extract startPos endPos).toNat!
     if h : i < n then
       let i : Fin n := ⟨i, h⟩
       return toExpr i

Smt/Reconstruct/Util.lean

@@ -173,8 +173,8 @@ partial def expandLet : Expr → MetaM Expr
     | some (.ldecl _ _ userName _ value _ _) =>
       match userName with
       | .str _ userNameStr =>
-        let userNamePref: String := userNameStr.take 3
-        if userNamePref = "let" then expandLet value else pure (fvar fid)
+        let userNamePref := userNameStr.take 3
+        if userNamePref == "let" then expandLet value else pure (fvar fid)
       | _ => pure (fvar fid)
     | _ => pure (fvar fid)
 | app f x => do pure (app (← expandLet f) (← expandLet x))