[Agda] Computation and patterns in called functions

[Francesco Mazzoli]

Hi Nils,

Thanks for the answer.

At Mon, 28 Jan 2013 16:24:16 +0100,
Nils Anders Danielsson wrote:
> 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 (λ ())

That would be great and would also solve the problem that you have to explicitly
pattern match to use absurd patterns.  See
<https://personal.cis.strath.ac.uk/conor.mcbride/pub/Hmm/Hier.agda> for an
extreme instance of this problem.

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

I don’t get what you mean here.  In my case the short version of optExp-correct:

    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

Would get expanded to

    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₁@(const (suc _)) e₂) =
      cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
    optExp-correct {vs} (plus e₁@(var _) e₂) =
      cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
    optExp-correct {vs} (plus e₁@(plus _ _) e₂) =
      cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
    optExp-correct (var _) = refl
    optExp-correct (const _) = refl

Where I’m using haskell-style @, but in Agda you could simply desugar those to
‘let’s.  Maybe I’m missing something...

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

Yes that works but feels overkill, especially if it’s a one-off proof - which is
often the case.

Francesco