transparency escalation

src/Lean/Meta/ExprDefEq.lean

@@ -26,6 +26,12 @@ register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
   descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
 }
 
+register_builtin_option backward.isDefEq.transparencyEscalation : Bool := {
+  defValue := false
+  group    := "backward compatibility"
+  descr    := "increases transparency level when processing implicit arguments."
+}
+
 /--
   Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
   Remark: `n`, `k` may be 0.
@@ -186,6 +192,12 @@ private def trySynthPending (e : Expr) : MetaM Bool := do
   | some mvarId => Meta.synthPending mvarId
   | none        => pure false
 
+abbrev withEscalatedTransparency {α : Type} (x : MetaM α) : MetaM α := do
+  if backward.isDefEq.transparencyEscalation.get (← getOptions) then
+    withInferTypeConfig x
+  else
+    withAtLeastTransparency .instances x
+
 /--
   Result type for `isDefEqArgsFirstPass`.
 -/
@@ -308,14 +320,14 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     if info.isInstImplicit then
       discard <| trySynthPending a₁
       discard <| trySynthPending a₂
-    unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
+    unless (← withEscalatedTransparency <| Meta.isExprDefEqAux a₁ a₂) do
       return false
   for i in postponedHO do
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     let info := finfo.paramInfo[i]!
     if info.isInstImplicit then
-      unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
+      unless (← withEscalatedTransparency <| Meta.isExprDefEqAux a₁ a₂) do
        return false
     else
       unless (← Meta.isExprDefEqAux a₁ a₂) do
@@ -1601,7 +1613,7 @@ private def etaEq (t s : Expr) : Bool :=
   Then, we can enable the flag only when applying `simp` and `rw` theorems.
 -/
 private def withProofIrrelTransparency (k : MetaM α) : MetaM α :=
-  withInferTypeConfig k
+  withEscalatedTransparency k
 
 private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do
   if (← getConfig).proofIrrelevance then

tests/lean/951.lean

@@ -8,6 +8,7 @@ deriving Ord
 instance : LE ThingA where
   le a b := (compare a b).isLE
 
+set_option backward.isDefEq.transparencyEscalation true in
 instance (t₁ t₂ : ThingA) : Decidable (t₁ <= t₂) := inferInstance
 #check instDecidableLeThingA
 
@@ -16,5 +17,6 @@ inductive ThingB where
 deriving Ord
 instance : LE ThingB where
   le a b := (compare a b).isLE
+set_option backward.isDefEq.transparencyEscalation true in
 instance (t₁ t₂ : ThingB) : Decidable (t₁ <= t₂) := inferInstance
 #check instDecidableLeThingB

tests/lean/run/1302.lean

@@ -1,4 +1,8 @@
-@[simp] theorem get_cons_zero {as : List α} : (a :: as).get (0 : Fin (as.length + 1)) = a := rfl
+-- Extra boiler plate
+instance : NeZero (a :: as).length where
+  out := by simp
+
+@[simp] theorem get_cons_zero {as : List α} : (a :: as).get (0 : Fin ((a :: as).length)) = a := rfl
 
 example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
   simp
@@ -9,5 +13,8 @@ example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by
 example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by
   simp
 
-example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
-  rw [Fin.zero_eta, get_cons_zero]
+-- Need to change Fin.zero_eta.
+theorem zero_eta [NeZero n] : (⟨0, h⟩ : Fin n) = 0 := rfl
+
+example (a b c : α) : [a, b, c].get ⟨0, id <| by simp (config := { decide := true })⟩ = a := by
+  rw [zero_eta, get_cons_zero]

tests/lean/run/3807.lean

@@ -2439,6 +2439,7 @@ theorem subset_adjoin : S ⊆ adjoin F S := sorry
 
 instance (F : Subfield E) : Algebra F E := inferInstanceAs (Algebra F.toSubsemiring E)
 
