<p>An algorithm to decide pattern match coverage can be complete by computing the complement for each case. For example:</p>
<ul>
<li><p><code>Nat</code> The primitive constructors are <code>0</code> and <code>suc (n : Nat)</code>.</p>
<p>Suppose the user provides the cases <code>0</code>, <code>suc (suc x)</code>, and <code>suc 0</code>. We can refine the set of uncovered patterns by examining each case in turn:</p>
<ol>
<li><code>{0, suc n} -&gt; {suc n}</code> by <code>0</code></li>
<li><code>{suc n} -&gt; {suc 0}</code> by <code>suc (suc x)</code> match part of <code>n</code> and rest <code>0</code> case (inductively if deeper)</li>
<li><code>{suc 0} -&gt; {}</code> by final pattern</li>
</ol>
</li>
<li><p><code>A x B</code> For product, consider each combination</p>
</li>
</ul>
<p>The algorithm is based on a generative approach, and for decidable propositions, interpreting as a boolean will work too, but what will happen in the case of any regular proposition?</p>

<type-theory><pattern-matching>
Is it possible to confirm that a pattern-matching statement is exhaustive when cases can be arbitrary predicates?
CC BY-SA 4.0
2023-08-14T07:24:02.723Z
Would it be correct to rephrase the question in your title as "Is it possible to confirm that a pattern-matching statement is exhaustive when cases can be arbitrary predicates?"?
Michael Homer
CC BY-SA 4.0
2023-08-14T07:26:26.727Z
Yes, it's correct.
林子篆
CC BY-SA 4.0
2023-08-14T17:09:10.387Z
What system of logic do you want to use for the predicates?
David Young
CC BY-SA 4.0
2023-08-14T18:09:39.577Z
Variants of dependent type.
林子篆
<p>Not for truly arbitrary predicates, because of undecidable and open problems.</p>
<pre class="lang-ocaml prettyprint-override"><code>let ARBITRARY_PROGRAM : string = ...

let counterexample : () =
  match n with
  | n if (eval ARBITRARY_PROGRAM n) -&gt; ()
  (* If we can prove ARBITRARY_PROGRAM evaluates to true for all inputs, we don't
     need another case. But for an arbitrary program this is undecidable *)
  ;;
</code></pre>
<hr />
<p>In theorem-proving languages, you can guide the type-checker to prove some match cases will never be reached, and they will permit those cases not returning anything. Essentially, <strong>if <em>you</em> can prove that the match statement is exhaustive, you can get the compiler to accept it</strong>. You can do this a lot of ways, but probably the most straightforward is to convert your predicate as a dependent function and guide the compiler's type resolution to compute it at compile time.</p>
<h2>Dependent predicate</h2>
<p>In languages with dependent types*, matching on one constructor can cause another type to have no valid constructors. Then you can return something like <code>absurd instance_with_no_constructors</code> or <code>match instance_with_no_constructors with {}</code>, an expression which takes the impossible instance and returns an instance of an arbitrary type, which is sound because <a href="https://ncatlab.org/nlab/show/ex+falso+quodlibet" rel="noreferrer">&quot;ex falso&quot;</a>.</p>
<p>First, we convert the predicate into a type function which can only have an instance if it's met. This conversion is straightforward: <code>bool</code> becomes <code>Prop</code>, <code>Set</code>, or <code>Type</code> (basically the type of types: instances would be <code>Int</code>, <code>String</code>, and other types), <code>true</code> becomes <code>⊤</code> (the unit type, has 1 instance) and <code>false</code> becomes <code>⊥</code> (the empty type, has 0 instances). You can be even more straightforward: every boolean predicate <code>is_foo</code> has the corresponding dependent predicate <code>is_foo = true</code>, so if you're using the predicate in actual computations, you may want to just use that. However for the purposes of this, we'll use dependent predicates directly, since the <code>is_foo = true</code> predicates have extra boilerplate.</p>
<p>Then, we write the pattern match, but use the compiler's type-checking as well as our own hints and lemmas to resolve the predicate. In cases where it's resolved to <code>⊥</code> (false), we use ex-falso to skip writing an actual body.</p>
<p>* and also GADTs, but writing predicates with those isn't so straightforward</p>
<h3><a href="https://wiki.portal.chalmers.se/agda/pmwiki.php" rel="noreferrer">Agda</a> example</h3>
<p>In Agda, we use the <a href="https://agda.readthedocs.io/en/v2.5.2/language/function-definitions.html#absurd-patterns" rel="noreferrer">absurd pattern</a> to match an instance of a type with no constructors, and when it matches, we skip writing the case body entirely (<a href="https://stackoverflow.com/a/42288848">example derived from here</a>).</p>
<pre><code>open import Data.List
open import Data.Bool
open import Data.Unit
open import Data.Empty

