Module CoqAddOn

Miscellaneous extensions of "Coq" standard library

Require List.
Require Import Sorting.Permutation.
Import List.ListNotations.
Local Open Scope list_scope.

A "fixpoint" variant of "List.Forall" (in the style of "List.In")
Fixpoint Forall {A} (P: A -> Prop) (l: list A) : Prop :=
  match l with
  | [] => True
  | x::l' => P x /\ Forall P l'
  end.

Lemma Forall_monotone {A} (l: list A) (P Q: A -> Prop):
  Forall P l -> (forall x, P x -> Q x) -> Forall Q l.
Proof.
  induction l; simpl; intuition.
Qed.

Lemma Forall_ListForall {A} (l: list A) (P: A -> Prop):
  Forall P l <-> List.Forall P l.
Proof.
  constructor 1.
    - induction l; simpl; intuition.
    - induction 1; simpl; intuition.
Qed.

Lemma Forall_ListForIn {A} (l: list A) (P: A -> Prop):
  Forall P l <-> (forall x, List.In x l -> P x).
Proof.
  induction l; simpl; intuition (subst; auto).
Qed.

Lemma Forall_cons {A} (x : A) (l : list A) (P: A -> Prop): P x -> Forall P l -> Forall P (x :: l).
Proof.
  simpl; intuition.
Qed.

Lemma Forall_app {A} (l1 l2 : list A) (P: A -> Prop): Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2).
Proof.
  induction l1; simpl; intuition auto.
Qed.
Hint Resolve Forall_app.

Lemma Forall_Forall_cons {A} l1: forall a (P: A -> A -> Prop) (l2: list A),
   Forall (fun x => P x a) l1 -> Forall (fun x => Forall (P x) l2) l1 -> Forall (fun x => Forall (P x) (a::l2)) l1.
Proof.
  simpl; induction l1; simpl; intuition auto.
Qed.



Section FilterProp.

Variable A : Type.
Variable f : A -> bool.

Lemma Forall_negb_true_false (l: list A):
  Forall (fun x => negb (f x) = true) l -> Forall (fun x => (f x)=false) l.
Proof.
  intros; eapply Forall_monotone; eauto.
  simpl; intros x; case (f x); simpl; auto.
Qed.

Lemma Forall_false_negb_true (l: list A):
  Forall (fun x => (f x)=false) l -> Forall (fun x => negb (f x) = true) l.
Proof.
  intros; eapply Forall_monotone; eauto.
  simpl; intros x; case (f x); simpl; auto.
Qed.

Lemma filter_app l1 l2: List.filter f (l1++l2) = (List.filter f l1) ++ (List.filter f l2).
Proof.
  induction l1; simpl; auto.
  destruct (f a); simpl; congruence.
Qed.

Lemma filter_triv_true l: (Forall (fun x => f x = true) l) -> List.filter f l = l.
Proof.
  induction l; simpl; intuition auto.
  rewrite H0; simpl; congruence.
Qed.

Lemma filter_triv_false l: (Forall (fun x => f x = false) l) -> List.filter f l = [].
Proof.
  induction l; simpl; intuition auto.
  rewrite H0; simpl; congruence.
Qed.

Lemma filter_empty_false l: List.filter f l = [] -> (Forall (fun x => f x = false) l).
Proof.
  induction l; simpl; auto.
  case (f a); simpl; intuition discriminate.
Qed.


Local Hint Constructors Permutation.
Local Hint Resolve Permutation_sym Permutation_middle.
Lemma filter_split l: Permutation ((List.filter f l)++(List.filter (fun x => negb (f x)) l)) l.
Proof.
  induction l; simpl; auto.
  destruct (f a); simpl; auto.
  apply Permutation_sym.
  eapply Permutation_trans.
  2: eauto.
  auto.
Qed.

End FilterProp.



