resolves #52

Author: PratherConid

Auto/Lib/MetaExtra.lean

@@ -156,4 +156,72 @@ def Meta.Context.modifyLCtx (ctx : Context) (lctx : LocalContext) : CoreM Contex
 def Meta.Context.modifyLocalInstances (ctx : Context) (localInsts : LocalInstances) : CoreM Context :=
   MetaM.run' (withLCtx ctx.lctx localInsts read) ctx
 
+/--
+Replace occurrences of `p` in non-dependent positions in `e` with `q`. The type
+of the resulting expression should be identical to the type of `e`
+· Both `e` and `q` are not supposed to contain loose bvars
+· We detect subterms equivalent to `p` using key-matching.
+  That is, only perform `isDefEq` tests when the head symbol of substerm is equivalent to head symbol of `p`.
+· We only abstract non-dependent positions
+  That is, if there is a function application `f a` and the argument of
+  `f` is dependent, then occurrences of `p` in `a` will not be abstracted
+
+By default, all occurrences are abstracted,
+but this behavior can be controlled using the `occs` parameter.
+
+All matches of `p` in `e` are considered for occurrences,
+but for each match that is included by the `occs` parameter,
+metavariables appearing in `p` (or `e`) may become instantiated,
+affecting the possibility of subsequent matches.
+For matches that are not included in the `occs` parameter, the metavariable context is rolled back
+to prevent blocking subsequent matches which require different instantiations.
+-/
+partial def Meta.replaceNonDep (e : Expr) (p : Expr) (q : Expr) (occs : Occurrences := .all) : MetaM Expr := do
+  let e ← instantiateMVars e
+  let pHeadIdx := p.toHeadIndex
+  let pNumArgs := p.headNumArgs
+  let rec visit (e : Expr) : StateRefT Nat MetaM Expr := do
+    let visitChildren : Unit → StateRefT Nat MetaM Expr := fun _ => do
+      match e with
+      | .app f a         => do
+        let type ← Meta.whnf (← Meta.inferType f)
+        let .forallE _ _ b _ := type
+          | throwError "{decl_name%} :: {type} is not a `∀`"
+        if b.hasLooseBVar 0 then
+          return e.updateApp! (← visit f) a
+        else
+          return e.updateApp! (← visit f) (← visit a)
+      | .mdata _ b       => return e.updateMData! (← visit b)
+      | .proj _ _ b      => return e.updateProj! (← visit b)
+      | .letE n t v b _ =>
+        Meta.withLetDecl n t (← visit v) fun x =>
+          return ← mkLetFVars #[x] (← visit (b.instantiate1 x))
+      | .lam ..     =>
+        Meta.lambdaTelescope e fun xs b => do
+          return ← mkLambdaFVars xs (← visit b)
+      | .forallE n d b bi => do
+        let d' ← (if b.hasLooseBVar 0 then return d else visit d)
+        Meta.withLocalDecl n bi d' fun x => do
+          return ← mkForallFVars #[x] (← visit (b.instantiate1 x))
+      | e                => return e
+    if e.toHeadIndex != pHeadIdx || e.headNumArgs != pNumArgs then
+      visitChildren ()
+    else
+      -- We save the metavariable context here,
+      -- so that it can be rolled back unless `occs.contains i`.
+      let mctx ← getMCtx
+      if (← isDefEq e p) then
+        let i ← get
+        set (i+1)
+        if occs.contains i then
+          return q
+        else
+          -- Revert the metavariable context,
+          -- so that other matches are still possible.
+          setMCtx mctx
+          visitChildren ()
+      else
+        visitChildren ()
+  visit e |>.run' 1
+
 end Auto

Auto/Tactic.lean

@@ -454,13 +454,12 @@ def queryNative
 def rewriteIteCondDecide (lemmas : Array Lemma) : MetaM (Array Lemma) := do
   -- Simplify `ite`
   let ite_simp_lem ← Lemma.ofConst ``Auto.Bool.ite_simp (.leaf "hw Auto.Bool.ite_simp")
-  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem ite_simp_lem)
   -- Simplify `cond`
   let cond_simp_lem ← Lemma.ofConst ``Auto.Bool.cond_simp (.leaf "hw Auto.Bool.cond_simp")
-  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem cond_simp_lem)
   -- Simplify `decide`
   let decide_simp_lem ← Lemma.ofConst ``Auto.Bool.decide_simp (.leaf "hw Auto.Bool.decide_simp")
-  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem decide_simp_lem)
+  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigidNonDep
+    lem #[ite_simp_lem, cond_simp_lem, decide_simp_lem])
   return lemmas
 
 /--

