Set Implicit Arguments.

Require Import Utils.

Strings and Nonempty Strings

Strings are just lists and nonempty string are realized as a separate inductive type. It is useful to have an extra type of nonempty strings as for some applications later it is crucial that some strings are nonempty. This file contains
  • operations on nonempty strings
  • some additional operations on empty strings
  • conversion of strings to nonempty strings and vice versa

Notation Str:= list.

Basic Operations on Nonempty Strings


Section NonEmptyStrings.

  Context (X: Type).

  Inductive NStr :=
    | sing (a:X) : NStr
    | ncons (a:X) (x:NStr) : NStr.

  Fixpoint nstr_to_str (x: NStr) := match x with
    | sing a => [a]
    | ncons a x => a :: (nstr_to_str x)
  end.

  Lemma nstr_to_str_eq (x y : NStr): nstr_to_str x = nstr_to_str y -> x = y.
  Proof.
    revert y. induction x; simpl; intros y ; destruct y; simpl; intros L; auto.
    - congruence.
    - exfalso. destruct y; simpl in L; congruence.
    - exfalso. destruct x; simpl in L; congruence.
    - f_equal.
      + congruence.
      + apply IHx. congruence.
  Qed.

  Fixpoint delta (x: NStr) := match x with
    | sing _ => 0
    | ncons _ x => S (delta x)
  end.

  Fixpoint nstr_nth (x: NStr) (n:nat) := match x,n with
     | sing a, _ => a
     | ncons a x , 0 => a
     | ncons a x , S n => nstr_nth x n
  end.

  Fixpoint nstr_concat (x: Str X) (y: NStr) : NStr := match x with
    | [] => y
    | a::x => ncons a (nstr_concat x y)
  end.

  Fixpoint nstr_concat' (x: NStr) (y: NStr) : NStr := match x with
    | sing a => ncons a y
    | ncons a x => ncons a (nstr_concat' x y)
  end.

  Fixpoint nstr_drop_last (x: NStr):= match x with
    | sing a => sing a
    | ncons a x => match x with
                  | ncons b y => ncons a (nstr_drop_last x )
                  | sing b => sing a end
  end.

  Fixpoint nstr_last (x: NStr) := match x with
    | sing a => a
    | ncons _ x => nstr_last x
  end.

  Lemma nstr_last_delta x : nstr_last x = nstr_nth x (delta x).
  Proof.
    induction x; simpl; auto.
  Qed.

  Lemma nstr_concat'_delta x y : delta (nstr_concat' x y) = S(delta x) + delta y.
  Proof.
    induction x; simpl; auto.
  Qed.

  Lemma nstr_drop_last_delta x : delta x > 0 -> S(delta (nstr_drop_last x)) = delta x.
  Proof.
    induction x; simpl; intros L.
    - now exfalso.
    - f_equal. destruct x; auto.
      rewrite <-IHx by comega. reflexivity.
  Qed.

  Lemma nstr_drop_last_nth x n : n < delta x -> nstr_nth (nstr_drop_last x) n = nstr_nth x n.
  Proof.
    revert n; induction x; simpl; intros n L; auto.
    destruct x; destruct n; simpl in *; auto.
  Qed.

  Lemma nstr_concat'_nth_fst x y n: n <= delta x -> nstr_nth (nstr_concat' x y) n = nstr_nth x n.
  Proof.
    revert n; induction x; simpl; intros [|n] L; auto.
  Qed.

  Lemma nstr_concat'_nth_snd x y n: delta x < n <= S(delta x) + delta y -> nstr_nth (nstr_concat' x y) n = nstr_nth y (n - S(delta x)).
  Proof.
    revert n; induction x; simpl; intros [|n] L; simpl; auto.
  Qed.

  Fixpoint nstr_finIter (x:NStr) n := match n with
    | 0 => x
    | S n => nstr_concat' x (nstr_finIter x n)
  end.

  Lemma nstr_finIter_delta x n : delta (nstr_finIter x n) = (S n) * delta x + n.
  Proof.
    induction n.
    - simpl. omega.
    - simpl delta. rewrite mult_succ_l, nstr_concat'_delta. omega.
  Qed.

  Lemma nstr_concat_last x y : nstr_last (nstr_concat x y) = nstr_last y.
  Proof.
    induction x; simpl; auto.
  Qed.

