Merge pull request #199 from opencompl/fix-generalize

fix: replace generalize! by vanilla generalize by unfolding `Var.toSnoc` and `Var.last` first

SSA/Core/Tactic.lean

@@ -34,44 +34,6 @@ elab "change_mlir_context " V:ident : tactic => do
 
 end
 
-section
-open Lean Elab Tactic Meta
-syntax (name := generalize!) "generalize! " Parser.Tactic.generalizeArg,+ (Parser.Tactic.location)? : tactic
-
-/--
-`generalize!` uses a more aggressive unfolding strategy than `generalize` to
-that models the historic behavior of `generalize` dropped in
-https://github.com/leanprover/lean4/pull/3575. We should investigate if we
-can perform unfolding independently of generalize and then just use lean's
-default tactic.
--/
-@[tactic generalize!] def evalGeneralize! : Tactic := fun stx =>
-  let transparency := TransparencyMode.default
-  withMainContext do
-    let mut xIdents := #[]
-    let mut hIdents := #[]
-    let mut args := #[]
-    for arg in stx[1].getSepArgs do
-      let hName? ← if arg[0].isNone then
-        pure none
-      else
-        hIdents := hIdents.push arg[0][0]
-        pure (some arg[0][0].getId)
-      let expr ← elabTerm arg[1] none
-      xIdents := xIdents.push arg[3]
-      args := args.push { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
-    let hyps ← match expandOptLocation stx[2] with
-    | .targets hyps _ => getFVarIds hyps
-    | .wildcard => pure (← getLCtx).getFVarIds
-    let mvarId ← getMainGoal
-    mvarId.withContext do
-      let (_, newVars, mvarId) ← mvarId.generalizeHyp args hyps (transparency := transparency)
-      mvarId.withContext do
-        for v in newVars, id in xIdents ++ hIdents do
-          Term.addLocalVarInfo id (.fvar v)
-        replaceMainGoal [mvarId]
-end
-
 /--
 `simp_peephole [t1, t2, ... tn]` at Γ simplifies the evaluation of the context Γ,
 leaving behind a bare Lean level proposition to be proven.
@@ -90,12 +52,14 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident :
         DialectMorphism.mapOp, DialectMorphism.mapTy, List.map, Ctxt.snoc, List.map,
         Function.comp, Valuation.ofPair, Valuation.ofHVector, Function.uncurry,
         $ts,*]
-      try generalize! $ll { val := 0, property := _ } = a;
-      try generalize! $ll { val := 1, property := _ } = b;
-      try generalize! $ll { val := 2, property := _ } = c;
-      try generalize! $ll { val := 3, property := _ } = d;
-      try generalize! $ll { val := 4, property := _ } = e;
-      try generalize! $ll { val := 5, property := _ } = f;
+
+      try simp (config := {failIfUnchanged := false}) only [Ctxt.Var.toSnoc, Ctxt.Var.last]
+      try generalize $ll { val := 0, property := _ } = a;
+      try generalize $ll { val := 1, property := _ } = b;
+      try generalize $ll { val := 2, property := _ } = c;
+      try generalize $ll { val := 3, property := _ } = d;
+      try generalize $ll { val := 4, property := _ } = e;
+      try generalize $ll { val := 5, property := _ } = f;
       try simp (config := {decide := false, zetaDelta := true}) [TyDenote.toType] at a b c d e f;
       try clear f;
       try clear e;

SSA/Projects/InstCombine/AliveHandwrittenExamples.lean

@@ -60,7 +60,9 @@ theorem alive_DivRemOfSelect (w : Nat) :
     LLVM.mul?, LLVM.udiv?, LLVM.sdiv?, LLVM.urem?, LLVM.srem?,
     LLVM.sshr, LLVM.lshr?, LLVM.ashr?, LLVM.shl?, LLVM.select?,
     LLVM.const?, LLVM.icmp?, LLVM.udiv?,
-    HVector.toTuple, List.nthLe, BitVec.bitvec_minus_one]
+    HVector.toTuple, List.nthLe, BitVec.bitvec_minus_one,
+    Ctxt.Var.zero_eq_last, Ctxt.Var.succ_eq_toSnoc
+    ]
   intro y x c
   simp only [List.length_singleton, Fin.zero_eta, List.get_cons_zero, List.map_eq_map, List.map_cons,
     List.map_nil, CharP.cast_eq_zero, Ctxt.Valuation.snoc_last, pairBind, bind, Option.bind, Int.ofNat_eq_coe]