Coq inference behavior

Question

I'm trying to write the following Agda snippet in Coq.

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ; suc; zero)

thin : {n : ℕ} -> Fin (suc n) -> Fin n -> Fin (suc n)
thin zero    y       = suc y
thin (suc x) zero    = zero
thin (suc x) (suc y) = suc (thin x y)

I thought this could be straightforwardly translated to Coq as:

Inductive Fin : nat -> Type :=
| fz {n : nat} : Fin (S n)
| fs {n : nat} : Fin n -> Fin (S n).

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n) :=
  match x, y with
  | fz,    y' => fs y'
  | fs x', fz => fz
  | fs x', fs y' => fs (thin x' y')
  end.
In environment
thin : forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n : nat
x : Fin (S n)
y : Fin n
n0 : nat
x' : Fin n0
n1 : nat
y' : Fin n1
The term "x'" has type "Fin n0"
while it is expected to have type "Fin (S ?n1)".

I believe Coq should be able to figure out the implicit parameter n so I have no idea what is going on. I think I am unaware of a difference between the type systems of Agda and Coq since the former typechecks fine.

Answer

When pattern matching with dependent types, Coq does not usually consider some essential relations between the variables in the context and the variables introduced in the branches.

The easiest solution is to define the function in proof mode, at least to understand what is going on.

This gives:

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n).
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x: Fin (S n)
y: Fin n
Fin (S n)
Proof.
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x: Fin (S n)
y: Fin n
Fin (S n)
  remember (S n) as n1. (* trick to keep the information when destructing *)
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n, n1: nat
Heqn1: n1 = S n
x: Fin n1
y: Fin n
Fin n1
  destruct x; apply eq_add_S in Heqn1; subst n0.
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
y: Fin n
Fin (S n)
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x, y: Fin n
Fin (S n)
  -
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
y: Fin n
Fin (S n) apply fs.
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
y: Fin n
Fin n assumption.
  -
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x, y: Fin n
Fin (S n) destruct y.
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x: Fin (S n)
Fin (S (S n))
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x: Fin (S n)
y: Fin n
Fin (S (S n))
    +
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x: Fin (S n)
Fin (S (S n)) apply fz.
    +
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x: Fin (S n)
y: Fin n
Fin (S (S n)) apply fs.
thin: forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n: nat
x: Fin (S n)
y: Fin n
Fin (S n) apply thin; assumption.
Defined. (* to create a transparent constant, as given by a classic Fixpoint *)

You can then print the value and read the lambda term to understand how to define it directly. This could give:

thin = 
fix thin
  (n : nat) (x : Fin (S n)) (y : Fin n) {struct x} :
    Fin (S n) :=
  let n1 := S n in
  let Heqn1 : n1 = S n := eq_refl in
  match x in (Fin n0) return (n0 = S n -> Fin n0) with
  | @fz n0 =>
      fun Heqn2 : S n0 = S n =>
      let Heqn3 : n0 = n := eq_add_S n0 n Heqn2 in
      eq_rec_r (fun n2 : nat => Fin (S n2)) (fs y)
        Heqn3
  | @fs n0 x0 =>
      fun Heqn2 : S n0 = S n =>
      let Heqn3 : n0 = n := eq_add_S n0 n Heqn2 in
      eq_rec_r (fun n2 : nat => Fin n2 -> Fin (S n2))
        (fun x1 : Fin n =>
         match
           y in (Fin n2) return (Fin n2 -> Fin (S n2))
         with
         | @fz n2 => fun _ : Fin (S n2) => fz
         | @fs n2 y0 =>
             fun x2 : Fin (S n2) => fs (thin n2 x2 y0)
         end x1) Heqn3 x0
  end Heqn1
     : forall n : nat, Fin (S n) -> Fin n -> Fin (S n)

Arguments thin {n}%nat_scope _ _

The return clauses of the pattern matchings is used to solve the problem presented above: they connect the variables introduced in the branches and the ones in the context. This is discussed more deeply here: http://adam.chlipala.net/cpdt/html/MoreDep.html.

Also note that this particular inductive type was discussed a few weeks ago on the coq-club mailing list. See https://sympa.inria.fr/sympa/arc/coq-club/2016-03/msg00206.html.

Q: This helps a lot, thanks! I should have finished Chlipala's book before actually trying to do stuff in Coq. One more question I have: is it considered bad practice to define functions in proof mode?

A: I don't really know. Usually, I do that to check the lambda term and write it myself. Anyway, I try to use mostly low-level tactics to create a readable lambda term. Tactics like inversion create

A: Tactics like inversion create non-natural terms and should be avoided. Maybe other users have stronger opinions on this particular subject.