I am having a problem with the definition of a recursive sum. Here is a minimal example :

```
From Coq Require Import Classical_Prop PeanoNat.
Open Scope nat_scope.
Definition nat_lt (n : nat) := { i : nat | i < n }.
Definition inj_lt {n m : nat} (h : n <= m) : nat_lt n -> nat_lt m :=
fun e => let i:= (proj1_sig e) in
exist (fun i => i < m) i (Nat.lt_le_trans i n m (proj2_sig e) h).
Definition restriction {A : Type} {n m : nat}
(h : n <= m) (f : nat_lt m -> A) := fun (j : nat_lt n) => f (inj_lt h j).
Fixpoint sum_lt {n : nat} (f : nat_lt n -> nat) :=
match n with
0 => 0
| (S n') => sum_lt (restriction (Nat.le_succ_diag_r n') f) + (f n)
end.
```

The last definition is rejected with the following error message :

```
In environment
sum_lt : forall n : nat, (nat_lt n -> nat) -> nat
n : nat
f : nat_lt n -> nat
n' : nat
The term "f" has type "nat_lt n -> nat" while it is expected to have type
"nat_lt (S n') -> ?A" (cannot unify "nat_lt (S n')" and
"nat_lt n").
```

What can I do to make coq understand that `(S n') = n`

?

remove the `f`

argument and put it in a `fun f`

in each branch instead.

```
Fixpoint sum_lt {n : nat} : (nat_lt n -> nat) -> _ :=
match n with
| O => fun f => _
| S n' => fun f => _
end.
```

The go-to reference for dependent pattern matching in Coq is CPDT: http://adam.chlipala.net/cpdt/html/Cpdt.MoreDep.html

Agree. Summary if it helps: what you need is to let Coq replace `n`

by `S n'`

. Coq will _never_ do that for occurrences of `n`

already in context of the match, and Coq _will_ do that for occurrences of `n`

in the goal. And Li-yao's fix moves `f`

from the context to the goal.

Thank you very much @Li-yao ! For the solution and also for the link ! I have made great progress today thanks to you !

Last updated: Jun 16 2024 at 01:42 UTC