(** * Coq codes *)
(** ** Dependencies *)

Require Export Ascii.
Require Export String.
Require Export List.
Require Export Relation_Definitions.

(** ** Equality and equivalence *)

Definition bool_eq (a a':bool) : Prop := a = a'.

Lemma bool_eq_equiv : equiv bool bool_eq.
Proof.
(* Goal: equiv string string_eq *)
  unfold equiv. split.
(* Goal: and (transitive string string_eq) (symmetric string string_eq) *)
    unfold reflexive. intro. unfold bool_eq. auto. split.
(* Goal: @eq bool (andb true (andb true true)) true *)
    unfold transitive. intros. unfold bool_eq in *. transitivity y; auto.
(* Goal: @eq bool (andb true (andb true true)) true *)
    unfold symmetric. intros. unfold bool_eq in *. auto.
Qed.

Definition ascii_eq (a a':ascii) : Prop := a = a'.
Lemma ascii_eq_equiv : equiv ascii ascii_eq.
Proof.
(* Goal: equiv string string_eq *)
  unfold equiv. split.
(* Goal: and (transitive string string_eq) (symmetric string string_eq) *)
    unfold reflexive. intros. unfold ascii_eq. auto. split.
(* Goal: @eq bool (andb true (andb true true)) true *)
    unfold transitive. intros. unfold ascii_eq in *. transitivity y; auto.  
(* Goal: @eq bool (andb true (andb true true)) true *)
    unfold symmetric. intros. unfold ascii_eq in *. auto.  
Qed.

Definition string_eq (a a':string) : Prop := a = a'.
Lemma string_eq_equiv : equiv string string_eq.
Proof.
(* Goal: equiv string string_eq *)
  unfold equiv. split.
(* Goal: and (transitive string string_eq) (symmetric string string_eq) *)
    unfold reflexive. intros. unfold string_eq. auto. split.
(* Goal: @eq bool (andb true (andb true true)) true *)
    unfold transitive. intros. unfold string_eq in *. transitivity y; auto.  
(* Goal: @eq bool (andb true (andb true true)) true *)
    unfold symmetric. intros. unfold string_eq in *. auto.  
Qed.

(** ** Lemmas for string *)

Lemma string_assoc : forall s s' s'':string, 
  ((s ++ s') ++ s'')%string = (s ++ (s' ++ s''))%string.
Proof.
(* Goal: forall s s' s'' : string, @eq string (append (append s s') s'') (append s (append s' s'')) *)
  induction s; simpl.
(* Goal: @eq bool (andb true (andb true true)) true *)
    auto.
(* Goal: @eq bool (andb true (andb true true)) true *)
    intros s' s''. erewrite IHs. auto.
Qed.

Fixpoint str_length (s:string) : nat :=
match s with
| ""%string => O
| String _ s' => S (str_length s')
end.

Lemma str_length_append : forall s s', 
  str_length (s ++ s')%string = str_length s + str_length s'.
Proof.
(* Goal: forall s : string, @eq string (append s EmptyString) s *)
  induction s.
(* Goal: @eq bool (andb (@forallb A f xs) (@forallb A f (@cons A x (@nil A)))) true *)
    simpl.  reflexivity.
(* Goal: forall s' : string, @eq nat (S (str_length (append s s'))) (S (Nat.add (str_length s) (str_length s'))) *)
    simpl.  intros. erewrite IHs.  reflexivity.
Qed.

Lemma string_right_id : forall s, (s ++ "")%string = s.
Proof.
(* Goal: forall s : string, @eq string (append s EmptyString) s *)
  induction s.
(* Goal: @eq bool (andb true (andb true true)) true *)
    auto.
(* Goal: @eq bool (andb true (andb true true)) true *)
    simpl.  erewrite IHs.  auto.
Qed.

Definition bneq_empty_string(s:string):bool :=
match (string_dec s ""%string) with
| left _ => false
| right _ => true
end.

(** ** Lemmas for list *)

Definition concat_list_string(xs:list string) := 
  fold_right (fun s s' : string => (s ++ s')%string) ""%string xs.

Lemma concat_list_string_x_xs : forall (x:string)(xs:list string),
  concat_list_string (x :: xs) = (x ++ (concat_list_string xs))%string.
Proof.
(* Goal: @eq bool (andb true (andb true true)) true *)
  induction xs; auto.
Qed.

Lemma concat_list_string_xs_x : forall (xs:list string)(x:string),
  concat_list_string (xs ++ x::nil) = ((concat_list_string xs) ++ x)%string.
Proof.
(* Goal: forall (xs : list string) (x : string), @eq string (concat_list_string (@app string xs (@cons string x (@nil string)))) (append (concat_list_string xs) x) *)
  induction xs; simpl; intro x.
(* Goal: @eq bool (andb true (andb true true)) true *)
    erewrite string_right_id.  auto.
(* Goal: @eq bool (andb true (andb true true)) true *)
    erewrite IHxs.  erewrite string_assoc.  auto.
Qed.

Lemma In_list_append_left : forall A (a:A) l l', In a l -> In a (l ++ l')%list.
Proof.
(* Goal: @eq bool (andb (@forallb A f xs) (@forallb A f (@cons A x (@nil A)))) true *)
  induction l; simpl.
(* Goal: forall (l' : list A) (_ : @In A a l'), or (@eq A a0 a) (@In A a (@app A l l')) *)
    intros l' H.  elim H.
(* Goal: forall (l' : list A) (_ : @In A a l'), or (@eq A a0 a) (@In A a (@app A l l')) *)
    intros l' H.  destruct H as [H1 | H2].
(* Goal: @eq bool (andb true (andb true true)) true *)
      left; auto.
(* Goal: @eq bool (andb true (andb true true)) true *)
      right; eapply IHl; auto.
Qed.

Lemma In_list_append_right : forall A (a:A) l l', In a l' -> In a (l ++ l')%list.
Proof.
(* Goal: @eq bool (andb (@forallb A f xs) (@forallb A f (@cons A x (@nil A)))) true *)
  induction l; simpl.
(* Goal: @eq bool (andb true (andb true true)) true *)
    intros l' H.  auto. 
(* Goal: @eq bool (andb true (andb true true)) true *)
    intros l' H.  right.  eapply IHl.  auto.
Qed.

Lemma In_snoc : forall A (a:A) l, In a (l ++ a::nil)%list.
Proof.
(* Goal: @eq bool (andb (@forallb A f xs) (@forallb A f (@cons A x (@nil A)))) true *)
  induction l; simpl.
(* Goal: @eq bool (andb true (andb true true)) true *)
    left; auto.
(* Goal: @eq bool (andb true (andb true true)) true *)
    right; auto.
Qed.

(* Other useful lemmas are:
Lemma forallb_forall : forall l, forallb l = true <-> (forall x, In x l -> f x = true).
Lemma forallb_app : forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2.
*)

Lemma forallb_divide_left : forall (A:Type)(f:A -> bool) (l l':list A), 
  forallb f (l ++ l') = true -> forallb f l = true.
Proof.
(* Goal: forall (A : Type) (f : forall _ : A, bool) (l l' : list A) (_ : @eq bool (@forallb A f (@app A l l')) true), @eq bool (@forallb A f l') true *)
  intros A f l l' H.  erewrite forallb_app in H.
(* Goal: @eq bool (@forallb A f l) true *)
  destruct(forallb f l).
(* Goal: @eq bool (andb true (andb true true)) true *)
    auto.
(* Goal: @eq bool false true *)
    destruct(forallb f l'); simpl in H; discriminate H. 
Qed.
  
Lemma forallb_divide_right : forall (A:Type)(f:A -> bool) (l l':list A), 
  forallb f (l ++ l') = true -> forallb f l' = true.
Proof.
(* Goal: forall (A : Type) (f : forall _ : A, bool) (l l' : list A) (_ : @eq bool (@forallb A f (@app A l l')) true), @eq bool (@forallb A f l') true *)
  intros A f l l' H.  erewrite forallb_app in H.
(* Goal: @eq bool (@forallb A f l') true *)
  destruct(forallb f l').
(* Goal: @eq bool true true *)
(* Goal: @eq bool false true *)
    reflexivity.
(* Goal: @eq bool false true *)
    destruct(forallb f l); simpl in H; discriminate H. 
Qed.

Lemma forallb_list_x_xs : forall A (f:A -> bool)(x:A)(xs:list A),
  f x = true -> forallb f xs = true -> forallb f (x::xs) = true.
Proof.
(* Goal: forall (A : Type) (f : forall _ : A, bool) (x : A) (xs : list A) (_ : @eq bool (f x) true) (_ : @eq bool (@forallb A f xs) true), @eq bool (@forallb A f (@cons A x xs)) true *)
  intros A f x xs Hx Hxs.
(* Goal: @eq bool (@forallb A f (@cons A x xs)) true *)
  replace (x :: xs) with ((x :: nil) ++ xs).
(* Goal: @eq bool (andb true (andb true true)) true *)
  erewrite forallb_app.  simpl.  rewrite Hx; rewrite Hxs.  auto.
(* Goal: @eq bool (andb true (andb true true)) true *)
  simpl.  auto.
Qed.

Lemma forallb_list_xs_x : forall A (f:A -> bool)(xs:list A)(x:A),
  forallb f xs = true -> f x = true -> forallb f (xs ++ x::nil)%list = true.
Proof.
(* Goal: forall (A : Type) (f : forall _ : A, bool) (xs : list A) (x : A) (_ : @eq bool (@forallb A f xs) true) (_ : @eq bool (f x) true), @eq bool (@forallb A f (@app A xs (@cons A x (@nil A)))) true *)
  intros A f xs x Hxs Hx.
(* Goal: @eq bool (andb true (andb true true)) true *)
  erewrite forallb_app.  simpl.  rewrite Hx; rewrite Hxs.  auto.
Qed.  
