include "basics/lists/list.ma".
include "ASM/Util.ma". (* coercion from bool to Prop *)

lemma All_map : ∀A,B,P,Q,f,l.
All A P l →
(∀a.P a → Q (f a)) →
All B Q (map A B f l).
#A #B #P #Q #f #l elim l //
#h #t #IH * #Ph #Pt #F % [@(F ? Ph) | @(IH Pt F)] qed.

lemma Exists_map : ∀A,B,P,Q,f,l.
Exists A P l →
(∀a.P a → Q (f a)) →
Exists B Q (map A B f l).
#A #B #P #Q #f #l elim l //
#h #t #IH * #H #F
[ %1 @(F ? H) | %2 @(IH H F) ]
qed.

lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r).
#A #P #l elim l
[ //
| #hd #tl #IH #r * #H1 #H2 #H3 % // @IH //
] qed.

lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l.
#A #P #l elim l
[ //
| #hd #tl #IH #r * #H1 #H2 % /2/
] qed.

lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r.
#A #P #l elim l
[ //
| #h #t #IH #r * /2/
] qed.

(* An alternative form of All that can be easier to use sometimes. *)
lemma All_alt : ∀A,P,l.
  (∀a,pre,post. l = pre@a::post → P a) →
  All A P l.
#A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?);
generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %);
[ #pre #E %
| #a #tl #IH #pre #E %
  [ @(H a pre tl E)
  | @(IH (pre@[a])) >associative_append @E
  ]
] qed.

lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x.
#A #P #l elim l
[ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS)
| #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ)
  [ @(IH Ptl … (refl …))
  | @Phd
  ]
]
qed.

let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
match la with
[ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ]
| cons ha ta ⇒
    match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ]
].

lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|.
#A #B #P #la elim la
[ * [ // | #x #y * ]
| #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl
] qed.

lemma All2_mp : ∀A,B,P,Q,la,lb. (∀a,b. P a b → Q a b) → All2 A B P la lb → All2 A B Q la lb.
#A #B #P #Q #la elim la
[ * [ // | #h #t #_ * ]
| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
] qed.

let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝
match l return λl. All A P l → ? with
[ nil ⇒ λ_. nil B
| cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H))
] H.

lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l).
#A#P#l elim l //
#h #t #Hi * #Ph #Pt normalize
>rev_append_def
@All_append
[ @(Hi Pt)
| %{Ph I}
]
qed.

lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l).
#A#P#l elim l //
#h #t #Hi normalize >rev_append_def
* [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)]
qed.

include "utilities/option.ma".

lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) →
  ∀l. All ? P l → opt_All ? Q (find … f l).
#A#B#P#Q#f#H#l elim l [#_%]
#x #l' #Hi
* #Px #AllPl'
whd in ⊢ (???%);
lapply (H x Px)
lapply (refl ? (f x))
generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//]
#_ whd in ⊢ (???%); @(Hi AllPl')
qed.

include "utilities/monad.ma".

definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
// qed.

definition List ≝ MakeMonadProps
  list
  (λX,x.[x])
  (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l)
  ????. normalize
