Library rt.util.bigcat

(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.10.1 (October 2019)

----------------------------------------------------------------------------- *)

Require Export rt.util.tactics rt.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Lemmas about the big concatenation operator. *)
Section BigCatLemmas.

  Lemma mem_bigcat_nat:
    ∀ (T: eqType) x m n j (f: _ → list T),
      m ≤ j < n →
      x \in (f j) →
      x \in \cat_(m ≤ i < n) (f i).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 38)
  
  ============================
  forall (T : eqType) (x : T) (m n j : nat) (f : nat -> seq T),
  m <= j < n -> x \in f j -> x \in \big[cat/[::]]_(m <= i < n) f i

----------------------------------------------------------------------------- *)

  Proof.
    intros T x m n j f LE IN; move: LE ⇒ /andP [LE LE0].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 88)
  
  T : eqType
  x : T
  m, n, j : nat
  f : nat -> seq T
  IN : x \in f j
  LE : m <= j
  LE0 : j < n
  ============================
  x \in \big[cat/[::]]_(m <= i < n) f i

----------------------------------------------------------------------------- *)

    rewrite → big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 93)
  
  T : eqType
  x : T
  m, n, j : nat
  f : nat -> seq T
  IN : x \in f j
  LE : m <= j
  LE0 : j < n
  ============================
  x \in \big[cat/[::]]_(m <= i < j) f i ++ \big[cat/[::]]_(j <= i < n) f i

----------------------------------------------------------------------------- *)

    rewrite mem_cat; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  T : eqType
  x : T
  m, n, j : nat
  f : nat -> seq T
  IN : x \in f j
  LE : m <= j
  LE0 : j < n
  ============================
  x \in \big[cat/[::]]_(j <= i < n) f i

----------------------------------------------------------------------------- *)

    destruct n; first by rewrite ltn0 in LE0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 144)
  
  T : eqType
  x : T
  m, n, j : nat
  f : nat -> seq T
  IN : x \in f j
  LE : m <= j
  LE0 : j < n.+1
  ============================
  x \in \big[cat/[::]]_(j <= i < n.+1) f i

----------------------------------------------------------------------------- *)

    rewrite big_nat_recl; last by ins.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 193)
  
  T : eqType
  x : T
  m, n, j : nat
  f : nat -> seq T
  IN : x \in f j
  LE : m <= j
  LE0 : j < n.+1
  ============================
  x \in f j ++ \big[cat/[::]]_(j <= i < n) f i.+1

----------------------------------------------------------------------------- *)

    by rewrite mem_cat; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma mem_bigcat_nat_exists :
    ∀ (T: eqType) x m n (f: nat → list T),
      x \in \cat_(m ≤ i < n) (f i) →
      ∃ i, x \in (f i) ∧
                m ≤ i < n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 59)
  
  ============================
  forall (T : eqType) (x : T) (m n : nat) (f : nat -> seq T),
  x \in \big[cat/[::]]_(m <= i < n) f i ->
  exists i : nat, x \in f i /\ m <= i < n

----------------------------------------------------------------------------- *)

  Proof.
    intros T x m n f IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 65)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IN : x \in \big[cat/[::]]_(m <= i < n) f i
  ============================
  exists i : nat, x \in f i /\ m <= i < n

----------------------------------------------------------------------------- *)

    induction n; first by rewrite big_geq // in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 79)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  ============================
  exists i : nat, x \in f i /\ m <= i < n.+1

----------------------------------------------------------------------------- *)

    destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 146)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

----------------------------------------------------------------------------- *)

    rewrite big_nat_recr // /= mem_cat in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 261)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  IN : (x \in \big[cat/[::]]_(m <= i < n) f i) || (x \in f n)
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

----------------------------------------------------------------------------- *)

    move: IN ⇒ /orP [HEAD | TAIL].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 306)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

subgoal 2 (ID 307) is:
 exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

----------------------------------------------------------------------------- *)

    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 306)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

----------------------------------------------------------------------------- *)

      apply IHn in HEAD; destruct HEAD; ∃ x0.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 316)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  x0 : nat
  H : x \in f x0 /\ m <= x0 < n
  ============================
  x \in f x0 /\ m <= x0 < n.+1

----------------------------------------------------------------------------- *)

 move: H ⇒ [H /andP [H0 H1]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 368)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  x0 : nat
  H : x \in f x0
  H0 : m <= x0
  H1 : x0 < n
  ============================
  x \in f x0 /\ m <= x0 < n.+1

