# [Agda] Computation and patterns in called functions

Francesco Mazzoli f at mazzo.li
Mon Jan 28 13:35:17 CET 2013

```Hi list,

I frequently encounter a nasty problem when having to prove properties about
functions with that pattern match only on certain constructors, since in the
proof I have to consider every possible case for the terms to compute.  I think
that an heuristic that checks whether the matched constructors have been matched
already and takes the last branch otherwise would be very useful - or maybe
there is already a solution that I’m not aware of.

The issue is better explained with an example (in this case taken from CPDT):

Var : Set
Var = ℕ

Vars : Set
Vars = Var → Var

data Exp : Set where
const : ℕ         → Exp
var   : Var       → Exp
plus  : Exp → Exp → Exp

evalExp : Vars → Exp → ℕ
evalExp vs (const n)    = n
evalExp vs (var v)      = vs v
evalExp vs (plus e₁ e₂) = evalExp vs e₁ + evalExp vs e₂

optExp : Exp → Exp
optExp (plus (const 0) e) = optExp e
optExp (plus e₁ e₂)       = plus (optExp e₁) (optExp e₂)
optExp e                  = e

Now, we predictably we want to prove that the optimisation preserves the value
of the expression:

optExp-correct : ∀ {vs} e → evalExp vs e ≡ evalExp vs (optExp e)
optExp-correct (const n) = refl
optExp-correct (var v) = refl
optExp-correct (plus (const 0) e) = optExp-correct e
optExp-correct {vs} (plus (const (suc n)) e) =
cong₂ _+_ (optExp-correct {vs} (const (suc n))) (optExp-correct e)
optExp-correct {vs} (plus (var v) e) =
cong₂ _+_ (optExp-correct {vs} (var v)) (optExp-correct e)
optExp-correct {vs} (plus (plus e₁ e₂) e₃) =
cong₂ _+_ (optExp-correct {vs} (plus e₁ e₂)) (optExp-correct e₃)

This is very ugly, since after we have matched the ‘plus (const 0) e’ we know
that the ‘plus e₁ e₂’ branch in ‘optExp’ will be taken.  I don’t have an
implementation in mind but I don’t think it would be too hard to have Agda
understand this so that we can simply write

optExp-correct : ∀ {vs} e → evalExp vs e ≡ evalExp vs (optExp e)
optExp-correct (plus (const 0) e) = optExp-correct e
optExp-correct {vs} (plus e₁ e₂) =
cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
optExp-correct e = refl

This problem can often be avoided by pairing the proof with the program:

optExp′ : (e : Exp) → ∃ (λ e′ → ∀ {vs} → evalExp vs e′ ≡ evalExp vs e)
optExp′ (plus (const 0) e) = let (e′ , p ) = optExp′ e in e′ , p
optExp′ (plus e₁ e₂)       = let (e₁′ , p) = optExp′ e₁
(e₂′ , q) = optExp′ e₂
in plus e₁′ e₂′ , cong₂ _+_ p q
optExp′ e                  = e , refl

However, I don’t think this is satisfactory since the programs themselves will
be much less readable if intertwined with the proofs.

Maybe in this case there is an easier path that I haven’t seen, but I think that
in any case the addition I described would be very useful.

Francesco
```