Additional lemmas on Q
Module Q.
  Require Import NArith.
  Require Import ZArith.
  Require Import QArith.


  Lemma PZMul: forall n1 n2 n3: positive, Zmult (Zpos n1) (Zpos (Pmult n2 n3)) = Zmult (Zpos (Pmult n1 n2)) (Zpos n3).
    intros n1 n2 n3; unfold Zmult; rewrite Pmult_assoc; trivial.
  Qed.

  Lemma Qplus_lt_compat: forall n1 n2 n3 n4: Q, Qlt n1 n2 -> Qlt n3 n4 -> Qlt (Qplus n1 n3) (Qplus n2 n4).
    unfold Qlt, Qplus.
    intros [n1 d1] [n2 d2] [n3 d3] [n4 d4].
    simpl.
    intros h1 h2.
    repeat ring_simplify.
    apply Zplus_lt_compat.

    rewrite (Pmult_comm d2 d4), (Pmult_comm d1 d3).
    repeat rewrite <- Zmult_assoc.
    rewrite (PZMul d3 d4 d2), (PZMul d4 d3 d1).
    rewrite (Zmult_comm (Zpos (Pmult d3 d4)) (Zpos d2)).
    rewrite (Zmult_comm (Zpos (Pmult d4 d3)) (Zpos d1)).
    repeat rewrite Zmult_assoc.
    rewrite (Pmult_comm d4 d3).
    apply Zmult_lt_compat_r;
      [ apply Zgt_lt; apply Zgt_pos_0 | assumption ].

    rewrite (Pmult_comm d2 d4), (Pmult_comm d1 d3).
    rewrite (Zmult_comm (Zpos (Pmult d4 d2)) n3), (Zmult_comm (Zpos (Pmult d3 d1)) n4).
    repeat rewrite <- Zmult_assoc.
    repeat rewrite <- PZMul.
    repeat rewrite Zmult_assoc.
    rewrite (Pmult_comm d2 d1).
    apply Zmult_lt_compat_r;
    [ apply Zgt_lt; apply Zgt_pos_0 | assumption ].
  Qed.
  Lemma Qplus_eqlt_compat: forall n1 n2 n3 n4: Q, n1 = n2 -> Qlt n3 n4 -> Qlt (Qplus n1 n3) (Qplus n2 n4).
    intros [n1 d1] [n2 d2] [n3 d3] [n4 d4] h1.
    rewrite h1.
    unfold Qlt, Qplus.
    simpl.
    intro h2.
    repeat ring_simplify.
    rewrite <- (Zmult_assoc n2 (Zpos d3) (Zpos (Pmult d2 d4))), <- (Zmult_assoc n2 (Zpos d4) (Zpos (Pmult d2 d3))).
    rewrite (Pmult_comm d2 d4), (Pmult_comm d2 d3).
    rewrite (PZMul d3 d4 d2), (PZMul d4 d3 d2).
    rewrite (Pmult_comm d4 d3).
    apply Zplus_lt_compat_l.
    rewrite (Zmult_comm (Zpos (Pmult d4 d2)) n3).
    rewrite <- Zmult_assoc.
    rewrite <- (PZMul d4 d2 d2).
    rewrite Zmult_assoc.
    rewrite (Pmult_comm d3 d2).
    rewrite (PZMul d2 d2 d3).
    rewrite <- (Zmult_assoc (Zpos (Pmult d2 d2)) (Zpos d3) n4).
    rewrite (Zmult_comm (Zpos (Pmult d2 d2)) (Zmult (Zpos d3) n4)).
    rewrite (Zmult_comm (Zpos d3) n4).
    apply Zmult_lt_compat_r;
    [ apply Zgt_lt; apply Zgt_pos_0 | assumption ].
  Qed.
End Q.

