Library UniMath.Combinatorics.MoreLists

Additional definitions, lemmas and notations for lists.

Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021

Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Combinatorics.Vectors.
Require Export UniMath.Combinatorics.Lists.
Require Export UniMath.Combinatorics.DecSet.
Require Export UniMath.Combinatorics.Maybe.

Notations for lists.

Introduces a new scope, list_scope, delimited by list, which adds useful notations for lists. A list of elements x1, x2, ..., xn may be written a [x1; x2; ...; xn]. Moreover [] denotes the empty list, :: is the cons operator and ++ the list concatenation operator.

Declare Scope list_scope.

Delimit Scope list_scope with list.

Bind Scope list_scope with list.

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..): list_scope.

Notation "[]" := nil (at level 0, format "[]"): list_scope.

Infix "::" := cons: list_scope.

Infix "++" := concatenate: list_scope.

Local Open Scope list_scope.

Proofs that cons is injective on both arguments.

Introduces the head and tail operations on lists, using the maybe monad defined in UniMath.Algebra.Universal.Maybe for dealing with invalid function applications. Then, proves that cons is injective on both arguments and that there are no paths between cons and nil.

Definition head {A: UU}: list A → maybe A.
Proof.
  apply list_ind.
  - exact nothing.
  - exact (λ x xs IH, ii1 x).
Defined.

Definition tail {A: UU}: list A → maybe (list A).
Proof.
  apply list_ind.
  - exact nothing.
  - exact (λ x xs IH, ii1 xs).
Defined.

Lemma list_head_cons {A: UU} (x: A) (xs: list A)
  : head (x :: xs) = ii1 x.
Proof.
  apply idpath.
Defined.

Lemma list_tail_cons {A: UU} (x: A) (xs: list A)
  : tail (x :: xs) = ii1 xs.
Proof.
  apply idpath.
Defined.

Theorem cons_inj1 {A: UU} (a1 a2: A) (r1 r2: list A)
  : a1 :: r1 = a2 :: r2 → a1 = a2.
Proof.
  intro H.
  apply (maponpaths head) in H.
  change (just a1 = just a2) in H.
  apply ii1_injectivity in H.
  assumption.
Defined.

Theorem cons_inj2 {A: UU} (a1 a2: A) (r1 r2: list A)
  : a1 :: r1 = a2 :: r2 → r1 = r2.
Proof.
  intro H.
  apply (maponpaths tail) in H.
  change (just r1 = just r2) in H.
  apply ii1_injectivity in H.
  assumption.
Defined.

Lemma negpathsconsnil {A: UU} (a: A) (l: list A): a :: l != [].
Proof.
  intro X.
  apply (maponpaths pr1) in X.
  cbv in X.
  apply negpathssx0 in X.
  assumption.
Defined.

Lemma negpathsnilcons {A: UU} (a: A) (l: list A): [] != a :: l.
Proof.
  intro X.
  apply pathsinv0 in X.
  apply negpathsconsnil in X.
  assumption.
Defined.

Several properties for the length of a list.


Lemma length_cons {A: UU} (x: A) (xs: list A)
  : length (x :: xs) = S (length xs).
Proof.
  apply idpath.
Defined.

Lemma length_zero_back {A: UU} (l: list A): length l = 0 → l = [].
Proof.
  revert l.
  refine (list_ind _ _ _).
  - reflexivity.
  - intros x xs _ HP.
    apply negpathssx0 in HP.
    contradiction.
Defined.

Lemma length_one_back {A: UU} (l: list A) (l1: length l = 1): ∑ x: A, l = [x].
Proof.
  induction l.
  cbn in l1.
  induction (! l1).
  induction pr2 as [x xs].
  ∃ x.
  induction xs.
  apply idpath.
Defined.

Lemma length_concatenate {A: UU} (l1: list A) (l2: list A)
  : length (l1 ++ l2) = length l1 + length l2.
Proof.
  revert l1.
  apply list_ind.
  - apply idpath.
  - intros x xs IH.
    change (S (length (xs ++ l2)) = S (length xs + length l2)).
    apply maponpaths.
    apply IH.
Defined.

Lemma length_sublist1 {A: UU} (l1: list A) (l2: list A)
  : length l1 ≤ length (l1 ++ l2).
Proof.
  rewrite length_concatenate.
  apply natlehnplusnm.
Defined.

Lemma length_sublist2 {A: UU} (l1: list A) (l2: list A)
  : length l2 ≤ length (l1 ++ l2).
Proof.
  rewrite length_concatenate.
  rewrite natpluscomm.
  apply natlehnplusnm.
Defined.

Lemma length_map {A B: UU} (l: list A) (f: A → B): length (map f l) = length l.
Proof.
  revert l.
  apply list_ind.
  - apply idpath.
  - intros x xs HPind.
    change (map f (x :: xs)) with (f x :: map f xs).
    change (S (length (map f xs)) = S(length xs)).
    apply maponpaths.
    exact HPind.
