Stream: Coq users

Topic: match with sigma type problem


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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