Library tutorial.tutorial


Tutorial for Heq.

Author: Chung-Kil Hur

Institution: Laboratoire Preuves Programmes Systemes, CNRS & Universite Paris Diderot

Require Import Program Heq.

Set Implicit Arguments.

Introduction


Heq is a library supporting

  • rewriting for heterogeneous equality; and
  • manipulation of casts.
We take equality of dependent pairs as a notion of heterogeneous equality, which is equivalent to eq_dep but has some advantages over it as we will see later.

Heq library only assumes Streicher's Axiom K, which is planned to be interalized in a later version of Coq.

The goal of Heq is to make as little as possible the overhead of reasoning about heterogeneous equality. The slogan is

  • reasoning about heterogeneous equality as if it is a leibniz equality.
As an example, we turned the Coq standard library for List (about 2000 lines) into a library for Vector in a few hours without understanding the proofs, \ie, by chaning the syntax and adding some extra tactics to manipulate casts (this overhead is almost zero). Indeed, the definitions, functions and proof structures of List and Vector are almost identical.

We also turned the Hugo Herbelin's merge sort of List and its correctness into a merge sort of Vector and its correctness in the same way. (The proof script is almost identical.)

We also supports deeply dependent types, like heterogeneous vector 'vectorH' of type

vectorH : forall (U:Type) (P:U -> Type) (n : nat), vector U n -> Type

In this tutorial, we will see how to reason about vectors, matrices, heterogeneous vectors and matrices using Heq.

Note: we also simplified the strongly-typed formalization of system F [1] using the Heq library, and formalized the proof of strong normalization of system F given in the book 'proofs and types' [2].

[1] Nick Benton, Chung-Kil Hur, Andrew Kennedy and Conor McBride. Strongly typed term representations in Coq. Submitted, 2009.

[2] Jean Y. Girard, Paul Taylor, Yves Lafont. Proofs and Types. Cambridge University Press, 1989.

Note: we have developed a complete, simple and fast algorithm (tactic) to find dependent occurrences of a term C in a term T, which plays a key role in this work.

Note: if we assume the injectivity of inductive type constructors, we can use JMeq instead of Heq, but we have shown that in general it is inconsistent with the law of excluded middle, or the existence of impredicative type like Prop (see Agda and Coq-Club mailing list).

Acknowledgement: we are very grateful to Hugo Herbelin for many useful discussions.

Definition of Heq


Let us start by looking at at the definitions of Heq and hcast.

Notation "{{ Sig # u , a }}" := (@existT _ Sig u a) (at level 50).

