The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Talia,

Well you can mimic the eliminator for vectors ;-)

Best,

Dominique

--------------

Require Import List Arith.

Set Implicit Arguments.

Section vec_as_lists.

  Variable X : Type.

  Definition vec (n : nat) := { l : list X | length l = n }.

  Definition vec_nil : vec 0.
  Proof. now exists nil. Defined.

  Definition vec_cons n (x : X) (v : vec n) : vec (S n).
  Proof.
    refine (let (l,Hl) := v in exist _ (x::l) _).
    simpl; f_equal; trivial.
  Defined.

  Section vec_rect.

    Variables (P : forall n, vec n -> Type)
              (HP0 : P vec_nil)
              (HP1 : forall n x v, @P n v -> P (vec_cons x v)).

    Theorem vec_rect n v : @P n v.
    Proof.
      destruct v as (l,<-).
      induction l as [ | x l IHl ].
      + apply HP0.
      + apply (HP1 x IHl).
    Defined.

  End vec_rect.

End vec_as_lists.

---

De: "Talia Ringer" <tringer AT cs.washington.edu>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Vendredi 21 Février 2020 20:19:30
Objet: Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}

Interesting feedback. Does anyone have any examples that don't use SSReflect? I am really not used to SSReflect, and I find it hard to understand what is happening in proofs written in that style.

Is there a useful induction principle for { l : list T & length l = n } that people use in general? For example if you'd like to write your list functions and proofs separately from the invariants about their lengths and proofs about those invariants. Is there an easy way to glue them together in general? Could I define this as a single induction principle, something that takes separately a proof about lists and a proof about its lengths?

It should be pretty easy to show that the equality type [bar = bar] is isomorphic to the equality type [nat = nat], which is nontrivial if you assume univalence.  Does this help?

Interesting, so the type of your index really matters, not just the structure? What is the intuition behind this? It's just weird to me because I could define another type:

Inductive C : unit -> Type :=

| baz : C tt.

and then you could define indexer functions between B and C that let you prove an equivalence between B and C at those indices. It should be very easy to work over equalities between C (because all proofs of unit are equal to each other). What happens when you transport those equalities to proofs about equalities between B?

Talia

On Fri, Feb 21, 2020 at 9:04 AM Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

Very nice, indeed fixing `n`, unlike in the more general `Vector.caseS`, makes the problems I had go away!

- Valentin

On Fri, 21 Feb 2020 at 17:34, Daniel Schepler <dschepler AT gmail.com> wrote:

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