[ / by /
| #X#m elim m normalize //
| #X#Y#Z #m #f#g
  elim m normalize [//]
  #x#l' #Hi elim (f x)
  [@Hi] normalize #hd #tl #IH >associative_append >IH %
|#X#Y#m #f #g #H elim m normalize [//]
  #hd #tl #IH >H >IH % 
] qed.

alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
unification hint 0 ≔ X ;
N ≟ max_def List
(*---------------------------*)⊢
list X ≡ monad N X.

definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l.

lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x.
#A#P#l#x #Pl #xl elim (Exists_All … xl Pl)
#x' * #EQx' >EQx' //
qed.

lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l.
#A#P#l elim l
[#_ %
|#x #l' #IH #H %
  [ @H % %
  | @IH #y #G @H %2 @G
  ]
]
qed.


lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1.
#A#l1 elim l1 normalize
[ #l2 #n #ABS elim (absurd ? ABS ?) //
| #x #l' #IH #l2 #n cases n normalize
  [//
  | #n #H @IH @le_S_S_to_le assumption
  ]
]
qed.

lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
#A#l1 elim l1
[#l2 #n #_ <minus_n_O %
|#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???);
  cases n -n
  [  #ABS elim (absurd ? ABS ?) //
  | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption
  ]
]
qed.

lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x →
  nth_opt A n (l1 @ l2) = Some ? x.
#A #l1 elim l1 normalize
[ #l2 #n #x #ABS destruct
| #hd #tl #IH #l2 * [2: #n] #x normalize /2 by /
]
qed.

lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? →
  nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
#A #l1 elim l1 normalize
[ #l2 #n #_ <minus_n_O %
| #hd #tl #IH #l2 * [2: #n] normalize
  [ @IH
  | #ABS destruct(ABS)
  ]
]
qed.

 
(* count occurrences satisfying a test *)
let rec count A (f : A → bool) (l : list A) on l : ℕ ≝
  match l with
  [ nil ⇒ 0
  | cons x l' ⇒ (if f x then 1 else 0) + count A f l'
  ].
  
theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2.
#A #f #l1 elim l1
[ #l2 %
| #hd #tl #IH #l2 normalize elim (f hd) normalize >IH %
]
qed.


include "utilities/option.ma".

lemma position_of_from_aux : ∀A,test,l,n.
  position_of_aux A test l n = !n' ← position_of A test l; return n + n'.
#A #test #l elim l
[ normalize #_ %
| #hd #tl #IH #n
  normalize in ⊢ (??%?); >IH
  normalize elim (test hd) normalize
  [ <plus_n_O %
  | >(IH 1) whd in match (position_of ???);
    elim (position_of_aux ??? 0) normalize
    [ % | #x <plus_n_Sm % ]
  ]
]
qed.

definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1.
  opt_safe ? (position_of A test l) ?.
  lapply prf -prf elim l normalize
  [ #ABS elim (absurd ? ABS (not_le_Sn_O 0))
  |#hd #tl #IH elim (test hd) normalize
    [2: >position_of_from_aux #H
      change with (position_of_aux ????) in match (position_of ???);
      >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x]
    #_ % #ABS destruct(ABS)
qed.

definition index_of ≝
  λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?.
  lapply prf -prf @eqb_elim #EQ * >EQ %
qed.

lemma position_of_append_hit : ∀A,test,l1,l2,x.
  position_of A test (l1@l2) = Some ? x →
    position_of A test l1 = Some ? x ∨
      (position_of A test l1 = None ? ∧
        ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x).
#A#test#l1 elim l1
[ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2
  % %
| #hd #tl #IH #l2 #x
  normalize elim (test hd) normalize
  [#H %{H}
  | >position_of_from_aux
    lapply (refl … (position_of A test (tl@l2)))
    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
    normalize #EQ destruct(EQ)
    elim (IH … Heq) -IH
    [ #G %
    | * #G #H
     lapply (refl … (position_of A test l2))
     generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize
     #EQ destruct (EQ) %2 %]
    >position_of_from_aux
    [1,2: >G % | >H' %]
  ]
]
qed.

lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x →
  count A test l ≥ 1.
#A#test#l elim l normalize
[#x #ABS destruct(ABS)
|#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //]
  >position_of_from_aux
  lapply (refl … (position_of ? test tl))
  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
  #EQ destruct(EQ) @(IH … Heq)
]
qed.

lemma position_of_miss : ∀A,test,l.position_of A test l = None ? →
  count A test l = 0.
#A#test#l elim l normalize
[ #_ %
|#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)]
  >position_of_from_aux
  lapply (refl … (position_of ? test tl))
  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
  #EQ destruct(EQ) @(IH … Heq)
]
qed.


lemma position_of_append_miss : ∀A,test,l1,l2.
  position_of A test (l1@l2) = None ? →
    position_of A test l1 = None ? ∧ position_of A test l2 = None ?.
#A#test#l1 elim l1
[ #l2 change with l2 in match (? @ l2); #EQ >EQ % %
| #hd #tl #IH #l2
  normalize elim (test hd) normalize
  [#H destruct(H)
  | >position_of_from_aux
    lapply (refl … (position_of A test (tl@l2)))
    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
    normalize #EQ destruct(EQ)
    elim (IH … Heq) #H1 #H2
    >position_of_from_aux
    >position_of_from_aux
    >H1 >H2 normalize % %
  ]
]
qed.