(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* List.ma: Polymorphic lists, and routine operations on them.                *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

include "Util.ma".
include "Universes.ma".
include "Bool.ma".
include "Nat.ma".
(* include "Maybe.ma". *)
include "Equality.ma".

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* The datatype.                                                              *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ninductive List (A: Type[0]): Type[0] ≝
  Empty: List A
| Cons: A → List A → List A.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Syntax.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

notation "hvbox(hd break :: tl)"
  right associative with precedence 47
  for @{ 'Cons $hd $tl }.

interpretation "List empty" 'Empty = (Empty ?).
interpretation "List cons" 'Cons = (Cons ?).
  
notation "[ list0 x sep ; ]"
  non associative with precedence 90
  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
  
notation "hvbox(l break !! break n)"
  non associative with precedence 90
  for @{ 'get_index $l $n }.
  
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lookup.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
   
(*   
nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝
  match n with
    [ Z ⇒
      match l with
        [ Empty ⇒ Nothing A
        | Cons hd tl ⇒ Just A hd
        ]
    | S o ⇒
      match l with
        [ Empty ⇒ Nothing A
        | Cons hd tl ⇒ get_index A tl o
        ]
    ].
    
interpretation "List get_index" 'get_index l n = (get_index ? l n).

nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝
  match n with
    [ Z ⇒
      match l with
        [ Empty ⇒ Nothing (List A)
        | Cons hd tl ⇒ Just (List A) (Cons A a tl)
        ]
    | S o ⇒
      match l with
        [ Empty ⇒ Nothing (List A)
        | Cons hd tl ⇒
            let settail ≝ set_index A tl o a in
              match settail with
                [ Nothing ⇒ Nothing (List A)
                | Just j ⇒ Just (List A) (Cons A hd j)
                ]
        ]
    ].

nlet rec drop (A: Type[0]) (l: List A) (n: Nat) on n ≝
  match n with
    [ Z ⇒ Just (List A) l
    | S o ⇒
        match l with
          [ Empty ⇒ Nothing (List A)
          | Cons hd tl ⇒ drop A tl o
          ]
    ].
*)
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Building lists from scratch                                                *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
  match n with
    [ Z ⇒ Empty A
    | S o ⇒ a :: replicate A o a
    ].
    
nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
  match l with
    [ Empty ⇒ m
    | Cons hd tl ⇒ hd :: (append A tl m)
    ].
    
notation "hvbox(l break @ r)"
  right associative with precedence 47
  for @{ 'append $l $r }.    
  
interpretation "List append" 'append = (append ?).    

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Other manipulations.                                                       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec length (A: Type[0]) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Z
    | Cons hd tl ⇒ S $ length A tl
    ].
    
nlet rec reverse (A: Type[0]) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Empty A
    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Deletions.                                                                 *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec remove_first_with_aux (A: Type[0]) (f: A → A → Bool) (a: A)
                               (l: List A) (b: List A) on l ≝
  match l with
    [ Empty ⇒ reverse A b
    | Cons hd tl ⇒
      match f hd a with
        [ True ⇒ (reverse A b) @ tl
        | False ⇒ remove_first_with_aux A f a tl (hd :: b)
        ]
    ].

ndefinition remove_first_with ≝
  λA: Type[0].
  λf: A → A → Bool.
  λa: A.
  λl: List A.
    remove_first_with_aux A f a l (Empty A).
    
nlet rec remove_all_with_aux (A: Type[0]) (f: A → A → Bool) (a: A)
                             (l: List A) (b: List A) on l ≝
  match l with
    [ Empty ⇒ reverse A b
    | Cons hd tl ⇒
      match f hd a with
        [ True ⇒ remove_all_with_aux A f a tl b
        | False ⇒ remove_all_with_aux A f a tl (hd :: b)
        ]
    ].
    
ndefinition remove_all_with ≝
  λA: Type[0].
  λf: A → A → Bool.
  λa: A.
  λl: List A.
    remove_all_with_aux A f a l (Empty A).

nlet rec drop_while (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Empty A
    | Cons hd tl ⇒
      match f hd with
        [ True ⇒ drop_while A f tl
        | False ⇒ Cons A hd tl
        ]
    ].
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Folds and builds.                                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec fold_right (A: Type[0]) (B: Type[0])
                    (f: A → B → B) (x: B) (l: List A) on l ≝
  match l with
    [ Empty ⇒ x
    | Cons hd tl ⇒ f hd (fold_right A B f x tl)
    ].
    
nlet rec fold_left (A: Type[0]) (B: Type[0])
                   (f: A → B → A) (x: A) (l: List B) on l ≝
  match l with
    [ Empty ⇒ x
    | Cons hd tl ⇒ f (fold_left A B f x tl) hd
    ].
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Filters and existence tests.                                               *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec filter (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Empty A
    | Cons hd tl ⇒
      match f hd with
        [ True ⇒ hd :: (filter A f tl)
        | False ⇒ filter A f tl
        ]
    ].
    
nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool ≝
  match l with
    [ Empty ⇒ cic:/matita/Cerco/Bool/Bool.con(0,2,0)
    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
    ].
    
nlet rec nub_with (A: Type[0]) (f: A → A → Bool) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Empty A
    | Cons hd tl ⇒
      match member_with A hd f tl with
        [ True ⇒ nub_with A f tl
        | False ⇒ hd :: (nub_with A f tl)
        ]
    ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Maps and zips.                                                             *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec map (A: Type[0]) (B: Type[0])
             (f: A → B) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Empty B
    | Cons hd tl ⇒ f hd :: map A B f tl
    ].
    
nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
  match l with
    [ Empty ⇒ Empty A
    | Cons hd tl ⇒ hd @ (flatten A tl)
    ].
    
ndefinition map_flatten ≝
  λA: Type[0].
  λf: A → List A.
  λl: List A.
    flatten A (map A (List A) f l).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Set-like operations.                                                       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec intersection_with (A: Type[0]) (f: A → A → Bool)
                           (l: List A) (m: List A) on l ≝
  match l with
    [ Empty ⇒ Empty A
    | Cons hd tl ⇒
      match member_with A hd f m with
        [ True ⇒ hd :: (intersection_with A f tl m)
        | False ⇒ intersection_with A f tl m
        ]
    ]. 

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
(* Rotates and shifts.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec rotate_left (A: Type[0]) (l: List A) (m: Nat) on m ≝
  match m with
    [ Z ⇒ l
    | S n ⇒
      match l with
        [ Empty ⇒ Empty A
        | Cons hd tl ⇒ hd :: rotate_left A tl n
        ]
    ].

ndefinition rotate_right ≝
  λA: Type[0].
  λl: List A.
  λm: Nat.
    reverse A (rotate_left A (reverse A l) m).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lemmas.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
nlemma append_empty_left_neutral:
  ∀A: Type[0].
  ∀l: List A.
    l @ (Empty A) = l.
  #A l.
  nelim l.
  nnormalize.
  @.
  #H L H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.

nlemma append_associative:
  ∀A: Type[0].
  ∀l,m,n: List A.
    l @ (m @ n) = (l @ m) @ n.
  #A l m n.
  nelim l.
  nnormalize.
  @.
  #H L H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.
    
nlemma reverse_distributes_append:
  ∀A: Type[0].
  ∀l, m: List A.
    reverse A (l @ m) = reverse A m @ reverse A l.
  #A l m.
  nelim l.
  nnormalize.
  nrewrite > (append_empty_left_neutral ? ?).
  @.
  #H L A.
  nnormalize.
  nrewrite > A.
  nrewrite > (append_associative ? (reverse ? m) (reverse ? L) (Cons ? H (Empty ?))).
  @.
nqed.

nlemma length_distributes_append:
  ∀A: Type[0].
  ∀l, m: List A.
    length A (l @ m) = length A l + length A m.
  #A l m.
  nelim l.
  nnormalize.
  @.
  #H L H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.

(*  
nlemma length_reverse:
  ∀A: Type[0].
  ∀l: List A.
    length A (reverse A l) = length A l.
  #A l.
  nelim l.
  nnormalize.
  @.
  #H L H2.
  nnormalize.
  napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))).
*)
  
