Update src/Lean/Meta/SynthInstance.lean

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Lean/Meta/SynthInstance.lean

@@ -321,6 +321,26 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
     subgoals := inst.synthOrder.map (mvars[·]!) |>.toList
   }
 
+/--
+Similar to `mkLambdaFVars`, but ensures result is eta-reduced.
+For example, suppose `e` is the local variable `inst x y`, and `xs` is `#[x, y]`, then
+the result is `inst` instead of `fun x y => inst x y`.
+
+We added this auxiliary function because of aliases such as `DecidablePred`. For example,
+consider the following definition.
+```
+def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :=
+  match xs with
+  | [] => []
+  | x :: xs' => if p x then x :: filter p xs' else filter p xs'
+```
+Without `mkLambdaFVars'`, the implicit instance at the `filter` applications would be `fun x => inst x` instead of `inst`.
+Moreover, the equation lemmas associated with `filter` would have `fun x => inst x` on their right-hand-side. Then,
+we would start getting terms such as `fun x => (fun x => inst x) x` when using the equational theorem.
+-/
+private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
+  return (← mkLambdaFVars xs e).eta
+
 /--
   Try to synthesize metavariable `mvar` using the instance `inst`.
   Remark: `mctx` is set using `withMCtx`.
@@ -335,7 +355,7 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
     withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
         return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
-      let instVal ← mkLambdaFVars xs instVal
+      let instVal ← mkLambdaFVars' xs instVal
       if (← isDefEq mvar instVal) then
         return some ((← getMCtx), subgoals)
     return none
@@ -448,7 +468,7 @@ private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM
         let ys := ys.toArray
         let mvarType' ← mkForallFVars ys body
         withLocalDeclD `redf mvarType' fun f => do
-          let transformer ← mkLambdaFVars #[f] (← mkLambdaFVars xs (mkAppN f ys))
+          let transformer ← mkLambdaFVars' #[f] (← mkLambdaFVars' xs (mkAppN f ys))
           trace[Meta.synthInstance.unusedArgs] "{mvarType}\nhas unused arguments, reduced type{indentExpr mvarType'}\nTransformer{indentExpr transformer}"
           return some (mvarType', transformer)
 

tests/lean/3057.lean.expected.out

@@ -1,7 +1,7 @@
 instReprTree
 instReprListTree
-fun a b => instDecidableEqTree a b
-fun a b => instDecidableEqListTree a b
+instDecidableEqTree
+instDecidableEqListTree
 instBEqTree
 instBEqListTree
 instHashableTree

tests/lean/815b.lean.expected.out

@@ -41,7 +41,7 @@
         has unused arguments, reduced type
           ∀ (b : β), IsSmooth (f b)
         Transformer
-          fun redf a b => redf b
+          fun redf a => redf
     [Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
       [Meta.synthInstance.instances] #[inst✝]
   [Meta.synthInstance] ❌ apply inst✝ to ∀ (b : β), IsSmooth (f b)
@@ -74,7 +74,7 @@
         has unused arguments, reduced type
           ∀ (b : β), IsSmooth (f b)
         Transformer
-          fun redf a a b => redf b
+          fun redf a a => redf
   [Meta.synthInstance] ❌ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
   [Meta.synthInstance] ✅ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1

tests/lean/jason1.lean

@@ -1,50 +0,0 @@
-section
-  variable (G : Type) (T : Type) (Tm : Type)
-           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
-           (getCtx : T → G) (getTy : Tm → T)
-  inductive CtxSyntaxLayer where
-    | emp : CtxSyntaxLayer
-    | snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer
-end
-section
-  variable (G : Type) (T : Type) (Tm : Type)
-           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
-           (getCtx : T → G) (getTy : Tm → T)
--- : CtxSyntaxLayer G T EG getCtx → G)
-
-  inductive TySyntaxLayer where
-  | top : {Γ : G} → TySyntaxLayer
-  | bot : {Γ : G} → TySyntaxLayer
-  | nat : {Γ : G} → TySyntaxLayer
-  | arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer
-
-  def getCtxStep : TySyntaxLayer G T EG getCtx → G
-    | TySyntaxLayer.top (Γ := Γ) .. => Γ
-    | TySyntaxLayer.bot (Γ := Γ) .. => Γ
-    | TySyntaxLayer.nat (Γ := Γ) .. => Γ
-    | TySyntaxLayer.arrow (Γ := Γ) .. => Γ
-end
-section
-  variable (G : Type) (T : Type) (Tm : Type)
-           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
-           (EGrfl : ∀ {Γ}, EG Γ Γ)
-           (getCtx : T → G) (getTy : Tm → T)
-           (GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T)
-
-  inductive TmSyntaxLayer where
-    | tt : {Γ : G} → TmSyntaxLayer
-    | zero : {Γ : G} → TmSyntaxLayer
-    | succ : {Γ : G} → TmSyntaxLayer
-    | app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
-        → (f x : Tm)
-        → ET (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx)) (getTy f)
-        → ET A (getTy x)
-        → TmSyntaxLayer
-
-  set_option pp.all true
-  def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T
-    | TmSyntaxLayer.tt ..   => TAlgebra TySyntaxLayer.top
-    | TmSyntaxLayer.zero .. => TAlgebra TySyntaxLayer.nat
-    | TmSyntaxLayer.succ .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra TySyntaxLayer.nat) (TAlgebra TySyntaxLayer.nat) EGrfl EGrfl)
-    | TmSyntaxLayer.app (B:=B) .. => B
-end

tests/lean/jason1.lean.expected.out

@@ -1,124 +0,0 @@
-jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.arrow G T EG getCtx
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G

tests/lean/run/instEtaIssue.lean

@@ -0,0 +1,24 @@
+def filter (p : α → Prop) [DecidablePred p] (xs : List α) : List α :=
+  match xs with
+  | [] => []
+  | x :: xs' => if p x then x :: filter p xs' else filter p xs'
+
+attribute [simp] filter
+
+set_option pp.explicit true
+
+/--
+info: filter._eq_2.{u_1} {α : Type u_1} (p : α → Prop) [@DecidablePred α p] (x : α) (xs' : List α) :
+  @Eq (List α) (@filter α p inst✝ (@List.cons α x xs'))
+    (@ite (List α) (p x) (inst✝ x) (@List.cons α x (@filter α p inst✝ xs')) (@filter α p inst✝ xs'))
+-/
+#guard_msgs in
+#check filter._eq_2 -- We should not have terms of the form `@filter α p (fun x => inst✝ x) xs'`
+
+
+def filter_length (p : α → Prop) [DecidablePred p] : (filter p xs).length ≤ xs.length := by
+  induction xs with
+  | nil => simp [filter]
+  | cons x xs ih =>
+    simp only [filter]
+    split <;> simp only [List.length] <;> omega