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.

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

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

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....

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

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

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

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.

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

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

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.

I guess `Program Fixpoint`

might help with remembering scrutinee equality?

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

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 :-).

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