Module Qc.
  Require Import QArith.
  Require Import Qcanon.

  Lemma Qcplus_lt_compat: forall n1 n2 n3 n4: Qc,
      Qclt n1 n2 -> Qclt n3 n4 -> Qclt (Qcplus n1 n3) (Qcplus n2 n4).
    unfold Qcplus, Qclt, Q2Qc, this.
    intros [n1 nP1] [n2 nP2] [n3 nP3] [n4 nP4] h1 h2.
    repeat rewrite Qred_correct.
    apply Q.Qplus_lt_compat; assumption.
  Qed.
  Lemma Qcplus_eqlt_compat: forall n1 n2 n3 n4: Qc,
      n1 = n2 -> Qclt n3 n4 -> Qclt (Qcplus n1 n3) (Qcplus n2 n4).
    intros [n1 nP1] [n2 nP2] [n3 nP3] [n4 nP4] h1; rewrite h1.
    unfold Qcplus, Qclt, Q2Qc, this.
    repeat rewrite Qred_correct.
    apply Q.Qplus_eqlt_compat; trivial.
  Qed.
  Lemma Qcopp_lt_compat1: forall n1 n2: Qc,
                           Qclt n1 n2 -> Qclt (Qcopp n2) (Qcopp n1).
    intros n1 n2 h.
    apply (Qcplus_eqlt_compat (Qcopp n2) (Qcopp n2) n1 n2 eq_refl) in h.
    apply (Qcplus_eqlt_compat (Qcopp n1) (Qcopp n1) _ _ eq_refl) in h.
    rewrite (Qcplus_comm (Qcopp n2) n1) in h.
    rewrite (Qcplus_assoc (Qcopp n1) n1 (Qcopp n2)) in h.
    rewrite (Qcplus_comm (Qcopp n1) n1) in h.
    rewrite (Qcplus_comm (Qcopp n2) n2) in h.
    repeat rewrite Qcplus_opp_r in h.
    rewrite Qcplus_0_l, Qcplus_0_r in h.
    exact h.
  Qed.
  Lemma Qcopp_lt_compat2: forall n1 n2: Qc,
                            Qclt (Qcopp n1) (Qcopp n2) -> Qclt n2 n1.
    intros n1 n2 h.
    apply Qcopp_lt_compat1 in h.
    repeat rewrite Qcopp_involutive in h.
    exact h.
  Qed.
  Lemma Qcopp_lt_compat: forall n1 n2: Qc,
                           Qclt n1 n2 <-> Qclt (Qcopp n2) (Qcopp n1).
    exact (fun n1 n2 => conj (Qcopp_lt_compat1 n1 n2) (Qcopp_lt_compat2 n2 n1)).
  Qed.
  Lemma QcQLt: forall q1 q2: Q, Qlt q1 q2 <-> Qclt (Q2Qc q1) (Q2Qc q2).
    intros q1 q2.
    split;
      intro h.
    - apply Qclt_alt.
      unfold Qccompare.
      simpl.
      rewrite <- Qred_compare.
      assumption.
    - apply (proj1 (Qclt_alt _ _)) in h.
      unfold Qccompare in h.
      simpl in h.
      rewrite <- Qred_compare in h.
      assumption.
  Qed.
End Qc.

Require BinNums.
Require String.
Axiom posPr: BinNums.positive -> String.string.
Axiom posPrRaw: BinNums.positive -> String.string.
Axiom zPr: BinNums.Z -> String.string.
Axiom zPrRaw: BinNums.Z -> String.string.

Require List.
Import Ascii String.
Local Open Scope string_scope.

New line
Definition nl: string := String (ascii_of_nat 10%nat) EmptyString.

Append one character at the end of a string. This is really not an efficient way to build a string, build this will do for now.
Definition append1: string -> ascii -> string
  := fun s c => append s (String c EmptyString).

Concatenate the elements of a list of strings, separating each pair of elements by sep.
Fixpoint concat (sep: string) (l: list string): string
  := match l with
       | nil => EmptyString
       | cons h1 l1 =>
         match l1 with
           | nil => h1
           | cons h2 l2 => h1 ++ sep ++ (concat sep l1)
         end
     end.

Definition substStr: string -> list string -> string
  := fun s l =>
       match l with
         | List.nil => append s "[missing arg]"
         | List.cons h _ => append s h
       end.

Fixpoint sprintfAux (s: string): list string -> string -> string
  := fun l acc =>
       match s with
         | EmptyString => acc
         | String c s1 =>
           match ascii_dec "%"%char c with
             | left _ =>
               match s1 with
                 | EmptyString => append acc "[bad %_]"
                 | String c' s2 =>
                   match ascii_dec "s"%char c' with
                     | left _ => sprintfAux s2 (List.tl l) (substStr acc l)
                     | right _ =>
                   match ascii_dec "%"%char c' with
                     | left _ => sprintfAux s2 l (append1 acc c')
                     | right _ => sprintfAux s2 l (append acc "[bad %_]")
                   end
                   end
               end
             | right _ =>
           match ascii_dec "\"%char c with
             | left _ =>
               match s1 with
                 | EmptyString => append acc "[bad \_]"
                 | String c' s2 =>
                   match ascii_dec "n"%char c' with
                     | left _ => sprintfAux s2 l (append acc nl)
                     | right _ =>
                   match ascii_dec "\"%char c' with
                     | left _ => sprintfAux s2 l (append1 acc c')
                     | right _ => sprintfAux s2 l (append acc "[bad \_]")
                   end
                   end
               end
             | right _ => sprintfAux s1 l (append1 acc c)
           end
           end
       end.

Poor man's implementation of sprintf. It only recognizes only "%s" and "%%" specifications. For "%s" specification, a corresponding parameter is looked up in the list string argument. "\n" substrings are replaced by new line charaters. Use "\\" to output a backslash. Invalid arguments (e.g. bad specifications or wrong number of string arguments) lead to inline errors in the output string.
Definition sprintf: string -> list string -> string
  := fun s l => sprintfAux s l EmptyString.
Generated by coq2html