leftpad.v

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.

Section Padding.

Variable T : Type.

Implicit Types (c def : T) (i n : nat) (s : seq T).

Definition left_pad c n s := nseq (n - size s) c ++ s.

Lemma left_pad1 c n s : size (left_pad c n s) = maxn n (size s).
Proof.
by rewrite /left_pad size_cat size_nseq maxnC maxnE [RHS]addnC.
Qed.

Lemma left_pad2 c n s i def :
  i < n - size s ->
  nth def (left_pad c n s) i = c.
Proof.
move=> bound.
by rewrite /left_pad nth_cat size_nseq bound nth_nseq bound.
Qed.

Lemma left_pad3 c n s i def :
  nth def (left_pad c n s) (n - size s + i) = nth def s i.
Proof.
by rewrite /left_pad nth_cat size_nseq ltnNge leq_addr /= addKn.
Qed.

End Padding.