逆配列のユニーク性

gistfile1.coq

Require Import Bool.
Require Import Lists.List.
Require Import String.
Require Import Ascii.

Definition eqc (x y : ascii) : bool :=
  if ascii_dec x y
    then true
    else false.

Fixpoint list_of_string (s : string) : list ascii :=
  match s with
  | EmptyString => nil
  | String c s => c :: (list_of_string s)
  end.

Fixpoint contain (c : ascii) (chars : list ascii) : bool :=
  match chars with
    | nil => false
    | x :: xs =>
      if eqc x c then
        true
      else
        contain c xs
  end.

Fixpoint snoc (l: list ascii) (v: ascii) : list ascii :=
  match l with
  | nil => v :: nil
  | h :: t => h :: (snoc t v)
  end.

Fixpoint rev (l: list ascii) : list ascii :=
  match l with
  | nil => nil
  | h :: t => snoc (rev t) h
  end.

Fixpoint uniq_i (chars : list ascii) : bool :=
  match chars with
    | nil => true
    | x :: xs => 
      if contain x xs
        then false
        else uniq_i xs
  end.

Definition uniq (str : string) : bool :=
  uniq_i (list_of_string str).


Eval compute in uniq "abcde".
Eval compute in uniq "abcdaae".


(************** 以下 uniq(uniq_i)の性質の証明 ***************)

(* eqcに関する補題を証明し eqc a b = eqc b aを証明しておく *)
Lemma lemma_eqc1:
  forall (a b: ascii), 
    a = b -> (if ascii_dec a b then true else false) = true.
Proof.
  intros.
  case (ascii_dec a b).
  intros.
  reflexivity.
  intros.
  intuition.
Qed.

Lemma lemma_eqc2:
  forall (a b: ascii), 
    a <> b -> (if ascii_dec a b then true else false) = false.
Proof.
  intros.
  case (ascii_dec a b).
  intros.
  contradiction.
  intros.
  reflexivity.
Qed.

Lemma lemma_eqc3:
  forall (a b : ascii), eqc a b = false -> eqc b a = false.
Proof.
  intros.
  refine (match ascii_dec a b with
            | left _ => _
            | right _ => _
          end).
  rewrite e in H.
  unfold eqc in H.
  rewrite (lemma_eqc1 b) in H.
  apply False_ind.
  assert (G: true = true).
  reflexivity.
  intuition.
  reflexivity.
  apply lemma_eqc2.
  intuition.
Qed.

Lemma lemma_eqc4:
  forall (a b : ascii), eqc a b = true -> eqc b a = true.
Proof.
  intros.
  destruct (ascii_dec a b).
  rewrite e in H.
  rewrite e.
  exact H.
  unfold eqc in H.
  refine (match ascii_dec a b with
            | left _ => _
            | right _ => _
          end).
  contradiction.
  apply lemma_eqc2 in n.
  rewrite n in H.
  apply False_ind.
  intuition.
Qed.

(* 定理　同じ文字は等しい *)
Theorem eqc_id_theorem:
  forall (a : ascii), eqc a a = true.
Proof.
  intros.
  unfold eqc.
  apply lemma_eqc1.
  reflexivity.
Qed.

(* 定理　文字を入れ替えて比較したものは等しい *)
Theorem eqc_eq_theorem:
  forall (a b : ascii), eqc a b = eqc b a.
Proof.
  intros.
  case_eq (eqc a b).
  intros.
  apply lemma_eqc4 in H; intuition.
  intros.
  apply lemma_eqc3 in H; intuition.
Qed.


(* containやuniq_iで出てくるif then elseの性質を証明しておく *)
Lemma logic_false_true:
  forall (A B : bool),
    ((if A then false else B) = true) -> A = false /\ B = true.
Proof.
  intros.
  split.
  induction A.
  rewrite H.
  reflexivity.
  reflexivity.
  induction B.
  reflexivity.
  induction A.
  apply H.
  apply H.
Qed.

Lemma logic_false_false:
  forall (A B : bool),
    ((if A then false else B) = false) -> A = true \/ A = false /\ B = false.
