Stream: Coq users

Topic: remembering case equality in match


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

view this post on Zulip Enrico Tassi (Apr 30 2021 at 14:07):

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

view this post on Zulip Jonas Oberhauser (Apr 30 2021 at 15:19):

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

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

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

view this post on Zulip 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: Jan 29 2023 at 06:02 UTC