Lean中斜堆fusion_lf定理证明遇阻，求教与Agda差异原因

Let's break down the differences between your Lean and Agda code, and why your proof attempt is getting stuck.

First: The Core Difference in Definition Handling #

In Agda, when you write fusion_lf t = refl, Agda automatically unfolds the definition of fusion and immediately sees that fusion lf t reduces directly to t (matching the first clause of fusion). Agda's type checker handles this trivial equality without needing explicit case analysis or induction.

In Lean, the story is a bit different: Lean doesn't automatically unfold definitions unless you tell it to, especially if the definition's termination isn't immediately obvious to its recursive checker. Let's fix your proof first, then address the termination aspect.

Fixing the fusion_lf Proof #

Your theorem doesn't need induction at all—induction is for cases where you need an inductive hypothesis about subterms, but here fusion lf t directly returns t regardless of what t is. A simpler proof uses case analysis (not induction) and explicitly unfolds the fusion definition:

theorem fusion_lf : ∀ (t : tree), fusion lf t = t :=
begin
  intro t,
  cases t, -- Split into lf and nd cases
  { refl }, -- fusion lf lf = lf is trivial
  { dsimp [fusion], refl }, -- Unfold fusion: fusion lf (nd g x d) matches the first clause, returns nd g x d
end

Or even more concisely:

theorem fusion_lf : ∀ (t : tree), fusion lf t = t :=
λ t, by cases t; refl

The reason your original induction attempt got stuck is that Lean wasn't unfolding the fusion definition in the nd case. Adding dsimp [fusion] tells Lean to expand the definition, making the equality nd g x d = nd g x d obvious to the checker.

The Termination Issue (Why Lean Might Be Fussy) #

Looking at your fusion definition, Lean's default structural recursion checker might struggle to confirm it terminates. The third clause makes recursive calls like fusion r1 (nd l2 x2 r2)—here, the second argument is a full nd node, not a direct subterm of the original input. Unlike Agda, Lean requires explicit proof that recursive definitions terminate unless they use strict structural recursion.

To fix this, we can add a termination measure based on the total size of the two input trees:

1. First, define a function to calculate the size of a tree:

   def size : tree → nat
   | tree.lf := 0
   | (tree.nd l x r) := 1 + size l + size r
   

2. Update your fusion definition with a termination_by clause to prove termination:

   def fusion : tree → tree → tree
   | tree.lf t2 := t2
   | t1 tree.lf := t1
   | (tree.nd l1 x1 r1) (tree.nd l2 x2 r2) := 
     if x1 ≤ x2 then 
       tree.nd (fusion r1 (tree.nd l2 x2 r2)) x1 l1 
     else 
       tree.nd (fusion (tree.nd l1 x1 l1) r2) x2 l2
   termination_by fusion t1 t2 := size t1 + size t2
   

   This tells Lean that the sum of the sizes of the two input trees strictly decreases with each recursive call, which guarantees termination. With this clause, Lean will fully recognize the equality rules for fusion, making proofs even smoother.

Key Takeaways #

• Lean requires explicit definition unfolding: Use dsimp [fusion] or rw fusion to expand definitions when needed, unlike Agda which does this automatically.
• Termination matters for Lean's equality rules: For non-structural recursive definitions (like skew heap fusion), you need to provide a termination measure to ensure Lean accepts the definition's equalities as rewrite rules.

内容的提问来源于stack exchange，提问作者Oblivier