## Stream: Coq users

### Topic: match with sigma type problem

#### Pierre Rousselin (Nov 11 2022 at 21:38):

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` ?

#### Li-yao (Nov 12 2022 at 01:18):

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

#### Li-yao (Nov 12 2022 at 01:21):

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

#### Paolo Giarrusso (Nov 12 2022 at 18:24):

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.

#### Pierre Rousselin (Nov 12 2022 at 21:37):

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: Jan 31 2023 at 13:02 UTC