Case-split causes problems for coverage checker

[GoogleCodeExporter]

Here is a self-contained module (a simple proof of determinacy for lambda
calculus; it won't work because I've omitted the beta rule for purposes of
reducing the test-case) which demonstrates the problem:

module casebug where

  -- stdlib nonsense
  postulate
    Level : Set 
    lZ : Level
    lS : Level -> Level
    lmax : Level -> Level -> Level

  {-# BUILTIN LEVEL     Level #-}
  {-# BUILTIN LEVELZERO lZ  #-}
  {-# BUILTIN LEVELSUC  lS   #-}
  {-# BUILTIN LEVELMAX lmax #-}

  module List where
    data List {l : Level} (A : Set l) : Set l where
      []  : List A
      _::_ : A -> List A -> List A

    {-# COMPILED_DATA List [] [] (:) #-}
    {-# BUILTIN LIST List #-}
    {-# BUILTIN NIL [] #-}
    {-# BUILTIN CONS _::_ #-}

    infixr 99 _::_

  open List

  data _==_ {l : Level} {A : Set l} (M : A) : A → Set l where
    Refl : M == M

  {-# BUILTIN EQUALITY _==_ #-}
  {-# BUILTIN REFL Refl #-}

  data _∈_ {A : Set} : (x : A) (l : List A) → Set where -- type \in
    i0 : {x : A} {xs : List A} → x ∈ x :: xs
    iS : {x y : A} {xs : List A} → x ∈ xs → x ∈ y :: xs

  data Tp : Set where
    bool : Tp
    _⇒_ : Tp → Tp → Tp

  Ctx = List Tp
  _,,_ : Ctx → Tp → Ctx
  Γ ,, τ = τ :: Γ

  infixr 10 _⇒_
  infixr 9 _,,_
  infixr 8 _⊢_

  data _⊢_ (Γ : Ctx) : Tp → Set where
    #t  : Γ ⊢ bool
    #f  : Γ ⊢ bool
    if_then_else_ : {τ : Tp} → Γ ⊢ bool → Γ ⊢ τ → Γ ⊢ τ → Γ ⊢ τ
    var : {τ : Tp} 
        → τ ∈ Γ
        → Γ ⊢ τ 
    lam : {τ1 τ2 : Tp} 
        → Γ ,, τ1 ⊢ τ2
        → Γ ⊢ τ1 ⇒ τ2
    app : {τ1 τ2 : Tp} 
        → Γ ⊢ τ1 ⇒ τ2 
        → Γ ⊢ τ1 
        → Γ ⊢ τ2

  data value :  {τ : Tp} → [] ⊢ τ → Set where
    Value/true : value #t
    Value/false : value #f
    Value/lam : {τ₁ τ₂ : Tp} {e : [] ,, τ₁ ⊢ τ₂} → value (lam e)

  module OpSem where
    data _↦c_ : {τ : Tp} → [] ⊢ τ → [] ⊢ τ → Set where
      -- beta omitted to avoid defining substitutions
      Step/if-true : {τ : Tp} {e₁ e₂ : [] ⊢ τ}
             → if #t then e₁ else e₂ ↦c e₁
      Step/if-false : {τ : Tp} {e₁ e₂ : [] ⊢ τ}
             → if #f then e₁ else e₂ ↦c e₂

    data _↦_ : {τ : Tp} → [] ⊢ τ → [] ⊢ τ → Set where
      Step/here : {τ : Tp} {e e' : [] ⊢ τ} → e ↦c e' → e ↦ e'
      Step/app1 : {τ₁ τ₂ : Tp} {e e' : [] ⊢ τ₁ ⇒ τ₂} {e₁ : [] ⊢ τ₁}
             → e ↦ e'
             → (app e e₁) ↦ (app e' e₁)
      Step/app2 : {τ₁ τ₂ : Tp}  {e : [] ,, τ₁ ⊢ τ₂} {e₁ e₁' : [] ⊢ τ₁}
             → e₁ ↦ e₁'
             → (app (lam e) e₁) ↦ (app (lam e) e₁')
      Step/if-cond : {τ : Tp} {e e' : [] ⊢ bool} {e₁ e₂ : [] ⊢ τ}
              → e ↦ e'
              → if e then e₁ else e₂ ↦ if e' then e₁ else e₂

    data _↦*_ : {τ : Tp} → [] ⊢ τ → [] ⊢ τ → Set where
      Done : {τ : Tp} {e : [] ⊢ τ} → e ↦* e
      Step : {τ : Tp} {e e' e'' : [] ⊢ τ} 
           → e ↦ e'  →  e' ↦* e''
           → e ↦* e''

    data _⇓_ {τ : Tp} : [] ⊢ τ → [] ⊢ τ → Set where
      N : {e v : [] ⊢ τ} → value v → e ↦* v → e ⇓ v

    determinacy : {e v₁ v₂ : [] ⊢ bool} → e ⇓ v₁ → e ⇓ v₂ → v₁ == v₂
    determinacy (N x Done) (N x₂ Done) = {!!}
    determinacy (N Value/true Done) (N x₂ (Step (Step/here x) x₃)) = {!!}
    determinacy (N Value/false Done) (N x₂ (Step (Step/here x) x₃)) = {!!}
    determinacy (N x (Step (Step/here x₁) x₂)) (N Value/true Done) = {!!}
    determinacy (N x (Step CASE-ME x₂)) (N Value/false Done) = {!!}
    determinacy (N x (Step x₁ x₂)) (N x₃ (Step x₄ x₅)) = {!!}

Navigate to the second to last hole and attempt to case-split on CASE-ME.

Q: What version of Agda are you using? On what operating system (if relevant)?
A: Latest Darcs checkout as of August 22, 2013.

Original issue reported on code.google.com by ezy...@mit.edu on 22 Aug 2013 at 5:09

[GoogleCodeExporter]

I suppose I should add, case-split results in this code:

    determinacy : {e v₁ v₂ : [] ⊢ bool} → e ⇓ v₁ → e ⇓ v₂ → v₁ == v₂
    determinacy (N x Done) (N x₂ Done) = {!!}
    determinacy (N Value/true Done) (N x₂ (Step (Step/here x) x₃)) = {!!}
    determinacy (N Value/false Done) (N x₂ (Step (Step/here x) x₃)) = {!!}
    determinacy (N x (Step (Step/here x₁) x₂)) (N Value/true Done) = {!!}
    determinacy (N x (Step (Step/here x₁) x₂)) (N Value/false Done) = ?
    determinacy (N x (Step x₁ x₂)) (N x₃ (Step x₄ x₅)) = {!!}

And this error from the coverage checker:

/srv/code/oplss-agda/handson/casebug.agda:101,5-106,55
Incomplete pattern matching for determinacy. Missing cases:
  determinacy {._} {._} {._}
              (N {._} {_} _
                 (Step {._} {._} {._} {._} (Step/app1 {_} {._} {_} {_} {_} _) _))
              (N {._} {._} _ (Done {._} {._}))
  determinacy {._} {._} {._}
              (N {._} {_} _
                 (Step {._} {._} {._} {._} (Step/app2 {_} {._} {_} {_} {_} _) _))
              (N {._} {._} _ (Done {._} {._}))
  determinacy {._} {._} {._}
              (N {._} {_} _
                 (Step {._} {._} {._} {._} (Step/if-cond {._} {_} {_} {_} {_} _) _))
              (N {._} {._} _ (Done {._} {._}))
when checking the definition of determinacy

I'd also like to know a workaround to convince the type-checker to accept this
definition in some way; it's the only undischarged proof in my development left!

Original comment by ezy...@mit.edu on 22 Aug 2013 at 5:10

[GoogleCodeExporter]

> I'd also like to know a workaround to convince the type-checker to
> accept this definition in some way; it's the only undischarged proof
> in my development left!

You could presumably add the missing cases manually.

Original comment by nils.anders.danielsson on 28 Aug 2013 at 9:07

• Changed state: Accepted
• Added labels: CaseSplitting, PatternMatching, Priority-Medium, Type-Enhancement

[GoogleCodeExporter]

Maybe related to issue #408.

Original comment by andreas....@gmail.com on 14 Oct 2013 at 10:03

• Added labels: Coverage

[andreasabel]

Bug still exists as of today (2016-06-20). Updated test case:

data List {l} (A : Set l) : Set l where
  []  : List A
  _::_ : A -> List A -> List A

infixr 99 _::_

data _==_ {l} {A : Set l} (M : A) : A → Set l where
  Refl : M == M

-- {-# BUILTIN EQUALITY _==_ #-}
-- {-# BUILTIN REFL Refl #-}

data _∈_ {A : Set} : (x : A) (l : List A) → Set where
  i0 : {x : A} {xs : List A} → x ∈ x :: xs
  iS : {x y : A} {xs : List A} → x ∈ xs → x ∈ y :: xs

data Tp : Set where
  bool : Tp
  _⇒_ : Tp → Tp → Tp

Ctx = List Tp
_,,_ : Ctx → Tp → Ctx
Γ ,, τ = τ :: Γ

infixr 10 _⇒_
infixr 9 _,,_
infixr 8 _⊢_
infix  4 if_then_else_

data _⊢_ (Γ : Ctx) : Tp → Set where
  #t  : Γ ⊢ bool
  #f  : Γ ⊢ bool
  if_then_else_ : {τ : Tp} → Γ ⊢ bool → Γ ⊢ τ → Γ ⊢ τ → Γ ⊢ τ
  var : {τ : Tp}
      → τ ∈ Γ
      → Γ ⊢ τ
  lam : {τ1 τ2 : Tp}
      → Γ ,, τ1 ⊢ τ2
      → Γ ⊢ τ1 ⇒ τ2
  app : {τ1 τ2 : Tp}
      → Γ ⊢ τ1 ⇒ τ2
      → Γ ⊢ τ1
      → Γ ⊢ τ2

data value :  {τ : Tp} → [] ⊢ τ → Set where
  Value/true : value #t
  Value/false : value #f
  Value/lam : {τ₁ τ₂ : Tp} {e : [] ,, τ₁ ⊢ τ₂} → value (lam e)

module OpSem where
  infix  2 _↦_ _↦c_

  data _↦c_ : {τ : Tp} → [] ⊢ τ → [] ⊢ τ → Set where
    -- beta omitted to avoid defining substitutions
    Step/if-true : {τ : Tp} {e₁ e₂ : [] ⊢ τ}
           → if #t then e₁ else e₂ ↦c e₁
    Step/if-false : {τ : Tp} {e₁ e₂ : [] ⊢ τ}
           → if #f then e₁ else e₂ ↦c e₂

  data _↦_ : {τ : Tp} → [] ⊢ τ → [] ⊢ τ → Set where
    Step/here : {τ : Tp} {e e' : [] ⊢ τ} → e ↦c e' → e ↦ e'
    Step/app1 : {τ₁ τ₂ : Tp} {e e' : [] ⊢ τ₁ ⇒ τ₂} {e₁ : [] ⊢ τ₁}
           → e ↦ e'
           → (app e e₁) ↦ (app e' e₁)
    Step/app2 : {τ₁ τ₂ : Tp}  {e : [] ,, τ₁ ⊢ τ₂} {e₁ e₁' : [] ⊢ τ₁}
           → e₁ ↦ e₁'
           → (app (lam e) e₁) ↦ (app (lam e) e₁')
    Step/if-cond : {τ : Tp} {e e' : [] ⊢ bool} {e₁ e₂ : [] ⊢ τ}
            → e ↦ e'
            → if e then e₁ else e₂ ↦ if e' then e₁ else e₂

  data _↦*_ : {τ : Tp} → [] ⊢ τ → [] ⊢ τ → Set where
    Done : {τ : Tp} {e : [] ⊢ τ} → e ↦* e
    Step : {τ : Tp} {e e' e'' : [] ⊢ τ}
         → e ↦ e'  →  e' ↦* e''
         → e ↦* e''

  data _⇓_ {τ : Tp} : [] ⊢ τ → [] ⊢ τ → Set where
    N : {e v : [] ⊢ τ} → value v → e ↦* v → e ⇓ v

  determinacy : {e v₁ v₂ : [] ⊢ bool} → e ⇓ v₁ → e ⇓ v₂ → v₁ == v₂
  determinacy (N x Done) (N x₂ Done) = {!!}
  determinacy (N Value/true Done) (N x₂ (Step (Step/here x) x₃)) = {!!}
  determinacy (N Value/false Done) (N x₂ (Step (Step/here x) x₃)) = {!!}
  determinacy (N x (Step (Step/here x₁) x₂)) (N Value/true Done) = {!!}
  determinacy (N x (Step CASE-ME x₂)) (N Value/false Done) = {!CASE-ME!}
  determinacy (N x (Step x₁ x₂)) (N x₃ (Step x₄ x₅)) = {!!}

[UlfNorell]

It's worth noting that you can build the definition of determinacy using only case splits, so there is no weird pattern matching going on.

The missing cases that the coverage checker wants are

  determinacy (N _ (Step (Step/app1 _) _)) (N _ Done) = {!!}
  determinacy (N _ (Step (Step/app2 _) _)) (N _ Done) = {!!}
  determinacy (N _ (Step (Step/if-cond _) _)) (N _ Done) = {!!}

[UlfNorell]

Here's the case tree before splitting:

case 3 of
  N ->
    case 6 of
      Done ->
        case 8 of
          N ->
            case 11 of
              Done -> ?
              Step ->
                case 5 of
                  Value/true ->
                    case 14 of
                      Step/here -> ?
                  Value/false ->
                    case 14 of
                      Step/here -> ?
      Step ->
        case 10 of  -- (*) This is the interesting step
          Step/here ->
            case 15 of
              N ->
                case 17 of
                  Value/true ->
                    case 17 of
                      Done -> ?
          _ -> case 12 of
                 N ->
                   case 14 of
                     Value/false ->
                       case 14 of
                         Done -> ?
                     _ -> case 15 of
                            Step -> ?

At (*) we've only matched the first argument against N and Step so the current split would be

determinacy (N x (Step y z)) w

matching the clauses

determinacy (N x (Step (Step/here x₁) x₂)) (N Value/true Done) = ?
determinacy (N x (Step CASE-ME x₂)) (N Value/false Done) = ?
determinacy (N x (Step x₁ x₂)) (N x₃ (Step x₄ x₅)) = ?

Instead of splitting on w which has a constructor in each matching clause we for some reason decide to split on y resulting in a catch-all for the last two clauses. Should the split strategy prefer w? @andreasabel @jespercockx any thoughts?

[jespercockx]

This seems to be working fine now, Agda no longer complains about missing clauses. I think I may have fixed this in 242684b (not sure though).