Defined.

Miscellanea of properties and definitions.


Definition listset (A: hSet): hSet := make_hSet (list A) (isofhlevellist 0 (setproperty A)).

Definition fill {A: UU} (a: A): nat → list A := λ n, n ,, vec_fill a n.

Lemma map_const {A B: UU} (b: B) (l: list A): map (λ _, b) l = fill b (length l).
Proof.
  revert l.
  apply list_ind.
  - apply idpath.
  - intros x xs HPind.
    change (b :: map (λ _: A, b) xs = b :: fill b (length xs)).
    apply maponpaths.
    exact HPind.
Defined.

Lemma length_fill {A: UU} (a: A) (n: nat): length (fill a n) = n.
Proof.
  apply idpath.
Defined.

The drop operation and related properties.

If l is a list and n a natural number, drop l n returns the list obtained from l after removing the first n elements. If n > length l, then drop l n = [].

Definition drop {A: UU} (l: list A) (n: nat): list A.
Proof.
  revert l.
  induction n.
  - exact (idfun _).
  - apply list_ind.
    + exact [].
    + intros x xs _.
      exact (IHn xs).
Defined.

Lemma drop_nil {A: UU} {n: nat}: @drop A [] n = [].
Proof.
  induction n ; apply idpath.
Defined.

Lemma drop_zero {A: UU} (l: list A): drop l 0 = l.
Proof.
  revert l.
  apply list_ind; trivial.
Defined.

Lemma drop_step {A: UU} (x: A) (xs: list A) (n: nat)
  : drop (x :: xs) (S n) = drop xs n.
Proof.
  apply idpath.
Defined.

Lemma drop_full {A: UU} (l: list A): drop l (length l) = [].
Proof.
  revert l; apply list_ind ; trivial.
Defined.

Lemma drop_concatenate {A: UU} (l1 l2: list A) (n: nat) (nok: n ≤ length l1): drop (l1 ++ l2) n = (drop l1 n) ++ l2.
Proof.
  revert l1 nok.
  induction n.
  - reflexivity.
  - refine (list_ind _ _ _).
    + intros.
      contradiction (negnatlehsn0 _ nok).
    + intros x xs _ sok.
      rewrite concatenateStep.
      do 2rewrite drop_step.
      apply (IHn xs sok).
Defined.

Lemma length_drop {A: UU} (l: list A) (n: nat): length (drop l n) = length l - n.
Proof.
  revert l n.
  refine (list_ind _ _ _).
  - intro n.
    rewrite drop_nil.
    induction n.
    + apply idpath.
    + change (0 = 0 - (1+ n)).
      rewrite <- natminusminus.
      assumption.
  - intros x xs IH.
    induction n.
    + apply idpath.
    + rewrite drop_step.
      rewrite length_cons.
      apply (IH n).
Defined.

The prefix_remove operation and related properties.

If l2 is a prefix of l1, then prefix_remove l1 l2 returns just l where l is the only list such that l2 ++ l = l1. Otherwise prefix_remove l1 l2 returns nothing. It is required for l1 and l2 to be of type list A with A: decSet.

Definition prefix_remove {A: decSet} (l1 l2: list A): maybe (list A).
Proof.
  revert l1 l2.
  refine (list_ind _ _ _).
  - exact (λ l, just l).
  - intros x xs HP.
    refine (list_ind _ _ _).
    + exact nothing.
    + intros y ys _.
      induction (decproperty A x y).
      × exact (HP ys).
      × exact nothing.
Defined.

Lemma prefix_remove_stepeq {A: decSet} (x: A) (xs1 xs2: list A)
  : prefix_remove (x :: xs1) (x :: xs2) = prefix_remove xs1 xs2.
Proof.
  unfold prefix_remove.
  cbn.
  induction (decproperty A x x).
  - cbn.
    apply idpath.
  - contradiction (b (idpath x)).
Defined.

Lemma prefix_remove_stepneq {A: decSet} {x1 x2: A} (p: x1 != x2) (xs1 xs2: list A)
  : prefix_remove (x1 :: xs1) (x2 :: xs2) = nothing.
Proof.
  unfold prefix_remove.
  cbn.
  induction (decproperty A x1 x2).
  - contradicts a p.
  - apply idpath.
Defined.

Lemma prefix_remove_stepback {A: decSet} (x1 x2: A) (xs1 xs2: list A)
  : prefix_remove (x1 :: xs1) (x2 :: xs2) != nothing → x1 = x2.
Proof.
  induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2] ; intro HP.
  - assumption.
  - rewrite (prefix_remove_stepneq x1neqx2) in HP.
    apply fromempty.
    apply (HP (idpath _)).