isNonEmpty {A : Set} → (xs : List A) → Prop
isNonEmpty [] = ⊥
isNonEmpty (x ∷ xs) = ⊤

-- The second argument is a predicate that can only has an instance when the
-- list is nonempty, so we don't need to return anything from the first case
head : {A : Set} → (xs : List A) → (nonEmpty : IsNonEmpty xs) → A
head [] () -- `()` is the absurd pattern. Since `IsNonEmpty [] = ⊥` and no
           -- instances of `⊥` exist, it matches.
head (x ∷ xs) _ = x
</code></pre>
<hr />
<p>But (you may already know) the best solution is usually to turn your pattern-matching statement into something which doesn't have predicates, only constructors. The downside is that this can be non-straightforward and sometimes impossible to do safely (see: undecidable problems), but when it's practical, you don't need a theorem-proving language to prove exhaustiveness. For instance, instead of something like:</p>
<pre class="lang-ocaml prettyprint-override"><code>let handle_packet p :=
  if is_connect p then
    handle_connect (connect_data p)
  else if is_disconnect p then
    handle_disconnect (disconnect_data p)
  else if is_data_packet f then
    handle_data_packet (packet_data p)
  else
    error &quot;unreachable!&quot;
  ;;
</code></pre>
<p>you'd want to use</p>
<pre class="lang-ocaml prettyprint-override"><code>type packet := Connect connect_data | Disconnect disconnect_data | Data bytes

let parse_packet p : packet := ...

let handle_packet p 
  match (parse_packet p) with
  | Connect data -&gt; handle_connect data
  | Disconnect data -&gt; handle_disconnect data
  | Data data -&gt; handle_data_packet data
  ;;