End NonEmptyStrings.

Instance nstr_dec_eq (X: eqType) (x y: NStr X) : dec (x = y).
Proof.
  revert y. induction x as [a | a x]; intros y.
  - destruct y as [b | b y].
    + decide (a = b).
      * left. now subst a.
      * right. intros E. congruence.
    + right. congruence.
  - destruct y as [b | b y].
    + right. congruence.
    + decide (a = b).
      * destruct (IHx y) as [D|D].
        -- left. congruence.
        -- right. congruence.
      * right. congruence.
Qed.

Coercion nstr_to_str :NStr >-> Str.

Coercion nstr_nth: NStr >-> Funclass.

Lemma delta_length (X:Type) (x: NStr X) : S(delta x) = length x.
Proof.
  induction x; simpl; omega.
Qed.

Lemma in_nstr (Y:Type) a (l : NStr Y) : a el l -> (exists l1 l2, l = nstr_concat l1 l2 /\ l2 0 = a).
Proof.
  intros M. induction l as [b | b l].
  - exists [], (sing b). split; auto. cbn. destruct M as [<-|M]; auto. now exfalso.
  - destruct M as [M | M].
    + subst. now exists [], (ncons a l).
    + destruct (IHl M) as [l1 [l2 [E F]]]. subst.
      now exists (b :: l1), l2.
Qed.

Lemma nstr_size_induction (Y: Type) {P: NStr Y -> Prop}: (forall (y: NStr Y), (forall (z: NStr Y), delta z < delta y -> P z) -> P y) -> (forall (y: NStr Y), P y).
  Proof.
  intros Step y. apply Step. induction y.
  - intros z H. cbn in *. apply Step. intros z' H'. exfalso. omega.
  - intros z H. apply Step. intros z' H'. apply IHy. cbn in *. omega.
Qed.

