For more complex programs, I often run into the problem mentioned here, where I need to deduce extra information from the result of a match: https://stackoverflow.com/questions/27316254/coq-keeping-information-in-a-match-statement

That approach works well, until I need to manipulate those definitions in later proofs. Here's an example:

```
Parameter foo : nat -> list nat.
Parameter bar : forall n, foo n <> nil -> nat.
(* Want baz to equal 42 when foo returns nil, and otherwise to equal bar. *)
Definition baz (n : nat) : nat.
refine (match foo n with
| nil => 42
| cons m ls => _ end).
(* We have no info about foo n... *)
Abort.
```

I employ the trick in the above link:

```
Definition baz (n : nat) : nat.
refine (match foo n as x return foo n = x -> nat with
| nil => fun _ => 42
| _ => _ end eq_refl).
intro; apply (bar n); congruence. Defined.
```

But let's say I want to prove something:

```
Axiom bar_fact : forall n H, bar n H <> 0.
Theorem baz_fact : forall n, baz n <> 0.
Proof. intros; unfold baz. destruct (foo n).
(* ERROR: Abstracting over the term "l" leads to a term ... which is ill-typed. *)
```

There appear to be a number of threads on this:

https://stackoverflow.com/questions/14867685/abstracting-leads-to-a-term-ill-typed-yet-well-typed?rq=3

https://stackoverflow.com/questions/63027162/abstraction-typing-error-resulting-from-case-eq-and-rewriting-in-coq

https://stackoverflow.com/questions/59223096/abstracting-over-the-terms-is-ill-defined-when-destructuring

but only the second presents what I regard as a generally applicable workaround to Coq's gaucheness with match terms. Indeed, importing ssreflect and continuing with `generalize (eq_refl (foo n)); case: {2 3}(foo n)`

allows the proof of `baz_fact`

to be completed.

My question is, are there any alternative ways to define `baz`

and/or prove `baz_fact`

, especially within base Coq? This seems to be something of an unnatural solution to a problem that arises naturally among beginners.

In this particular instance, it would be straightforward to rewrite `baz`

with an if-then using a sumbool type:

```
Definition is_nil : forall ls : list nat, { ls = nil } + { ls <> nil }.
Proof. now destruct ls; left+right. Qed.
Definition baz (n : nat) : nat.
refine (if is_nil (foo n) then 42 else _). now apply (bar n). Defined.
(* baz =
fun n : nat =>
match is_nil (foo n) with
| left _ => 42
| right x => bar n x
end
: nat -> nat *)
```

and `destruct`

is much better behaved for this definition. Is using sum types the preferred approach, even in the more general situation where you might have many match branches, possibly introducing new variables? For example, suppose I didn't want `baz n`

to equal `bar n`

when `foo n = cons m ls`

, but instead to equal `m + bar n`

. I could make do with more sum and product types:

```
Definition is_cons : forall ls : list nat, {x | ls = cons (fst x) (snd x)} + { ls = nil }.
Proof. destruct ls eqn:K. now right. now left; exists (n,l). Qed.
Definition baz (n : nat) : nat.
refine (if is_cons (foo n) then _ else 42). destruct s as [(m,ls) H].
refine (m + bar n _); congruence. Defined.
```

and work from there, although even this gets a bit inelegant.

standard advice: use Equations to write any pattern matching definitions, then you for example get equational theorems with info from (implicit) matches for free

Or if you allow yourself to use destruct, you can use `destruct H eqn:heqˋ

Pierre Courtieu said:

Or if you allow yourself to use destruct, you can use `destruct H eqn:heqˋ

That appears to amount to the same thing behind the scenes as my first definition of `baz`

, with the same problems about unfolding and destructing it later.

Sometimes it's possible to generalize the definition (so that it no longer mentions `eq_refl`

). In your case it is:

```
Definition baz' (n : nat) (p : list nat) (Hp : foo n = p) : nat.
refine (match p as x return foo n = x -> nat with
| nil => fun _ => 42
| _ => _ end Hp).
intro; apply (bar n). rewrite H. apply cons_nil_ne. Defined.
Lemma eqeq n : baz n = baz' n (foo n) eq_refl.
Proof. reflexivity. Qed.
Theorem baz'_fact : forall n p Hp, baz' n p Hp <> 0.
Proof. intros; unfold baz'. destruct p; try congruence. apply bar_fact. Qed.
```

Now `baz_fact`

follows from `baz'_fact`

and `eqeq`

.

This seems to be something of an unnatural solution to a problem that arises naturally among beginners.

That solution is not as unnatural as it may seem at a glance. In fact it's the same trick (`return foo n = x -> _`

, aka. the convoy pattern, or "abstract over an equality proof before destructing"), replicated at the proof level, modulo a small generalization that the return clause may also mention the proof of equality (`return forall e : foo n = x -> _`

).

Last updated: Jun 13 2024 at 19:02 UTC