Library Combi.Combi.std: Standard Words, i.e. Permutation as Words
Standard words
- is_std s == s is a standard word
- is_std_of_n n s == s is a standard word of size n
- wordperm p == the standard word associated with a permutation p of 'S_n
- stdwordn n == a type for seq nat which standard words size n; it is canonically a finType
- std s == given a word w over an ordType returns the standard word with the same set of inversion (lemmas stdP and std_eq_invP)
- versions w i j == i j is an non-inversion of w that is
i <= j < size w and w_i <= w_j - eq_inv w1 w2 == w1 and w2 have the same versions which is equivalent
to the same set of inversions; in particular w1 and w2
have the same size.
- std_spec s p == p is a standard word with the same versions as s
- linvseq s t == t is the left inverse of s
- invseq s t == s and t are inverse on of each other
- invstd w == the inverse of the standardized of w that is the permutation which sorts w in a stable way.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm fingroup.
Require Import tools combclass ordtype permcomp.
Set Implicit Arguments.
Import Order.TTheory.
Open Scope nat_scope.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm fingroup.
Require Import tools combclass ordtype permcomp.
Set Implicit Arguments.
Import Order.TTheory.
Open Scope nat_scope.
Section StandardWords.
Implicit Type n : nat.
Definition is_std (s : seq nat) := perm_eq s (iota 0 (size s)).
Lemma perm_std u v : is_std u -> perm_eq v u -> is_std v.
Lemma std_perm u v : is_std u -> is_std v -> size u = size v -> perm_eq v u.
Lemma mem_std p i : is_std p -> (i \in p) = (i < size p).
Lemma std_uniq u : is_std u -> uniq u.
Lemma std_max s0 s : is_std (s0 :: s) -> maxL s0 s = size s.
Lemma is_stdP s : reflect (forall n, n < size s -> n \in s) (is_std s).
Definition wordperm n (p : 'S_n) := [seq (p i : nat) | i : 'I_n].
Open Scope group_scope.
Lemma wordperm_iota n (p : 'S_n) : (wordperm p) =i iota 0 n.
Lemma uniq_wordperm n (p : 'S_n) : uniq (wordperm p).
Lemma wordperm_std n (p : 'S_n) : is_std (wordperm p).
Lemma perm_of_std s : is_std s -> { p : 'S_(size s) | s = wordperm p }.
Lemma is_std_wordpermP s :
reflect (exists p : 'S_(size s), s = wordperm p) (is_std s).
Lemma wordperm_invP n (p : 'S_n) i (j : 'I_n) :
nth n (wordperm p) i = j <-> i = (p^-1) j.
End StandardWords.
Implicit Type n : nat.
Definition is_std (s : seq nat) := perm_eq s (iota 0 (size s)).
Lemma perm_std u v : is_std u -> perm_eq v u -> is_std v.
Lemma std_perm u v : is_std u -> is_std v -> size u = size v -> perm_eq v u.
Lemma mem_std p i : is_std p -> (i \in p) = (i < size p).
Lemma std_uniq u : is_std u -> uniq u.
Lemma std_max s0 s : is_std (s0 :: s) -> maxL s0 s = size s.
Lemma is_stdP s : reflect (forall n, n < size s -> n \in s) (is_std s).
Definition wordperm n (p : 'S_n) := [seq (p i : nat) | i : 'I_n].
Open Scope group_scope.
Lemma wordperm_iota n (p : 'S_n) : (wordperm p) =i iota 0 n.
Lemma uniq_wordperm n (p : 'S_n) : uniq (wordperm p).
Lemma wordperm_std n (p : 'S_n) : is_std (wordperm p).
Lemma perm_of_std s : is_std s -> { p : 'S_(size s) | s = wordperm p }.
Lemma is_std_wordpermP s :
reflect (exists p : 'S_(size s), s = wordperm p) (is_std s).
Lemma wordperm_invP n (p : 'S_n) i (j : 'I_n) :
nth n (wordperm p) i = j <-> i = (p^-1) j.
End StandardWords.
Section StdCombClass.
Variable n : nat.
Definition is_std_of_n := [pred w | (is_std w) && (size w == n) ].
Structure stdwordn : Set :=
StdWordN {stdwordnval :> seq nat; _ : is_std_of_n stdwordnval}.
Lemma stdwordnP (s : stdwordn) : is_std (val s).
Lemma size_sdtn (s : stdwordn) : size (val s) = n.
Definition enum_stdwordn := [seq wordperm p | p : 'S_n].
Lemma enum_stdwordnE : enum_stdwordn =i is_std_of_n.
Lemma wordperm_inj : injective (@wordperm n).
Lemma enum_stdwordn_uniq : uniq enum_stdwordn.
Lemma card_stdwordn : #|{:stdwordn}| = n`!.
End StdCombClass.
Variable n : nat.
Definition is_std_of_n := [pred w | (is_std w) && (size w == n) ].
Structure stdwordn : Set :=
StdWordN {stdwordnval :> seq nat; _ : is_std_of_n stdwordnval}.
Lemma stdwordnP (s : stdwordn) : is_std (val s).
Lemma size_sdtn (s : stdwordn) : size (val s) = n.
Definition enum_stdwordn := [seq wordperm p | p : 'S_n].
Lemma enum_stdwordnE : enum_stdwordn =i is_std_of_n.
Lemma wordperm_inj : injective (@wordperm n).
Lemma enum_stdwordn_uniq : uniq enum_stdwordn.
Lemma card_stdwordn : #|{:stdwordn}| = n`!.
End StdCombClass.
Section Standardisation.
Context {disp : unit} {Alph : orderType disp}.
Implicit Type s u v w : seq Alph.
Fixpoint std_rec n s :=
if n is n'.+1 then
let rec := std_rec n' (rembig s) in
let pos := posbig s in
take pos rec ++ n' :: drop pos rec
else [::].
Definition std s := std_rec (size s) s.
Lemma size_std_rec n s : size (std_rec n s) = n.
Lemma size_std s : size (std s) = size s.
Lemma std_is_std s : is_std (std s).
Lemma in_std_ltn_size s i : i \in std s = (i < size s).
Lemma allLtn_std_rec s : allLtn (std s) (size s).
Lemma rembig_ins_std s pos :
rembig (take pos (std s) ++ size s :: drop pos (std s)) = std s.
Lemma std_rembig s : std (rembig s) = rembig (std s).
Lemma std_posbig s : posbig (std s) = posbig s.
End Standardisation.
Lemma std_std s : is_std s -> std s = s.
Lemma std_stdE (disp : unit) (T : orderType disp)
(s : seq T) : std (std s) = std s.
Context {disp : unit} {Alph : orderType disp}.
Implicit Type s u v w : seq Alph.
Fixpoint std_rec n s :=
if n is n'.+1 then
let rec := std_rec n' (rembig s) in
let pos := posbig s in
take pos rec ++ n' :: drop pos rec
else [::].
Definition std s := std_rec (size s) s.
Lemma size_std_rec n s : size (std_rec n s) = n.
Lemma size_std s : size (std s) = size s.
Lemma std_is_std s : is_std (std s).
Lemma in_std_ltn_size s i : i \in std s = (i < size s).
Lemma allLtn_std_rec s : allLtn (std s) (size s).
Lemma rembig_ins_std s pos :
rembig (take pos (std s) ++ size s :: drop pos (std s)) = std s.
Lemma std_rembig s : std (rembig s) = rembig (std s).
Lemma std_posbig s : posbig (std s) = posbig s.
End Standardisation.
Lemma std_std s : is_std s -> std s = s.
Lemma std_stdE (disp : unit) (T : orderType disp)
(s : seq T) : std (std s) = std s.
Section EqInvDef.
Definition versions d (T : inhOrderType d) (w : seq T) : rel nat :=
fun i j => (i <= j < size w) && (nth inh w i <= nth inh w j)%O.
Definition eq_inv d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(w1 : seq T1) (w2 : seq T2) :=
(versions w1) =2 (versions w2).
Variables (disp1 disp2 disp3 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2)
(U : inhOrderType disp3).
Lemma eq_inv_refl (w : seq T) : eq_inv w w.
Lemma eq_inv_nil : eq_inv (@nil S) (@nil T).
Lemma eq_inv_sym (w1 : seq S) (w2 : seq T) :
eq_inv w1 w2 -> eq_inv w2 w1.
Lemma eq_inv_trans (w1 : seq S) (w2 : seq T) (w3 : seq U) :
eq_inv w1 w2 -> eq_inv w2 w3 -> eq_inv w1 w3.
End EqInvDef.
Lemma eq_inv_size d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(w1 : seq T1) (w2 : seq T2) :
eq_inv w1 w2 -> size w1 = size w2.
Section EqInvAltDef.
Variables (disp1 disp2 disp3 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2)
(U : inhOrderType disp3).
Lemma eq_invP (w1 : seq S) (w2 : seq T) :
(size w1 = size w2 /\
forall i j, i <= j < size w1 ->
((nth inh w1 i <= nth inh w1 j) =
(nth inh w2 i <= nth inh w2 j))%O)
<-> (eq_inv w1 w2).
Lemma eq_inv_inversionP (w1 : seq S) (w2 : seq T) :
(size w1 = size w2 /\
forall i j, i <= j < size w1 ->
(nth inh w1 i > nth inh w1 j) =
(nth inh w2 i > nth inh w2 j))%O
<-> (eq_inv w1 w2).
Lemma eq_inv_consK (a : S) u (b : T) v :
eq_inv (a :: u) (b :: v) -> eq_inv u v.
Lemma eq_inv_rconsK (a : S) u (b : T) v :
eq_inv (rcons u a) (rcons v b) -> eq_inv u v.
End EqInvAltDef.
Lemma eq_inv_allgt_imply
d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (a : S) u (b : T) v :
eq_inv (a :: u) (b :: v) -> (allLtn u a) -> (allLtn v b).
Lemma eq_inv_allgtnX
d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (a : S) u (b : T) v :
eq_inv (a :: u) (b :: v) -> (allLtn u a) = (allLtn v b).
Section EqInvPosRemBig.
Variables (disp1 disp2 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2).
Lemma eq_inv_posbig (u : seq S) (v : seq T) :
eq_inv u v -> posbig u = posbig v.
Lemma eq_inv_rembig (u : seq S) (v : seq T) :
eq_inv u v -> eq_inv (rembig u) (rembig v).
Lemma std_eq_inv (u : seq S) (v : seq T) :
eq_inv u v -> std u = std v.
Lemma eq_inv_std (u : seq T) : eq_inv u (std u).
End EqInvPosRemBig.
Section Spec.
Variables (disp1 disp2 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2).
Variant std_spec (s : seq T) (p : seq nat) : Prop :=
| StdSpec : is_std p -> eq_inv s p -> std_spec s p.
Lemma std_spec_uniq (u : seq T) p q :
std_spec u p -> std_spec u q -> p = q.
Lemma std_specP (s : seq T) : std_spec s (std s).
Lemma stdP (s : seq T) p :
reflect (std_spec s p) (std s == p).
Lemma std_eq_invP (u : seq S) (v : seq T) :
reflect (eq_inv u v) (std u == std v).
Lemma std_rconsK (u : seq S) (v : seq T) a b :
std (rcons u a) = std (rcons v b) -> std u = std v.
Lemma eq_inv_catl (u1 v1 : seq S) (u2 v2 : seq T) :
eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> eq_inv u1 u2.
Lemma eq_inv_catr (u1 v1 : seq S) (u2 v2 : seq T) :
eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> eq_inv v1 v2.
End Spec.
Section StdTakeDrop.
Variables (disp1 disp2 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2).
Implicit Type u v : seq T.
Lemma std_take_std u v : std (take (size u) (std (u ++ v))) = std u.
Lemma std_drop_std u v : std (drop (size u) (std (u ++ v))) = std v.
End StdTakeDrop.
Section PermEq.
Variable disp : unit.
Variable Alph : orderType disp.
Implicit Type u v : seq Alph.
Theorem perm_stdE u v : perm_eq u v -> std u = std v -> u = v.
End PermEq.
Definition versions d (T : inhOrderType d) (w : seq T) : rel nat :=
fun i j => (i <= j < size w) && (nth inh w i <= nth inh w j)%O.
Definition eq_inv d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(w1 : seq T1) (w2 : seq T2) :=
(versions w1) =2 (versions w2).
Variables (disp1 disp2 disp3 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2)
(U : inhOrderType disp3).
Lemma eq_inv_refl (w : seq T) : eq_inv w w.
Lemma eq_inv_nil : eq_inv (@nil S) (@nil T).
Lemma eq_inv_sym (w1 : seq S) (w2 : seq T) :
eq_inv w1 w2 -> eq_inv w2 w1.
Lemma eq_inv_trans (w1 : seq S) (w2 : seq T) (w3 : seq U) :
eq_inv w1 w2 -> eq_inv w2 w3 -> eq_inv w1 w3.
End EqInvDef.
Lemma eq_inv_size d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(w1 : seq T1) (w2 : seq T2) :
eq_inv w1 w2 -> size w1 = size w2.
Section EqInvAltDef.
Variables (disp1 disp2 disp3 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2)
(U : inhOrderType disp3).
Lemma eq_invP (w1 : seq S) (w2 : seq T) :
(size w1 = size w2 /\
forall i j, i <= j < size w1 ->
((nth inh w1 i <= nth inh w1 j) =
(nth inh w2 i <= nth inh w2 j))%O)
<-> (eq_inv w1 w2).
Lemma eq_inv_inversionP (w1 : seq S) (w2 : seq T) :
(size w1 = size w2 /\
forall i j, i <= j < size w1 ->
(nth inh w1 i > nth inh w1 j) =
(nth inh w2 i > nth inh w2 j))%O
<-> (eq_inv w1 w2).
Lemma eq_inv_consK (a : S) u (b : T) v :
eq_inv (a :: u) (b :: v) -> eq_inv u v.
Lemma eq_inv_rconsK (a : S) u (b : T) v :
eq_inv (rcons u a) (rcons v b) -> eq_inv u v.
End EqInvAltDef.
Lemma eq_inv_allgt_imply
d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (a : S) u (b : T) v :
eq_inv (a :: u) (b :: v) -> (allLtn u a) -> (allLtn v b).
Lemma eq_inv_allgtnX
d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (a : S) u (b : T) v :
eq_inv (a :: u) (b :: v) -> (allLtn u a) = (allLtn v b).
Section EqInvPosRemBig.
Variables (disp1 disp2 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2).
Lemma eq_inv_posbig (u : seq S) (v : seq T) :
eq_inv u v -> posbig u = posbig v.
Lemma eq_inv_rembig (u : seq S) (v : seq T) :
eq_inv u v -> eq_inv (rembig u) (rembig v).
Lemma std_eq_inv (u : seq S) (v : seq T) :
eq_inv u v -> std u = std v.
Lemma eq_inv_std (u : seq T) : eq_inv u (std u).
End EqInvPosRemBig.
Section Spec.
Variables (disp1 disp2 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2).
Variant std_spec (s : seq T) (p : seq nat) : Prop :=
| StdSpec : is_std p -> eq_inv s p -> std_spec s p.
Lemma std_spec_uniq (u : seq T) p q :
std_spec u p -> std_spec u q -> p = q.
Lemma std_specP (s : seq T) : std_spec s (std s).
Lemma stdP (s : seq T) p :
reflect (std_spec s p) (std s == p).
Lemma std_eq_invP (u : seq S) (v : seq T) :
reflect (eq_inv u v) (std u == std v).
Lemma std_rconsK (u : seq S) (v : seq T) a b :
std (rcons u a) = std (rcons v b) -> std u = std v.
Lemma eq_inv_catl (u1 v1 : seq S) (u2 v2 : seq T) :
eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> eq_inv u1 u2.
Lemma eq_inv_catr (u1 v1 : seq S) (u2 v2 : seq T) :
eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> eq_inv v1 v2.
End Spec.
Section StdTakeDrop.
Variables (disp1 disp2 : unit).
Variables (S : inhOrderType disp1)
(T : inhOrderType disp2).
Implicit Type u v : seq T.
Lemma std_take_std u v : std (take (size u) (std (u ++ v))) = std u.
Lemma std_drop_std u v : std (drop (size u) (std (u ++ v))) = std v.
End StdTakeDrop.
Section PermEq.
Variable disp : unit.
Variable Alph : orderType disp.
Implicit Type u v : seq Alph.
Theorem perm_stdE u v : perm_eq u v -> std u = std v -> u = v.
End PermEq.
Section Transp.
Variable disp : unit.
Variable Alph : inhOrderType disp.
Implicit Type u v : seq Alph.
Lemma nth_transp u v a b i :
i != size u -> i != (size u).+1 ->
nth inh (u ++ [:: a; b] ++ v) i = nth inh (u ++ [:: b; a] ++ v) i.
Lemma nth_sizeu u v a b :
nth inh (u ++ [:: a; b] ++ v) (size u) = a.
Lemma nth_sizeu1 u v a b :
nth inh (u ++ [:: a; b] ++ v) (size u).+1 = b.
Lemma nth_sizeu2 u v a b c :
nth inh (u ++ [:: a; b; c] ++ v) (size u).+2 = c.
End Transp.
Lemma eq_inv_transp d1 d2 (S : inhOrderType d1) (T : inhOrderType d2)
(u v : seq S) a b (U V : seq T) A B :
(a < b)%O -> (A < B)%O -> size u = size U ->
eq_inv (u ++ [:: a; b] ++ v) (U ++ [:: A; B] ++ V) ->
eq_inv (u ++ [:: b; a] ++ v) (U ++ [:: B; A] ++ V).
Lemma std_transp d (T : inhOrderType d)
(u v : seq T) a b
(U V : seq nat) A B :
(a < b)%O -> size u = size U ->
std (u ++ [:: a; b] ++ v) = (U ++ [:: A; B] ++ V) ->
std (u ++ [:: b; a] ++ v) = (U ++ [:: B; A] ++ V).
Lemma std_cutabc d (T : orderType d) (u v : seq T) a b c :
exists U V A B C, size u = size U /\
std (u ++ [:: a; b; c] ++ v) = (U ++ [:: A; B; C] ++ V).
Variable disp : unit.
Variable Alph : inhOrderType disp.
Implicit Type u v : seq Alph.
Lemma nth_transp u v a b i :
i != size u -> i != (size u).+1 ->
nth inh (u ++ [:: a; b] ++ v) i = nth inh (u ++ [:: b; a] ++ v) i.
Lemma nth_sizeu u v a b :
nth inh (u ++ [:: a; b] ++ v) (size u) = a.
Lemma nth_sizeu1 u v a b :
nth inh (u ++ [:: a; b] ++ v) (size u).+1 = b.
Lemma nth_sizeu2 u v a b c :
nth inh (u ++ [:: a; b; c] ++ v) (size u).+2 = c.
End Transp.
Lemma eq_inv_transp d1 d2 (S : inhOrderType d1) (T : inhOrderType d2)
(u v : seq S) a b (U V : seq T) A B :
(a < b)%O -> (A < B)%O -> size u = size U ->
eq_inv (u ++ [:: a; b] ++ v) (U ++ [:: A; B] ++ V) ->
eq_inv (u ++ [:: b; a] ++ v) (U ++ [:: B; A] ++ V).
Lemma std_transp d (T : inhOrderType d)
(u v : seq T) a b
(U V : seq nat) A B :
(a < b)%O -> size u = size U ->
std (u ++ [:: a; b] ++ v) = (U ++ [:: A; B] ++ V) ->
std (u ++ [:: b; a] ++ v) = (U ++ [:: B; A] ++ V).
Lemma std_cutabc d (T : orderType d) (u v : seq T) a b c :
exists U V A B C, size u = size U /\
std (u ++ [:: a; b; c] ++ v) = (U ++ [:: A; B; C] ++ V).
Lemma perm_size_uniq (T : eqType) (s1 s2 : seq T) :
uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> perm_eq s1 s2.
Section InvSeq.
Implicit Type n : nat.
Definition linvseq s :=
[fun t => all (fun i => nth (size s) t (nth (size t) s i) == i)
(iota 0 (size s))].
Definition invseq s t := linvseq s t && linvseq t s.
Lemma linvseqP s t :
reflect
(forall i, i < size s -> nth (size s) t (nth (size t) s i) = i)
(linvseq s t).
Lemma invseq_sym s t : invseq s t -> invseq t s.
Lemma size_all_leq n t : (forall i, i < n -> i \in t) -> n <= size t.
Lemma linvseq_ltn_szt s t :
linvseq s t -> forall i, i < size s -> nth (size t) s i < size t.
Lemma size_leq_invseq s t : linvseq s t -> size s <= size t.
Lemma size_invseq s t : invseq s t -> size s = size t.
Lemma linvseq_subset_iota s t : linvseq s t -> {subset iota 0 (size s) <= t}.
Lemma invseq_is_std s t : invseq s t -> is_std s.
Lemma linvseq_sizeP s t :
linvseq s t -> size s = size t -> invseq s t.
Lemma invseq_nthE s t :
invseq s t ->
forall i j, i < size s -> j < size t ->
(i = nth (size s) t j <-> nth (size t) s i = j).
uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> perm_eq s1 s2.
Section InvSeq.
Implicit Type n : nat.
Definition linvseq s :=
[fun t => all (fun i => nth (size s) t (nth (size t) s i) == i)
(iota 0 (size s))].
Definition invseq s t := linvseq s t && linvseq t s.
Lemma linvseqP s t :
reflect
(forall i, i < size s -> nth (size s) t (nth (size t) s i) = i)
(linvseq s t).
Lemma invseq_sym s t : invseq s t -> invseq t s.
Lemma size_all_leq n t : (forall i, i < n -> i \in t) -> n <= size t.
Lemma linvseq_ltn_szt s t :
linvseq s t -> forall i, i < size s -> nth (size t) s i < size t.
Lemma size_leq_invseq s t : linvseq s t -> size s <= size t.
Lemma size_invseq s t : invseq s t -> size s = size t.
Lemma linvseq_subset_iota s t : linvseq s t -> {subset iota 0 (size s) <= t}.
Lemma invseq_is_std s t : invseq s t -> is_std s.
Lemma linvseq_sizeP s t :
linvseq s t -> size s = size t -> invseq s t.
Lemma invseq_nthE s t :
invseq s t ->
forall i j, i < size s -> j < size t ->
(i = nth (size s) t j <-> nth (size t) s i = j).
Definition invstd s := mkseq (fun i => index i s) (size s).
Lemma invseq_invstd s : is_std s -> invseq s (invstd s).
Lemma size_invstd p : size (invstd p) = size p.
Lemma invstd_is_std p : is_std p -> is_std (invstd p).
Lemma invseqE s t1 t2 : invseq s t1 -> invseq s t2 -> t1 = t2.
Lemma invstdK s : is_std s -> invstd (invstd s) = s.
Lemma invstd_inj s t :
is_std s -> is_std t -> (invstd s) = (invstd t) -> s = t.
End InvSeq.
Section Examples.
Let u := [:: 4; 1; 2; 2; 5; 3].
Let v := [:: 0; 4; 3; 3].
Goal std u = [:: 4; 0; 1; 2; 5; 3].
Goal invstd (std u) = filter (gtn (size u)) (invstd (std (u ++ v))).
End Examples.