source: Deliverables/D4.1/Matita/List.ma @ 231

include "Maybe.ma".
include "Nat.ma".
include "Util.ma".

include "Plogic/equality.ma".

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

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 } }.
  
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 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 ?).
  
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
    ].
    
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 null (A: Type[0]) (l: List A) on l ≝
  match l with
    [ Empty ⇒ True
    | Cons hd tl ⇒ False
    ].
    
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)
    ].
    
ndefinition head ≝
  λA: Type[0].
  λl: List A.
    match l with
      [ Empty ⇒ Nothing A
      | Cons hd tl ⇒ Just A hd
      ].
    
ndefinition tail ≝
  λA: Type[0].
  λl: List A.
    match l with
      [ Empty ⇒ Nothing (List A)
      | Cons hd tl ⇒ Just (List A) tl
      ].
      
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
    ].
    
nlemma append_empty:
  ∀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_append:
  ∀A: Type[0].
  ∀l, m: List A.
    reverse A (l @ m) = reverse A m @ reverse A l.
  #A l m.
  nelim l.
  nnormalize.
  napplyS append_empty.
  #H L A.
  nnormalize.
  nrewrite > A.
  napplyS append_associative.
nqed.

nlemma length_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.
  napplyS length_append.
    
nlemma reverse_reverse:
  ∀A: Type[0].
  ∀l: List A.
    reverse A (reverse A l) = l.
  #A l.
  nelim l.
  nnormalize.
  @.
  #H L H2.
  nnormalize.
*)