Proof.
  intros.
  destruct A; destruct B.
  left; reflexivity.
  left; reflexivity.
  right.
  split.
  reflexivity.
  apply H.
  right.
  split.
  reflexivity.
  reflexivity.
Qed.

Lemma logic_true_false:
  forall (A B : bool),
    ((if A then true else B) = false) -> A = false /\ B = false.
Proof.
  intros.
  destruct A; destruct B.
  split; exact H; exact H.
  split; intuition.
  split; intuition.
  split; reflexivity.
Qed.

Lemma logic_true_true:
  forall (A B : bool),
    ((if A then true else B) = true) -> A = true \/ A = false /\ B = true.
Proof.
  intros.
  destruct A; destruct B.
  left.
  reflexivity.
  left.
  reflexivity.
  right.
  split.
  reflexivity.
  reflexivity.
  auto.
Qed.

(*
  uniq_iの性質1
   全ての uniq_i l = trueとなるようなlist lに対して、
   lの先頭の文字aはlのその後の文字列に含まれない
*)
Theorem uniq_theorem1:
  forall (l l0 : list ascii) (a : ascii), l = a::l0 /\ uniq_i l = true ->
    contain a l0 = false.
Proof.
  intros.
  decompose [and] H.
  rewrite H0 in H1.
  unfold uniq_i in H1.
  fold uniq_i in H1.
  apply logic_false_true in H1.
  apply H1.
Qed.

(*
  uniq_iの性質2
   全ての uniq_i l = trueとなるようなlist lに対して、
   lの先頭の文字を除いた文字列もユニークとなる
*)
Theorem uniq_theorem2:
  forall (l : list ascii) (a : ascii), uniq_i (a::l) = true ->
    uniq_i l = true.
Proof.
  intros.
  unfold uniq_i in H.
  fold uniq_i in H.
  apply logic_false_true in H.
  decompose [and] H.
  apply H1.
Qed.

(* 性質1と性質2の合成 帰納法の証明時によく利用する *)
Theorem uniq_unshift_theorem:
  forall (l : list ascii) (a : ascii), uniq_i (a::l) = true ->
    contain a l = false /\ uniq_i l = true.
Proof.
  intros.
  unfold uniq_i in H.
  fold uniq_i in H.
  apply logic_false_true in H.
  decompose [and] H.
  exact H.
Qed.

(* uniqとcontainの補題 lemma_uniq_snoc_falseで利用 *)
Lemma contain_false_uniq:
  forall (l : list ascii) (a : ascii), 
    contain a l = false -> uniq_i(a :: l) = uniq_i l.
Proof.
  intros.
  unfold uniq_i.
  fold uniq_i.
  rewrite -> H.
  reflexivity.
Qed.

(* lemma_uniq_snoc_trueで利用する基本的な命題 *)
Lemma logic_basic_prop:
  forall (A B C: Prop), A /\ B -> (A -> B -> C) -> (A -> B -> C).
Proof.
  intros.
  apply H0 in H1.
  exact H1.
  exact H2.
Qed.

(* containに関する補題 帰納法時によく利用 *)
Lemma lemma_unshift_contain:
   forall (l : list ascii) (a b : ascii), 
     contain a (b :: l) = false -> contain a l = false /\ eqc b a = false.
Proof.
  intros.
  unfold contain in H.
  fold contain in H.
  apply logic_true_false in H.
  intuition.
Qed.

(* 配列に要素をappendした際の重要な補題 rev系の証明では必須 *)
Lemma in_app_or_contain:
  forall (l : list ascii) (a b : ascii),
    contain a (snoc l b) = (contain a l) || eqc b a.
Proof.
  intros l b a.
  induction l.
  simpl.
  case (eqc a b).
  reflexivity.
  reflexivity.
  simpl.
  rewrite -> IHl.
  case (eqc a0 b).
  reflexivity.
  reflexivity.
Qed.

