Merge pull request #193 from opencompl/bump_std

Bump std

SSA/Core/ErasedContext.lean

@@ -170,7 +170,7 @@ theorem toSnoc_injective {Γ : Ctxt Ty} {t t' : Ty} :
   let ofSnoc : (Γ.snoc t').Var t → Option (Γ.Var t) :=
     fun v => Ctxt.Var.casesOn v some none
   intro x y h
-  simpa using congr_arg ofSnoc h
+  simpa (config := {zetaDelta := true}) using congr_arg ofSnoc h
 
 abbrev Hom (Γ Γ' : Ctxt Ty) := ⦃t : Ty⦄ → Γ.Var t → Γ'.Var t
 

SSA/Core/HVector.lean

@@ -1,5 +1,4 @@
 import Mathlib.Tactic.Basic
-import Mathlib.Tactic.LibrarySearch
 
 
 /-- An heterogeneous vector -/

SSA/Core/Tactic.lean

@@ -34,6 +34,44 @@ 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.
@@ -42,7 +80,7 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident :
   `(tactic|
       (
       change_mlir_context $ll
-      try simp (config := {unfoldPartialApp := true}) only [
+      try simp (config := {unfoldPartialApp := true, zetaDelta := true}) only [
         Int.ofNat_eq_coe, Nat.cast_zero, DerivedCtxt.snoc, DerivedCtxt.ofCtxt,
         DerivedCtxt.ofCtxt_empty, Valuation.snoc_last,
         Com.denote, Expr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc,
@@ -52,13 +90,13 @@ 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 := {decide := false}) [TyDenote.toType] at a b c d e f;
+      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;
       try clear d;

SSA/Projects/CSE/CSE.lean

@@ -258,7 +258,7 @@ def State.snocOldExpr2Cache
       let lastVar := (Ctxt.Var.last Γ α)
       let ⟨eneedle', heneedle'⟩ := ExprRemapVar lets homRemap vold lastVar (by {
         intros Vstart
-        simp [Ctxt.Hom.remapLast, Ctxt.Valuation.comap]
+        simp (config := {zetaDelta := true}) [Ctxt.Hom.remapLast, Ctxt.Valuation.comap]
         done
       })  eneedle
       match s.expr2cache β eneedle' with
@@ -273,10 +273,10 @@ def State.snocOldExpr2Cache
           funext ty var
           cases var using Ctxt.Var.casesOn
           case e_Γv.h.h.toSnoc v =>
-            simp [Ctxt.Valuation.comap, Ctxt.Hom.remapLast]
+            simp (config := {zetaDelta := true}) [Ctxt.Valuation.comap, Ctxt.Hom.remapLast]
             done
           case e_Γv.h.h.last =>
-            simp [Ctxt.Valuation.comap, Ctxt.Hom.remapLast]
+            simp (config := {zetaDelta := true}) [Ctxt.Valuation.comap, Ctxt.Hom.remapLast]
             rw [henew]
             rw [hv]
             done
@@ -371,7 +371,7 @@ unsafe def State.cseExpr
       let e' : Expr Op Γ α  := .mk op ty_eq args' regArgs'
       ⟨⟨e', by {
         intros V
-        simp [E, hargs', Expr.denote_unfold]
+        simp (config := { zetaDelta := true}) [E, hargs', Expr.denote_unfold]
         congr 1
         unfold Ctxt.Valuation.eval at hargs'
         rw [hargs']

SSA/Projects/DCE/DCE.lean

@@ -337,37 +337,37 @@ partial def dce_ [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (
         ⟩⟩
     | .lete (α := α) e body =>
       let DEL := Deleted.deleteSnoc Γ α
-        -- Try to delete the variable α in the body.
-        match Com.deleteVar? DEL body with
-        | .none => -- we don't succeed, so DCE the child, and rebuild the same `let` binding.
-          let ⟨Γ', hom', ⟨body', hbody'⟩⟩
-            :   Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' (Ctxt.snoc Γ α)), { body' : Com Op Γ' t //  ∀ (V : (Γ.snoc α).Valuation), body.denote V = body'.denote (V.comap hom)} :=
-            (dce_ body)
-          let com' := Com.lete (α := α) e (body'.changeVars hom')
-          ⟨Γ, Ctxt.Hom.id, com', by
+      -- Try to delete the variable α in the body.
+      match Com.deleteVar? DEL body with
+      | .none => -- we don't succeed, so DCE the child, and rebuild the same `let` binding.
+        let ⟨Γ', hom', ⟨body', hbody'⟩⟩
+          :   Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' (Ctxt.snoc Γ α)), { body' : Com Op Γ' t //  ∀ (V : (Γ.snoc α).Valuation), body.denote V = body'.denote (V.comap hom)} :=
+          (dce_ body)
+        let com' := Com.lete (α := α) e (body'.changeVars hom')
+        ⟨Γ, Ctxt.Hom.id, com', by
+          intros V
+          simp (config := {zetaDelta := true}) [Com.denote]
+          rw[hbody']
+          rfl
+        ⟩
+      | .some ⟨body', hbody⟩ =>
+        let ⟨Γ', hom', ⟨com', hcom'⟩⟩
+        : Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' Γ), { com' : Com Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)} :=
+          ⟨Γ, Ctxt.Hom.id, ⟨body', by -- NOTE: we deleted the `let` binding.
+            simp[HCOM]
             intros V
             simp[Com.denote]
-            rw[hbody']
-            rfl
-          ⟩
-        | .some ⟨body', hbody⟩ =>
-          let ⟨Γ', hom', ⟨com', hcom'⟩⟩
-          : Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' Γ), { com' : Com Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)} :=
-            ⟨Γ, Ctxt.Hom.id, ⟨body', by -- NOTE: we deleted the `let` binding.
-              simp[HCOM]
-              intros V
-              simp[Com.denote]
-              apply hbody
-            ⟩⟩
-          let ⟨Γ'', hom'', ⟨com'', hcom''⟩⟩
-            :   Σ (Γ'' : Ctxt Ty) (hom: Ctxt.Hom Γ'' Γ'), { com'' : Com Op Γ'' t //  ∀ (V' : Γ'.Valuation), com'.denote V' = com''.denote (V'.comap hom)} :=
-            dce_ com' -- recurse into `com'`, which contains *just* the `body`, not the `let`, and return this.
-          ⟨Γ'', hom''.comp hom', com'', by
-            intros V
-            rw[← HCOM]
-            rw[hcom']
-            rw[hcom'']
-            rfl⟩
+            apply hbody
+          ⟩⟩
+        let ⟨Γ'', hom'', ⟨com'', hcom''⟩⟩
+          :   Σ (Γ'' : Ctxt Ty) (hom: Ctxt.Hom Γ'' Γ'), { com'' : Com Op Γ'' t //  ∀ (V' : Γ'.Valuation), com'.denote V' = com''.denote (V'.comap hom)} :=
+          dce_ com' -- recurse into `com'`, which contains *just* the `body`, not the `let`, and return this.
+        ⟨Γ'', hom''.comp hom', com'', by
+          intros V
+          rw[← HCOM]
+          rw[hcom']
+          rw[hcom'']
+          rfl⟩
 /-
 decreasing_by {
   simp[invImage, InvImage, WellFoundedRelation.rel, Nat.lt_wfRel]

SSA/Projects/FullyHomomorphicEncryption/Basic.lean

@@ -238,7 +238,6 @@ theorem R.representative_fromPoly_toFun : forall a : (ZMod q)[X], ((R.fromPoly (
   intro a
   simp [R.representative]
   have ⟨i,⟨hiI,hi_eq⟩⟩ := R.fromPoly_rep'_eq_ideal q n a
-  simp [MonoidHomClass.toMonoidHom]
   apply Polynomial.modByMonic_eq_of_dvd_sub (f_monic q n)
   ring_nf
   apply Ideal.mem_span_singleton.1

SSA/Projects/InstCombine/AliveHandwrittenExamples.lean

@@ -52,7 +52,7 @@ theorem alive_DivRemOfSelect (w : Nat) :
   unfold alive_DivRemOfSelect_src alive_DivRemOfSelect_tgt
   intros Γv
   simp_peephole at Γv
-  simp (config := {decide := false}) only [OpDenote.denote,
+  simp (config := {decide := false, zetaDelta := true}) only [OpDenote.denote,
     InstCombine.Op.denote, HVector.toPair, HVector.toTriple, pairMapM, BitVec.Refinement,
     bind, Option.bind, pure, DerivedCtxt.ofCtxt, DerivedCtxt.snoc,
     Ctxt.snoc, ConcreteOrMVar.instantiate, Vector.get, HVector.toSingle,

SSA/Projects/InstCombine/AliveStatements.lean

@@ -5,9 +5,8 @@ import SSA.Projects.InstCombine.LLVM.Semantics
 import Std.Data.BitVec
 import Mathlib.Data.BitVec.Lemmas
 
-open Std
-open Std.BitVec
 open LLVM
+open BitVec
 
 @[simp] lemma getLsb_negOne' (w : ℕ) (i : Fin w) :
     getLsb (-1#w) i := by

SSA/Projects/InstCombine/Base.lean

@@ -23,7 +23,7 @@ import SSA.Projects.InstCombine.LLVM.Semantics
 
 namespace InstCombine
 
-open Std (BitVec)
+open BitVec
 
 open LLVM
 

SSA/Projects/InstCombine/ForMathlib.lean

@@ -1,21 +1,44 @@
 import Mathlib.Tactic.Ring
-import Std.Data.BitVec
 import Mathlib.Data.BitVec.Lemmas
-import Mathlib.Data.BitVec.Defs
 
-namespace Std.BitVec
+namespace BitVec
 open Nat
 
+theorem ofInt_negSucc (w n : Nat ) :
+    BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
+  simp [BitVec.ofInt]
+  apply BitVec.toNat_injective
+  simp only [Int.toNat, toNat_ofNatLt, toNat_not, toNat_ofNat]
+  split
+  · simp_all [Int.negSucc_emod]
+    symm
+    rw [← Int.cast_eq_cast_iff_Nat]
+    rw [Nat.cast_sub]
+    rw [Nat.cast_sub]
+    have h : 0 < 2 ^ w := by simp
+    simp_all only [gt_iff_lt, ofNat_pos, pow_pos, cast_pow, Nat.cast_ofNat, cast_one,
+      Int.ofNat_emod]
+    have h : 0 < 2 ^ w := by simp
+    omega
+    omega
+
+  · have nonneg : Int.negSucc n % 2 ^ w ≥ 0 := by
+      simp only [ge_iff_le, ne_eq, pow_eq_zero_iff', OfNat.ofNat_ne_zero, false_and,
+        not_false_eq_true, Int.emod_nonneg (Int.negSucc n) _]
+    simp_all only [ofNat_pos, gt_iff_lt, pow_pos, ne_eq, pow_eq_zero_iff', OfNat.ofNat_ne_zero,
+      false_and, not_false_eq_true, ge_iff_le, Int.negSucc_not_nonneg]
+
 theorem ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = Int.cast z := by
   cases w
   case zero =>
     simp only [eq_nil]
   case succ w =>
-    simp only [Int.cast, IntCast.intCast, BitVec.ofInt]
+    simp only [Int.cast, IntCast.intCast]
     unfold Int.castDef
     cases' z with z z
     · rfl
-    · simp only [cast_add, cast_one, neg_add_rev]
+    · rw [ofInt_negSucc]
+      simp only [cast_add, cast_one, neg_add_rev]
       rw [← add_ofFin, ofFin_neg, ofFin_ofNat, ofNat_eq_ofNat, ofFin_neg, ofFin_natCast,
         natCast_eq_ofNat, negOne_eq_allOnes, ← sub_toAdd, allOnes_sub_eq_not]
 

SSA/Projects/InstCombine/ForStd.lean

@@ -1,8 +1,6 @@
-import Std.Data.BitVec
 
-open Std
+namespace BitVec
 
-namespace Std.BitVec
 
 notation:50 x " ≤ᵤ " y => BitVec.ule x y
 notation:50 x " <ᵤ " y => BitVec.ult x y
@@ -48,22 +46,22 @@ theorem trans {α : Type u} : ∀ x y z : Option α, Refinement x y → Refineme
   rename_i x y hxy y h
   rw [hxy, h]; apply refl
 
-instance {α : Type u} [DecidableEq α] : DecidableRel (@Refinement α) := by
+instance {α : Type u} [DEQ : DecidableEq α] : DecidableRel (@Refinement α) := by
   intro x y
   cases x <;> cases y
   { apply isTrue; exact Refinement.noneAny}
   { apply isTrue; exact Refinement.noneAny }
   { apply isFalse; intro h; cases h }
   { rename_i val val'
-    cases (decEq val val')
+    cases (DEQ val val')
     { apply isFalse; intro h; cases h; contradiction }
     { apply isTrue; apply Refinement.bothSome; assumption }
   }
 
 end Refinement
 
 infix:50 (priority:=low) " ⊑ " => Refinement
-instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
+instance : Coe Bool (BitVec 1) := ⟨BitVec.ofBool⟩
 
 def coeWidth {m n : Nat} : BitVec m → BitVec n
   | x => BitVec.ofNat n x.toNat
@@ -73,17 +71,49 @@ def coeWidth {m n : Nat} : BitVec m → BitVec n
 --instance {m n: Nat} : CoeTail (BitVec m) (BitVec n) := ⟨BitVec.coeWidth⟩
 
 instance decPropToBitvec1 (p : Prop) [Decidable p] : CoeDep Prop p (BitVec 1) where
-  coe := ofBool $ decide p
+  coe := BitVec.ofBool $ decide p
+
+open Std
+
+theorem Int.natCast_pred_of_pos (x : Nat) (h : 0 < x) :
+    (x : Int) - 1 = Nat.cast (x - 1) := by
+  simp only [Nat.cast, NatCast.natCast]
+  cases x
+  case zero => contradiction
+  case succ x =>
+    simp only [(· - ·), Sub.sub, Int.sub, (· + ·), Add.add, Int.add,
+      (-·), Int.neg, Int.negOfNat, Int.subNatNat]
+    simp
 
 -- This should become a lot simpler, if not obsolete after:
 -- https://github.com/leanprover/lean4/pull/3474
-theorem bitvec_minus_one : BitVec.ofInt w (Int.negSucc 0) = (-1 : BitVec w) := by
-  change (BitVec.ofInt w (-1) = (-1 : BitVec w))
-  ext i
-  simp_all only [BitVec.ofInt, Neg.neg, Int.neg, Int.negOfNat]
-  simp_all only [BitVec.getLsb_not, Bool.not_false, BitVec.ofNat_eq_ofNat,
-    BitVec.neg_eq, Fin.is_lt, getLsb_ofNat]
-  simp only [Bool.and_true, decide_True]
-  rw [negOne_eq_allOnes]
-  rw [getLsb_allOnes]
+theorem bitvec_minus_one : BitVec.ofInt w (Int.negSucc 0) = (-1 : _root_.BitVec w) := by
   simp
+  by_cases zeroBitwidth : 0 < w
+  case pos =>
+    apply BitVec.eq_of_toInt_eq
+    simp
+    unfold BitVec.toInt
+    simp
+    have xx : 1 % 2 ^ w = 1 := by
+      rw [Nat.mod_eq_of_lt]
+      simp [Nat.pow_one]
+      omega
+    simp [xx]
+    split
+    · rename_i h
+      rw [Nat.mod_eq_of_lt] at h
+      · have xxx : 2 * (2 ^ w - 1) = 2 * 2 ^ w - 2 * 1 := by omega
+        rw [xxx] at h
+        simp at h
+        omega
+      · omega
+    · simp only [Int.bmod, Int.reduceNeg, Int.natCast_pred_of_pos _ (Nat.two_pow_pos w),
+        Int.neg_emod]
+      omega
+  case neg =>
+    simp_all
+    rw [zeroBitwidth]
+    simp
+
+  end BitVec