----------------------------------------------------------------------------- *)

      split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 371)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  x0 : nat
  H : x \in f x0
  H0 : m <= x0
  H1 : x0 < n
  ============================
  m <= x0 < n.+1

----------------------------------------------------------------------------- *)

      by apply/andP; split; [by done | by apply ltnW].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 307)

subgoal 1 (ID 307) is:
 exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 307)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  TAIL : x \in f n
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

----------------------------------------------------------------------------- *)

    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 307)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  TAIL : x \in f n
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

----------------------------------------------------------------------------- *)

      ∃ n; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 404)
  
  T : eqType
  x : T
  m, n : nat
  f : nat -> seq T
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  TAIL : x \in f n
  ============================
  m <= n < n.+1

----------------------------------------------------------------------------- *)

      apply/andP; split; [by done | by apply ltnSn].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma bigcat_nat_uniq :
    ∀ (T: eqType) n1 n2 (F: nat → list T),
      (∀ i, uniq (F i)) →
      (∀ x i1 i2,
         x \in (F i1) → x \in (F i2) → i1 = i2) →
      uniq (\cat_(n1 ≤ i < n2) (F i)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 85)
  
  ============================
  forall (T : eqType) (n1 n2 : nat) (F : nat -> seq T),
  (forall i : nat, uniq (F i)) ->
  (forall (x : T) (i1 i2 : nat), x \in F i1 -> x \in F i2 -> i1 = i2) ->
  uniq (\big[cat/[::]]_(n1 <= i < n2) F i)

----------------------------------------------------------------------------- *)

  Proof.
    intros T n1 n2 f SINGLE UNIQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 91)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n2) f i)

----------------------------------------------------------------------------- *)

    case (leqP n1 n2) ⇒ [LE | GT]; last by rewrite big_geq // ltnW.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 94)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n2) f i)

----------------------------------------------------------------------------- *)

    rewrite -[n2](addKn n1).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 140)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + n2 - n1) f i)

----------------------------------------------------------------------------- *)

    rewrite -addnBA //; set delta := n2 - n1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 171)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta := n2 - n1 : nat
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)

----------------------------------------------------------------------------- *)

    induction delta; first by rewrite addn0 big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 180)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + delta.+1) f i)

----------------------------------------------------------------------------- *)

    rewrite addnS big_nat_recr /=; last by apply leq_addr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 212)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i ++ f (n1 + delta))

----------------------------------------------------------------------------- *)

    rewrite cat_uniq; apply/andP; split; first by apply IHdelta.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 245)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  ~~
  has
    (pred_of_simpl (T:=T) (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)))
    (f (n1 + delta)) && uniq (f (n1 + delta))

----------------------------------------------------------------------------- *)

    apply /andP; split; last by apply SINGLE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 271)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  ~~
  has
    (pred_of_simpl (T:=T) (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)))
    (f (n1 + delta))

----------------------------------------------------------------------------- *)

    rewrite -all_predC; apply/allP; intros x INx.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 308)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  ============================
  predC
    (pred_of_simpl (T:=T) (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)))
    x

----------------------------------------------------------------------------- *)

    simpl; apply/negP; unfold not; intro BUG.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 333)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  BUG : x \in \big[cat/[::]]_(n1 <= i < n1 + delta) f i
  ============================
  False

----------------------------------------------------------------------------- *)

    apply mem_bigcat_nat_exists in BUG.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 334)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  BUG : exists i : nat, x \in f i /\ n1 <= i < n1 + delta
  ============================
  False

----------------------------------------------------------------------------- *)

    move: BUG ⇒ [i [IN /andP [_ LTi]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 397)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  i : nat
  IN : x \in f i
  LTi : i < n1 + delta
  ============================
  False

----------------------------------------------------------------------------- *)

    apply UNIQ with (i1 := i) in INx; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 398)
  
  T : eqType
  n1, n2 : nat
  f : nat -> seq T
  SINGLE : forall i : nat, uniq (f i)
  UNIQ : forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  i : nat
  INx : i = n1 + delta
  IN : x \in f i
  LTi : i < n1 + delta
  ============================
  False

----------------------------------------------------------------------------- *)

    by rewrite INx ltnn in LTi.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End BigCatLemmas.