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: Oct 13 2024 at 01:02 UTC