## Stream: Coq users

### Topic: A dependent match issue

#### Pierre Rousselin (Aug 20 2023 at 09:04):

I tried to answer this SE question in a direct way and failed. I want to understand why.

Here is the context:

``````Fixpoint F (n: nat): Set :=
match n with
| 0 => bool
| S n' => bool -> (F n')
end.

Fixpoint B (n: nat): Set :=
match n with
| 0 => bool
| 1 => bool
| S n' => bool * (B n')
end.
``````

The user then wants to define recursively a function `apply_f`giving the result of applying an n-ary function `f` to an n-tuple `x`. Here is my try:

``````Fixpoint apply_f {n: nat} : F n -> B n -> bool :=
match n return F n -> B n -> bool with
0 => fun f _ => f
| S n' => match n' return F (S n') -> B (S n') -> bool with
0 => fun f x => (f x)
| S p => fun f x =>
(@apply_f n' (f (fst x)) (snd x))
end
end.
``````

It fails with this error message:

``````In environment
apply_f : forall n : nat, F n -> B n -> bool
n : nat
n' : nat
p : nat
f : F (S (S p))
x : B (S (S p))
The term "f (fst x)" has type
"bool ->
(fix F (n : nat) : Set :=
match n with
| 0 => bool
| S n' => bool -> F n'
end) p" while it is expected to have type "F n'".
``````

indicating that somehow, Coq does not in this context recognize that `bool -> F p` is convertible to `F n'`.
I would like to understand why and how it can be solved.
I tried to read the reference manual, but I don't understand this section, I don't know what an "elimination predicate" is and what is its purpose.

#### Karl Palmskog (Aug 20 2023 at 09:07):

probably not helpful in this case (if low-level understanding is the goal), but the standard answer to most dependent matching problems: switch to using Equations

#### Pierre Rousselin (Aug 20 2023 at 09:09):

Thanks for pointing it out, but I still feel I need to understand completely what happens with `match`. After all, it is the only primitive construct in Coq. (But trying Equations at some point is on my todo list).

#### Karl Palmskog (Aug 20 2023 at 10:04):

the Equations example here looks relevant: https://github.com/mattam82/Coq-Equations/blob/main/examples/MoreDep.v#L44-L139

if I was going to teach Coq, I'd probably have students use Equations instead of `Fixpoint` everywhere, and then writing the `match`es/`Fixpoint` manually would be a form of advanced exercises....

#### Paolo Giarrusso (Aug 20 2023 at 13:12):

I think you should pass S p to f, not n', for this to pass typechecking.

#### Paolo Giarrusso (Aug 20 2023 at 13:14):

but I'm not sure that will pass guard-checking — I'm only talking about the typechecking part.

#### Paolo Giarrusso (Aug 20 2023 at 13:14):

I was puzzled because you've already used the convoy pattern and written the return annotation I'd expect here.

#### Paolo Giarrusso (Aug 20 2023 at 13:16):

To see why, you should be able to use refine to see the type of the match branch: matching n' against S p will replace n' by S p in the goal, but it will not remember that n' := S p, since that's not possible when the scrutinee is an expression.

#### Paolo Giarrusso (Aug 20 2023 at 13:16):

one could record a propositional equality, but you must do that by hand.

#### Paolo Giarrusso (Aug 20 2023 at 13:18):

Therefore, Coq is NOT allowed to consider n' and S p convertible, and that's why the typechecker demands S p here.

#### Paolo Giarrusso (Aug 20 2023 at 13:21):

That's also a general problem: AFAIK, Coq primitive pattern matching, like the `destruct expr` or `case: expr` tactics, will never remember that the scrutinee is equal to the match pattern. (Destruct has extra smarts, but not ones relevant in this scenario; case: avoids those). For that you need `destruct expr eqn:?.`, or the generated proof term, which uses propositional equality.

#### Karl Palmskog (Aug 20 2023 at 13:29):

I guess `Program Fixpoint` might help with remembering scrutinee equality?

#### Paolo Giarrusso (Aug 20 2023 at 16:54):

“yes”, but “with friends like that who needs enemies” comes to mind, given the quadratic blowup to term size this can cause

#### Paolo Giarrusso (Aug 20 2023 at 16:58):

My perspective might be biased because of extra circumstances that made this pretty painful, but let’s just say Equations’ design makes two important changes: this behavior is opt-in, and Equations proves unfolding lemmas to hide the generated proof term :-).

#### Pierre Rousselin (Aug 21 2023 at 08:16):

Here is where I am at the moment. I still do not understand everything but it's getting better.
As @Paolo Giarrusso suggested, I tried using `refine` and `destruct` with an equation to build the function in proof mode.

``````Fixpoint apply_f {n: nat} : F n -> B n -> bool.
Proof.
refine
match n return F n -> B n -> bool with
0 => fun f _ => f
| S n' => _
end.
destruct n' as [| p] eqn:E.
- exact (fun f x => (f x)).
- intros f x.
rewrite <-E in f.
refine (apply_f n' (f (fst x)) _).
rewrite E. exact (snd x).
Defined.
``````

This works and is accepted. Inspecting the proof term and a lot of cleaning now gives:

``````Fixpoint apply_f2 {n : nat} : F n -> B n -> bool :=
match n return (F n -> B n -> bool) with
| 0 => fun f _ => f
| S n' =>
match n' as k return (k = n' -> F (S k) -> B (S k) -> bool) with
| 0 => fun _ f x => f x
| S p =>
(fun E f x =>
apply_f2 ((eq_rec _ (fun i => F (S i)) f _ E) (fst x))
(eq_rec (S p) B (snd x) _ E))
end (eq_refl n')
end.
``````

For clarity, here is the definition of `eq_rec` (well, of `eq_rect` but it is the same):

``````eq_rect =
fun (A : Type) (x : A) (P : A -> Type) (f : P x) (a : A) (e : x = a) =>
match e in (_ = a0) return (P a0) with
| eq_refl => f
end
: forall (A : Type) (x : A) (P : A -> Type),
P x -> forall a : A, x = a -> P a

Arguments eq_rect [A]%type_scope x P%function_scope f y e
(where some original arguments have been renamed)
``````

Last updated: Jun 13 2024 at 21:01 UTC