[Agda] Eta reduction of a function argument in a where block

[Wojciech Jedynak]

2011/8/8 Nils Anders Danielsson <nad at chalmers.se>:
> On 2011-08-07 19:38, Wojciech Jedynak wrote:
>>
<cut>
>
> If you define
>
>  f₁ args₁ = body₁
>    where
>    f₂ : Type
>    f₂ args₂ = body₂
>
> then Agda behaves as if you wrote (roughly) the following code:
>
>  mutual
>
>    f₁ args₁ = body₁[f₂ ≔ _M.f₂ <pattern variables from args₁>]
>
>    module _M <typed pattern variables from args₁> where
>
>      f₂ : Type
>      f₂ args₂ = body₂[f₂ ≔ _M.f₂ <pattern variables from args₁>]
>
<cut>

OK, now I know what is my question :-) Would it be possible to have
Agda automagically simplify the helper module so the main functions'
(here f1) arguments that are not used in f2 are not abstracted upon?

I don't know if it would be worth the effort, but here is a short
example where this makes a provable-or-not-provable difference:

\begin{code}

module Test where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

nat-ind : (C : ℕ → Set)
        → C zero → ((n : ℕ) → C n → C (suc n))
        → (n : ℕ) → C n
nat-ind C z s zero = z
nat-ind C z s (suc n) = s _ (nat-ind C z s n)

-- m + n, not n + m
plus : ℕ → ℕ → ℕ
plus n m = nat-ind (λ _ → ℕ) n iter m module PLUS where
  iter : ℕ → ℕ → ℕ
  -- make iter strict in the first arg
  iter zero     rec = suc rec
  iter (suc n') rec = suc rec

-- only change: eta reduce m
plus2 : ℕ → ℕ → ℕ
plus2 n = nat-ind (λ _ → ℕ) n iter module PLUS2 where
  iter : ℕ → ℕ → ℕ
  iter zero     rec = suc rec
  iter (suc n') rec = suc rec

lemma : ∀ (n m : ℕ) → plus n m ≡ m + n
lemma n zero = refl
lemma n (suc zero) = refl
lemma n (suc (suc m)) with lemma n (suc m)
... | rec = cong suc {!rec!}

lemma2 : ∀ (n m : ℕ) → plus2 n m ≡ m + n
lemma2 n zero = refl
lemma2 n (suc zero) = refl
lemma2 n (suc (suc m)) with lemma2 n (suc m)
... | rec = cong suc rec

\end{code}

The proof of lemma gets stuck:

Goal: PLUS.iter n (suc (suc m)) m
      (nat-ind (λ _ → ℕ) n (PLUS.iter n (suc (suc m))) m)
      ≡ suc (m + n)
————————————————————————————————————————————————————————————
rec : PLUS.iter n (suc m) m
      (nat-ind (λ _ → ℕ) n (PLUS.iter n (suc m)) m)
      ≡ suc (m + n)

it looks like PLUS.iter uses m, but it actually doesn't.

-- 
Greetings,
Wojciech Jedynak