Set Implicit Arguments.

Section uniq_seq.

Structure uniq_seq {A : eqType} := {useq :> seq A ; buniq : uniq useq}.

Lemma andP_to_uniq {A : eqType} {t : A} {b : uniq_seq} (H : t \notin (useq b) ∧ uniq b) : uniq (t::b).

Canonical uniq_seq_subType {A : eqType} := Eval hnf in [subType for @useq A].

Canonical uniq_seq_eqType {A : eqType} := Eval hnf in EqType _ [eqMixin of (@uniq_seq A) by <:].
Canonical uniq_seq_choiceType {A : choiceType} := Eval hnf in ChoiceType _ [choiceMixin of (@uniq_seq A) by <:].
Canonical uniq_seq_countType {A : countType} := Eval hnf in CountType _ [countMixin of (@uniq_seq A) by <:].
Canonical uniq_seq_subCountType {A : countType} := Eval hnf in [subCountType of (@uniq_seq A)].

Lemma notinnil {A : eqType} (x : A) : x \notin [::].

Definition unil {A : eqType} : @uniq_seq A := {| useq := [::]; buniq := is_true_true |}.
Definition ucons1 {A : eqType} (t : A) :=
  {| useq := [:: t]; buniq := notinnil t |}.
Definition ucons {A : eqType} (t : A) (b : uniq_seq) (H : t \notin (useq b)) : uniq_seq :=
{| useq := t :: b; buniq := (andP_to_uniq (conj H (buniq b))) |}.
Definition pucons {A : eqType} (t : A) (b : @uniq_seq A) : @uniq_seq A :=
 match Sumbool.sumbool_of_bool (t \notin (useq b)) with
    | left H ⇒ ucons H
    | in_right ⇒ b
  end.

Lemma uniq_behead {A : eqType} (s : seq A) : uniq s → uniq (behead s).

Definition useq_behead {A : eqType} (us : @uniq_seq A) : @uniq_seq A :=
  match us with
    | {| useq := s; buniq := Hus |} ⇒ {| useq := behead s; buniq := uniq_behead Hus |}
end.

Definition useq_hd {A : eqType} (us : @uniq_seq A) : option A :=
  match us with
    | {| useq := [::] |} ⇒ None
    | {| useq := hd :: tl |} ⇒ Some hd end.

Lemma size_useq {A : finType} (d : @uniq_seq A) : size d < #|A|.+1.

