Pierre Rousselin (Nov 11 2022 at 21:38): 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.
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: Apr 19 2024 at 02:02 UTC