ArgCong bug fix

Duper/Match.lean

@@ -1,7 +1,7 @@
 import Lean
+import Duper.Util.Reduction
 
-open Lean
-open Lean.Meta
+open Lean Lean.Meta Duper
 
 initialize Lean.registerTraceClass `duper.match.debug
 
@@ -15,8 +15,8 @@ partial def Lean.Meta.performMatch (l : Array (Expr × Expr)) (protected_mvars :
     trace[duper.match.debug] "About to attempt to match {l}"
 
     for (match_target, e) in l do
-      let match_target_type := (← instantiateMVars (← inferType match_target))
-      let e_type := (← instantiateMVars (← inferType e))
+      let match_target_type ← betaEtaReduceInstMVars $ ← inferType match_target
+      let e_type ← betaEtaReduceInstMVars $ ← inferType e
       if not (← match1 match_target_type e_type protected_mvars) then
         state.restore
         return false
@@ -29,14 +29,15 @@ partial def Lean.Meta.performMatch (l : Array (Expr × Expr)) (protected_mvars :
     trace[duper.match.debug] "Successfully matched {l}"
     return true
   catch ex =>
+    trace[duper.match.debug] "Encountered error {ex.toMessageData} in match procedure"
     state.restore
     throw ex
 where
   match1 (match_target e : Expr) (protected_mvars : Array MVarId) : MetaM Bool := do
     let match_target ← instantiateMVars match_target
     let e ← instantiateMVars e
     if match_target == e then return true else
-    match_target.withApp fun match_target_hd match_target_tl => e.withApp fun e_hd e_tl =>
+    match_target.withApp fun match_target_hd match_target_tl => e.withApp fun e_hd e_tl => do
       match match_target_hd, e_hd with
       | Expr.fvar fid, Expr.fvar gid => do
         if fid == gid then
@@ -50,7 +51,9 @@ where
         else
           return false
       | Expr.forallE .., Expr.forallE .. =>
-        return match_target == e
+        return match_target_hd == e_hd && (← matchArgs match_target_tl e_tl)
+      | Expr.lam .., Expr.lam .. =>
+        return match_target_hd == e_hd && (← matchArgs match_target_tl e_tl)
       | Expr.fvar .., Expr.mvar .. =>
         matchRigidFlex match_target e protected_mvars
       | Expr.const .., Expr.mvar .. =>

Duper/Rules/ArgumentCongruence.lean

@@ -9,13 +9,14 @@ open Meta
 
 initialize Lean.registerTraceClass `duper.rule.argCong
 
-def mkArgumentCongruenceProof (i : Nat) (mVarTys : Array Expr) (premises : List Expr) (parents : List ProofParent)
+def mkArgumentCongruenceProof (i : Nat) (premises : List Expr) (parents : List ProofParent)
   (transferExprs : Array Expr) (c : Clause) : MetaM Expr :=
   Meta.forallTelescope c.toForallExpr fun xs body => do
     let cLits := c.lits.map (fun l => l.map (fun e => e.instantiateRev xs))
     let (parentsLits, appliedPremises, transferExprs) ← instantiatePremises parents premises xs transferExprs
     let parentLits := parentsLits[0]!
     let appliedPremise := appliedPremises[0]!
+    let mVarTys := transferExprs
 
     let mut caseProofs := Array.mkEmpty parentLits.size
     for j in [:parentLits.size] do
@@ -64,7 +65,7 @@ def argCongAtLit (given : Clause) (c : MClause) (i : Nat) : RuleM (Array ClauseS
       let loaded ← getLoadedClauses
       for m in mVars do
         newMVars := newMVars.push m
-        mVarTys := mVarTys.push (← inferType m)
+        mVarTys := mVarTys.push (← instantiateMVars (← inferType m))
         let newlhs := mkAppN lhs newMVars
         let newrhs := mkAppN rhs newMVars
         let newty ← inferType newlhs
@@ -77,7 +78,7 @@ def argCongAtLit (given : Clause) (c : MClause) (i : Nat) : RuleM (Array ClauseS
         let ug ← unifierGenerator #[]
         let yC := do
           setLoadedClauses loaded
-          yieldClause c' "argument congruence" (mkProof := mkArgumentCongruenceProof i mVarTys)
+          yieldClause c' "argument congruence" (mkProof := mkArgumentCongruenceProof i) (transferExprs := mVarTys)
         streams := streams.push (ClauseStream.mk ug given yC "argument congruence")
     return streams
 

Duper/Tests/test_regression.lean

@@ -683,3 +683,10 @@ def sk (a b : Nat) (c : Nat × Nat) (h1 : c = (a, b)) : c.1 = a := by
   duper [h1]
 
 #print sk
+--###############################################################################################################################
+-- This test previously failed due to a bug in ArgCong
+example (a b : Nat) (matrix : Fin a → Fin b → Nat)
+  (transpose : ∀ n : Nat, ∀ m : Nat, (Fin n → Fin m → Nat) → (Fin m → Fin n → Nat))
+  (h : ∀ n : Nat, ∀ m : Nat, (fun x => transpose n m (transpose m n x)) = (fun x => x)) :
+  transpose b a (transpose a b matrix) = matrix := by
+  duper [h]