Definition Heq (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) : Prop := {{ Sig # u , a }} = {{ Sig # v , b }}.

Notation "{{ Sig , u , v # a == b }}" := (@Heq _ Sig u a v b) (at level 50, only parsing).
Notation "{{ Sig , Pat # a == b }}" := (@Heq _ Sig Pat a Pat b) (at level 50, only parsing).
Notation "{{ Sig # a == b }}" := (Heq Sig a b) (at level 50).

Definition hcast (U : Type) (Sig : U -> Type) (u v : U) (pf : u = v) (a : Sig u) : Sig v := @eq_rect U u Sig a v pf.

Notation "<< Sig , u # C >> a" := (hcast Sig u a C) (right associativity, at level 65, only parsing).
Notation "<< Sig # C >> a" := (hcast Sig _ a C) (right associativity, at level 65).


As you see, Heq is simply an equality between dependent pairs and hcast is just eq_rect. Note the simple notation for dependent pair, Heq and hcast.

First Example: Vector


Now we take the inductive type vector as our first example. The following is the usual definition of vector.

Section Vector.

  Variable A : Type.

  Inductive vector : nat -> Type :=
    | nil : vector 0
    | cons (a:A) n (l:vector n): vector (S n).

To use Heq for vector, the first step we should do is to define a signature for vector as follows. The difference between the signature Svec and the type constructor vector is that Svec is an eta-expansion of vector, so that

  • Svec
  • fun n => Svec n
  • fun n => vector n
are all convertible, but vector is not convertible to any of the three. So, you must use Svec as a signature for Heq.

  Definition Svec (n:nat) : Type := vector n.

Here are the usual definitions of hd, tail and app.

  Infix "::" := cons (at level 60, right associativity).

  Definition hd n (l:vector (S n)) : A :=
   match l with
     | cons x _ _ => x
   end.

  Definition tail n (l:vector n) : vector (pred n) :=
    match l with
      | nil => nil
      | cons a _ m => m
    end.

  Fixpoint app n (l: vector n) n' (l':vector n') {struct l} : vector (n+n') :=
    match l with
      | nil => l'
      | cons a _ l1 => a :: app l1 l'
    end.

  Infix "++" := app (right associativity, at level 60).

Now we will prove some lemmas using Heq. Through these examples, we will learn the following four tactics:
  • Hgeneralize
  • Hrewrite
  • Helim
  • Hclear

  Lemma app_nil : forall n (l:vector n), {{ Svec # l ++ nil == l }}.

The first lemma to prove is app_nil_end saying that a vector l is equal to the vector l ++ nil. However, one cannot put an equality between them because l has type vector n but l ++ nil has type vector (n+0), which is not convirtible to vector n. Instead, we can formulate this using dependent pairs

{{ Svec # n , l ++ nil }} = {{ Svec # n+0, l }},

which is exactly the form of Heq and is equal to

{{ Svec # l ++ nil == l }}.

  Proof.

We proove by induction on l, and the base case is easily discharged by auto.

    induction l; simpl; auto.

Now let us look at the induction step.
  A : Type
  a : A
  n : nat
  l : vector n
  IHl : {{Svec # l ++ nil == l}}
  ============================
   {{Svec # a :: l ++ nil == a :: l}}


We discharge this goal by rewriting l++nil to l according to the induction hypothesis IHl, followed by reflexivity, as if IHl is a leibniz equality.

    Hrewritec IHl. reflexivity.
  Qed.

Now, let us look at what happened in the proof.

  Goal forall n (l:vector n), {{ Svec # l ++ nil == l }}.
  Proof.
    induction l; simpl; auto.

We first turn IHl into a leibniz equality l ++ nil = << Svec # C >> l by inserting an appropriate cast C, and then performs rewriting. The cast is automatically calculated (see the lemma Hrw and the definition Hty).

    rewrite (Hrw IHl).

  A : Type
  a : A
  n : nat
  l : vector n
  IHl : {{Svec # l ++ nil == l}}
  ============================
   {{Svec # a :: (<< Svec # Hty IHl >> l) == a :: l}}


Now we want to eliminate the cast. The cast Hty IHl has type n = n + 0 and we want to turn it into a cast of type n = n . To do this, we need generalize the cast first.

    Hgeneralize.

  A : Type
  a : A
  n : nat
  l : vector n
  IHl : {{Svec # l ++ nil == l}}
  ============================
   forall C : n = n + 0, {{Svec # a :: (<< Svec # C >> l) == a :: l}}


***** The tactic Hgeneralize generalizes all casts appearing in the conclusion.

Alternatively, one can perform these two steps rewrite (Hrw IHl); Hgeneralize in one go by
    Hrewrite IHl.


***** The tactic Hrewrite eqn rewrites the lhs of eqn into the rhs of eqn by inserting an appropriate generic cast.

We now simplify the cast by the tactic Helim.

    Helim C.

  A : Type
  a : A
  n : nat
  l : vector n
  IHl : {{Svec # l ++ nil == l}}
  ============================
   forall C0 : n = n, {{Svec # a :: (<< Svec # C0 >> l) == a :: l}}


***** The tactic Helim C tries to turn a given cast C into a reflexive cast by proof search.
The algorithm tries to rewrite the rhs of the type of C to its lhs. In this example, C has type n = n + 0, so it rewrote n + 0 to n.

Now we clear the cast.

    Hclear.

  A : Type
  a : A
  n : nat
  l : vector n
  IHl : {{Svec # l ++ nil == l}}
  ============================
   {{Svec # a :: l == a :: l}}


***** The tactic Hclear turns all reflexive casts into refl_equal _ using Streicher's Axiom K and clear them.

One can perform these two steps Helim C; Hclear in one go by
    Helimc C.


When the cast C is the first cast appearing in the conclusion, one can ommit it:
    Helimc.


One can simplify the two steps Hrewrite IHl; Helimc by
    Hrewritec IHl.


This is what we did in the first place.

    Abort.

We can prove the same lemma in a different way.

  Goal forall n (l:vector n), {{ Svec # l ++ nil == l }}.
  Proof.
    induction l; simpl; auto.

  A : Type
  a : A
  n : nat
  l : vector n
  IHl : {{Svec # l ++ nil == l}}
  ============================
   {{Svec # a :: l ++ nil == a :: l}}


Instead of rewriting l ++ nil to l, we can rewrite the other way round: l to l ++ nil, but only in the second occurence.

    Hrewritec <- IHl at 2.

  A : Type
  a : A
  n : nat
  l : vector n
  IHl : {{Svec # l ++ nil == l}}
  ============================
   {{Svec # a :: l ++ nil == a :: l ++ nil}}

    auto.
  Abort.

The following lemma is an exercise.

  Lemma app_ass : forall n (l:vector n) n' (l':vector n') n'' (l'':vector n''), {{ Svec # (l ++ l') ++ l'' == l ++ l' ++ l'' }}.

Here is the proof.

  Proof.
    intros. induction l; simpl; auto.
    Hrewritec IHl. auto.
  Qed.

  Hint Resolve app_ass.

The tactic dependent destruction is useful.

  Lemma hdtail : forall n (l : vector (S n)), l = hd l :: tail l.
    intros. dependent destruction l. reflexivity.
  Qed.

Use of hcast in Definitions


Now we try to define the reverse function. The following is the standard definition.
  Fixpoint rev n (l:vector n) : vector n :=
    match l in vector n return vector n with
      | nil => nil
      | cons x _ l' => rev l' ++ x :: nil
    end.


But, this fails with the following error message:
  The term "rev n0 l' ++ x :: nil" has type "vector (n0 + 1)" while it is expected to have type "vector (S n0)".


We can simply fix it by inserting an appropriate cast. The cast we need is the commutativity of plus. The lemma plus_comm in the standard library is opaque. We can use it as a cast, but a transparent one is better because Coq can compute it.

  Definition plus_n_O n : n = n + 0.
  fix 1. intros. destruct n. reflexivity. simpl. apply f_equal. apply plus_n_O.
  Defined.

  Definition plus_Snm_nSm n m : S n + m = n + S m.
  fix 1. destruct n. reflexivity. intro. simpl. apply f_equal. apply plus_Snm_nSm.
  Defined.

  Definition plus_comm n m : n + m = m + n.
  fix 2. destruct m. symmetry. apply plus_n_O.
  eapply trans_eq. symmetry. apply plus_Snm_nSm. simpl. apply f_equal. apply plus_comm.
  Defined.

We insert the cast plus_comm in the definition of rev.

  Fixpoint rev n (l:vector n) : vector n :=
    match l in vector n return vector n with
      | nil => nil
      | cons x _ l' => << Svec # plus_comm _ _ >> rev l' ++ x :: nil
    end.

The function rev_append is an exercise.
  rev_append n (l:vector n) n' (l': vector n') : vector (n+n')

Here is the definition.

  Fixpoint rev_append n (l:vector n) n' (l': vector n') : vector (n+n') :=
    match l in vector n return vector (n+n') with
      | nil => l'
      | cons a _ l => << Svec # sym_eq (plus_Snm_nSm _ _) >> rev_append l (a::l')
    end.

We prove the distributivity of rev by induction. In this example, we learn the tactic
  • Hsimpl

  Lemma distr_rev : forall n (x:vector n) m (y:vector m), {{ Svec # rev (x ++ y) == rev y ++ rev x }}.
  Proof.
    induction x as [| a n l IHl].

    destruct y as [| a n l].
      auto.

We need to prove the following subgoal.
  A : Type
  a : A
  n : nat
  l : vector n
  ============================
   {{Svec # rev (nil ++ a :: l) == rev (a :: l) ++ rev nil}}


First we unfold the defintion of rev.

      simpl rev.

  A : Type
  a : A
  n : nat
  l : vector n
  ============================
   {{Svec
   # << Svec
     # trans_eq (sym_eq (plus_Snm_nSm n 0)) (f_equal S (sym_eq (plus_n_O n))) >>
     rev l ++ a :: nil ==
   (<< Svec
    # trans_eq (sym_eq (plus_Snm_nSm n 0)) (f_equal S (sym_eq (plus_n_O n))) >>
    rev l ++ a :: nil) ++ nil}}


We see complicated casts, but can generalize them.

      Hgeneralize.

  A : Type
  a : A
  n : nat
  l : vector n
  ============================
   forall C C0 : n + 1 = S n,
   {{Svec # << Svec # C0 >> rev l ++ a :: nil ==
   (<< Svec # C >> rev l ++ a :: nil) ++ nil}}


Here the cast C0 is in the head postion of lhs of Heq. Such casts can be easily eliminated by the following lemmas.

Lemma cast_intro : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (C : u = w),
{{ Sig # a == b }} -> {{ Sig # << Sig # C >> a == b }}.

Lemma cast_intro_r : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (C : v = w),
{{ Sig # a == b }} -> {{ Sig # a == << Sig # C >> b }}.

Also, one can compose casts in composible positions by the lemma.

Lemma cast_compose: forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v w:U) (C : u = v) (C' : v = w),
<< Sig # C' >> << Sig # C >> a = << Sig # trans_eq C C' >> a.

The tactic Hsimpl performs these two simplifications.

      Hsimpl.

  A : Type
  a : A
  n : nat
  l : vector n
  ============================
   forall C : n + 1 = S n,
   {{Svec # rev l ++ a :: nil == (<< Svec # C >> rev l ++ a :: nil) ++ nil}}


***** The tatic Hsimpl generalizes casts by Hgeneralize and then simplifies casts using the lemmas cast_intro, cast_intro_r and cast_compose.

As Hsimpl subsumes Hgeneralize, one can simply run Hsimpl instead of Hgeneralize; Hsimpl.

Now we eliminate the cast and discharge the goal by applying sym_Heq and app_nil.

      Helimc.
      apply sym_Heq, app_nil.

Also, the two steps Hsimpl; Helimc can be done in one step by Hsimplc.

The induction step is an exercise.

Here is the proof.

    intros m y.
    simpl rev.
    Hsimplc.
    Hrewritec (IHl _ y).
    apply app_ass.
  Qed.

We have some remarks on this proof.

  Goal forall n (x:vector n) m (y:vector m), {{ Svec # rev (x ++ y) == rev y ++ rev x }}.
  Proof.
    induction x as [| a n l IHl].

    destruct y as [| a n l].
      auto.

At this point, we unfold rev by simpl rev. Let us see what happen if we simplify everything by simpl.

      simpl.
      Hsimplc.

  A : Type
  a : A
  n : nat
  l : vector n
  ============================
   forall C0 : n + 1 = S n,
   {{Svec # rev l ++ a :: nil == (<< Svec # C0 >> rev l ++ a :: nil) ++ nil}}


The cast was not eliminated. The reason is that simpl simplified S n + 0 into S (n + 0), so the rewriting of S n into n + 1 failed. You can see this by printing hidden arguments.

      Set Printing Implicit. Unset Printing Notations. idtac.

  A : Type
  a : A
  n : nat
  l : vector n
  ============================
   forall C0 : @eq nat (plus n (S O)) (S n),
   @Heq nat Svec (plus n (S O)) (@app n (@rev n l) (S O) (@cons a O nil))
     (S (plus n O))
     (@app (S n)
        (@hcast nat Svec (plus n (S O)) (S n)
           (@app n (@rev n l) (S O) (@cons a O nil)) C0) O nil)


Now we change S (n+0) into S n + 0 and try Hsimplc (or Helimc) again.

      change (S (n+0)) with (S n + 0).
      Hsimplc.

      Unset Printing Implicit. Set Printing Notations. idtac.

  A : Type
  a : A
  n : nat
  l : vector n
  ============================
   {{Svec # rev l ++ a :: nil == (rev l ++ a :: nil) ++ nil}}


The elimination succeeds.

If the elimincation fails when you think it should succeed, you may need to suspect simpl. Also, looking at the hidden arguments might be helpful.

  Abort.

  Lemma rev_append_rev : forall n (l:vector n) n' (l':vector n'), rev_append l l' = rev l ++ l'.
  Proof.
    induction l; auto; intros.
  A : Type
  a : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'), rev_append l l' = rev l ++ l'
  n' : nat
  l' : vector n'
  ============================
   rev_append (a :: l) l' = rev (a :: l) ++ l'


It is always more convinient to turn the 'leibniz equality' in the conclusion to a 'heterogeneous equality'. We can do it by applying the following lemma.

Lemma Heq_eq : forall (U:Type) (Sig: U -> Type) (u:U) (a b:Sig u),
{{ Sig # a == b }} -> a = b.

    apply (Heq_eq Svec).

  A : Type
  a : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'), rev_append l l' = rev l ++ l'
  n' : nat
  l' : vector n'
  ============================
   {{Svec # rev_append (a :: l) l' == rev (a :: l) ++ l'}}


***** The tatic apply (Heq_eq Sig) turns the 'leibniz equality' in the conclusion to a 'heterogeneous equality'.
You should not forget to give the signature Svec, otherwise Coq type checker will infer it as vector.

    simpl rev. simpl rev_append.
    Hsimplc. rewrite IHl.
    Hrewritec (app_ass (rev l) (a::nil) l'). auto.
  Qed.

Example : Permutation


As an example, we consider the predicate Permutation and prove some properties about it without much trouble

  Inductive Permutation : forall n, vector n -> forall m, vector m -> Prop :=
    | perm_nil: Permutation nil nil
    | perm_skip: forall (x:A) n (l:vector n) n' (l':vector n'), Permutation l l' -> Permutation (x :: l) (x :: l')
    | perm_swap: forall (x y:A) n (l:vector n), Permutation (y :: x :: l) (x :: y :: l)
    | perm_trans: forall n (l :vector n) n' (l':vector n') n'' (l'':vector n''), Permutation l l' -> Permutation l' l'' -> Permutation l l''.
  Hint Constructors Permutation.

  Lemma Permutation_refl : forall n (l : vector n), Permutation l l.
  Proof.
    induction l; constructor; auto.
  Qed.

  Lemma Permutation_sym : forall n (l:vector n) n' (l':vector n'), Permutation l l' -> Permutation l' l.
  Proof.
    intros n l n' l' Hperm. induction Hperm; auto.
    eapply perm_trans. apply IHHperm2. auto.
  Qed.

  Hint Resolve Permutation_refl Permutation_sym perm_trans.

  Lemma Permutation_cons_app : forall n (l:vector n) n1 (l1:vector n1) n2 (l2:vector n2) a,
    Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
  Proof.
    intros n l n1 l1. revert n l.
    induction l1 as [| a n1 l1 ].
      simpl; intros.
      apply perm_skip. auto.

      simpl; intros.
      eapply perm_trans. apply perm_skip. apply H.
      eapply perm_trans. apply perm_swap. auto.
  Qed.

  Lemma Permutation_app_swap : forall n (l:vector n) n' (l' : vector n'), Permutation (l++l') (l'++l).
  Proof.
    induction l as [|x n l].
      simpl; intros.
      Hrewritec (app_nil l'). auto.

      induction l' as [|y n' l'].
        simpl. Hrewritec (app_nil l). auto.

        simpl. eapply perm_trans. apply perm_skip. apply IHl.
        simpl. eapply perm_trans. apply perm_swap.
        apply perm_skip.
        eapply perm_trans. apply perm_skip.
        apply Permutation_sym. apply IHl.
        apply IHl'.
  Qed.

Example : PermutationN


In order to make reasoning harder, we consider more dependently typed notion of Permutation, called PermutationN. By construction, only two vectors of the same length are related by PermutationN.

  Inductive PermutationN : forall n, vector n -> vector n -> Prop :=
    | permN_nil: PermutationN nil nil
    | permN_skip: forall (x:A) n (l l':vector n), PermutationN l l' -> PermutationN (x :: l) (x :: l')
    | permN_swap: forall (x y:A) n (l:vector n), PermutationN (y :: x :: l) (x :: y :: l)
    | permN_trans n (l l' l'':vector n): PermutationN l l' -> PermutationN l' l'' -> PermutationN l l''.

  Hint Constructors PermutationN.

  Lemma PermutationN_refl : forall n (l : vector n), PermutationN l l.
    induction l; constructor; auto.
  Qed.

  Lemma PermutationN_sym : forall n (l l':vector n), PermutationN l l' -> PermutationN l' l.
    intros n l l' Hperm. induction Hperm; auto.
    eapply permN_trans. apply IHHperm2. auto.
  Qed.

  Hint Resolve PermutationN_refl PermutationN_sym perm_trans.

In order to state PermutationN_cons_app, we need the following cast.

  Definition n1n2_Sn n1 n2 n (C:n1+n2=n) : n1 + S n2 = S n.
  intros. rewrite <- plus_Snm_nSm. rewrite <- C. auto.
  Defined.

  Lemma PermutationN_cons_app : forall n (l:vector n) n1 (l1:vector n1) n2 (l2:vector n2) a (C:n1+n2=n),
    PermutationN l (<< Svec # C >> l1 ++ l2) -> PermutationN (a :: l) (<< Svec # n1n2_Sn _ _ C >> l1 ++ a :: l2).
  Proof.
    intros n l n1 l1. revert n l.
    induction l1 as [| a n1 l1 ].

      simpl; intros.

  A : Type
  n : nat
  l : vector n
  n2 : nat
  l2 : vector n2
  a : A
  C : n2 = n
  H : PermutationN l (<< Svec # C >> l2)
  ============================
   PermutationN (a :: l) (<< Svec # n1n2_Sn 0 n2 C >> a :: l2)


Now we want to eliminate the cast n1n2_Sn 0 n2 C, but it does not seem easy because PermutationN (a :: l) (a :: l2) does not type check.
    Check (PermutationN (a :: l) (a :: l2)).

    The term "a :: l2" has type "vector (S n2)" while it is expected to have type "vector (S n)".


But, in this example, luckily the variable n is generic, so it can be substituted with n2 by C : n2 = n. However, this substitution is not that simpl: try both subst or Hgeneralize; subst , but they will not work.

But, our proof search engine is more clever. just try.

      Hsimplc.

  A : Type
  n2 : nat
  l2 : vector n2
  a : A
  l : vector n2
  C : n2 = n2
  H : PermutationN l (<< Svec # C >> l2)
  ============================
   PermutationN (a :: l) (a :: l2)


As you see, the variable n has gone away and the vector l has type vector n2.

In order to eliminate the cast C in the hypothesis H, we can move H into the conclusion by revert and eliminate the cast C by Hsimplc (or just Hclear because C is already a reflexive cast).

      revert H. Hsimplc. intro.

  A : Type
  n2 : nat
  l2 : vector n2
  a : A
  l : vector n2
  H : PermutationN l l2
  ============================
   PermutationN (a :: l) (a :: l2)


Note that we can eliminate the both casts at the same time by doing revert first. That is to say, instead of Hsimplc; revert H; Hsimplc; intro, we can do revert H; Hsimplc; intro.

Let us discharge the subgoal and move onto the induction step.

      apply permN_skip. auto.

      simpl; intros.
      Hsimplc.
      eapply permN_trans. apply permN_skip. apply H.

  A : Type
  a : A
  n1 : nat
  l1 : vector n1
  IHl1 : forall (n : nat) (l : vector n) (n2 : nat) 
           (l2 : vector n2) (a : A) (C : n1 + n2 = n),
         PermutationN l (<< Svec # C >> l1 ++ l2) ->
         PermutationN (a :: l) (<< Svec # n1n2_Sn n1 n2 C >> l1 ++ a :: l2)
  n2 : nat
  l2 : vector n2
  a0 : A
  l : vector (n1 + S n2)
  C : S (n1 + n2) = n1 + S n2
  H : PermutationN l (<< Svec # C >> a :: l1 ++ l2)
  ============================
   PermutationN (a0 :: (<< Svec # C >> a :: l1 ++ l2)) (a :: l1 ++ a0 :: l2)


Now we are in real trouble. We cannot eliminate the cast C because a0 :: a :: l1 ++ l2 has type vector (S (S (n1 + n2))), but a :: l1 ++ a0 :: l2 has type vector (S (n1 + S n2)).

Though we cannot eliminate it, we can move it to another place. Note that what we want to do is to swap a0 and a in the left vector, and then to skip a. So, we will turn the conclusion to the following one, with an appropriate cast C0 :

PermutationN (a0 :: a :: l1 ++ l2) (a :: << Svec # C0 >> l1 ++ a0 :: l2)

Let's see how to do this. First put a reflexive cast in front of l1 ++ a0 :: l2 by Hrefl.

      Hrefl (l1 ++ a0 :: l2 : Svec _).

  A : Type
  a : A
  n1 : nat
  l1 : vector n1
  IHl1 : forall (n : nat) (l : vector n) (n2 : nat) 
           (l2 : vector n2) (a : A) (C : n1 + n2 = n),
         PermutationN l (<< Svec # C >> l1 ++ l2) ->
         PermutationN (a :: l) (<< Svec # n1n2_Sn n1 n2 C >> l1 ++ a :: l2)
  n2 : nat
  l2 : vector n2
  a0 : A
  l : vector (n1 + S n2)
  C : S (n1 + n2) = n1 + S n2
  H : PermutationN l (<< Svec # C >> a :: l1 ++ l2)
  ============================
   forall (C0 : S (n1 + n2) = n1 + S n2) (C1 : n1 + S n2 = n1 + S n2),
   PermutationN (a0 :: (<< Svec # C0 >> a :: l1 ++ l2))
     (a :: (<< Svec # C1 >> l1 ++ a0 :: l2))


***** The tatic Hrefl (T : Sig Pat) ( at occ ) inserts a reflexive cast in front of all (or the occ-th) occurrences of T.
Don't forget to give a signature Sig and a pattern Pat. In the case of vector, the pattern is just _, but we will see other patterns later for other signatures.

Now we eliminate the cast C0.

      Helimc C0.

  A : Type
  a : A
  n1 : nat
  l1 : vector n1
  IHl1 : forall (n : nat) (l : vector n) (n2 : nat) 
           (l2 : vector n2) (a : A) (C : n1 + n2 = n),
         PermutationN l (<< Svec # C >> l1 ++ l2) ->
         PermutationN (a :: l) (<< Svec # n1n2_Sn n1 n2 C >> l1 ++ a :: l2)
  n2 : nat
  l2 : vector n2
  a0 : A
  l : vector (n1 + S n2)
  C : S (n1 + n2) = n1 + S n2
  H : PermutationN l (<< Svec # C >> a :: l1 ++ l2)
  ============================
   forall C0 : n1 + S n2 = S (n1 + n2),
   PermutationN (a0 :: a :: l1 ++ l2) (a :: (<< Svec # C0 >> l1 ++ a0 :: l2))


We now tackle the goal as we planned.

      intros. eapply permN_trans. apply permN_swap.
      apply permN_skip.

We further apply IHl1.

      eapply permN_trans. apply IHl1 with (l2:=l2) (C:= refl_equal _). apply PermutationN_refl.

  A : Type
  a : A
  n1 : nat
  l1 : vector n1
  IHl1 : forall (n : nat) (l : vector n) (n2 : nat) 
           (l2 : vector n2) (a : A) (C : n1 + n2 = n),
         PermutationN l (<< Svec # C >> l1 ++ l2) ->
         PermutationN (a :: l) (<< Svec # n1n2_Sn n1 n2 C >> l1 ++ a :: l2)
  n2 : nat
  l2 : vector n2
  a0 : A
  l : vector (n1 + S n2)
  C : S (n1 + n2) = n1 + S n2
  H : PermutationN l (<< Svec # C >> a :: l1 ++ l2)
  C0 : n1 + S n2 = S (n1 + n2)
  ============================
   PermutationN (<< Svec # n1n2_Sn n1 n2 refl >> l1 ++ a0 :: l2)
     (<< Svec # C0 >> l1 ++ a0 :: l2)


Now we see that there are two casts of the same type. We can unify such casts by Hunify.

      Hunify.

  A : Type
  a : A
  n1 : nat
  l1 : vector n1
  IHl1 : forall (n : nat) (l : vector n) (n2 : nat) 
           (l2 : vector n2) (a : A) (C : n1 + n2 = n),
         PermutationN l (<< Svec # C >> l1 ++ l2) ->
         PermutationN (a :: l) (<< Svec # n1n2_Sn n1 n2 C >> l1 ++ a :: l2)
  n2 : nat
  l2 : vector n2
  a0 : A
  l : vector (n1 + S n2)
  C : S (n1 + n2) = n1 + S n2
  H : PermutationN l (<< Svec # C >> a :: l1 ++ l2)
  ============================
   forall C1 : n1 + S n2 = S (n1 + n2),
   PermutationN (<< Svec # C1 >> l1 ++ a0 :: l2)
     (<< Svec # C1 >> l1 ++ a0 :: l2)


***** The tatic Hunify unifies all casts of the same type.

Now discharge the goal.

      auto.
  Qed.

Here is another example.

  Lemma PermutationN_app_swap : forall n (l: vector n) n' (l' : vector n'),
    PermutationN (l ++ l') (<< Svec # plus_comm _ _ >> l' ++ l).
  Proof.
    induction l as [|x n l].
      simpl; intros.
      Hrewritec (app_nil l'). auto.

      induction l' as [|y n' l'].
        simpl. Hrewritec (app_nil l). auto.

        simpl. eapply permN_trans. apply permN_skip.
        apply IHl.
        simpl. Hsimpl. Helimc C0. intros.
        eapply permN_trans. apply permN_swap.

  A : Type
  x : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'),
        PermutationN (l ++ l') (<< Svec # plus_comm n' n >> l' ++ l)
  y : A
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  C0 : S (n' + S n) = S (S (n' + n))
  ============================
   PermutationN (y :: x :: l' ++ l) (<< Svec # C0 >> y :: l' ++ x :: l)


Now we want to skip y. For this, we will move the cast around. We can insert a cast in front of x :: l' ++ l in the left vector, but also it is possible to insert a cast in front of l' ++ x :: l in the right vector. This time we try the latter.

        Hrefl (l' ++ x :: l : Svec _).

  A : Type
  x : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'),
        PermutationN (l ++ l') (<< Svec # plus_comm n' n >> l' ++ l)
  y : A
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  ============================
   forall (C0 : S (n' + S n) = S (S (n' + n))) (C : n' + S n = n' + S n),
   PermutationN (y :: x :: l' ++ l)
     (<< Svec # C0 >> y :: (<< Svec # C >> l' ++ x :: l))


Now if you try Helimc C0, it will fail to eliminate C0. The reason is because Helimc C0 tries to rewrite the rhs to the lhs of C0 : S (n'+S n) = S (S(n'+n')). But, this time we need to rewrite the other way round from the lhs to the rhs.

        Helimc -> C0.

  A : Type
  x : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'),
        PermutationN (l ++ l') (<< Svec # plus_comm n' n >> l' ++ l)
  y : A
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  ============================
   forall C0 : n' + S n = S (n' + n),
   PermutationN (y :: x :: l' ++ l) (y :: (<< Svec # C0 >> l' ++ x :: l))

        intros. apply permN_skip.

        specialize IHl with _ l'.
        apply PermutationN_sym in IHl.

  A : Type
  x : A
  n : nat
  l : vector n
  n' : nat
  l' : vector n'
  IHl : PermutationN (<< Svec # plus_comm n' n >> l' ++ l) (l ++ l')
  y : A
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  C0 : n' + S n = S (n' + n)
  ============================
   PermutationN (x :: l' ++ l) (<< Svec # C0 >> l' ++ x :: l)


Now we will move the cast on the left vector in the hypothesis IHl onto the right vector. For this, we can revert IHl and do the job. Before we do that, we can also hide the current conclusion from the proof search engine by Hhide_concl.

        Hhide_concl.

  A : Type
  x : A
  n : nat
  l : vector n
  n' : nat
  l' : vector n'
  IHl : PermutationN (<< Svec # plus_comm n' n >> l' ++ l) (l ++ l')
  y : A
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  C0 : n' + S n = S (n' + n)
  hgoal := HHideConcl
             (PermutationN (x :: l' ++ l) (<< Svec # C0 >> l' ++ x :: l))
        : Prop
  ============================
   hgoal


Now we move the cast in IHl.

        revert IHl. Hrefl (l++l' : Svec _). Helimc C. intros ? IHl.

  A : Type
  x : A
  n : nat
  l : vector n
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  C0 : n' + S n = S (n' + n)
  hgoal := HHideConcl
             (PermutationN (x :: l' ++ l) (<< Svec # C0 >> l' ++ x :: l))
        : Prop
  C : n + n' = n' + n
  IHl : PermutationN (l' ++ l) (<< Svec # C >> l ++ l')
  ============================
   hgoal


Now we show the hidden conclusion.

        Hshow_concl.

  A : Type
  x : A
  n : nat
  l : vector n
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  C0 : n' + S n = S (n' + n)
  C : n + n' = n' + n
  IHl : PermutationN (l' ++ l) (<< Svec # C >> l ++ l')
  ============================
   PermutationN (x :: l' ++ l) (<< Svec # C0 >> l' ++ x :: l)


***** The tactic Hhide_concl hides the currenct conclusion from the proof serach engine.

***** The tactic Hshow_concl shows the hidden conclusion.

        eapply permN_trans. apply permN_skip.
        apply IHl.

        Hsimpl. Helimc C1. intros.
        eapply permN_trans. apply IHl'.
        Hunify. auto.
  Qed.

Manual manipulation of Casts


Heq also supports manual manipulation of casts. We will see how to use our new tactic to find dependent occurrences of a term. For this, we revisit the above lemma.

  Goal forall n (l: vector n) n' (l' : vector n'),
    PermutationN (l ++ l') (<< Svec # plus_comm _ _ >> l' ++ l).
  Proof.
    induction l as [|x n l].
      simpl; intros.
      Hrewritec (app_nil l'). auto.

      induction l' as [|y n' l'].
        simpl. Hrewritec (app_nil l). auto.

        simpl. eapply permN_trans. apply permN_skip.
        apply IHl.
        simpl. Hsimpl. Helimc C0. intros.
        eapply permN_trans. apply permN_swap.

        Hrefl (l' ++ x :: l : Svec _).

  A : Type
  x : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'),
        PermutationN (l ++ l') (<< Svec # plus_comm n' n >> l' ++ l)
  y : A
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  ============================
   forall (C0 : S (n' + S n) = S (S (n' + n))) (C : n' + S n = n' + S n),
   PermutationN (y :: x :: l' ++ l)
     (<< Svec # C0 >> y :: (<< Svec # C >> l' ++ x :: l))


Now we will manually eliminate the cast C0 by rewriting the lhs of C0 : S (n' + S n) = S (S (n' + n)) to the rhs. First, obstain the necessary equation from C0.

        Hgeteq -> C0.

  A : Type
  x : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'),
        PermutationN (l ++ l') (<< Svec # plus_comm n' n >> l' ++ l)
  y : A
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  H1 : n' + S n = S (n' + n)
  ============================
   forall (C : S (n' + S n) = S (S (n' + n))) (C0 : n' + S n = n' + S n),
   PermutationN (y :: x :: l' ++ l)
     (<< Svec # C >> y :: (<< Svec # C0 >> l' ++ x :: l))


Note that we obtained a refined equation n' + S n = S (n' + n), rather than S (n' + S n) = S (S (n' + n)). Now we try to rewrite.
    rewrite H1.

    Error: Abstracting over the term "n' + S n" leads to a term
    "fun n0 : nat =>
     forall (C : S n0 = S (S (n' + n))) (C0 : n0 = n0),
     PermutationN (y :: x :: l' ++ l)
       (<< Svec # C >> y :: (<< Svec # C0 >> l' ++ x :: l))" which is ill-typed.


But, it fails. For this to succeed, we need to rewrite some occurrences of n' + S n, not all. What we want to rewrite is the first occurence of n' + S n, but we cannot rewrite only the first occurrence because many other occurrencies depend on the first one.

If you print all hidden arguments and carefullly look at them, you will find that only 1, 3, 4, 5, 7-th occurrences are inter-dependent and 2, 6-th occurrences are independent from them. So, the following will successfully rewrite.
    pattern (n' + S n) at 1 3 4 5 7.
    rewrite H1.


But, finding these occurrences is quite painful.

So, let's try our new tactic hpattern.

        hpattern (n' + S n) at 1.

  A : Type
  x : A
  n : nat
  l : vector n
  IHl : forall (n' : nat) (l' : vector n'),
        PermutationN (l ++ l') (<< Svec # plus_comm n' n >> l' ++ l)
  y : A
  n' : nat
  l' : vector n'
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  H1 : n' + S n = S (n' + n)
  ============================
   (fun n0 : nat =>
    forall (C : S n0 = S (S (n' + n))) (C0 : n' + S n = n0),
    PermutationN (y :: x :: l' ++ l)
      (<< Svec # C >> y :: (<< Svec # C0 >> l' ++ x :: l))) 
     (n' + S n)


As you see, it successfully abstracted the first and its dependent occurreces of n' + S n. The algorithm to find these occurrences is very simpl (wrriten in 50 lines of OCaml code) and fast (almost linear in the size of the conclusion). Most importantly, the algorithm is complete in the sense that hpattern C at p succeeds whenever there exists a set of occurrences including p that can be abstracted.

        rewrite H1.
        clear H1.
        Hclear.

Instead of hpattern (n' + S n) at 1; rewrite H1, one can do hrewrite H1 at 1. Also, instead of hrewrite H1 at 1; clear H1; Hclear, one can do hrewritec H1 at 1. Also, we can do hrewritec H1, as it tries every occurrence from the first to the last.


***** The tactic hpattern C at p abstracts the p-th and its dependent occurrences of C in the conclusion.

***** The tactic hpattern C is equivalent to first [ hpattern C at 1 | ... | hpattern C at n ] for n the last occurrence of C.

***** The tactic hrewrite ( <- ) eqn ( at p ) is equivalent to happtern C1 ( at p ); rewrite ( <- ) eqn when eqn has type C1 = C2.

***** The tactic hrewritec ( <- ) eqn ( at p ) is a shorthand for hrewrite ( <- ) eqn ( at p ); try (clear eqn); Hclear.

        intros. apply permN_skip.

        specialize IHl with _ l'.
        apply PermutationN_sym in IHl.
        Hhide_concl.
        revert IHl. Hsimpl.

Here is an exercise.
  A : Type
  x : A
  n : nat
  l : vector n
  n' : nat
  l' : vector n'
  y : A
  IHl' : PermutationN ((x :: l) ++ l')
           (<< Svec # plus_comm n' (S n) >> l' ++ x :: l)
  C0 : n' + S n = S (n' + n)
  hgoal := HHideConcl
             (PermutationN (x :: l' ++ l) (<< Svec # C0 >> l' ++ x :: l))
        : Prop
  ============================
   forall C : n' + n = n + n',
   PermutationN (<< Svec # C >> l' ++ l) (l ++ l') -> hgoal



        Hrefl (l++l' : Svec _).
        Hgeteq C1.
        hrewritec H. intros.
        Hshow_concl.

  Abort.

Other useful tactics



***** The tactic Hsubst is an Heq version of subst tactic.
This tactic is useful especially when one wants to simplify equations generated by inversion tactic.

  Fixpoint In (a:A) n (l:vector n) {struct l} : Prop :=
    match l with
      | nil => False
      | cons b _ m => b = a \/ In a m
    end.

  Lemma in_app_or : forall n (l:vector n) n' (l':vector n') (a:A), In a (l ++ l') -> In a l \/ In a l'.
  Proof.
    intros n l n' l' a. elim l; simpl; auto.
    intros a0 n0 y H H0. elim H0; auto.
    intro H1. elim (H H1); auto.
  Qed.

  Lemma in_or_app : forall n (l:vector n) n' (l':vector n') (a:A), In a l \/ In a l' -> In a (l ++ l').
  Proof.
    intros n l n' l' a. elim l; simpl; intro H.
    elim H; auto; intro H0; elim H0.
    intros n0 y H0 H1. elim H1; auto 4.
    intro H2. elim H2; auto.
  Qed.

  Inductive NoDup : forall n, vector n -> Prop :=
    | NoDup_nil : NoDup nil
    | NoDup_cons : forall x n (l:vector n), ~ In x l -> NoDup l -> NoDup (x::l).

  Lemma NoDup_remove_1 : forall n (l:vector n) n' (l':vector n') a, NoDup (l++a::l') -> NoDup (l++l').
  Proof.
    induction l; simpl; intros.
  A : Type
  n' : nat
  l' : vector n'
  a : A
  H : NoDup (a :: l')
  ============================
   NoDup l'


We do inversion on H.

      inversion H.

  A : Type
  n' : nat
  l' : vector n'
  a : A
  H : NoDup (a :: l')
  x : A
  n : nat
  l : vector n'
  H3 : ~ In a l
  H4 : NoDup l
  H0 : n = n'
  H1 : x = a
  H2 : {{fun n : nat => vector n # n', l}} =
       {{fun n : nat => vector n # n', l'}}
  ============================
   NoDup l'


inversion H generated three equations H0, H1, H2. If you try subst, then it will simplify only H0 and H1, not H2. But, with Hsubst, we can simplify all of them.

      Hsubst.
      auto.

We can do the same here.

      inversion H.
      Hsubst.

      constructor.
      red; intro; apply H3.
      apply in_or_app. destruct (in_app_or _ _ _ H0); simpl; tauto.
      apply IHl with a0; auto.
  Qed.

Here, we have some remarks. The tactic dependent destruction is intended to generalize the tactic inversion. But, sometimes dependent destruction does not work properly when inversion does (see 'strnorm.v' for this problem). We discussed this problem with Matthieu Sozeau, the developer of dependent destruction, and found an algorithm to improve it. So, the next version of dependent destruction will not have such problems.

For the moment, when dependent destruction does not work, try inversion; Hsubst. It may work. In the proof of strnong normalization of System F, this happened several times.


***** The tactic Hhide_evars hides evars from the proof search engine.

***** The tactic Hshow_evars shows the hidden evars.
If there are evars in the conclusion, Heq tactics may not work properly. So, you should hide them before you run any Heq tactics.

Here is an example.

  Lemma hide_evars_example: forall a n (l: vector n) n' (l': vector n'),
    PermutationN (<< Svec # trans_eq (sym_eq (plus_Snm_nSm _ _)) (f_equal S (plus_comm _ _)) >> l ++ a :: l') (a :: l' ++ l).
  Proof.
    intros.
    eapply permN_trans.

    Hhide_evars.
      Hrefl (hev0 : Svec _). Helimc C.
      intros. eapply permN_trans. apply PermutationN_app_swap.
      Hunify.
    Hshow_evars.

    intros. apply PermutationN_refl. auto.
  Qed.


***** The tactic Hset_concl attach a tag to the current conclusion to explicitly say that it is the conclusion.

***** The tactic Hunset_concl removes the tag.
If the conclusion includes (hetergeneous) equations, the proof search engine might confuse them with casts. In such cases, one can use Hset_concl to explicitly set the conclusion.

Here is an example.

  Lemma set_concl_example: forall n (l1 l2: vector n), {{ Svec # l1 == l2 ++ nil }} -> exists l2', l1 = l2'.
  Proof.
    intros.
    revert H.
    Hset_concl.
      Hrewritec (app_nil l2).
    Hunset_concl.
    intro.
    eexists. apply (Heq_eq Svec). apply H.
  Qed.


***** The tactic Hsimpl_hyps eliminates all casts in head positions in all hypotheses.
It applies the following two lemmas to all hypotheses.

Lemma cast_elim : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (H : u = w),
{{ Sig # << Sig # H >> a == b }} -> {{ Sig # a == b }}.

Lemma cast_elim_r : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (H : v = w),
{{ Sig # a == << Sig # H >> b }} -> {{ Sig # a == b }}.

  Lemma simpl_hyps_example: forall n (l: vector n) m (l': vector m) a,
    {{ Svec # l' == rev (a::l) }} -> {{ Svec # rev l ++ a :: nil == l' }}.
  Proof.
    intros.
    simpl in H.
    Hsimpl_hyps.
    auto.
  Qed.

End Vector.

Implicit Arguments nil [ [A] ].

Infix "::" := cons (at level 60, right associativity).
Infix "++" := app (right associativity, at level 60).

Section Map.

  Variables A B : Type.
  Variable f : A -> B.

  Fixpoint map n (l:vector A n) : vector B n :=
    match l with
      | nil => nil
      | cons a _ t => f a :: map t
    end.

End Map.

Note: we will soon add more comments to the following sections.

Advanced Example : Maxtrix


Section Matrix.

  Variable A : Type.

  Notation vec := (vector A) (only parsing).

  Definition matrix n m := vector (vec m) n.

Note the signature Smat and the pattern Pmat. The pattern is (_,_) because the domain of Smat is nat * nat, so its elements are pairs.

  Definition Smat (p : nat * nat) := matrix (fst p) (snd p).
  Notation Pmat := (_,_) (only parsing).

  Fixpoint hdcol n m (M: matrix n (S m)) : vec n :=
    match M with
      | nil => nil
      | cons row _ M' => hd row :: hdcol M'
    end.

  Fixpoint tlcol n m (M: matrix n m) : matrix n (pred m) :=
    match M with
      | nil => nil
      | cons row _ M' => tail row :: tlcol M'
    end.

  Fixpoint conscol n (col: vec n) m (M: matrix n m) : matrix n (S m) :=
    match M in vector _ n return vec n -> matrix n (S m) with
      | nil => fun _ => nil
      | cons row _ M' => fun col => (hd col :: row) :: (conscol (tail col) M')
    end col.

  Lemma conshdtlcol: forall n m (M: matrix n (S m)), M = conscol (hdcol M) (tlcol M).
    induction M; intros.
      auto.
      simpl in *. rewrite <- hdtail, <- IHM. auto.
  Qed.

  Lemma hdconscol: forall n m (col: vec n) (M: matrix n m), hdcol (conscol col M) = col.
    induction M; intros.
      dependent destruction col. auto.
      simpl. rewrite IHM, hdtail. auto.
  Qed.

  Lemma tlconscol: forall n m (col: vec n) (M: matrix n m), tlcol (conscol col M) = M.
    induction M; intros.
      dependent destruction col. auto.
      simpl. rewrite IHM. auto.
  Qed.

  Definition appmatrow n1 n2 m (M1 : matrix n1 m) (M2 : matrix n2 m) : matrix (n1+n2) m := app M1 M2.

  Fixpoint appmatcol n m1 m2 (M1 : matrix n m1) (M2 : matrix n m2) : matrix n (m1+m2) :=
    match m1 return matrix n m1 -> matrix n (m1+m2) with
      | 0 => fun _ => M2
      | S m1' => fun M1 => conscol (hdcol M1) (appmatcol (tlcol M1) M2)
    end M1.

  Lemma appmatrow_assoc: forall n1 n2 n3 m (M1: matrix n1 m) (M2: matrix n2 m) (M3: matrix n3 m),
    {{ Smat,Pmat # appmatrow M1 (appmatrow M2 M3) == appmatrow (appmatrow M1 M2) M3 }}.
    intros. unfold appmatrow. Hrewritec (app_ass M1 M2 M3). auto.
  Qed.

  Lemma appmatcol_assoc: forall n m1 m2 m3 (M1: matrix n m1) (M2: matrix n m2) (M3: matrix n m3),
    {{ Smat,Pmat # appmatcol M1 (appmatcol M2 M3) == appmatcol (appmatcol M1 M2) M3 }}.

  induction m1; intros.
    auto.
    rewrite (conshdtlcol M1). simpl. rewrite ! hdconscol, ! tlconscol.
    Hrewritec (IHm1 _ _ (tlcol M1) M2 M3). auto.
  Qed.

End Matrix.

Notation Pmat := (_,_) (only parsing).

Advanced Example : Heterogeneous Vector


Section VectorH.

  Variable U : Type.
  Variable P: U -> Type.

  Notation vecU := (vector U) (only parsing).

  Inductive vectorH : forall n, vecU n -> Type :=
    | nilH : vectorH nil
    | consH (u:U) (a:P u) n (un:vecU n) (l:vectorH un) : vectorH (u :: un).

Note the signature SvecH and the pattern PvecH. The pattern is {{Svec _ # _, _}} because the domain of SvecH is sig T (Svec _), which is the sigma type { n : nat & Svec _ n }, so its elements are dependent pairs with signature Svec _

  Definition SvecH (p: sigT (Svec U)) := vectorH (projT2 p).
  Notation PvecH := ({{Svec _ # _,_}}) (only parsing).

  Infix ":::" := consH (at level 60, right associativity).

  Definition n_Spred n (un: vecU n) n' (pf: n = S n') : vecU (S (pred n)).
  intros. destruct n. inversion pf. exact un.
  Defined.

  Definition hdH n (un: vecU (S n)) (l:vectorH un) : P (hd un) :=
   match l in @vectorH n' un' return forall pf : n' = S n, P (hd (n_Spred un' pf)) with
     | nilH => fun pf => False_rect _ (O_S _ pf)
     | consH _ a _ _ _ => fun _ => a
   end (refl_equal _).

  Definition tailH n (un: vecU n) (l:vectorH un) : vectorH (tail un) :=
    match l in vectorH un return vectorH (tail un) with
      | nilH => nilH
      | consH _ a _ _ l => l
    end.

  Fixpoint appH n (un: vecU n) (l: vectorH un) n' (un': vecU n') (l':vectorH un') : vectorH (un++un') :=
    match l with
      | nilH => l'
      | consH _ a _ _ l1 => a ::: appH l1 l'
    end.

  Infix "+++" := appH (right associativity, at level 60).

  Lemma app_nilH : forall n (un: vecU n) (l:vectorH un), {{ SvecH,PvecH # l +++ nilH == l }}.
  Proof.
    induction l; simpl; auto.
    Hrewritec IHl. auto.
  Qed.

  Lemma app_assH : forall n (un:vecU n) (l:vectorH un) n' (un':vecU n') (l':vectorH un') n'' (un'':vecU n'') (l'':vectorH un''),
    {{ SvecH,PvecH # (l +++ l') +++ l'' == l +++ l' +++ l'' }}.
  Proof.
    intros. induction l; simpl; auto.
    Hrewritec IHl. auto.
  Qed.
  Hint Resolve app_ass.

  Lemma hdtailH : forall n (un: vecU (S n)) (l : vectorH un), {{ SvecH,PvecH # l == hdH l ::: tailH l }}.
    intros. dependent destruction l. auto.
  Qed.

  Fixpoint revH n (un: vecU n) (l:vectorH un) : vectorH (rev un) :=
    match l in vectorH un return vectorH (rev un) with
      | nilH => nilH
      | consH _ a _ _ l' => << SvecH,PvecH # sym_Heq (distr_rev (_::nil) _) >> revH l' +++ a ::: nilH
    end.

  Lemma revappC: forall n (un:vecU n) u n' (un':vecU n'), {{ Svec U # rev un ++ u :: un' == rev (u :: un) ++ un' }}.
    intros. simpl rev. Hsimplc.
    Hrewritec (app_ass (rev un) (u::nil) un'). auto.
  Defined.

  Fixpoint rev_appendH n (un:vecU n) (l:vectorH un) n' (un':vecU n') (l': vectorH un') {struct l} : vectorH (rev un ++ un') :=
    match l in vectorH un return vectorH (rev un ++ un') with
      | nilH => l'
      | consH _ a _ _ l => << SvecH,PvecH # revappC _ _ _ >> rev_appendH l (a:::l')
    end.

  Lemma distr_revH : forall n (un: vecU n) (x:vectorH un) m (um: vecU m) (y:vectorH um),
    {{ SvecH,PvecH # revH (x +++ y) == revH y +++ revH x }}.
  Proof.
    induction x as [| u a n un l IHl].
    destruct y as [| u a n un l].
    auto.

    simpl rev; simpl revH. Hsimplc.
    apply sym_Heq, app_nilH.

    intros m um y.
    simpl rev; simpl revH. Hsimplc.
    Hrewritec (IHl _ _ y).
    apply (app_assH (revH y) (revH l) (a ::: nilH)).
  Qed.

  Lemma rev_append_revH : forall n (un:vecU n) (l:vectorH un) n' (un':vecU n') (l':vectorH un'), rev_appendH l l' = revH l +++ l'.
  Proof.
    induction l; auto; intros.
    apply (Heq_eq SvecH PvecH).
    simpl rev; simpl revH; simpl rev_appendH.
    Hsimplc. rewrite IHl.
    Hrewritec (app_assH (revH l) (a:::nilH) l'). auto.
  Qed.

PermutationH

  Inductive PermutationH : forall n (un:vecU n), vectorH un -> forall m (um: vecU m), vectorH um -> Prop :=
    | permH_nil: PermutationH nilH nilH
    | permH_skip: forall u (x:P u) n (un:vecU n) (l:vectorH un) n' (un':vecU n') (l':vectorH un'), PermutationH l l' -> PermutationH (x ::: l) (x ::: l')
    | permH_swap: forall u (x:P u) v (y: P v) n (un:vecU n) (l:vectorH un), PermutationH (y ::: x ::: l) (x ::: y ::: l)
    | permH_trans n (un:vecU n) (l:vectorH un) n' (un':vecU n') (l':vectorH un') n'' (un'':vecU n'') (l'':vectorH un''): PermutationH l l' -> PermutationH l' l'' -> PermutationH l l''.

  Hint Constructors PermutationH.

  Lemma PermutationH_refl : forall n (un:vecU n) (l : vectorH un), PermutationH l l.
  Proof.
    induction l; constructor. exact IHl.
  Qed.

  Lemma PermutationH_sym : forall n (un:vecU n) (l:vectorH un) n' (un': vecU n') (l':vectorH un'), PermutationH l l' -> PermutationH l' l.
  Proof.
    intros n un l n' un' l' Hperm.
    induction Hperm; auto.
    apply permH_trans with (l':=l'); assumption.
  Qed.

  Hint Resolve PermutationH_refl PermutationH_sym permH_trans.

  Lemma PermutationH_cons_app : forall n (un: vecU n) (l:vectorH un) n1 (un1:vecU n1) (l1:vectorH un1) n2 (un2:vecU n2) (l2:vectorH un2) u (a:P u),
    PermutationH l (l1 +++ l2) -> PermutationH (a ::: l) (l1 +++ a ::: l2).
  Proof.
    intros n un l n1 un1 l1; revert n un l.
    induction l1.
    simpl.
    intros; apply permH_skip; auto.
    simpl; intros.
    apply permH_trans with _ _ (a0:::a:::l1+++l2).
    apply permH_skip; auto.
    apply permH_trans with _ _ (a:::a0:::l1+++l2).
    apply permH_swap; auto.
    apply permH_skip; auto.
  Qed.

  Lemma PermutationH_app_swap : forall n (un:vecU n) (l:vectorH un) n' (un':vecU n') (l' : vectorH un'), PermutationH (l+++l') (l'+++l).
  Proof.
    induction l as [|u x n un l].
    simpl. intros n' un' l'. Hrewritec (app_nilH l'). auto.
    induction l' as [|u' y n' un' l' IHl'].
    simpl. Hrewritec (app_nilH l). auto.
    simpl. eapply permH_trans. apply permH_skip. apply IHl.
    simpl. eapply permH_trans. apply permH_swap. apply permH_skip.
    eapply permH_trans. apply permH_skip. apply PermutationH_sym. apply IHl.
    apply IHl'.
  Qed.

PermutationHN

  Inductive PermutationHN : forall n (un un':vecU n), vectorH un -> vectorH un' -> Prop :=
    | permHN_nil: PermutationHN nilH nilH
    | permHN_skip: forall u (x:P u) n (un un':vecU n) (l:vectorH un) (l':vectorH un'), PermutationHN l l' -> PermutationHN (x ::: l) (x ::: l')
    | permHN_swap: forall u (x:P u) v (y: P v) n (un:vecU n) (l:vectorH un), PermutationHN (y ::: x ::: l) (x ::: y ::: l)
    | permHN_trans n (un un' un'':vecU n) (l:vectorH un) (l':vectorH un') (l'':vectorH un''): PermutationHN l l' -> PermutationHN l' l'' -> PermutationHN l l''.

  Hint Constructors PermutationHN.

  Lemma PermutationHN_refl : forall n (un:vecU n) (l : vectorH un), PermutationHN l l.
    induction l; constructor; auto.
  Qed.

  Lemma PermutationHN_sym : forall n (un un':vecU n) (l:vectorH un) (l':vectorH un'), PermutationHN l l' -> PermutationHN l' l.
    intros n un un' l l' Hperm. induction Hperm; auto.
    eapply permHN_trans. apply IHHperm2. auto.
  Qed.

  Hint Resolve PermutationHN_refl PermutationHN_sym permHN_trans.

  Definition n1n2_SnHN n1 (un1:vecU n1) n2 (un2:vecU n2) n u (C:n1+n2=n) :
    {{Svec U # un1 ++ u :: un2 == <<Svec U # n1n2_Sn _ _ C >> un1 ++ u :: un2 }}.
    intros. Hsimpl. auto.
  Defined.

  Lemma PermutationHN_cons_app : forall n (un:vecU n) (l:vectorH un) n1 (un1:vecU n1) (l1:vectorH un1) n2 (un2:vecU n2) (l2:vectorH un2) u (a: P u) (C: {{Svec U # un1 ++ un2 == un}}),
    PermutationHN l (<< SvecH,PvecH # C >> l1 +++ l2) -> PermutationHN (a ::: l) (<< SvecH,PvecH # n1n2_SnHN _ _ _ (Heq_proj1 C) >> l1 +++ a ::: l2).
  Proof.
    intros n un l n1 un1 l1; revert n un l.
    induction l1 as [| u a n1 un1 l1 IHl1 ].

    simpl. intros. revert H. do 2 Hsimplc. auto.

    simpl app; simpl appH. intros. Hsimplc.
    eapply permHN_trans. apply permHN_skip. apply H.
    Hreflrec (a ::: l1 +++ a0 ::: l2 : SvecH PvecH). Helimc C0.

    intros. eapply permHN_trans. apply permHN_swap.

    Hreflrec (a0:::l1+++l2 : SvecH PvecH). Helimc C2.

    intros. apply permHN_skip.
    Hreflrec (l1 +++ a0 ::: l2 : SvecH PvecH). Helimc C1.

    intros. eapply permHN_trans. apply IHl1 with (l2:=l2) (C:= refl_equal _) . auto.
    Hsimplc. auto.
  Qed.

  Definition plus_commHN n1 (un1:vecU n1) n2 (un2:vecU n2) : {{Svec U # un1 ++ un2 == <<Svec U # plus_comm _ _ >> un1 ++ un2 }}.
  intros. Hsimpl. auto.
  Defined.

  Lemma PermutationHN_app_swap : forall n (un:vecU n) (l: vectorH un) n' (un': vecU n') (l' : vectorH un'),
    PermutationHN (l +++ l') (<< SvecH,PvecH # plus_commHN _ _ >> l' +++ l).
  Proof.
    induction l; simpl; intros.
      Hrewritec (app_nilH l'). auto.

      induction l'; simpl.
        Hrewrite (app_nilH (a:::l)). Helimc C1. auto.

        eapply permHN_trans. apply permHN_skip. apply IHl.

        Hsimpl. Helimc C1.
        intros. simpl. eapply permHN_trans. apply permHN_swap.
        Hreflrec (a ::: l' +++ l : SvecH PvecH). Helimc C0.
        intros. apply permHN_skip.
        Hreflrec (l'+++a:::l : SvecH PvecH). Helimc C0.
        intros. specialize IHl with _ _ l'. apply PermutationHN_sym in IHl.
        Hhide_concl.
          revert IHl. Hreflrec (l+++l' : SvecH PvecH). Helimc C. intros ? ? IHl.
        Hshow_concl.
        eapply permHN_trans. apply permHN_skip. apply IHl.
        Hsimpl. Helimc C. intros.
        eapply permHN_trans. apply IHl'. Hunify. auto.
  Qed.

End VectorH.

Implicit Arguments nilH [ [U] [P] ].
Implicit Arguments consH [ U P u n un ].

Notation PvecH := ({{Svec _ # _,_}}) (only parsing).
Infix ":::" := consH (at level 60, right associativity).
Infix "+++" := appH (right associativity, at level 60).

Section MapH.

  Variable U : Type.
  Variable P : U -> Type.
  Variable V : Type.
  Variable Q : V -> Type.

  Variable f : U -> V.
  Variable F : forall u (a: P u), Q (f u).

  Fixpoint mapH n (un:vector U n) (l: vectorH P un) : vectorH Q (map f un) :=
    match l in vectorH _ un return vectorH Q (map f un) with
      | nilH => nilH
      | consH _ a _ _ t => consH (F a) (mapH t)
    end.

End MapH.

Advanced Examples : Heterogeneous Matrix


Section MatrixH.

  Variable U : Type.
  Variable P: U -> Type.

  Notation vecU := (vector U) (only parsing).
  Notation matU := (matrix U) (only parsing).
  Notation vecH := (@vectorH _ P) (only parsing).

  Definition matrixH n m (unm: matU n m) := vectorH (vecH m) unm.

Note the signature SmatH and the pattern PmatH. The pattern is {{Smat _ # (_,_), _}} because the domain of SmatH is sig T (Smat _), which is the sigma type { nm : nat * nat & Smat _ nm }, so its elements are dependent pairs with signature Smat _ whose first components are pairs.

  Definition SmatH (p : sigT (Smat U)) := matrixH (projT2 p).
  Notation PmatH := ({{Smat _ # (_,_),_}}) (only parsing).

  Fixpoint hdcolH n m (unm: matU n (S m)) (M: matrixH unm) : vecH n (hdcol unm) :=
    match M in vectorH _ unm return vecH _ (hdcol unm) with
      | nilH => nilH
      | consH _ row _ _ M' => hdH row ::: hdcolH M'
    end.

  Fixpoint tlcolH n m (unm: matU n m) (M: matrixH unm) : matrixH (tlcol unm) :=
    match M with
      | nilH => nilH
      | consH _ row _ _ M' => tailH row ::: tlcolH M'
    end.

  Fixpoint conscolH n (un:vecU n) (col: vecH _ un) m (unm: matU n m) (M: matrixH unm) : matrixH (conscol un unm) :=
    match M in vectorH _ unm return forall un, vecH _ un -> matrixH (conscol un unm) with
      | nilH => fun _ _ => nilH
      | consH _ row _ _ M' => fun un col => (hdH col ::: row) ::: (conscolH (tailH col) M')
    end un col.

  Lemma conshdtlcolH: forall n m (unm: matU n (S m)) (M: matrixH unm),
    {{ SmatH,PmatH # M == conscolH (hdcolH M) (tlcolH M) }}.

    induction M; intros.
      auto.
      simpl. Hrewritec <- (hdtailH a). Hrewritec <- IHM. auto.
  Qed.

  Lemma hdconscolH: forall n (un: vecU n) (col: vecH _ un) m (unm: matU n m) (M: matrixH unm),
    {{ SvecH P,PvecH # hdcolH (conscolH col M) == col }}.

    induction M; intros.
      dependent destruction col. auto.
      simpl. Hrewritec (IHM _ (tailH col)). Hrewritec <- (hdtailH col). auto.
  Qed.

  Lemma tlconscolH: forall n (un: vecU n) (col: vecH _ un) m (unm: matU n m) (M: matrixH unm),
    {{ SmatH,PmatH # tlcolH (conscolH col M) == M }}.
    induction M; intros.
      dependent destruction col. auto.
      simpl. Hrewritec (IHM _ (tailH col)). auto.
  Qed.

  Definition appmatrowH n1 m (unm1: matU n1 m) (M1 : matrixH unm1) n2 (unm2: matU n2 m) (M2 : matrixH unm2) : matrixH (appmatrow unm1 unm2)
    := appH M1 M2.

  Fixpoint appmatcolH n m1 (unm1: matU n m1) (M1 : matrixH unm1) m2 (unm2: matU n m2) (M2 : matrixH unm2) : matrixH (appmatcol unm1 unm2) :=
    match m1 return forall unm1 : matU n m1, matrixH unm1 -> matrixH (appmatcol unm1 unm2) with
      | 0 => fun _ _ => M2
      | S m1' => fun unm1 M1 => conscolH (hdcolH M1) (appmatcolH (tlcolH M1) M2)
    end unm1 M1.

  Lemma appmatrow_assocH: forall n1 m (unm1: matU n1 m) (M1 : matrixH unm1) n2 (unm2: matU n2 m) (M2 : matrixH unm2) n3 (unm3: matU n3 m) (M3 : matrixH unm3),
    {{ SmatH,PmatH # appmatrowH M1 (appmatrowH M2 M3) == appmatrowH (appmatrowH M1 M2) M3 }}.
    intros. unfold appmatrowH, appmatrow. Hrewritec (app_assH M1 M2 M3). auto.
  Qed.

  Lemma appmatcol_assocH: forall n m1 (unm1: matU n m1) (M1 : matrixH unm1) m2 (unm2: matU n m2) (M2 : matrixH unm2) m3 (unm3: matU n m3) (M3 : matrixH unm3),
    {{ SmatH,PmatH # appmatcolH M1 (appmatcolH M2 M3) == appmatcolH (appmatcolH M1 M2) M3 }}.

  induction m1; intros.
    auto.
    Hrewritec (conshdtlcolH M1). Helimc. simpl.
    Hrewritec <- (conshdtlcolH M1).
    Hrewritec (hdconscolH (hdcolH M1) (appmatcolH (tlcolH M1) M2)).
    Hrewritec (tlconscolH (hdcolH M1) (appmatcolH (tlcolH M1) M2)).
    Hrewritec (IHm1 _ (tlcolH M1) _ _ M2 _ _ M3). auto.
  Qed.

End MatrixH.

Notation PmatH := ({{Smat _ # (_,_),_}}) (only parsing).