# [Agda] Computation and patterns in called functions

Nils Anders Danielsson nad at chalmers.se
Mon Jan 28 16:24:16 CET 2013

```On 2013-01-28 13:35, Francesco Mazzoli wrote:
> 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.

There are several solutions:

* One could perhaps change Agda so that overlapping patterns are
replaced with non-overlapping ones before the right-hand sides are
type-checked. (I believe that Coq does this.) For instance,

_≟_ : (x y : Bool) → Dec (x ≡ y)
true  ≟ true  = yes refl
false ≟ false = yes refl
_     ≟ _     = no (λ ())

could be expanded into the following, type-correct code:

_≟_ : (x y : Bool) → Dec (x ≡ y)
true  ≟ true  = yes refl
false ≟ false = yes refl
true  ≟ false = no (λ ())
false ≟ true  = no (λ ())

However, it's not quite clear to me what would happen if a duplicated
right-hand side contained a goal.

* One can use custom eliminators or views. Example (based on your code):

data OptExpP : Exp → Set where
plus-const-0  : ∀ e → OptExpP (plus (const 0) e)
plus          : ∀ e₁ e₂ → e₁ ≢ const 0 → OptExpP (plus e₁ e₂)
anything-else : ∀ e → ¬ (∃₂ λ e₁ e₂ → e ≡ plus e₁ e₂) → OptExpP e

optExpP : ∀ e → OptExpP e
optExpP (const n)                = anything-else (const n) (λ { (_ , _ , ()) })
optExpP (var x)                  = anything-else (var x)   (λ { (_ , _ , ()) })
optExpP (plus (const zero) e)    = plus-const-0 e
optExpP (plus (const (suc n)) e) = plus (const (suc n)) e  (λ ())
optExpP (plus (var x) e)         = plus (var x)         e  (λ ())
optExpP (plus (plus e₁ e₂) e₃)   = plus (plus e₁ e₂)    e₃ (λ ())

optExp : Exp → Exp
optExp e with optExpP e
optExp .(plus (const 0) e) | plus-const-0 e    = optExp e
optExp .(plus e₁ e₂)       | plus e₁ e₂ _      = plus (optExp e₁) (optExp e₂)
optExp .e                  | anything-else e _ = e

optExp-correct : ∀ {vs} e → evalExp vs e ≡ evalExp vs (optExp e)
optExp-correct e with optExpP e
optExp-correct .(plus (const 0) e) | plus-const-0 e               = optExp-correct e
optExp-correct .(plus e₁ e₂)       | plus e₁ e₂ _                 = cong₂ _+_ (optExp-correct e₁) (optExp-correct e₂)
optExp-correct .(const x)          | anything-else (const x)    _ = refl
optExp-correct .(var x)            | anything-else (var x)      _ = refl
optExp-correct .(plus e₁ e₂)       | anything-else (plus e₁ e₂) p = ⊥-elim (p (e₁ , e₂ , refl))

--