Skip to content

Instantly share code, notes, and snippets.

@pi8027
Created December 12, 2017 09:06
Show Gist options
  • Save pi8027/a9c85de3de6a01a7c13b12f2934ccbf7 to your computer and use it in GitHub Desktop.
Save pi8027/a9c85de3de6a01a7c13b12f2934ccbf7 to your computer and use it in GitHub Desktop.
Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Fixpoint vec (n : nat) (A : Type) : Type :=
if n is n'.+1 then A * vec n' A else unit.
Fixpoint vcat (n m : nat) (A : Type) : vec n A -> vec m A -> vec (n + m) A :=
if n is n'.+1
then fun '(l, ls) rs => (l, vcat ls rs)
else fun _ rs => rs.
Fixpoint vmap (n : nat) (A B : Type) (f : A -> B) : vec n A -> vec n B :=
if n is n'.+1
then fun '(x, xs) => (f x, vmap f xs)
else fun _ => tt.
Lemma v_map_cat
(n m : nat) (A B : Type) (f : A -> B) (xs : vec n A) (ys : vec m A) :
vmap f (vcat xs ys) = vcat (vmap f xs) (vmap f ys).
Proof. by elim: n xs ys => //= n IH [x xs] ys; rewrite -IH. Qed.
Lemma vcatA (n1 n2 n3 : nat) (A : Type)
(s1 : vec n1 A) (s2 : vec n2 A) (s3 : vec n3 A) :
vcat s1 (vcat s2 s3) =
ecast n (vec n A) (esym (addnA n1 n2 n3)) (vcat (vcat s1 s2) s3).
Proof.
elim: n1 s1 => //= [_ | n1 IH [h s1]].
- by rewrite (eq_irrelevance (esym _) (erefl _)).
- rewrite IH.
move: {IH s1 s2 s3} (vcat (vcat _ _) _) => s.
rewrite -!/(addn _ _).
Set Printing All.
Abort.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment