[Agda] Computation and patterns in called functions

[Francesco Mazzoli]

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