Auto/Translation/Assumptions.lean

@@ -3,6 +3,7 @@ import Auto.Lib.BoolExtra
 import Auto.Lib.MessageData
 import Auto.Lib.ExprExtra
 import Auto.Lib.ListExtra
+import Auto.Lib.MetaExtra
 import Auto.Lib.Containers
 import Auto.Lib.AbstractMVars
 open Lean
@@ -122,20 +123,29 @@ def Lemma.reorderForallInstDep (lem : Lemma) : MetaM Lemma := do
   · If `lhs` occurs in `lem.type`, perform rewrite and return result
   · If `lhs` does not occur in `lem.type`, return `.none`
 -/
-def Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) : MetaM (Option Lemma) := do
+def Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) (nonDep : Bool) : MetaM (Option Lemma) := do
   let ⟨rwproof, rwtype, rwDeriv⟩ := rw
   let .some (α, lhs, rhs) ← Meta.matchEq? rwtype
     | throwError "{decl_name%} :: {rwtype} is not an equality"
   let ⟨⟨proof, e, lemDeriv⟩, params⟩ := lem
-  let eAbst ← Meta.kabstract e lhs
+  let eAbst ← (do
+    if nonDep then
+      Meta.withLocalDeclD `_a α fun x => do return (← Meta.replaceNonDep e lhs x).abstract #[x]
+    else Meta.kabstract e lhs)
   unless eAbst.hasLooseBVars do
     return .none
   let eNew := eAbst.instantiate1 rhs
   let motive := mkLambda `_a BinderInfo.default α eAbst
   unless (← Meta.isTypeCorrect motive) do
     throwError "{decl_name%} :: Motive {motive} is not type correct"
   let eqPrf ← Meta.mkEqNDRec motive proof rwproof
-  return .some ⟨⟨eqPrf, eNew, .node "rw" #[lemDeriv, rwDeriv]⟩, params⟩
+  return .some ⟨⟨eqPrf, ← Core.betaReduce eNew, .node "rw" #[lemDeriv, rwDeriv]⟩, params⟩
+
+def checkNonRecEquality (e : Expr) : MetaM Unit := do
+  let .some (_, lhs, rhs) ← Meta.matchEq? e
+    | throwError "{decl_name%} :: {e} is not an equality"
+  if (← Meta.kabstract rhs lhs).hasLooseBVars then
+    throwError "{decl_name%} :: Right-hand side {rhs} of equality contains left-hand side {lhs}"
 
 /--
   Exhaustively rewrite using a universe-polymorphic rigid equality
@@ -147,19 +157,16 @@ def Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) : MetaM (Option Lemm
 def Lemma.rewriteUPolyRigid (lem : Lemma) (rw : Lemma) : MetaM Lemma := do
   let mut lem := lem
   let s ← saveState
-  -- Test whether `rhs` contains `lhs
-  let .some (_, lhs, rhs) ← Meta.matchEq? rw.type
-    | throwError "{decl_name%} :: {rw.type} is not an equality"
-  let lhs' := lhs.instantiateLevelParamsArray rw.params (← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar))
-  let rhs' := rhs.instantiateLevelParamsArray rw.params (← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar))
-  if (← Meta.kabstract rhs' lhs').hasLooseBVars then
-    throwError "{decl_name%} :: Right-hand side {rhs} of equality contains left-hand side {lhs}"
+  -- Test whether `rhs` contains `lhs`
+  let rwty' := rw.type.instantiateLevelParamsArray
+    rw.params (← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar))
+  checkNonRecEquality rwty'
   restoreState s
   while true do
     let umvars ← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar)
     let .some urw := (rw.instantiateLevelParamsArray umvars).toUMonoFact?
       | throwError "{decl_name%} :: Unexpected error"
-    let .some lem' ← Lemma.rewriteUMonoRigid? lem urw
+    let .some lem' ← Lemma.rewriteUMonoRigid? lem urw false
       | break
     let restmvars := (← umvars.mapM Level.collectLevelMVars).flatMap id
     for lmvar in restmvars do
@@ -169,6 +176,41 @@ def Lemma.rewriteUPolyRigid (lem : Lemma) (rw : Lemma) : MetaM Lemma := do
   restoreState s
   return ← lem.betaReduceType
 
+/--
+  Exhaustively rewrite using an array of universe-polymorphic rigid equalities
+  · Only `lhs`s occurring in non-dependent positions will be replaced by `rhs`
+  · If there are multiple instances of `lhs` with different universe
+    level instantiations, all of these instances will be replaced with `rhs`
+  · `rw.snd` should have the form `lhs = rhs`, where both sides are rigid
+    and `rhs` should not contain `lhs`
+-/
+def Lemma.rewriteUPolyRigidNonDep (lem : Lemma) (rws : Array Lemma) : MetaM Lemma := do
+  let mut lem := lem
+  let s ← saveState
+  -- Test whether `rhs` contains `lhs`
+  for rw in rws do
+    let rwty' := rw.type.instantiateLevelParamsArray
+      rw.params (← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar))
+    checkNonRecEquality rwty'
+  restoreState s
+  while true do
+    let lemRef := lem
+    for rw in rws do
+      let umvars ← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar)
+      let .some urw := (rw.instantiateLevelParamsArray umvars).toUMonoFact?
+        | throwError "{decl_name%} :: Unexpected error"
+      let .some lem' ← Lemma.rewriteUMonoRigid? lem urw true
+        | continue
+      let restmvars := (← umvars.mapM Level.collectLevelMVars).flatMap id
+      for lmvar in restmvars do
+        if !(← Meta.isLevelDefEq (.mvar lmvar) .zero) then
+          break
+      lem ← lem'.instantiateMVars
+    if lem == lemRef then
+      break
+  restoreState s
+  return lem
+
 /-
   An instance of a `Lemma`. If a lemma has proof `H`,
     then an instance of the lemma would be like

Test/Bugs.lean

@@ -15,21 +15,6 @@ set_option auto.smt.solver.name "z3"
 set_option trace.auto.native.printFormulas true
 attribute [rebind Auto.Native.solverFunc] Auto.Solver.Native.emulateNative
 
-set_option auto.native true
-set_option trace.auto.lamReif.printResult true
-set_option trace.auto.lamReif.printValuation true
-
-  set_option trace.auto.printLemmas true
-  set_option auto.redMode "instances"
-  example : (∀ (xs ys zs : List α), xs ++ ys ++ zs = xs ++ (ys ++ zs)) := by
-    intro xs; induction xs <;> (mono [*] d[List.append]; sorry)
-
-  example (x : α) : List.head? [x] = .some x := by
-    have list_head_unfold : @List.head? α = (fun x =>
-      @List.casesOn α (fun x => (fun x => Option α) x) x ((fun _ => @none α) Unit.unit) fun head tail =>
-        (fun a tail => @some α a) head tail) := by sorry
-    mono [list_head_unfold] d[List.rec]; sorry
-
 -- set_option auto.tptp true
 -- set_option trace.auto.tptp.premiseSelection true
 
@@ -90,3 +75,18 @@ end Set
 example (x : Nat) (primeset : Nat → Prop) (dvd : Nat → Nat → Prop) :
   ((∃ (i : _) (i_1 : primeset i), dvd i x) ↔ (∃ p, primeset p ∧ dvd p x)) := by
   auto
+
+section
+
+  variable (world : Type)
+
+  @[reducible] def F: Type := Nat → world
+
+  @[reducible] def G : Type := F world → (Nat → Prop)
+
+  set_option trace.auto.lamReif.printValuation true
+  set_option auto.mono.mode "fol"
+  example (f : Nat → world) (p : G world) : p f 0 ∨ ¬p f 0 := by
+    auto
+
+end

Test/Test_Regression.lean

@@ -599,6 +599,29 @@ section Adhoc
     (if True then x else y) = x ∧ (if False then z else t) = t := by
     auto
 
+  -- Nested `ite`
+
+  set_option auto.smt true in
+  set_option auto.tptp false in
+  example
+    (h : if (if 2 = 3 then 1 else 2) = (if 3 = 2 then 0 else 1) then True else False)
+    : False := by
+    auto
+
+  set_option trace.auto.mono.printInputLemmas true
+  open Classical
+  example
+    (node : Type) [node_dec : DecidableEq node] (ring_bottom : node)
+    (st0_x st0_up st1_x st1_up : node → Prop) (s x x_1 : node)
+    (bad_motive :
+      ¬if s = ring_bottom then True
+        else if st0_x s = st0_x x then True
+        else if ((¬st0_x s) = if x_1 = s then ¬st0_x s else st0_x x_1) ∧ ¬x_1 = s ∧ ¬st0_up x_1 then
+          (∀ (a_1 : node), (if a_1 = s then ¬st0_x s else st0_x a_1) = st1_x a_1) → ∃ x, ¬(¬x = s ∧ (¬x = s → st0_up x)) = st1_up x
+        else True) :
+    True := by
+    auto
+
   -- Boolean
   example : true ≠ false := by
     auto