+set_option backward.isDefEq.transparencyEscalation true in
 theorem subset_adjoin_of_subset_left {F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S :=
   sorry
 
@@ -2461,9 +2462,11 @@ variable {F E K : Type _} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F
 
 instance (L : IntermediateField F E) : IsScalarTower F L E := sorry
 
+set_option backward.isDefEq.transparencyEscalation true in
 instance (L : IntermediateField F E) : Algebra F (adjoin L S) :=
   (IntermediateField.adjoin { x // x ∈ L } S).algebra'
 
+set_option backward.isDefEq.transparencyEscalation true in
 private theorem exists_algHom_adjoin_of_splits'' {L : IntermediateField F E}
     (f : L →ₐ[F] K) :
     ∃ φ : adjoin L S →ₐ[F] K, φ.comp (IsScalarTower.toAlgHom F L _) = f := by
@@ -2473,7 +2476,8 @@ variable {L : Type _} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E
   (f : L →ₐ[F] K)
 
 -- This only required 16,000 heartbeats prior to #3807, and now takes ~210,000.
-set_option maxHeartbeats 16000
+set_option backward.isDefEq.transparencyEscalation true in
+set_option maxHeartbeats 16000 in
 theorem exists_algHom_adjoin_of_splits''' :
     ∃ φ : adjoin L S →ₐ[F] K, φ.comp (IsScalarTower.toAlgHom F L _) = f := by
   let L' := (IsScalarTower.toAlgHom F L E).fieldRange

tests/lean/run/4171.lean

@@ -685,6 +685,7 @@ def toComon_ : Comon_ (Mon_ C) ⥤ Comon_ C := (Mon_.forget C).mapComon
 theorem foo {V} [Quiver V] {X Y x} :
     @Quiver.Hom.unop V _ X Y (Opposite.op (unop := x)) = x := rfl
 
+set_option backward.isDefEq.transparencyEscalation true in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }
@@ -693,6 +694,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
     ext
     simp [(foo)] -- parentheses around `foo` works
 
+set_option backward.isDefEq.transparencyEscalation true in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }
@@ -704,6 +706,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 theorem foo' {V} [Quiver V] {X Y x} :
     @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl
 
+set_option backward.isDefEq.transparencyEscalation true in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }
@@ -720,6 +723,7 @@ trace: [simp] Diagnostics
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
+set_option backward.isDefEq.transparencyEscalation true in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }
@@ -741,6 +745,7 @@ trace: [simp] Diagnostics
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
+set_option backward.isDefEq.transparencyEscalation true in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }

tests/lean/run/grind_bitvec2.lean

@@ -963,6 +963,7 @@ theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
       x.getMsbD (w - (start + len - i)))) := by
   grind (splits := 13)
 
+set_option backward.isDefEq.transparencyEscalation true in
 theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
     (extractLsb' start len x).msb =
       (decide (0 < len) &&
@@ -987,6 +988,7 @@ theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
       x.getMsbD (w - 1 - (max hi lo - i)))) := by
   grind (splits := 14)
 
+set_option backward.isDefEq.transparencyEscalation true in
 theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo)) := by
   simp [BitVec.msb]
@@ -2041,6 +2043,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by grind
 
+set_option backward.isDefEq.transparencyEscalation true in
 theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n = 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by
   by_cases n0 : n = 0
@@ -4031,6 +4034,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
 
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by grind
 
+set_option backward.isDefEq.transparencyEscalation true in
 theorem replicate_one {w : Nat} {x : BitVec w} :
     (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by
   simp [replicate]
@@ -4432,6 +4436,9 @@ theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat els
     rw [Nat.mod_eq_of_lt (by omega)]
   · simp [h]
 
+-- set_option pp.raw true in
+set_option pp.oneline true in
+set_option trace.Meta.debug true in
 theorem getLsbD_abs {i : Nat} {x : BitVec w} :
     getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by
   grind [BitVec.abs]

tests/lean/run/ofNatNormNum.lean

@@ -31,7 +31,8 @@ instance [S α] : OfNatSound α where
 
 theorem S.ofNat_mul [S α] (n m : Nat) : (OfNat.ofNat n : α) * OfNat.ofNat m = OfNat.ofNat (n * m) := by
   induction m with
-  | zero => rw [S.mul_zero, Nat.mul_zero]
+  | zero => set_option backward.isDefEq.transparencyEscalation true in
+            rw [S.mul_zero, Nat.mul_zero]
   | succ m ih =>
     show OfNat.ofNat (α := α) n * OfNat.ofNat (m + 1) = OfNat.ofNat (n * m.succ)
     rw [Nat.mul_succ, ← ofNat_add, ← ofNat_add, ← ih, left_distrib]

tests/lean/run/structWithAlgTCSynth.lean

@@ -1285,6 +1285,7 @@ Typeclass synthesis should remain fast when multiple `with` patterns are nested
 
 Prior to #2478, this requires over 30000 heartbeats.
 -/
+set_option backward.isDefEq.transparencyEscalation true in
 set_option synthInstance.maxHeartbeats 400 in
 instance instAlgebra' (R M : Type _) [CommRing R] (I : Ideal (Quot_r R M)) :
     Algebra R ((Quot_r R M) ⧸ I) := inferInstance