[Agda] Computation and patterns in called functions

[Nils Anders Danielsson]

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))

-- 
/NAD