Definition tag_of_uniq_seq {A : finType} (d : @uniq_seq A) : {k : 'I_#|A|.+1 & k.-tuple A} :=
  @Tagged _ (Sub (size d) (size_useq d))
            (fun k : 'I_#|A|.+1 ⇒ k.-tuple A)
            (in_tuple d).

Definition uniq_seq_of_tag {A : finType} (t : {k : 'I_#|A|.+1 & k.-tuple A}) : option (@uniq_seq_countType A) :=
  insub (val (tagged t)).

Lemma tag_of_dbranchK {A : finType} : pcancel (@tag_of_uniq_seq A) uniq_seq_of_tag.

Definition uniq_seq_finMixin {A : finType} := PcanFinMixin (@tag_of_dbranchK A).
Canonical uniq_seq_finType {A : finType} := Eval hnf in FinType (@uniq_seq A) uniq_seq_finMixin.

End uniq_seq.

Section Wlist.

Inductive Wlist (X: Type): nat → Type :=
  Bnil : ∀ n, (Wlist X n)
| Bcons : ∀ n, X → (Wlist X n) → (Wlist X n.+1).

Section Cancel.

Variable A: Type.

Definition g (_: unit) := (Bnil A 0).

Definition f (x: Wlist A 0) := tt.

Lemma nil_list0 : ∀ n (x: Wlist A n), (n = 0) → (eq x (Bnil A n)).

Lemma nil0 : ∀ (x: Wlist A 0), (eq x (Bnil A 0)).

Lemma cancelfg : cancel f g.

Definition gg (n: nat) (x: unit + A × Wlist A n) : (Wlist A n.+1) :=
match x with
| inl _ ⇒ Bnil A n.+1
| inr (H1, H2) ⇒ Bcons H1 H2
end.

Equations ff (n : nat) (x : Wlist A n.+1) : (unit + A × Wlist A n) :=
  ff (Bnil _) := inl tt ;
  ff (Bcons a l) := inr (a,l).

Lemma cancelffgg: ∀ n, cancel (@ff n) (@gg n).

End Cancel.

Section WlistEqType.
Variable A: eqType.

Definition wlist0_eqMixin := CanEqMixin (@cancelfg A).
Definition wlist0_eqType := EqType (Wlist A 0) wlist0_eqMixin.

Fixpoint wlistn_eqMixin n : Equality.mixin_of (Wlist A n).
Defined.

Definition wlistn_eqType n := Eval hnf in EqType (Wlist A n) (wlistn_eqMixin n).
End WlistEqType.

Section WlistSubType.

Fixpoint wlist_to_seq {X : Type} {m : nat} (s : Wlist X m) : seq X := match s with
  | Bnil _ ⇒ [::]
  | Bcons _ a b ⇒ a :: (wlist_to_seq b) end.

Fixpoint seq_to_wlist {X : Type} (m : nat) (s : seq X) := match m with
  0 ⇒ Bnil X 0
  | m'.+1 ⇒ match s with
              [::] ⇒ Bnil X m'.+1
              | a :: l ⇒ Bcons a (seq_to_wlist m' l) end end.

Lemma seq_to_bnil {X : Type} (m : nat) : @seq_to_wlist X m [::] = Bnil X m.

Lemma wlist_seqK {X : Type} {m : nat} (l : Wlist X m) : (seq_to_wlist m (wlist_to_seq l)) = l.

Lemma seq_wlistK {X : Type} {m : nat} (l : seq X) (H : size l ≤ m) : (wlist_to_seq (seq_to_wlist m l)) = l.

Definition seq_to_wlist_uncut {X : Type} {m : nat} (s : seq X) (H : size s ≤ m) : Wlist X m :=
  seq_to_wlist m s.

Lemma wlist_to_seq_size {X : Type} {m : nat} (s : Wlist X m) : size (wlist_to_seq s) ≤ m.

Lemma wlist_elim {A : Type} {m : nat} : ∀ K : Wlist A m → Type,
 (∀ (s : seq A) (Ps : size s ≤ m), K (seq_to_wlist_uncut Ps)) → ∀ u : Wlist A m, K u.

Lemma wlist_ind {A : Type} {m : nat} : ∀ K : Wlist A m → Prop,
 (∀ (s : seq A) (Ps : size s ≤ m), K (seq_to_wlist_uncut Ps)) → ∀ u : Wlist A m, K u.

Lemma seq_wlist_uncut_K {A : Type} {m : nat} (s : seq A) (Ps : size s ≤ m) :
  wlist_to_seq (seq_to_wlist_uncut Ps) = s.

Definition wlist_subType {A : Type} {w : nat} :=
  Eval hnf in (SubType (@Wlist A w) (@wlist_to_seq A w) seq_to_wlist_uncut wlist_elim seq_wlist_uncut_K).

Coercion wlist_to_seq_co {A : Type} {m : nat} x := @wlist_to_seq A m x.

End WlistSubType.

Section WlistChoiceType.
Variable A: choiceType.
Definition wlist0_choiceMixin := CanChoiceMixin (@cancelfg A).
Definition wlist0_choiceType := ChoiceType (wlist0_eqType A) wlist0_choiceMixin.

Fixpoint wlistn_choiceMixin (n:nat) : Choice.mixin_of (Wlist A n).

Defined.

Definition wlistn_choiceType n := Eval hnf in (@ChoiceType (wlistn_eqType A n) (wlistn_choiceMixin n)).
End WlistChoiceType.

Section WlistCountType.

Variable A: countType.
Definition wlist0_countMixin := CanCountMixin (@cancelfg A).
Definition wlist0_countType := CountType (wlist0_choiceType A) wlist0_countMixin.

Fixpoint wlistn_countMixin (n:nat): Countable.mixin_of (Wlist A n).

Defined.

Definition wlistn_countType n := Eval hnf in (@CountType (wlistn_choiceType A n) (wlistn_countMixin n)).

Lemma cteq: wlistn_countType 0 = wlist0_countType.

End WlistCountType.

Section WlistFinType.

Variable A: finType.

Definition wlist0_finMixin := @CanFinMixin (wlist0_countType A) unit_finType (@f A) (@g A) (@cancelfg A).
Definition wlist0_finType := FinType (wlist0_countType A) wlist0_finMixin.

Fixpoint wlistn_finMixin (n:nat): Finite.mixin_of (wlistn_countType A n).
Defined.

Definition wlistn_finType n := Eval hnf in (@FinType (wlistn_choiceType A n) (wlistn_finMixin n)).
End WlistFinType.

Section WlistUtils.

Fixpoint wsize {X : Type} {m : nat} (t : Wlist X m) : nat := match t with
  | Bnil _ ⇒ 0
  | Bcons _ a b ⇒ (wsize b).+1 end.

Fixpoint wmap {X Y : Type} {m : nat} (f : X → Y) (t : Wlist X m) : Wlist Y m := match t with
  | Bnil a ⇒ Bnil Y a
  | Bcons n a b ⇒ Bcons (f a) (@wmap X Y _ f b) end.

Lemma size_wmap {X Y : Type} {m : nat} : ∀ (f : X → Y) (s : Wlist X m),
  wsize (wmap f s) = wsize s.

Lemma wmapcoK {X Y : Type} {m : nat} (f : X → Y) (t : Wlist X m) : wlist_to_seq_co (wmap f t) = map f (wlist_to_seq_co t).

Lemma wmapK {X Y : Type} {m : nat} (f : X → Y) (t : Wlist X m) : wlist_to_seq (wmap f t) = map f (wlist_to_seq t).

Fixpoint w_subtype {X : Type} {n : nat} (m : nat) (l : Wlist X n) : Wlist X (n+m) := match l with
  | Bnil n ⇒ Bnil X (n+m)
  | Bcons _ a b ⇒ Bcons a (w_subtype m b) end.

Fixpoint wapp {X : Type} {n m : nat} (l : Wlist X n) (ll : Wlist X m) : Wlist X (n+m)
 := match l with
  | Bnil n ⇒ eq_rect_r (Wlist X) ((w_subtype n ll)) (addnC n m)
  | Bcons _ a b ⇒ Bcons a (wapp b ll) end.

Fixpoint wall {X : Type} {m : nat} (P : X → bool) (s : Wlist X m) : bool := match s with
  | Bnil _ ⇒ true
  | Bcons _ a b ⇒ (P a) && (wall P b) end.

Lemma wall_allK {A : Type} {w : nat} {l : Wlist A w} {P : pred A} : wall P l = all P (wlist_to_seq l).

Lemma wall_to_all {A : Type} {w : nat} {l : Wlist A w} {P : pred A} : wall P l → all P (wlist_to_seq l).

Definition w_all_prop (T : Type) (a : T → Prop) :=
fix all {w : nat} (s : Wlist T w) : Prop :=
  match s with
  | Bnil _ ⇒ True
  | Bcons n x s' ⇒ a x ∧ all n s'
  end.


Fixpoint tuple_to_wlist {X : Type} {n : nat} (t : n.-tuple X) : Wlist X n.
Defined.

Lemma wmap_nil {X Y : Type} {n : nat} (f : X → Y) (l : Wlist X n):
  map f (wlist_to_seq_co l) = [::] → l = Bnil X n.

End WlistUtils.

End Wlist.