<span class="math-container">```</span>
</code></pre>

CC BY-SA 4.0
2023-08-14T18:06:19.427Z
2023-08-14T18:06:19.427Z
tarzh
CC BY-SA 4.0
2023-08-14T19:41:07.717Z
Originally I think the undecidable will have 3 cases, true, false, and unknown. I think there has a problem, but I didn't what it is, thanks! I think absurd pattern is a proper answer.
林子篆
# Is it possible to confirm that a pattern-matching statement is exhaustive when cases can be arbitrary predicates?
Posted by: username_0 on 2023-08-14
An algorithm to decide pattern match coverage can be complete by computing the complement for each case. For example:

* `Nat` The primitive constructors are `0` and `suc (n : Nat)`.

  Suppose the user provides the cases `0`, `suc (suc x)`, and `suc 0`. We can refine the set of uncovered patterns by examining each case in turn:

  1. `{0, suc n} -> {suc n}` by `0`
  2. `{suc n} -> {suc 0}` by `suc (suc x)` match part of `n` and rest `0` case (inductively if deeper)
  3. `{suc 0} -> {}` by final pattern
* `A x B` For product, consider each combination

The algorithm is based on a generative approach, and for decidable propositions, interpreting as a boolean will work too, but what will happen in the case of any regular proposition?
**Tags:** type-theory pattern-matching
> **Comments:**
> **username_1**: Would it be correct to rephrase the question in your title as "Is it possible to confirm that a pattern-matching statement is exhaustive when cases can be arbitrary predicates?"?  
> **username_0**: Yes, it's correct.  
> **username_2**: What system of logic do you want to use for the predicates?  
> **username_0**: Variants of dependent type.  
---
## 1 answers
### Answer by username_3 on 2023-08-14. Score: 6 | Accepted answer
Not for truly arbitrary predicates, because of undecidable and open problems.
let ARBITRARY_PROGRAM : string = ...

let counterexample : () =
  match n with
  | n if (eval ARBITRARY_PROGRAM n) -> ()
  (* If we can prove ARBITRARY_PROGRAM evaluates to true for all inputs, we don't
     need another case. But for an arbitrary program this is undecidable *)
  ;;


In theorem-proving languages, you can guide the type-checker to prove some match cases will never be reached, and they will permit those cases not returning anything. Essentially, if you can prove that the match statement is exhaustive, you can get the compiler to accept it. You can do this a lot of ways, but probably the most straightforward is to convert your predicate as a dependent function and guide the compiler's type resolution to compute it at compile time.
Dependent predicate
In languages with dependent types*, matching on one constructor can cause another type to have no valid constructors. Then you can return something like absurd instance_with_no_constructors or match instance_with_no_constructors with {}, an expression which takes the impossible instance and returns an instance of an arbitrary type, which is sound because "ex falso".
First, we convert the predicate into a type function which can only have an instance if it's met. This conversion is straightforward: bool becomes Prop, Set, or Type (basically the type of types: instances would be Int, String, and other types), true becomes ⊤ (the unit type, has 1 instance) and false becomes ⊥ (the empty type, has 0 instances). You can be even more straightforward: every boolean predicate is_foo has the corresponding dependent predicate is_foo = true, so if you're using the predicate in actual computations, you may want to just use that. However for the purposes of this, we'll use dependent predicates directly, since the is_foo = true predicates have extra boilerplate.
Then, we write the pattern match, but use the compiler's type-checking as well as our own hints and lemmas to resolve the predicate. In cases where it's resolved to ⊥ (false), we use ex-falso to skip writing an actual body.
* and also GADTs, but writing predicates with those isn't so straightforward
Agda example
In Agda, we use the absurd pattern to match an instance of a type with no constructors, and when it matches, we skip writing the case body entirely (example derived from here).
open import Data.List
open import Data.Bool
open import Data.Unit
open import Data.Empty

isNonEmpty {A : Set} → (xs : List A) → Prop
isNonEmpty [] = ⊥
isNonEmpty (x ∷ xs) = ⊤

-- The second argument is a predicate that can only has an instance when the
-- list is nonempty, so we don't need to return anything from the first case
head : {A : Set} → (xs : List A) → (nonEmpty : IsNonEmpty xs) → A
head [] () -- `()` is the absurd pattern. Since `IsNonEmpty [] = ⊥` and no
           -- instances of `⊥` exist, it matches.
head (x ∷ xs) _ = x


But (you may already know) the best solution is usually to turn your pattern-matching statement into something which doesn't have predicates, only constructors. The downside is that this can be non-straightforward and sometimes impossible to do safely (see: undecidable problems), but when it's practical, you don't need a theorem-proving language to prove exhaustiveness. For instance, instead of something like:
let handle_packet p :=
  if is_connect p then
    handle_connect (connect_data p)
  else if is_disconnect p then
    handle_disconnect (disconnect_data p)
  else if is_data_packet f then
    handle_data_packet (packet_data p)
  else
    error "unreachable!"
  ;;

you'd want to use
type packet := Connect connect_data | Disconnect disconnect_data | Data bytes

let parse_packet p : packet := ...

let handle_packet p 
  match (parse_packet p) with
  | Connect data -> handle_connect data
  | Disconnect data -> handle_disconnect data
  | Data data -> handle_data_packet data
  ;;
```
> **Comments:**
> **username_0** (2023-08-14): Originally I think the undecidable will have 3 cases, true, false, and unknown. I think there has a problem, but I didn't what it is, thanks! I think absurd pattern is a proper answer.  
---
