The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Feb 21, 2020 at 2:42 AM Valentin Robert
<valentin.robert.42 AT gmail.com>
 wrote:
> Or I have to painfully roll my own inversion:
>
> Goal forall T (P : Vector.t T 2 -> Type) v, P v.
>   move => T P v.
>   pose goal :=
>     (
>       fun n v =>
>         match n as n' return Vector.t T n' -> Type with
>         | 2 => P
>         | _ => fun _ => True
>         end v
>     ).

What if instead, you rolled the basic vectorS_inv and vector0_inv
once, and then used those as building blocks?  e.g.

Definition vectorS_inv {X:Type} {n:nat} :
  forall P : Vector.t X (S n) -> Type,
  (forall (h : X) (t : Vector.t X n), P (Vector.cons _ h _ t)) ->
  forall v : Vector.t X (S n), P v.
Admitted.
Definition vector0_inv {X:Type} :
  forall P : Vector.t X O -> Type,
  P (Vector.nil _) -> forall v : Vector.t X O, P v.
Admitted.

Goal forall {X:Type} (P : Vector.t X 2 -> Type),
  (forall a b : X, P (Vector.cons _ a _ (Vector.cons _ b _ (Vector.nil _)))) 
->
  forall v : Vector.t X 2, P v.
intros X P f v. destruct v as [a0 v'] using @vectorS_inv.
destruct v' as [b0 v''] using @vectorS_inv.
inversion v'' using @vector0_inv. apply f.
Defined.
-- 
Daniel Schepler