(* revに関する補題 *)
Lemma lemma_contain_rev_false:
  forall (l : list ascii) (a : ascii), contain a l = false -> contain a (rev l) = false.
Proof.
  intros.
  induction l as [|a0 l'].
  simpl.
  reflexivity.
  apply lemma_unshift_contain in H.
  decompose [and] H.
  simpl.
  rewrite (in_app_or_contain (rev l') a a0).
  rewrite H0 in IHl'.
  rewrite H1.
  rewrite orb_false_r.
  apply IHl'.
  reflexivity.
Qed.

(* containとsnocに関する補題 *)
Lemma lemma_snoc_origin:
  forall (l : list ascii) (a b : ascii),
    contain a l = false /\ eqc b a= false -> contain a (snoc l b) = false.
Proof.
  intros.
  decompose [and] H.
  rewrite in_app_or_contain.
  rewrite H0.
  rewrite H1.
  reflexivity.
Qed.

Lemma lemma_uniq_snoc_true:
  forall (l : list ascii) (a : ascii),
    contain a l = false /\ uniq_i l = true -> uniq_i (snoc l a) = true.
Proof.
  intros.
  decompose [and] H.
  induction l.
  simpl.
  reflexivity.
  simpl.
  apply (logic_basic_prop (contain a l = false) (uniq_i l = true) (uniq_i (snoc l a) = true)) in IHl.
  assert (G: contain a0 (snoc l a) = false).
  apply (lemma_snoc_origin l a0 a).
  split.
  apply (uniq_unshift_theorem l a0).
  apply H1.
  apply lemma_unshift_contain in H0.
  decompose [and] H0.
  rewrite eqc_eq_theorem in H3.
  exact H3.
  rewrite G.
  apply IHl.

  (* contain a l = false /¥ uniq_i l = true の証明 *)
  apply lemma_unshift_contain in H0.
  decompose [and] H0.
  apply uniq_unshift_theorem in H1.
  decompose [and] H1.
  auto.

  apply lemma_unshift_contain in H0.
  decompose [and] H0.
  apply uniq_unshift_theorem in H1.
  decompose [and] H1.
  auto.
  apply lemma_unshift_contain in H0.
  decompose [and] H0.
  exact H2.
  apply uniq_unshift_theorem in H1.
  decompose [and] H1.
  exact H3.
Qed.

Lemma lemma_unshift_uniq:
  forall (l : list ascii) (a : ascii),
    uniq_i (a :: l) = false /\ contain a l = false ->
    uniq_i l = false.
Proof.
  intros.
  decompose [and] H.
  simpl in H.
  rewrite H1 in H.
  decompose [and] H.
  exact H2.
Qed.

Lemma lemma_contain_snoc:
  forall (l : list ascii) (a : ascii),
    contain a (snoc l a) = true.
Proof.  
  intros.
  induction l.
  simpl.
  rewrite eqc_id_theorem; reflexivity.
  simpl.
  case_eq (eqc a0 a).
  auto.
  intros.
  exact IHl.
Qed.  

Lemma lemma_uniq_snoc_false:
  forall (l : list ascii) (a : ascii),
    uniq_i l = false -> uniq_i (snoc l a) = false.
Proof.
  intros.
  induction l.
  simpl.
  assumption.
  simpl.

  (* cotain a0 (snoc l a) = true の場合 *)
  case_eq (contain a0 (snoc l a)).
  intros.
  reflexivity.

  (* cotain a0 (snoc l a) = false の場合 *)
  intros.
  apply (lemma_unshift_uniq (snoc l a) a0).
  split.
  unfold uniq_i.
  fold uniq_i.
  rewrite H0.
  apply IHl.

  rewrite (in_app_or_contain l a0 a) in H0.
  apply (orb_false_iff (contain a0 l) (eqc a a0)) in H0.
  decompose [and] H0.
  apply (contain_false_uniq l a0) in H1.
  rewrite H in H1.
  auto.
  exact H0.
Qed.

Lemma lemma_unshift_contain_true:
  forall (l : list ascii) (a b : ascii),
    contain a (b :: l) = true -> contain a l = true \/  eqc a b = true.
Proof.
  intros.
  unfold contain in H.
  fold contain in H.
  apply logic_true_true in H.
  case_eq (eqc b a).
  intros.
  right.
  rewrite eqc_eq_theorem.
  exact H0.
  intros.
  left.
  decompose [or] H.
  rewrite H0 in H1.
  intuition.
  decompose [and] H1.
  exact H3.
Qed.

Lemma lemma_contain_uniq_snoc_false:
  forall (l : list ascii) (a : ascii),
    contain a l = true -> uniq_i (snoc l a) = false.
Proof.
  intros.
  decompose [and] H.
  induction l.
  simpl.
  simpl in H.
  auto.
  apply lemma_unshift_contain_true in H.
  simpl.
  decompose [or] H.
  rewrite H0 in IHl.
  intuition.

  case_eq (contain a0 (snoc l a)).
  intros.
  reflexivity.
  intros.
  rewrite H.
  reflexivity.

  assert (G: a0 = a).
  unfold eqc in H1.
  destruct (ascii_dec a a0).
  rewrite e; reflexivity.
  apply False_ind.
  intuition.

  rewrite G.
  rewrite lemma_contain_snoc.
  reflexivity.

  assert (G: a0 = a).
  unfold eqc in H0.
  destruct (ascii_dec a a0).
  rewrite e; reflexivity.
  apply False_ind.
  intuition.
  
  rewrite G.
  rewrite lemma_contain_snoc.
  reflexivity.
Qed.

Lemma lemma_contain_true1:
  forall (l : list ascii) (a b : ascii),
    contain a (b :: l) = true -> eqc a b = true \/ contain a l = true.
Proof.
  intros.
  unfold contain in H.
  fold contain in H.
  apply logic_true_true in H.
  decompose [or] H.
  left.
  rewrite eqc_eq_theorem.
  exact H0.
  right.
  decompose [and] H0.
  exact H2.
Qed.

Lemma lemma_contain_rev_true:
  forall (l : list ascii) (a : ascii), contain a l = true -> contain a (rev l) = true.
Proof.
  intros.
  induction l as [|a0 l'].
  simpl.
  simpl in H.
  intuition.
  simpl.
  apply lemma_unshift_contain_true in H.
  decompose [or] H.
  rewrite H0 in IHl'.
  intuition.
  rewrite in_app_or_contain.
  rewrite eqc_eq_theorem.
  apply orb_true_iff.
  left; exact H.
  assert (G: a0 = a).
  unfold eqc in H0.
  destruct (ascii_dec a a0).
  rewrite e; reflexivity.
  assert (G: forall (d e : ascii), eqc d e = true -> d = e).
  intros.
  unfold eqc in H2.
  destruct (ascii_dec d e).
  exact e0.
  assert (true = true).
  reflexivity.
  apply False_ind.
  intuition.
  apply G in H1.
  apply False_ind.
  intuition.
  rewrite G.
  rewrite lemma_contain_snoc.
  reflexivity.
  rewrite in_app_or_contain.
  apply orb_true_iff.
  right.
  rewrite eqc_eq_theorem.
  exact H0.
Qed.


Lemma lemma_uniq_rev_true:
  forall (l : list ascii),
    uniq_i l = true -> uniq_i (rev l) = true.
Proof.
  intros.
  induction l.
  simpl; reflexivity.
  simpl.
  simpl in H.
  apply logic_false_true in H.
  decompose [and] H.
  rewrite H1 in IHl.
  intuition.
  apply lemma_contain_rev_false in H2.
  apply (lemma_uniq_snoc_true (rev l) a).
  split.
  exact H2; exact H3.
  exact H.
Qed.

Lemma lemma_uniq_rev_false:
  forall (l : list ascii),
    uniq_i l = false -> uniq_i (rev l) = false.
Proof.
  intros.
  induction l.
  simpl; simpl in H.
  intuition.
  simpl; simpl in H.
  apply logic_false_false in H.
  decompose [or] H.
  apply lemma_contain_rev_true in H0.
  apply lemma_contain_uniq_snoc_false.
  exact H0.
  decompose [and] H0.
  rewrite H2 in IHl.
  intuition.
  apply lemma_uniq_snoc_false; exact H.
  apply lemma_uniq_snoc_false; exact H0.
Qed.

(* 定理 配列をリバースしてもuniq_iの結果は同じ *)
Theorem uniq_rev_theorem:
  forall (l : list ascii), uniq_i (rev l) = uniq_i l.
Proof.
  intros.
  case_eq (uniq_i l).
  apply lemma_uniq_rev_true.
  apply lemma_uniq_rev_false.
Qed.

Definition compress (l: list(asciinat)) (t: (ascii * nat))
: list(asciinat) :=
match t, l with
| _, [] => [t]
| (a1,n1),((a2,n2)::ls) =>
if ascii_dec a1 a2 then
((a2,n1+n2)::ls) else
(a1,n1)::(a2,n2)::ls
end.

Definition encode_to_tuples (s : string) : list (ascii * nat) :=
fold_left compress
(map (fun (a:ascii) => (a , 1))
(list_ascii_of_string s))
[].

Compute encode_to_tuples "abbccc" %string.

Definition decompress (t : (ascii*nat)) : string :=
string_of_list_ascii (List.repeat (fst t) (snd t)).

Compute (compress [("a"%char,2)]).

Definition decode_from_tuples (l:list(ascii*nat)) : string :=
concat
EmptyString
(map decompress l).

Definition decode_from_tuples_r (l:list(ascii*nat)) : string :=
fold_right
append
EmptyString
(rev (map decompress l)).

Compute decode_from_tuples (encode_to_tuples "abbcccc").
Compute decode_from_tuples_r (encode_to_tuples "abbcccc").

Lemma list_ascii_of_string_app : forall (a: ascii) (s: string),
list_ascii_of_string (String a s) = a::list_ascii_of_string(s).
intros.
induction s.

• reflexivity.
• reflexivity.
  Qed.

Lemma encode_app : forall (a: ascii) (s: string),
encode_to_tuples(String a s) = (a,1) :: encode_to_tuples s.
intros.
induction s.

• reflexivity.
• destruct (ascii_dec a0 a).

• unfold encode_to_tuples. simpl. rewrite e.
  SearchRewrite(fold_left _ _ _).
  Admitted.

Lemma encode_ascii : forall (a: ascii),
encode_to_tuples(String a "") = [(a,1)].
intros.
unfold encode_to_tuples.
reflexivity.
Qed.

Lemma encode_nil :
encode_to_tuples(EmptyString) = [].
unfold encode_to_tuples.
reflexivity.
Qed.

Lemma string_app_nil : forall (s: string),
(s ++ "")%string = s.
intros.
induction s.

• reflexivity.
• simpl. rewrite IHs. reflexivity.
  Qed.

Lemma string_assoc : forall (s1 s2 s3: string),
(s1 ++ s2 ++ s3)%string = ((s1 ++ s2)++s3)%string.
intros.
induction s1.

• reflexivity.
• simpl. rewrite IHs1. reflexivity.
  Qed.

Lemma fold_left_cons:
forall (A B : Type) (f : A -> B -> A) (l: list B) (e: B) (i : A),
fold_left f (e :: l) i = fold_left f l (f i e).
reflexivity.
Qed.

Lemma decode_cons : forall (t: (asciinat)) (l: list(asciinat)),
decode_from_tuples(t::l)= append (decompress t) (decode_from_tuples l).
intros.
unfold decode_from_tuples.
rewrite map_cons.
destruct (map decompress l).

• simpl. rewrite string_app_nil. reflexivity.
• reflexivity.
  Qed.

Theorem runlength_inverse_tuples : forall s : string,
decode_from_tuples(encode_to_tuples s) = s.
induction s.

• reflexivity.
• rewrite encode_app. rewrite decode_cons.
  simpl. rewrite IHs. reflexivity.
  Qed.