(*    
nlemma reverse_reverse:
  ∀A: Type[0].
  ∀l: List A.
    reverse A (reverse A l) = l.
  #A l.
  nelim l.
  nnormalize.
  @.
  #H L H2.
  nnormalize.
*)

nlemma map_fusion:
  ∀A, B, C: Type[0].
  ∀l: List A.
  ∀m: List B.
  ∀f: A → B.
  ∀g: B → C.
    map B C g (map A B f l) = map A C (λx. g (f x)) l.
  #A B C l m f g.
  nelim l.
  //.
  #H L H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.

nlemma map_preserves_length:
  ∀A, B: Type[0].
  ∀l: List A.
  ∀f: A → B.
    length B (map A B f l) = length A l.
  #A B l f.
  nelim l.
  //.
  #H L H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.

(*
nlemma empty_get_index_nothing:
  ∀A: Type[0].
  ∀n: Nat.
    ((Empty A) !! n) = Nothing A.
  #A n.
  nelim n.
  //.
  #N H.
  //.
nqed.
*)

nlemma rotate_right_empty:
  ∀A: Type[0].
  ∀n: Nat.
    rotate_right A (Empty A) n = Empty A.
  #A n.
  nelim n.
  //.
  #N H.
  //.
nqed.

nlemma rotate_left_empty:
  ∀A: Type[0].
  ∀n: Nat.
    rotate_left A (Empty A) n = Empty A.
  #A n.
  nelim n.
  //.
  #N H.
  //.
nqed.

nlemma reverse_singleton:
  ∀A: Type[0].
  ∀a: A.
    reverse A (Cons A a (Empty A)) = Cons A a (Empty A).
  #A a.
  //.
nqed.