## Stream: Coq users

### Topic: remembering case equality in match

#### Jonas Oberhauser (Apr 30 2021 at 13:54):

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?

#### Enrico Tassi (Apr 30 2021 at 14:07):

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

#### Jonas Oberhauser (Apr 30 2021 at 15:19):

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

#### Kenji Maillard (Apr 30 2021 at 15:28):

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 *)
``````

#### Kenji Maillard (Apr 30 2021 at 15:29):

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

#### Jonas Oberhauser (May 01 2021 at 13:30):

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: Jun 24 2024 at 14:01 UTC