In an environment with `B : forall n, T (S n) `

(and `N : nat`

, `a : X`

, `f : T N -> X`

), I'm trying to do

```
match N with
| 0 => a
| S N' => f (B N' : T N)
end.
```

but Coq complains that `B N'`

has type `T (S N')`

, not `T N`

.

After a little bit of thinking I was able to get what I want with

```
match N as Z return ((T Z -> X) -> X) with
| 0 => fun _ => a
| S N' => fun g => g (B N')
end f
```

but it is horrible. Is there a simpler way?

Short answer: using raw terms I don't think so, you just rediscovered the "convoy pattern".

:cry: is there a simple way to repeat this pattern with Ltac?

yes, the "standard" way to do a case-analysis:

```
Definition foo X (T : nat -> Type) (B : forall n, T (S n)) (a : X) (N : nat) (f : T N -> X): X.
Proof.
destruct N as [| n]; [exact a| exact (f (B n))].
Defined.
Print foo.
(* foo = *)
(* fun (X : Type) (T : nat -> Type) (B : forall n : nat, T (S n)) *)
(* (a : X) (N : nat) (f : T N -> X) => *)
(* match N as n return ((T n -> X) -> X) with *)
(* | 0 => fun _ : T 0 -> X => a *)
(* | S n => fun f0 : T (S n) -> X => f0 (B n) *)
(* end f *)
(* : forall (X : Type) (T : nat -> Type), *)
(* (forall n : nat, T (S n)) -> X -> forall N : nat, (T N -> X) -> X *)
```

Or if you prefer

```
Definition foo X (T : nat -> Type) (B : forall n, T (S n)) (a : X) (N : nat) (f : T N -> X): X :=
ltac:(destruct N as [| n]; [exact a| exact (f (B n))]).
```

That does not work in my case because N and f are parameters (Parameter f :...) and hence I get an ill-typed abstraction. (IIRC, it might also be that f is a definition using the parameter N, either way it is not a variable in the proof context and the destruct results in an ill-typed abstraction as the type of f doesn't change).

Right now I my solution is to do a lemma like the one you wrote, and then apply it with the actual f.

But this can get tedious when I have to do it in the middle of a proof for something trivial, resulting in a few highly technical lemmas.

Last updated: Jan 29 2023 at 06:02 UTC