feat: partially applied user congruence lemmas

see #988

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -225,10 +225,12 @@ where
       else
         return { expr := (← dsimp e) }
 
-  congrDefault (e : Expr) : M Result :=
-    withParent e <| e.withApp fun f args => do
-      let infos := (← getFunInfoNArgs f args.size).paramInfo
-      let mut r ← simp f
+  congrArgs (r : Result) (args : Array Expr) : M Result := do
+    if args.isEmpty then
+      return r
+    else
+      let infos := (← getFunInfoNArgs r.expr args.size).paramInfo
+      let mut r := r
       let mut i := 0
       for arg in args do
         trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
@@ -241,6 +243,10 @@ where
         i := i + 1
       return r
 
+  congrDefault (e : Expr) : M Result :=
+    withParent e <| e.withApp fun f args => do
+      congrArgs (← simp f) args
+
   /- Return true iff processing the given congruence lemma hypothesis produced a non-refl proof. -/
   processCongrHypothesis (h : Expr) : M Bool := do
     forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do
@@ -264,6 +270,13 @@ where
       return none
     let lhs := type.appFn!.appArg!
     let rhs := type.appArg!
+    let numArgs := lhs.getAppNumArgs
+    let mut e := e
+    let mut extraArgs := #[]
+    if e.getAppNumArgs > numArgs then
+      let args := e.getAppArgs
+      e := mkAppN e.getAppFn args[:numArgs]
+      extraArgs := args[numArgs:].toArray
     if (← isDefEq lhs e) then
       let mut modified := false
       for i in c.hypothesesPos do
@@ -286,7 +299,7 @@ where
         return none
       let eNew ← instantiateMVars rhs
       let proof ← instantiateMVars (mkAppN lemma xs)
-      return some { expr := eNew, proof? := proof }
+      congrArgs { expr := eNew, proof? := proof } extraArgs
     else
       return none
 

tests/lean/run/988.lean

@@ -0,0 +1,26 @@
+instance {α : Type u} : HAppend (Fin m → α) (Fin n → α) (Fin (m + n) → α) where
+  hAppend a b i := if h : i < m then a ⟨i, h⟩ else b ⟨i - m, sorry⟩
+
+def empty : Fin 0 → Nat := (nomatch ·)
+
+theorem append_empty (x : Fin i → Nat) : x ++ empty = x :=
+  funext fun i => dif_pos _
+
+constant f : (Fin 0 → Nat) → Prop
+example : f (empty ++ empty) = f empty := by simp only [append_empty] -- should work
+
+@[congr] theorem Array.get_congr (as bs : Array α) (h : as = bs) (i : Fin as.size) (j : Nat) (hi : i = j) :
+    as.get i = bs.get ⟨j, h ▸ hi ▸ i.2⟩ := by
+  subst bs; subst j; rfl
+
+example (as : Array Nat) (h : 0 + x < as.size) :
+    as.get ⟨0 + x, h⟩ = as.get ⟨x, Nat.zero_add x ▸ h⟩ := by
+  simp -- should work
+
+example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
+    as.get ⟨0 + x, h⟩ i = as.get ⟨x, Nat.zero_add x ▸ h⟩ i := by
+  simp -- should also work
+
+example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
+    as.get ⟨0 + x, h⟩ i = as.get ⟨x, Nat.zero_add x ▸ h⟩ (0+i) := by
+  simp -- should also work