Section NStrMap.
  Context {X Y : Type}.
  Variable (f: X -> Y).

  Fixpoint nstr_map (x: NStr X) := match x with
   | sing a => sing (f a)
   | ncons a x => ncons (f a) (nstr_map x)
  end.

  Lemma nstr_map_delta x : delta (nstr_map x) = delta x.
  Proof.
    induction x; simpl; auto.
  Qed.

  Lemma nstr_map_length x : | (nstr_map x) | = | x |.
  Proof.
    induction x; simpl; auto.
  Qed.

  Lemma nstr_map_nth x n : n <= delta x -> nstr_map x n = f (x n).
  Proof.
    revert n; induction x ; simpl; intros [|n] L ; simpl; auto.
  Qed.

  Lemma nstr_map_concat x y : nstr_map (nstr_concat' x y) = nstr_concat' (nstr_map x) (nstr_map y).
  Proof.
    induction x; cbn; auto.
    now f_equal.
  Qed.
End NStrMap.

Section NStrFlatten.
  Context {X: Type}.

  Fixpoint nstr_flatten (x : NStr (NStr X)) := match x with
    | sing y => y
    | ncons y x => nstr_concat' y (nstr_flatten x)
  end.

End NStrFlatten.

Section DropTake.

  Context {X: Type}.

  Fixpoint nstr_drop (x: NStr X) n : NStr X:= match n,x with
    | 0 , x=> x
    | S n, sing a => sing a
    | S n, ncons a x => nstr_drop x n
  end.

  Fixpoint closed_take (x: NStr X) n : NStr X := match n, x with
    | 0, sing a => sing a
    | 0, ncons a x => sing a
    | S n, sing a => sing a
    | S n, ncons a x => ncons a (closed_take x n)
  end.

  Lemma nstr_concat_delta x (y:NStr X) : delta (nstr_concat x y) = |x| + delta y.
  Proof.
    induction x; simpl; auto.
  Qed.

  Lemma closed_take_delta x n : n <= delta x -> delta (closed_take x n) = n.
  Proof.
    revert n; induction x; simpl; intros [|n]; simpl; auto.
  Qed.

End DropTake.

Section FilterLemmas.

  Context {X: Type}.
  Variable (P Q: X -> Prop).
  Context {decP: forall a, dec (P a)}.
  Context {decQ: forall a, dec (Q a)}.
  Context (decPQ: forall a, dec (P a \/ Q a)).
  Implicit Type (l : list X).

 Lemma filter_unchanged l: (forall a, a el l -> P a) -> filter (DecPred P) l = l.
 Proof.
   induction l as [| b l]; auto.
   intros H. simpl. rewrite decision_true; auto.
   f_equal. apply IHl. intros a M. apply H. auto.
 Qed.

 Lemma filter_empty l :(forall a, a el l -> ~P a) -> filter (DecPred P) l = [].
 Proof.
   induction l as [| b l]; auto.
   intros H. simpl. rewrite decision_false; auto.
 Qed.

 Lemma filter_partition l : (forall a, a el l -> ~ (P a /\ Q a)) -> (|filter (@DecPred X P decP) l|) + (|filter (@DecPred X Q decQ) l|) = |filter (@DecPred X(fun a => P a \/ Q a) decPQ) l|.
 Proof.
   intros H. induction l as [| b l]; auto.
   simpl. destruct decision as [Hp|Np].
   - rewrite decision_false.
     + rewrite decision_true by auto. simpl. f_equal. apply IHl.
       intros a M. apply H. auto.
     + intros Hq. apply (H b); auto.
   - destruct decision as [Hq | Nq].
     + rewrite decision_true by auto. simpl. rewrite <-plus_Snm_nSm. simpl. f_equal. apply IHl.
       intros a M. apply H. auto.
     + rewrite decision_false by tauto. apply IHl.
       intros a M. apply H. auto.
  Qed.

End FilterLemmas.

Conversion between Strings and Nonempty Strings

To make the conversion functions total we use dummy values. Instead of providing these dummy values by hand, we use typeclasses to derive them. Technical note: Sometimes some equal looking expression are not equal because the derived dummy values are not equal on both sides.
Typeclass providing a dummy value for some type.

Class Dummy T := dummy : T.
Arguments dummy {_} {_}.
Arguments delta {_} x.

Instance DummyDummy T : Dummy (Dummy T -> T).
Proof.
  intros D. apply dummy.
Qed.

Instance ElemDummy {T} : T -> Dummy T.
Proof.
  intros t. exact t.
Qed.

Instance DummyNat: Dummy nat.
Proof.
  constructor.
Qed.

It is important that this lemma is specialized to nat and not to just some types that provides a dummy because this causes type class resolution to diverge.
Instance DummyNatFunc {X} : (nat -> X) -> Dummy X.
Proof.
  intros f. apply f,0 .
Qed.

Instance DummyNStr X: NStr X -> Dummy X.
Proof.
  now intros [a | a _].
Qed.

Hint Immediate ElemDummy : typeclass_instances.
Hint Immediate DummyNStr : typeclass_instances.
Hint Immediate DummyNatFunc : typeclass_instances.

Conversion of strings to nonempty strings. In the case that the string was empty, we produce a singleton nonmepty string containing a dummy.
Section StrToNStr.
  Context {X: Type}.
  Context {D: Dummy X}.

  Fixpoint str_to_nstr (x: Str X) : NStr X :=
     match x with
     | [] => sing dummy
     | a::[] => sing a
     | a::x => ncons a (str_to_nstr x)
  end.

  Definition nonempty (x:Str X) : Prop := match x with
    | nil => False
    | a::x => True
  end.

  Lemma nstr_nonempty (x: NStr X): nonempty x.
  Proof.
   destruct x; simpl; auto.
  Qed.

  Lemma str_to_nstr_idem x : nonempty x -> x = str_to_nstr x.
  Proof.
    intros N. induction x.
    - now exfalso.
    - simpl. destruct x; auto.
      now rewrite IHx at 1.
  Qed.

  Lemma str_to_nstr_idem' a x : a::x = str_to_nstr (a::x).
  Proof.
    revert a. induction x as [|b x]; intros a.
    - reflexivity.
    - now rewrite IHx at 1.
  Qed.

  Lemma nstr_to_str_to_nstr_idem (x: NStr X) : x = str_to_nstr (nstr_to_str x).
  Proof.
    induction x; simpl; auto.
    destruct x.
    - reflexivity.
    - simpl. f_equal. apply IHx.
  Qed.

  Fixpoint str_nth (x: Str X) (n:nat) := match x,n with
     | a::x , 0 => a
     | a::x , S n => str_nth x n
     | [], _ => dummy
  end.

  Lemma str_nth_nstr (x: NStr X) n : n <= delta x -> str_nth (nstr_to_str x) n = nstr_nth x n.
  Proof.
    revert n. induction x; simpl; intros [|n] L; auto.
  Qed.

  Lemma nstr_to_str_length (x: NStr X) : S(delta x) = | x |.
  Proof.
    induction x; simpl; auto.
  Qed.

  Lemma str_nth_nstr' (x: NStr X) n : n < |x| -> str_nth (nstr_to_str x) n = nstr_nth x n.
  Proof.
    intros L. apply str_nth_nstr. rewrite <-nstr_to_str_length in L. omega.
  Qed.

End StrToNStr.

Instance Dummy_nonempty X (x: Str X): nonempty x -> Dummy X.
Proof.
  intros N. destruct x.
  - now exfalso.
  - apply x.
Qed.

Hint Immediate Dummy_nonempty : typeclass_instances.

Arguments sing {X} a.
Arguments ncons {X} a x.

Section IndexAccess.

  Context {X:Type}.


  Lemma nstr_finIter_length (x:NStr X) n : | nstr_finIter x n | = (S n) * | x |.
  Proof.
    rewrite <-2nstr_to_str_length.
    induction n.
    - simpl. omega.
    - simpl delta. rewrite mult_succ_l, nstr_concat'_delta. omega.
  Qed.

End IndexAccess.

Section FlattenList.

  Context {X:Type}.

  Fixpoint flatten_list (L:list (list X)) :list X := match L with
    | [] => []
    | x::xs => x ++ (flatten_list xs)
  end.

  Lemma in_flatten_list_iff L x: x el (flatten_list L) <-> exists l, l el L /\ x el l.
  Proof.
    split.
    - intros E. induction L as [|l L].
      + now exfalso.
      + simpl in E. apply in_app_iff in E. destruct E as [E|E].
        * now exists l.
        * destruct (IHL E) as [l' [P Q]].
          exists l'. split; auto.
    - intros [l [P Q]]. induction L as [|l' L].
      + now exfalso.
      + destruct P as [P|P].
        * subst l'. simpl. auto.
        * simpl. auto.
  Qed.

End FlattenList.

Decidability of Quantification over Strings of Bounded Length

Given a decidable predicate on strings, existential and universal quantification over strings with a given maximum length is decidable. Therefore we build a list of all possible such strings. As a byproduct, we obtain constructive choice of strings with bounded length. This restriction is not necessary, as strings itself are countable, but suffices for application in this project.
Section NStrBoundedDelta.

  Context {X: finType}.

  Fixpoint nstr_of_delta n : list (NStr X) := match n with
     | 0 => map sing (elem X)
     | S n => flatten_list (map (fun x => map (fun a => ncons a x) (elem X)) (nstr_of_delta n))
  end.

  Fixpoint nstr_of_leq_delta n : list (NStr X) := match n with
     | 0 => nstr_of_delta 0
     | S n => (nstr_of_delta (S n)) ++ (nstr_of_leq_delta n)
  end.

  Lemma in_nstr_of_delta_iff n x: x el (nstr_of_delta n) <-> delta x = n.
  Proof.
    split.
    - revert x. induction n; intros x; simpl.
      + now intros [a [<- Q]] % in_map_iff.
      + intros [l [[y [<- Q2]] %in_map_iff Q]] % in_flatten_list_iff.
        apply in_map_iff in Q. destruct Q as [a [P P2]].
        subst x. simpl. f_equal. now apply IHn.
    - revert n. induction x; intros n; simpl.
      + intros E. subst n. simpl. apply in_map_iff. exists a; auto.
      + intros E. destruct n.
        * now exfalso.
        * apply in_flatten_list_iff. exists (map (fun a => ncons a x) (elem X)). split.
          -- apply in_map_iff. exists x. split; auto.
          -- apply in_map_iff. exists a. split; auto.
  Qed.

  Lemma in_nstr_of_leq_delta_iff n x : x el (nstr_of_leq_delta n) <-> delta x <= n.
  Proof.
    split.
    - revert x. induction n; intros x.
      + now intros <- % in_nstr_of_delta_iff.
      + intros [<- % in_nstr_of_delta_iff |E] % in_app_iff; auto.
    - revert x. induction n; intros x.
      + destruct x as [a|a x]; intros E.
        * now apply in_nstr_of_delta_iff.
        * now exfalso.
      + destruct x as [a|a x]; intros E; apply in_app_iff.
        * right. apply IHn. simpl. omega.
        * simpl in E. decide (delta x = n).
          -- subst n. left. now apply in_nstr_of_delta_iff.
          -- right. apply IHn. simpl. omega.
  Qed.

Decidability and Constructive Choice Results for Strings of given or bounded length.

  Section DecAndChoice.
    Variable (P: NStr X -> Prop).
    Context {decP: forall x, dec(P x)}.

    Global Instance dec_string_exists_fixed_length n: dec (exists x, delta x = n /\ P x).
    Proof.
      enough (dec (exists x, x el (nstr_of_delta n) /\ P x)) as [H|H].
      - left. destruct H as [x [ M%in_nstr_of_delta_iff H]]. firstorder.
      - right. intros [x [M %in_nstr_of_delta_iff Q]]. apply H. firstorder.
      - auto.
    Qed.

    Global Instance dec_string_exists_bounded_length n: dec (exists x, delta x <= n /\ P x).
    Proof.
      enough (dec (exists x, x el (nstr_of_leq_delta n) /\ P x)) as [H|H].
      - left. destruct H as [x [ M%in_nstr_of_leq_delta_iff H]]. firstorder.
      - right. intros [x [M %in_nstr_of_leq_delta_iff Q]]. apply H. firstorder.
      - auto.
    Qed.

    Lemma string_fixed_length_cc n : (exists x, delta x = n /\ P x) -> {x | delta x = n /\ P x}.
    Proof.
      intros H.
      enough ({x| x el (nstr_of_delta n) /\ P x}) as [x [L % in_nstr_of_delta_iff Q]] by firstorder.
      apply list_cc; auto. destruct H as [x [L%in_nstr_of_delta_iff Q]]. firstorder.
    Defined.


    Lemma string_bounded_length_cc n : (exists x, delta x <= n /\ P x) -> {x | delta x <= n /\ P x}.
    Proof.
      intros H.
      enough ({x| x el (nstr_of_leq_delta n) /\ P x}) as [x [L % in_nstr_of_leq_delta_iff Q]] by firstorder.
      apply list_cc; auto. destruct H as [x [L%in_nstr_of_leq_delta_iff Q]]. now exists x.
    Defined.

  End DecAndChoice.
  Section DecAndChoice'.

     Variable (P P': NStr X -> Prop).
    Context {decP: forall x, dec(P x)}.
    Context {decP': forall x, dec(P' x)}.

    Global Instance dec_string_exists_fixed_length' n: dec (exists x, (delta x = n /\ P x) /\ P' x).
    Proof.
      enough (dec (exists x, delta x = n /\ (P x /\ P' x))) as [D|D].
      - left. firstorder.
      - right. intros H. apply D. firstorder.
      - auto.
    Qed.

    Lemma string_fixed_length_cc' n : (exists x, (delta x = n /\ P' x) /\ P x) -> {x | (delta x = n /\ P' x) /\ P x}.
    Proof.
      intros H.
      enough ({x| delta x = n /\ P' x /\ P x}) as [x [L [Q1 Q2]]] by firstorder.
      apply string_fixed_length_cc; auto.
      firstorder.
    Defined.

  End DecAndChoice'.


End NStrBoundedDelta.

Duplicates in Strings over Finite Types

For every string over a finite type X whose length is larger than the cardinality of X we canb obtain two positions in the string containing the same element.

Section DuplicateInString.

  Context {X: finType}.
  Context {D: Dummy X}.

  Fixpoint occurences (x: Str X) : (X -> list nat) := match x with
     | [] => (fun a => [])
     | b::x => (fun a => if (decision (a = b))
                         then 0::(map S (occurences x a))
                         else (map S (occurences x a)))
  end.



  Lemma occurences_bound x a n : n el (occurences x a) -> n < |x|.
  Proof.
    revert n. induction x; intros n.
    - intros L. now exfalso.
    - simpl. destruct decision.
      + intros[<-|[m [<- Q]] %in_map_iff]; oauto.
        enough (m < |x|) by omega. now apply IHx.
      + intros [m [<- Q]] %in_map_iff.
        enough (m < |x|) by omega. now apply IHx.
  Qed.

  Lemma occurences_dupfree x a :dupfree (occurences x a).
  Proof.
    induction x.
    - constructor.
    - simpl. destruct decision.
      + constructor.
        * now intros [n [O Q]] % in_map_iff.
        * apply dupfree_map; auto.
      + apply dupfree_map; auto.
  Qed.

  Lemma occurences_correct x a n : n el (occurences x a) -> str_nth x n = a.
  Proof.
    revert n. induction x; intros n L.
    - now exfalso.
    - simpl in L. destruct n; simpl.
      + destruct decision; auto.
        exfalso. apply in_map_iff in L. now destruct L as [m [H _]].
      + destruct decision.
        * destruct L as [L|L].
          -- now exfalso.
          -- apply in_map_iff in L. destruct L as [m [P Q]].
             assert (m = n) by omega. subst m.
             now apply IHx.
        * apply in_map_iff in L. destruct L as [m [P Q]].
          assert (m = n) by omega. subst m.
          now apply IHx.
  Qed.

  Fixpoint sum_occurences x (l: list X) := match l with
    | [] => 0
    | a::l => |occurences x a| + (sum_occurences x l)
  end.

  Lemma occurences_all_instances x a: | occurences x a | = | filter (DecPred (fun b : X => a = b)) x |.
  Proof.
    induction x; auto.
    simpl. destruct decision; trivial_decision; simpl ; [f_equal |];
    rewrite map_length; apply IHx.
  Qed.

  Lemma occurences_all x : sum_occurences x (elem X) = |x|.
  Proof.
    enough (forall l, dupfree l -> sum_occurences x l = |filter (DecPred (fun a => a el l)) x|) as H.
    - specialize (H (elem X)). rewrite H, filter_unchanged; auto using dupfree_elements.
    - intros l H. induction H as [| a l N H IHH].
      + simpl. rewrite filter_empty; auto.
      + simpl. rewrite <-(filter_partition (P:=fun b => a = b)(Q:=fun b => b el l)( (fun x0 : X => @list_in_dec X x0 (a :: l) (@decide_eq X)))).
        * rewrite IHH. f_equal. apply occurences_all_instances.
        * intros b M [P Q]. now subst a.
  Qed.

  Lemma duplicates x : Cardinality X < |x| -> { i : nat & {j | i < j < |x| /\ str_nth x i = str_nth x j}}.
  Proof.
    intros M.
    decide (exists a, |occurences x a| > 1) as [H|H].
    - apply finType_cc in H; auto. destruct H as [a H].
      pose proof (occurences_bound (x:=x) (a:=a)) as HB.
      pose proof (occurences_correct (x:=x) (a:=a)) as HC.
      pose proof (occurences_dupfree x a) as HD.
      destruct (occurences x a) as [ | i [ | j l]] ; simpl in H; try (exfalso; omega).
      decide (i < j).
      + exists i, j. repeat split; oauto.
        rewrite 2HC; auto.
      + exists j, i.
        repeat split; oauto.
        * enough (i <> j) by omega. intros E. subst i. inversion HD. auto.
        * rewrite 2HC; auto.
    - exfalso. enough (sum_occurences x (elem X) <= Cardinality X) as H2.
      + pose proof (occurences_all x). omega.
      + enough (forall l, dupfree l -> sum_occurences x l <= |l|) as H3 by apply H3, dupfree_elements.
        intros l H2. induction H2 as [|b l].
        * simpl. omega.
        * simpl. enough (|occurences x b| <= 1) by omega.
          decide (| occurences x b | <= 1); auto.
          exfalso. apply H. exists b. omega.
  Qed.

End DuplicateInString.

Notation "! x" := (str_to_nstr x) (at level 90).