Defined.

Definition prefix_remove_back {A: decSet} (l1 l2 l3: list A):
  prefix_remove l1 l2 = just l3 → l2 = l1 ++ l3.
Proof.
  revert l1 l2.
  refine (list_ind _ _ _).
  - intros l2 prefixnil.
    cbn in prefixnil.
    apply just_injectivity in prefixnil.
    cbn.
    assumption.
  - intros x1 xs1 HPind.
    refine (list_ind _ _ _).
    + intro prefixxs.
      cbn in prefixxs.
      apply negpathsii2ii1 in prefixxs.
      contradiction.
    + intros x2 xs2 HP2ind HP.
      induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2].
      × rewrite x1eqx2 in ×.
        rewrite prefix_remove_stepeq in HP.
        rewrite concatenateStep.
        rewrite (HPind xs2 HP).
        apply idpath.
      × rewrite (prefix_remove_stepneq x1neqx2) in HP.
        contradiction (negpathsii2ii1 _ _ HP).
Defined.

Lemma prefix_remove_self {A: decSet} (l: list A): prefix_remove l l = just [].
Proof.
  revert l.
  apply list_ind.
  - apply idpath.
  - intros x xs IH.
    rewrite prefix_remove_stepeq.
    apply IH.
Defined.

Definition isprefix {A: decSet} (l1 l2: list A): UU := prefix_remove l1 l2 != nothing.

Lemma isprefix_self {A: decSet} (l: list A): isprefix l l.
Proof.
  unfold isprefix.
  rewrite prefix_remove_self.
  apply negpathsii1ii2.
Defined.

Lemma prefix_remove_concatenate {A: decSet} (l1 l2 l3: list A) (tl: list A)
  : prefix_remove l1 l2 = ii1 tl → prefix_remove l1 (l2 ++ l3) = ii1 (tl ++ l3).
Proof.
  revert l1 l2.
  refine (list_ind _ _ _).
  - intros l2 prooftl.
    apply ii1_injectivity in prooftl.
    rewrite prooftl.
    apply idpath.
  - intros x xs HPind.
    refine (list_ind _ _ _).
    + intro HP.
      cbv in HP.
      apply negpathsii2ii1 in HP.
      contradiction.
    + intros x2 x2s HP2.
      rewrite concatenateStep.
      induction (decproperty A x x2) as [xeqx2 | xneqx2].
      × rewrite xeqx2.
        do 2 rewrite prefix_remove_stepeq.
        apply (HPind x2s).
      × rewrite (prefix_remove_stepneq xneqx2).
        intro HP.
        apply negpathsii2ii1 in HP.
        contradiction.
Defined.

Lemma prefix_remove_concatenate2 {A: decSet} (l1 l2 l3: list A)
  : length l1 ≤ length l2 → prefix_remove l1 l2 = nothing → prefix_remove l1 (l2 ++ l3) = nothing.
Proof.
  revert l1 l2.
  refine (list_ind _ _ _).
  - intros l2 Hlen Hpref.
    contradiction (negpathsii1ii2 _ _ Hpref).
  - intros x1 xs1 IH.
    refine (list_ind _ _ _).
    + intros Hlen Hpref.
      contradiction (negnatlehsn0 _ Hlen).
    + intros x2 xs2 _ Hlen Hpref.
      rewrite concatenateStep.
      induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2].
      × induction x1eqx2.
        rewrite prefix_remove_stepeq.
        rewrite prefix_remove_stepeq in Hpref.
        apply (IH xs2 Hlen Hpref).
      × apply (prefix_remove_stepneq x1neqx2).
Defined.

Lemma prefix_remove_prefix {A: decSet} (l1 l2: list A): prefix_remove l1 (l1 ++ l2) = just l2.
Proof.
  revert l1.
  refine (list_ind _ _ _).
  - reflexivity.
  - intros x xs IHl1.
    rewrite concatenateStep.
    rewrite prefix_remove_stepeq.
    assumption.
Defined.

Lemma prefix_remove_drop {A: decSet} (l1 l2: list A)
  : prefix_remove l1 l2 != nothing → prefix_remove l1 l2 = just (drop l2 (length l1)).
Proof.
  revert l1 l2.
  refine (list_ind _ _ _).
  - reflexivity.
  - intros x1 xs1 IH.
    refine (list_ind _ _ _).
    + contradiction.
    + intros x2 xs2 _ prefixok.
      induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2].
      × induction x1eqx2.
        rewrite prefix_remove_stepeq.
        rewrite prefix_remove_stepeq in prefixok.
        apply (IH xs2 prefixok).
      × rewrite (prefix_remove_stepneq x1neqx2) in prefixok.
        contradiction prefixok.
        apply idpath.
Defined.