text:
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Import notations decidable_prop Psatz.
Require Export list_tools.

(** * Lists over a decidable set *)
Section dec_list.
  Context { A : Set } { dec_A : decidable_set A }.

  (** Boolean equality for lists *)
  Fixpoint equal_list l m :=
    match (l,m) with
    | ([],[]) => true
    | (a::l,b::m) => eqX a b && equal_list l m
    | _ => false
    end.

  Lemma equal_list_spec l m : reflect (l = m) (equal_list l m).
  Proof.
    apply iff_reflect;revert m;induction l as [|a l];intros [|b m];
    simpl;split;try reflexivity||discriminate;
    rewrite andb_true_iff,<-IHl.
    - intro h;inversion h;split;auto;apply eqX_refl.
    - intros (h&->);apply eqX_correct in h as ->;reflexivity.
  Qed.

  (** The set of lists of [A]s is decidable. *)
  Global Instance dec_list : decidable_set (list A).
  Proof. apply (Build_decidable_set equal_list_spec). Qed.

  (** Boolean predicate testing whether an element belongs to a list. *)
  Definition inb (n : A) l := existsb (eqX n) l.

  Lemma inb_spec n l : inb n l = true <-> n ∈ l.
  Proof.
    case_eq (inb n l);intro E;unfold inb in *.
    - apply existsb_exists in E as (y&I&E).
      apply eqX_correct in E as ->;tauto.
    - rewrite <- not_true_iff_false, existsb_exists in E;split.
      -- discriminate.
      -- intro I;exfalso;apply E;eexists;split;[eauto|];apply eqX_refl.
  Qed.

  Lemma inb_false n l : inb n l = false <-> ~ n ∈ l.
  Proof. rewrite <- inb_spec,not_true_iff_false;reflexivity. Qed.

  (** This boolean predicate allows us to use the excluded middle with the predicate [In]. *)
  Lemma inb_dec n l : { inb n l = true /\ n ∈ l } + { inb n l = false /\ ~ n ∈ l }.
  Proof.
    case_eq (inb n l);intro E;[left|right];rewrite <- inb_spec;auto.
    split;auto;rewrite E;discriminate.
  Qed.

  Lemma In_dec (n : A) l : { n ∈ l } + { ~ n ∈ l }.
  Proof.
    case_eq (inb n l);intro E;[left|right];rewrite <- inb_spec,E;auto.
  Qed.
  (* begin hide *)
  Ltac case_in a l :=
    let I := fresh "I" in
    let E := fresh "E" in
    destruct (inb_dec a l) as [(E&I)|(E&I)];
    try rewrite E in *;clear E.
  (* end hide *)

  (** Boolean function implementing containment test. *)
  Definition inclb (a b : list A) :=
    forallb (fun x => inb x b) a.

  Lemma inclb_correct a b : inclb a b = true <-> a ⊆ b.
  Proof.
    unfold incl,inclb;rewrite forallb_forall.
    setoid_rewrite inb_spec;intuition.
  Qed.

  (** Boolean function testing for equivalence of lists. *)
  Definition equivalentb l1 l2 := inclb l1 l2 && inclb l2 l1.

  Lemma equivalentb_spec l1 l2 : equivalentb l1 l2 = true <-> l1 ≈ l2.
  Proof.
    unfold equivalentb;rewrite andb_true_iff,inclb_correct,inclb_correct.
    split.
    - intros (e1&e2);apply incl_PartialOrder;split;tauto.
    - intros ->;split;reflexivity.
  Qed.

  (** If [u=u1++a::u2], we call the triple [(u1,u2)] an [a]-decomposition of [u] if [a] does not appear in [u1]. *)

  (** If [a] is in [l], then there exists an [a]-decomposition of [l]. *)
  Lemma decomposition (a : A) l :
    a ∈ l <-> exists l1 l2, l = l1 ++ a :: l2 /\ ~ a ∈ l1.
  Proof.
    induction l as [|b l];simpl;auto.
    - split;try tauto.
      intros (?&?&?&_).
      apply app_cons_not_nil in H;tauto.
    - destruct_eqX a b.
      + split;auto.
        intros _;exists [],l;split;auto.
      + rewrite IHl;clear IHl;split.
        * intros [<-|(l1&l2&->&h)];[tauto|].
          exists (b::l1),l2;split;auto.
          intros [->|I];tauto.
        * intros (l1&l2&E&I);right.
          destruct l1 as [|c l1].
          -- simpl in *;inversion E;subst;tauto.
          -- simpl in E;inversion E;subst;clear E.
             exists l1,l2;split;auto.
             intro;apply I;now right.
  Qed.

  (** Decompositions are unique.*)
  Lemma decomp_unique (a:A) u1 u2 v1 v2 :
    u1++(a::u2) = v1++a::v2 -> ~ In a v1 -> ~ In a u1 -> u1 = v1 /\ u2 = v2.
  Proof.
    intros E I1 I2;destruct (Levi_strict E) as [(->&E2)|(c&w&[(->&E2)|(->&E2)])];
      inversion E2;subst;clear E2;auto.
    - exfalso;apply I2,in_app_iff;right;left;auto.
    - exfalso;apply I1,in_app_iff;right;left;auto.
  Qed.

  Lemma decomp_unambiguous (u1 u2 v1 v2 : list A) a b :
    u1++a::u2 = v1++b::v2 -> ~ In a v1 -> ~ In b u1 -> u1 = v1 /\ a=b /\ u2 = v2.
  Proof.
    intros E Ia Ib;destruct (Levi_strict E) as [(->&E2)|(c&w&[(->&E2)|(->&E2)])].
    - inversion E2;auto.
    - exfalso;apply Ib;rewrite in_app_iff;simpl.
      inversion E2;auto.
    - exfalso;apply Ia;rewrite in_app_iff;simpl.
      inversion E2;auto.
  Qed.

  (** [{{l}}] is a list containing the same elements as [l], but without duplication. *)
  Definition undup l :=
    fold_right (fun a acc =>
                  if inb a acc
                  then acc
                  else a::acc)
               nil
               l.

  Notation " {{ l }} " := (undup l) (at level 0).

  (** [{{l}}] is shorter than [l]. *)
  Lemma undup_length l : ⎢{{l}}⎥ <= ⎢l⎥ .
  Proof. induction l;rsimpl; [|destruct (inb a _);rsimpl];lia. Qed.

  (** [{{l}}] contains the same elements as [l]. *)
  Lemma In_undup a l: a ∈ {{l}} <-> a ∈ l.
  Proof.
    revert a; induction l;simpl;auto;try tauto.
    intro b;case_in a {{l}};simpl;rewrite IHl in *;try tauto.
    destruct_eqX a b;tauto.
  Qed.
  (*begin hide *)
  Ltac simpl_In :=
    repeat rewrite in_app_iff
    || rewrite <- In_rev
    || rewrite In_undup
    || rewrite filter_In.
  Tactic Notation "simpl_In" "in" hyp(h) :=
    repeat rewrite in_app_iff in h
    || rewrite <- In_rev in h
    || rewrite In_undup in h
    || rewrite filter_In in h.
  Tactic Notation "simpl_In" "in" "*" :=
    repeat rewrite in_app_iff in *
    || rewrite <- In_rev in *
    || rewrite In_undup in *
    || rewrite filter_In in *.
  (* end hide *)

  (** Put differently, [{{l}}] is equivalent to [l]. *)
  Lemma undup_equivalent l : {{l}} ≈ l.
  Proof. intros x;apply In_undup. Qed.

  (** The [{{}}] operator always produces a duplication free list. *)
  Lemma NoDup_undup l : NoDup {{l}}.
  Proof.
    induction l;simpl;auto using NoDup_nil.
    case_in a {{l}};auto using NoDup_cons.
  Qed.

  (** The [{{}}] operator doesn't change duplication free lists. *)
  Lemma NoDup_undup_eq l : NoDup l -> l = {{l}}.
  Proof.
    induction l;simpl;auto.
    intro h;apply NoDup_cons_iff in h as (I&h).
    apply IHl in h as <-;case_in a l;tauto.
  Qed.

  (** A list is without duplication if and only if its mirror is duplication free. *)
  Lemma NoDup_rev {X:Set} (l : list X) : NoDup l <-> NoDup (rev l).
  Proof.
    induction l;simpl;firstorder.
    - apply NoDup_cons_iff in H1 as (I&h1).
      apply NoDup_app;firstorder;simpl.
      + simpl_In in *;intros [->|?];tauto.
      + apply NoDup_cons;firstorder;apply NoDup_nil.
    - apply NoDup_remove in H1 as (h1&h2);rewrite app_nil_r in *;apply H0 in h1.
      simpl_In in *;apply NoDup_cons;auto.
  Qed.

  (** [{{}}] preserves both [⊆] and [≈]. *)
  Global Instance undup_incl_Proper : Proper (@incl A ==> @incl A) undup.
  Proof. intros l m I x;simpl_In;auto. Qed.
  Global Instance undup_equivalent_Proper : Proper (@equivalent A ==> @equivalent A) undup.
  Proof. intros l m I x;simpl_In;auto. Qed.

  (** If [l] is contained in [m] and doesn't contain duplicates, then it must be shorter than [m]. *)
  Lemma NoDup_length (l m : list A) :
    l ⊆ m -> NoDup l -> ⎢l⎥ <= ⎢m⎥ .
  Proof.
    revert m;induction l;rsimpl;intros m E ND.
    - lia.
    - cut (⎢l⎥ <= ⎢(fun x=> negb (x=?=a)) :> m⎥).
      + intro L;eapply PeanoNat.Nat.le_succ_l,PeanoNat.Nat.le_lt_trans;
          [apply L|].
        assert (Ia : a ∈ m) by (apply E;now left);revert Ia;clear.
        induction m as [|b m];simpl;[tauto|].
        intros [->|Ia].
        * rewrite eqX_refl;rsimpl;auto.
          apply PeanoNat.Nat.lt_succ_r,filter_length.
        * apply IHm in Ia;destruct_eqX b a;rsimpl;lia.
      + apply NoDup_cons_iff in ND as (Ia&ND).
        apply IHl;auto.
        rewrite <- E;simpl;rewrite eqX_refl;simpl.
        intro x;simpl_In; rewrite negb_true_iff,eqX_false.
        intros I;split;auto.
        intros ->;tauto.
  Qed.

  (** [l] is a fixpoint of [map f] if and only if [{{l}}] is a fixpoint of the same list homomorphism [map f]. *)
  Lemma map_undup_id (l : list A) (f : A -> A) :
    map f l = l <-> map f {{l}} = {{l}}.
  Proof.
    repeat rewrite map_eq_id.
    setoid_rewrite In_undup;tauto.
  Qed.

  (** If [f] is injective, [map f] and [{{}}] commute. *)
  Lemma map_undup_inj (l : list A) (f : A -> A) :
    (forall x y, f x = f y -> x = y) -> map f {{l}} = {{map f l}}.
  Proof.
    intro hp;induction l;auto.
    simpl;case_in a {{l}};case_in (f a) {{map f l}};simpl;rewrite IHl;auto;exfalso.
    - apply I0,In_undup,in_map_iff;exists a;simpl_In in I;tauto.
    - apply I;simpl_In in *.
      apply in_map_iff in I0 as (y&Ey&Iy);apply hp in Ey as ->;auto.
  Qed.

  (** [NoDup] is a decidable property. *)
  Definition NoDupb l := l =?= {{l}}.

  Lemma NoDupb_NoDup l : NoDupb l = true <-> NoDup l.
  Proof.
    unfold NoDupb;rewrite eqX_correct;split.
    + intros ->;apply NoDup_undup.
    + apply NoDup_undup_eq.
  Qed.

  (** Remove an element from a list. *)
  Definition rm (a : A) l := (fun x => negb (a=?=x)) :> l.
  Notation " l ∖ a " := (rm a l) (at level 50).

  Lemma rm_In b a l : b ∈ l ∖ a <-> b ∈ l /\ a<>b.
  Proof. unfold rm;rewrite filter_In,negb_true_iff,eqX_false;tauto. Qed.

  Lemma rm_equiv a l : a ∈ l -> l ≈ a::(l ∖ a).
  Proof. intros I x;simpl;rewrite rm_In;destruct_eqX a x;tauto. Qed.

  Global Instance rm_equivalent_Proper a : Proper ((@equivalent A)==> (@equivalent A)) (rm a).
  Proof. apply filter_equivalent_Proper. Qed.

  Global Instance rm_incl_Proper a : Proper ((@incl A)==> (@incl A)) (rm a).
  Proof. apply filter_incl_Proper. Qed.

  Lemma rm_notin a l : ~ a ∈ l -> l ∖ a = l.
  Proof.
    unfold rm;intro I.
    erewrite filter_ext_In;[apply filter_true|].
    intros b Ib.
    apply eq_true_iff_eq;split;[tauto|].
    intros _;apply negb_true_iff,eqX_false.
    intros ->;tauto.
  Qed.

  (** Remove the first occurrence of an element from a list. *)

  Fixpoint rmfst (a : A) l :=
  match l with
  | [] => []
  | b::l => if a=?=b then l else b::(rmfst a l)
  end.
  Notation " l ⊖ a " := (rmfst a l) (at level 50).

  Lemma rmfst_notin a l : ~ a ∈ l -> l ⊖ a = l.
  Proof.
    induction l;simpl;auto.
    intros N;simpl.
    destruct_eqX a a0.
    - exfalso;apply N;tauto.
    - f_equal;apply IHl;intro;tauto.
  Qed.

  Lemma rmfst_in a l1 l2 : ~ a ∈ l1 -> (l1 ++ a :: l2) ⊖ a = l1++l2.
  Proof.
    induction l1;simpl;auto.
    - rewrite eqX_refl;auto.
    - intros N;destruct_eqX a a0.
      + exfalso;apply N;tauto.
      + f_equal;apply IHl1;tauto.
  Qed.

  (** [l ⊖ a] is contained in the list [l]. *)
  Lemma rmfst_decr a l : l ⊖ a ⊆ l.
  Proof.
    case_in a l.
    - apply decomposition in I as (?&?&->&I).
      rewrite rmfst_in;auto;intro;simpl_In;simpl;tauto.
    - rewrite rmfst_notin;auto;reflexivity.
  Qed.

  (** The operation [rmfst] commutes with itself. *)
  Lemma rmfst_comm (l : list A) a b : (l ⊖ a) ⊖ b = (l ⊖ b) ⊖ a.
  Proof.
    induction l as [|c l];simpl;auto.
    destruct_eqX a c;subst.
    - destruct_eqX b c;auto.
      simpl;rewrite eqX_refl;reflexivity.
    - simpl;destruct_eqX b c;auto.
      simpl;apply eqX_false in N as ->.
      rewrite IHl;reflexivity.
  Qed.

  (** If we try to remove [a] from [l++m], one of three things may happen:
      - [a] appears in [l], so we obtain [(l⊖ a)++m];
      - [a] appears in [m] but not in [l], so we obtain [l++(m⊖ a)];
      - [a] does not appear in [l] or [m], so we obtain [l++m].
   *)
  Lemma rmfst_app_dec (l m:list A) a :
    (exists l1 l2, l = l1++a::l2 /\ ~ a ∈ l1 /\ (l++m) ⊖ a = l1++l2++m)
    \/ (exists m1 m2, m = m1++a::m2 /\ ~ a ∈ (l++m1) /\ (l++m) ⊖ a = l++m1++m2)
    \/ (~ a ∈ (l++m) /\ (l++m) ⊖ a = l++m).
  Proof.
    case_in a l.
    - left;apply decomposition in I as (l1&l2&->&I).
      exists l1,l2;repeat split;auto.
      rewrite app_ass;apply rmfst_in;auto.
    - case_in a m.
      + right;left;apply decomposition in I0 as (m1&m2&->&I0).
        exists m1,m2;simpl_In;repeat split;try tauto.
        repeat rewrite <-app_ass;apply rmfst_in;simpl_In;tauto.
      + right;right;rewrite rmfst_notin;simpl_In;tauto.
  Qed.

  (** This lemma highlights the existence of a list [l1-l2]: the list [m] shown to exist here is such that it contains no elements from [l1], but concatenating [l1] and [m] yields a list equivalent to [l1++l2]. Furthermore, we produce [m] without inserting any duplicates. *)
  Lemma split_app_unambiguous (l1 l2 : list A) :
    exists m, l1++l2 ≈ l1++m /\ NoDup m /\ (forall a, a ∈ m -> ~ a ∈ l1).
  Proof.
    induction l2 as [|b l];simpl.
    - exists [];repeat split;try tauto.
      apply NoDup_nil.
    - destruct IHl as (m&Em&nd&F).
      case_in b (l1++m).
      + exists m;split;[|split];try assumption.
        rewrite <- Em;clear F nd.
        intro;simpl_In in *;firstorder subst.
        * tauto.
        * cut (x∈(l1++l));[simpl_In;tauto|].
          rewrite Em;simpl_In;tauto.
      + exists (b::m);split;[|split].
        * transitivity (b::l1++l);[intro;repeat (simpl;simpl_In);tauto|].
          transitivity (b::l1++m);[|intro;repeat (simpl;simpl_In);tauto].
          rewrite Em;reflexivity.
        * apply NoDup_cons;[|assumption].
          intro I';apply I;simpl_In;tauto.
        * intros a [<-|Ia].
          -- intro Ib;apply I;simpl_In;tauto.
          -- apply F,Ia.
  Qed.

  (** Sometimes we will need to count the number of occurrences of a particular element in a given list. *)
  Notation nb a l := ⎢eqX a :> l⎥.

  (** An equivalent (but slightly less convenient) function was defined in the standard library. *)
  Lemma nb_count_occ (a : A) l : nb a l = count_occ X_dec l a.
  Proof.
    induction l;simpl;auto.
    destruct_eqX a0 a;rsimpl;auto.
    destruct_eqX a a0;subst;rsimpl;tauto.
  Qed.

  (** For convenience, we translate all the lemmas regarding [count_occ] in terms of [nb]. *)
  Lemma nb_nil (x : A) : nb x [] = 0.
  Proof. rewrite nb_count_occ;apply count_occ_nil. Qed.

  Lemma nb_In l (x : A) : x ∈ l <-> nb x l > 0.
  Proof. rewrite nb_count_occ;apply count_occ_In. Qed.

  Lemma nb_not_In (l : list A) (x : A): ~ x ∈ l <-> nb x l = 0.
  Proof. rewrite nb_count_occ;apply count_occ_not_In. Qed.

  Lemma NoDup_nb (l : list A) : NoDup l <-> (forall x : A, nb x l <= 1).
  Proof. setoid_rewrite nb_count_occ;apply NoDup_count_occ. Qed.

  Lemma nb_inv_nil (l : list A) : (forall x : A, nb x l = 0) <-> l = [].
  Proof. setoid_rewrite nb_count_occ;apply count_occ_inv_nil. Qed.

  Lemma nb_cons_neq (l : list A) (x y : A) : x <> y -> nb y (x :: l) = nb y l.
  Proof. repeat rewrite nb_count_occ;apply count_occ_cons_neq. Qed.

  Lemma nb_cons_eq (l : list A) (x y : A) : x = y -> nb y (x :: l) = S (nb y l).
  Proof. repeat rewrite nb_count_occ;apply count_occ_cons_eq. Qed.

  Lemma NoDup_nb' (l : list A) : NoDup l <-> (forall x : A, x ∈ l -> nb x l = 1).
  Proof. setoid_rewrite nb_count_occ;apply NoDup_count_occ'. Qed.

  (** If [l] is contained in [m] and if [m] has no duplicates, then the length of [l] can be obtained by summing over [m] the function that maps [a] to the number of occurrences of [a] in [l]. *)
  Lemma length_sum_filter l m:
    l ⊆ m -> NoDup m -> ⎢l⎥ = sum (fun a => nb a l) m.
  Proof.
    induction l.
    - simpl;intros.
      induction m;simpl;auto.
      apply IHm.
      + intro;simpl;tauto.
      + apply NoDup_cons_iff in H0;tauto.
    - intros I N.
      assert (IH : l ⊆ m) by (intros x h;apply I;now right).
      apply IHl in IH;auto;clear IHl.
      replace ⎢a::l⎥ with (S ⎢l⎥) by reflexivity.
      rewrite IH;clear IH.
      assert (Ia : a ∈ m) by (apply I;now left).
      apply in_split in Ia as (m1&m2&->).
      repeat rewrite sum_app.
      rsimpl;rewrite (@sum_ext_In _ _ (fun b =>  nb b (a::l))),
             (@sum_ext_In _ _ (fun b => nb b (a::l)) m2).
      + simpl;rewrite eqX_refl;rsimpl;lia.
      + intros;rsimpl.
        destruct_eqX x a;subst;auto.
        exfalso;apply NoDup_remove_2 in N.
        apply N,in_app_iff;tauto.
      + intros;simpl.
        destruct_eqX x a;subst;auto.
        exfalso;apply NoDup_remove_2 in N.
        apply N,in_app_iff;tauto.
  Qed.

  Lemma sum_incr_0_left f (l m : list A) :
    (forall x, ~ x ∈ l -> f x = 0) -> sum f {{l}} = sum f {{m++l}}.
  Proof.
    intros;induction m;simpl.
    - reflexivity.
    - case_in a {{m++l}}.
      + assumption.
      + rewrite IHm.
        simpl;rewrite H;[lia|].
        intro I';apply I;simpl_In;tauto.
  Qed.

  Lemma sum_incr_0_right f (l m : list A) :
    (forall x, ~ x ∈ l -> f x = 0) -> sum f {{l}} = sum f {{l++m}}.
  Proof.
    intros h;rewrite (sum_incr_0_left m h).
    apply sum_eq_ND.
    - rewrite app_comm;reflexivity.
    - apply NoDup_undup.
    - apply NoDup_undup.
  Qed.

    (** A list [m] appears in [shuffles l] exactly when for every [a:A] there are as may occurrences of [a] in [l] as in [m]. *)
  Lemma shuffles_spec (m l : list A) : m ∈ shuffles l <-> forall a, nb a l = nb a m.
  Proof.
    revert m;induction l as [|b l];intros m;simpl.
    - split.
      + intros [<-|F];[|tauto].
        intro a;reflexivity.
      + destruct m as [|c m];[tauto|].
        intros h;simpl.
        pose proof (h c) as e;revert e.
        simpl;simpl_beq;simpl.
        discriminate.
    - rewrite in_flat_map;setoid_rewrite IHl;setoid_rewrite insert_spec;split.
      + intros (l'&h&l1&l2&->&->) a.
        pose proof (h a) as e.
        rewrite filter_app in *;rsimpl in *.
        clear IHl h;destruct_eqX a b;rsimpl;lia.
      + intros h.
        exists (m ⊖ b);case_in b m.
        * apply decomposition in I as (l1&l2&->&I).
          rewrite rmfst_in;auto;split.
          -- intros a;pose proof (h a) as e;revert e;clear.
             destruct_eqX a b;simpl.
             ++ repeat rewrite filter_app.
                repeat rewrite app_length in *;simpl.
                simpl_beq;rsimpl.
                lia.
             ++ repeat rewrite filter_app.
                repeat rewrite app_length in *;simpl.
                simpl_beq;simpl.
                lia.
          -- eauto.
        * pose proof (h b) as e;revert e.
          simpl_beq;simpl.
          apply nb_not_In in I as ->.
          rewrite <- SizeLength;simpl;discriminate.
  Qed.

  (** Intersection of finite sets *)
  Definition intersect u v := (fun a => inb a v) :> u.
  Infix " ∩ " := intersect (at level 50).

  Lemma intersect_spec u v a : a ∈ u ∩ v <-> a ∈ u /\ a ∈ v.
  Proof. unfold intersect;simpl;simpl_In;rewrite inb_spec;tauto. Qed.

  Global Instance intersect_proper_incl :
    Proper (@incl _ ==> @incl _ ==> @incl _) intersect.
  Proof.
    intros l1 l2 el m1 m2 em a.
    repeat rewrite intersect_spec.
    intros;split;[apply el|apply em];tauto.
  Qed.

  Global Instance intersect_proper :
    Proper (@equivalent _ ==> @equivalent _ ==> @equivalent _) intersect.
  Proof.
    intros l1 l2 el m1 m2 em a.
    repeat rewrite intersect_spec.
    rewrite el,em;tauto.
  Qed.

  Lemma interect_nil u : u ∩ [] = [].
  Proof. apply incl_l_nil;intro;rewrite intersect_spec;simpl;tauto. Qed.

  Lemma intersect_app_l u v w : (u++v) ∩ w = (u∩w)++(v∩w).
  Proof. induction u;simpl;[|rewrite IHu;case_in a w];reflexivity. Qed.

  Lemma intersect_app_r u v w : u∩(v++w) ≈ (u∩v)++(u∩w).
  Proof. intro;repeat simpl_In||rewrite intersect_spec;tauto. Qed.

  Lemma intersect_ass u v w : u ∩ (v ∩ w) = (u ∩ v) ∩ w.
  Proof.
    induction u;simpl;[reflexivity|rewrite IHu].
    case_in a v;simpl.
    + case_in a w;case_in a (v∩w);simpl.
      * reflexivity.
      * exfalso;apply I1,intersect_spec;tauto.
      * exfalso;apply intersect_spec in I1;tauto.
      * reflexivity.
    + case_in a (v∩w);simpl.
      * exfalso;apply intersect_spec in I0;tauto.
      * reflexivity.
  Qed.
  Lemma intersect_comm u v : u ∩ v ≈ v ∩ u.
  Proof. intro a;repeat rewrite intersect_spec; tauto. Qed.

  Lemma intersect_meet_l u v : u ⊆ v -> u ∩ v = u.
  Proof.
    induction u as [|a u];intros huv;[reflexivity|].
    simpl;case_in a v.
    - rewrite IHu;[reflexivity|].
      intros b hb;apply huv;now right.
    - exfalso;apply I,huv;now left.
  Qed.

  Lemma intersect_incl u v : u ∩ v ⊆ u.
  Proof. intro a;rewrite intersect_spec;tauto. Qed.

  (** Difference of finite sets *)
  Definition difference u v := (fun a => negb (inb a v)) :> u.
  Infix " − " := difference (at level 50).

  Lemma difference_spec u v a : a ∈ u − v <-> a ∈ u /\ ~ a ∈ v.
  Proof.
    unfold difference;simpl;simpl_In.
    rewrite negb_true_iff,<-not_true_iff_false,inb_spec;tauto.
  Qed.

  Global Instance difference_proper :
    Proper (@equivalent _ ==> @equivalent _ ==> @equivalent _) difference.
  Proof.
    intros l1 l2 el m1 m2 em a.
    repeat rewrite difference_spec.
    rewrite el,em;reflexivity.
  Qed.

  Global Instance difference_proper_inf :
    Proper (@incl _ ==> Basics.flip (@incl _) ==> @incl _) difference.
  Proof.
    intros l1 l2 el m1 m2 em a.
    repeat rewrite difference_spec.
    rewrite el,em;tauto.
  Qed.

  Remark difference_right_subs u v w : u ≈ v -> w − u = w − v.
  Proof.
    intros e;induction w as [|a w];[reflexivity|].
    simpl;case_in a u;case_in a v;simpl;
      rewrite (e a) in *;rewrite IHw;reflexivity||tauto.
  Qed.

  Lemma difference_app_l u v w : (u++v)−w = (u−w)++(v−w).
  Proof.
    now induction u as [|a u];[|simpl;case_in a w;simpl;rewrite IHu].
  Qed.
  Lemma difference_app_r u v w : u−(v++w) ≈ (u−v)∩(u−w).
  Proof.
    intro a;repeat rewrite difference_spec
            ||rewrite intersect_spec||simpl_In.
    tauto.
  Qed.
  Lemma difference_inter_r u v w : u−(v∩w) ≈ (u−v)++(u−w).
  Proof.
    intro a;repeat rewrite difference_spec
            ||rewrite intersect_spec||simpl_In.
    case_in a v;tauto.
  Qed.
  Lemma difference_inter_l u v w : (u∩v)−w ≈ (u−w)∩(v−w).
  Proof.
    intro a;repeat rewrite difference_spec
            ||rewrite intersect_spec||simpl_In;tauto.
  Qed.
  Lemma difference_nil u : u − [] = u.
  Proof. now induction u as [|a u];simpl;[|rewrite IHu]. Qed.

  Lemma difference_incl u v : u − v ⊆ u.
  Proof. intro a;rewrite difference_spec;tauto. Qed.

  Lemma difference_intersect u v : v ∩ (u − v) = [].
  Proof.
    apply incl_l_nil;intro;rewrite intersect_spec,difference_spec.
    simpl;tauto.
  Qed.

End dec_list.
Notation " l ∖ a " := (rm a l) (at level 50).
Notation " l ⊖ a " := (rmfst a l) (at level 50).
Notation nb a l := ⎢eqX a :> l⎥.
Notation " {{ l }} " := (undup l) (at level 0).
Infix " ∩ " := intersect (at level 50).
  Infix " − " := difference (at level 50).

(* begin hide *)
Ltac case_in a l :=
  let I := fresh "I" in
  let E := fresh "E" in
  destruct (inb_dec a l) as [(E&I)|(E&I)];
  try rewrite E in *;clear E.
Lemma in_cons_iff {A} (l : list A) a b :
  a ∈ (b::l) <-> b = a \/ a ∈ l.
Proof. simpl;tauto. Qed.
Ltac simpl_In :=
  repeat rewrite in_app_iff
  || rewrite in_cons_iff
  || rewrite <- In_rev
  || rewrite In_undup
  || rewrite filter_In.
Tactic Notation "simpl_In" "in" hyp(h) :=
  repeat (rewrite in_app_iff in h)
  || (rewrite in_cons_iff in h)
  || (rewrite <- In_rev in h)
  || (rewrite In_undup in h)
  || (rewrite filter_In in h).
Tactic Notation "simpl_In" "in" "*" :=
  repeat (rewrite in_app_iff in * )
  || (rewrite in_cons_iff in * )
  || (rewrite <- In_rev in * )
  || (rewrite In_undup in * )
  || (rewrite filter_In in * ).
(* end hide *)

Lemma nb_map {A B :Set} `{decidable_set A,decidable_set B} (f : A -> B) :
  (forall x1 x2 : A, f x1 = f x2 -> x1 = x2) ->
  forall (x : A) (l : list A), nb x l = nb (f x) (map f l).
Proof. setoid_rewrite nb_count_occ;apply count_occ_map. Qed.

Lemma rmfst_flip {A B : Set} `{decidable_set A,decidable_set B} (s : list (A*B)) a b :
  s` ⊖ (a,b) = (s ⊖ (b,a))`.
Proof.
  case_in (b,a) s.
  - rewrite decomposition in I;destruct I as (s1&s2&->&I).
    rewrite rmfst_in;auto.
    rewrite flip_app;simpl.
    rewrite rmfst_in,flip_app;auto.
    rewrite In_flip;apply I.
  - rewrite rmfst_notin,rmfst_notin;auto.
    rewrite In_flip;apply I.
Qed.

(** [insert] commutes with [map]. *)
Lemma insert_map {A B : Set} `{decidable_set A,decidable_set B} :
  forall (f : A -> B) l a, insert (f a) (map f l) = map (map f) (insert a l).
Proof.
  intro f;induction l as [|b l];intro a;simpl.
  - reflexivity.
  - rewrite IHl,map_map,map_map.
    f_equal.
Qed.

(** [shuffles] commutes with [map]. *)
Lemma shuffles_map {A B : Set} `{decidable_set A,decidable_set B} :
  forall (f : A -> B) l, shuffles (map f l) = map (map f) (shuffles l).
Proof.
  intro f;induction l as [|a l];simpl.
  - reflexivity.
  - rewrite IHl,flat_map_concat_map,flat_map_concat_map.
    rewrite map_map,concat_map,map_map.
    f_equal;apply map_ext.
    intros;apply insert_map.
Qed.

Global Instance DecidableProp_In (A : Set) (x : A) l :
  decidable_set A -> DecidableProp (x ∈ l).
Proof. intro;case_in x l;[left|right];assumption. Qed.
Global Instance DecidableProp_Incl (A : Set) (l m : list A) :
  decidable_set A -> DecidableProp (l ⊆ m).
Proof.
  intro;case_eq (inclb l m);intro h;[left|right];
    revert h;[|rewrite <- not_true_iff_false];rewrite inclb_correct;tauto.
Qed.
Global Instance DecidableProp_Equiv (A : Set) (l m : list A) :
  decidable_set A -> DecidableProp (l ≈ m).
Proof.
  intro;case_eq (equivalentb l m);intro h;[left|right];
    revert h;[|rewrite <- not_true_iff_false];rewrite equivalentb_spec;tauto.
Qed.

author: monstrencage

repo: obs-alg-proofs


text:
(** * Example of an accumulator *)
Require Import Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq Ssreflect.fintype Ssreflect.tuple Ssreflect.ssrfun.
Require Import x86proved.x86.procstate x86proved.x86.procstatemonad x86proved.bitsops x86proved.bitsprops x86proved.bitsopsprops.
Require Import x86proved.spred x86proved.opred x86proved.septac x86proved.spec x86proved.obs x86proved.x86.basic x86proved.x86.basicprog x86proved.x86.program x86proved.x86.macros.
Require Import x86proved.x86.instr x86proved.x86.instrsyntax x86proved.x86.instrcodec x86proved.x86.instrrules x86proved.reader x86proved.pointsto x86proved.cursor.
Require Import x86proved.spectac x86proved.basicspectac.
Require Import x86proved.common_tactics x86proved.chargetac x86proved.common_definitions.
Require Import x86proved.x86.ioaction.
Require Coq.Lists.Streams.
Require Import Coq.Setoids.Setoid.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Generalizable All Variables.

Local Open Scope instr_scope.

Local Ltac t_accum' coq_test__is_finished fin_tac :=
  idtac;
  match goal with
    | _ => done
    | _ => evar_safe_syntax_unify_reflexivity
    | [ H : ?x = ~~?x |- _ ] => by destruct (@Bool.no_fixpoint_negb x (symmetry H))
    | [ H : ~~?x = ?x |- _ ] => by destruct (@Bool.no_fixpoint_negb x H)
    | [ H : is_true (?x == ?y) |- _ ] => move/eqP in H
    | [ H : context[?x == ?x] |- _ ] => rewrite eq_refl in H
    | _ => progress intros
    | _ => progress simpl in *
    | _ => progress destruct_head_hnf sigT
    | _ => progress destruct_head_hnf prod
    | _ => progress ssimpl
    | _ => progress hyp_destruct_atomic_in_match'
    | _ => progress destruct_atomic_in_match'
    | _ => progress specintros => *
    | _ => basic apply *
    | [ |- _ |-- parameterized_basic _ _ _ (lexists _) ] => eapply basic_post_exists
    | [ |- _ |-- parameterized_basic _ _ _ (_ /\\ _) ] => eapply basic_post_exists
    | [ H : context[if coq_test__is_finished ?x then _ else _],
            H' : context[only_last coq_test__is_finished ?x ?xs] |- _ ] => atomic xs; destruct xs; simpl only_last in H'
    | [ H : context[if coq_test__is_finished ?x then _ else _] |- _ ] => atomic x; destruct (coq_test__is_finished x)
    | [ |- _ |-- lexists _ ] => eapply lexistsR; by fin_tac
  end.

Local Ltac t_accum coq_test__is_finished := do ?t_accum' coq_test__is_finished ltac:(t_accum coq_test__is_finished).

(** Example: We can accumulate input while it satisfies some condition *)
(** This could be generalized so that the hypotheses only need to talk
    about things in the image of [initial] under repeated
    [accumulate]... *)
(** This version doesn't suffer from an off-by-one-error. *)
Lemma accumulator_while_rule ptest cond value pbody
      {T ioT}
      (P : T -> ioT -> SPred) (I : T -> ioT -> bool -> SPred) (accumulate : T -> ioT -> T)
      (Otest : T -> ioT -> PointedOPred)
      (Obody : T -> ioT -> PointedOPred)
      (coq_test__is_finished : ioT -> bool)
      S
      (H_test : forall initial x xs,
                  only_last coq_test__is_finished x xs
                  -> S
                       |-- (loopy_basic (P initial x) ptest
                                        (Otest initial x)
                                        (I initial x
                                           ((if coq_test__is_finished x then ~~ value else value) : bool) **
                                           ConditionIs cond
                                           ((if coq_test__is_finished x then ~~ value else value) : bool))))
      (H_body : forall initial x xs,
                  xs <> nil
                  -> only_last coq_test__is_finished x xs
                  -> S
                       |-- (loopy_basic (I initial x value ** ConditionIs cond value) pbody
                                        (Obody (accumulate initial x) (head x xs))
                                        (P (accumulate initial x) (head x xs))))
: S |-- (Forall initial x xs (pf1 : only_last coq_test__is_finished x xs),
         (loopy_basic (P initial x)
                      (while ptest cond value pbody)
                      (snd (foldl (fun xy v =>
                                     (accumulate (fst xy) v,
                                      catOP (snd xy) (catOP (Obody (fst xy) v) (Otest (fst xy) v))))
                                  (accumulate initial x, Otest initial x : OPred)
                                  xs))
                      (I (foldl accumulate initial (drop_last x xs)) (last x xs) (~~value) ** ConditionIs cond (~~value)))).
Proof.
  specintros => initial x xs pf.
  pose (existT (fun init_x_xs => only_last _ (snd (fst init_x_xs)) (snd init_x_xs)) (initial, x, xs) pf) as ixsp.
  change initial with (fst (fst (projT1 ixsp))).
  change x with (snd (fst (projT1 ixsp))).
  change xs with (snd (projT1 ixsp)).
  clearbody ixsp.
  clear x xs pf initial.
  let O := match goal with |- _ |-- parameterized_basic _ _ ?O _ => constr:(O) end in
  change O with (OPred_pred (default_PointedOPred O)).
  lrevert ixsp.
  eapply @while_rule_ind
  with (I_logic := fun ixsp b => let x := snd (fst (projT1 ixsp)) in (if coq_test__is_finished x then ~~value else value) == b)
         (Otest := fun ixsp => let initial := fst (fst (projT1 ixsp)) in
                               let x := snd (fst (projT1 ixsp)) in
                               Otest initial x)
         (Obody := fun ixsp => let initial := fst (fst (projT1 ixsp)) in
                               let x := snd (fst (projT1 ixsp)) in
                               let xs := snd (projT1 ixsp) in
                               Obody (accumulate initial x) (nth x xs 0))
         (I_state := fun ixsp => let initial := fst (fst (projT1 ixsp)) in
                                 let x := snd (fst (projT1 ixsp)) in
                                 I initial x)
         (transition_body := fun ixsp : sigT (fun init_x_xs : T * ioT * seq ioT => only_last coq_test__is_finished (snd (fst init_x_xs)) (snd init_x_xs))
                             => let initial := fst (fst (projT1 ixsp)) in
                                let x := snd (fst (projT1 ixsp)) in
                                let xs := snd (projT1 ixsp) in
                                existT (fun init_x_xs : T * ioT * seq ioT => only_last coq_test__is_finished (snd (fst init_x_xs)) (snd init_x_xs))
                                       (accumulate initial x, head x xs, behead xs)
                                       (only_last_behead _ _ _ (projT2 ixsp)))
         (O_after_test := fun ixsp => let initial := fst (fst (projT1 ixsp)) in
                                      let x := snd (fst (projT1 ixsp)) in
                                      let xs := snd (projT1 ixsp) in
                                      default_PointedOPred
                                        (snd (foldl (fun xy v =>
                                                       (accumulate (fst xy) v,
                                                        catOP (snd xy) (catOP (Obody (fst xy) v) (Otest (fst xy) v))))
                                                    (accumulate initial x, empOP)
                                                    xs)));
    simpl projT1; simpl projT2; simpl fst; simpl snd.
  { specintros => *; destruct_head_hnf sigT; simpl in *.
      by attempt basic apply H_test; eassumption. }
  { specintros => *; destruct_head_hnf sigT; destruct_head_hnf prod; simpl in *.
    attempt basic apply H_body; try (reflexivity || assumption).
    t_accum coq_test__is_finished. }
  { t_accum coq_test__is_finished.
    pose (fun (x : T) (v : ioT) => catOP (Obody x v) (Otest x v)) as f.
    change (fun (xy : T * OPred) (v : ioT) =>
              (accumulate (fst xy) v,
               catOP (snd xy) (catOP (Obody (fst xy) v) (Otest (fst xy) v))))
    with (fun xy v => (accumulate (fst xy) v, catOP (snd xy) (f (fst xy) v))).
    rewrite -> !foldl_catOP_to_functions.
    rewrite <- !catOP_foldl_helper'.
    by rewrite ?catOPA ?empOPL ?empOPR. }
  { t_accum coq_test__is_finished.
    pose (fun (x : T) (v : ioT) => catOP (Obody x v) (Otest x v)) as f.
    change (fun (xy : T * OPred) (v : ioT) =>
              (accumulate (fst xy) v,
               catOP (snd xy) (catOP (Obody (fst xy) v) (Otest (fst xy) v))))
    with (fun xy v => (accumulate (fst xy) v, catOP (snd xy) (f (fst xy) v))).
    rewrite -> !foldl_catOP_to_functions.
    rewrite <- !catOP_foldl_helper'.
    by rewrite ?catOPA ?empOPL ?empOPR. }
  { t_accum coq_test__is_finished. }
  { t_accum coq_test__is_finished. }
  { t_accum coq_test__is_finished. }
Qed.

Lemma accumulator_while_rule_state_independent_io ptest cond value pbody
      {T ioT}
      (P : T -> ioT -> SPred) (I : T -> ioT -> bool -> SPred) (accumulate : T -> ioT -> T)
      (Otest : ioT -> PointedOPred)
      (Obody : ioT -> PointedOPred)
      (coq_test__is_finished : ioT -> bool)
      S
      (H_test : forall initial x xs,
                  only_last coq_test__is_finished x xs
                  -> S
                       |-- (loopy_basic (P initial x) ptest
                                        (Otest x)
                                        (I initial x
                                           ((if coq_test__is_finished x then ~~ value else value) : bool) **
                                           ConditionIs cond
                                           ((if coq_test__is_finished x then ~~ value else value) : bool))))
      (H_body : forall initial x xs,
                  xs <> nil
                  -> only_last coq_test__is_finished x xs
                  -> S
                       |-- (loopy_basic (I initial x value ** ConditionIs cond value) pbody
                                        (Obody (head x xs))
                                        (P (accumulate initial x) (head x xs))))
: S |-- (Forall initial x xs (pf1 : only_last coq_test__is_finished x xs),
         (loopy_basic (P initial x)
                      (while ptest cond value pbody)
                      (catOP (Otest x)
                             (foldr catOP empOP (map (fun v => catOP (Obody v) (Otest v)) xs)))
                      (I (foldl accumulate initial (drop_last x xs)) (last x xs) (~~value) ** ConditionIs cond (~~value)))).
Proof.
  specintros => *.
  rewrite /= foldr_map.
  rewrite <- foldl_fun_catOP_foldr.
  attempt strict basic apply (@accumulator_while_rule
                                ptest cond value pbody
                                T ioT
                                P I accumulate
                                (fun _ => Otest)
                                (fun _ => Obody)
                                coq_test__is_finished
                                S
                                H_test
                                H_body); try assumption;
  [].
  rewrite <- foldl_fun_catOP_pull.
  etransitivity; [ | erewrite <- snd_foldl; reflexivity ]; reflexivity.
Qed.

Definition accumulate_prog (ptest: program)
           (cond: Condition) (value: bool)
           (pbody: program) in_ch
  := (IN in_ch, AL;;
      while ptest cond value (
        pbody;;
        IN in_ch, AL
     )).

Example accumulate_until_prog_safe ptest cond value pbody c
        {T}
        (P : T -> SPred) (I : T -> BYTE -> bool -> SPred) (accumulate : T -> BYTE -> T)
        (test_finished : BYTE -> bool)
        S al
        (H_test : forall initial x xs,
                    only_last test_finished x xs
                    -> S
                         |-- (loopy_basic (P initial ** AL ~= x)
                                          ptest
                                          empOP
                                          (I initial x
                                             ((if test_finished x then ~~ value else value) : bool) **
                                             ConditionIs cond
                                             ((if test_finished x then ~~ value else value) : bool))))
        (H_body : forall initial x xs,
                    xs <> nil
                    -> only_last test_finished x xs
                    -> S
                         |-- (loopy_basic (I initial x value ** ConditionIs cond value) pbody
                                          empOP
                                          (P (accumulate initial x) ** AL?)))
: S |-- (Forall initial x xs (pf1 : only_last test_finished x xs),
         (loopy_basic (P initial ** AL ~= al)
                      (accumulate_prog ptest cond value pbody c)
                      (foldr catOP empOP (map (inOP (zeroExtend n8 c)) (x::xs)))
                      (I (foldl accumulate initial (drop_last x xs)) (last x xs) (~~value) ** ConditionIs cond (~~value)))).
Proof.
  specintros => initial x xs pf.
  simpl.
  rewrite /accumulate_prog.
  basic apply *; simpl OPred_pred.
  attempt strict basic apply (@accumulator_while_rule_state_independent_io
                                ptest cond value (pbody;; IN c, AL) T BYTE
                                (fun initial x => AL ~= x ** P initial)
                                I
                                accumulate
                                (fun _ => default_PointedOPred empOP)
                                (fun v => default_PointedOPred (inOP (zeroExtend n8 c) v))
                                test_finished
                                S).
  { simpl OPred_pred; rewrite empOPL.
    apply foldr_catOP_map_respects_lentails => *.
    by rewrite empOPR. }
  { assumption. }
  { basic apply H_body; try eassumption.
    rewrite /stateIsAny; specintros => *.
    basic apply *. }
  { basic apply H_test; eassumption. }
Qed.

Definition accumulate_until_value_prog value
           (pbody: program) in_ch
  := accumulate_prog (CMP (AL : VReg OpSize1), (value : DWORD)) CC_Z false pbody in_ch.

(** TODO: put in the reasoning that [last x xs == value]; we'll need a lemma relating [last] and [only_last] *)
Example accumulate_until_value_prog_safe value
        {T} (P : T -> SPred)
        (accumulate : T -> BYTE -> T)
        pbody ch o s z c p
        S al
        (H_body : forall initial x xs,
                    xs <> nil
                    -> only_last (fun t : BYTE => t == (value : BYTE)) x xs
                    -> S
                         |-- (loopy_basic (P initial ** AL ~= x ** OF? ** SF? ** ZF ~= false ** CF? ** PF?) pbody
                                          empOP
                                          (P (accumulate initial x) ** AL? ** OF? ** SF? ** ZF? ** CF? ** PF?)))
: S |-- (Forall initial x xs (pf1 : only_last (fun t : BYTE => t == value) x xs),
         (loopy_basic (P initial ** AL ~= al ** OSZCP o s z c p)
                      (accumulate_until_value_prog value pbody ch)
                      (foldr catOP empOP (map (inOP (zeroExtend n8 ch)) (x::xs)))
                      (P (foldl accumulate initial (drop_last x xs)) ** AL ~= (last x xs) ** OF? ** SF? ** ZF ~= true ** CF? ** PF?))).
Proof.
  rewrite /OSZCP. specintros => *.
  rewrite /accumulate_until_value_prog.
  basic apply (fun ptest cond value' pbody ch
                => @accumulate_until_prog_safe ptest cond value' pbody ch T
                                               (fun initial => P initial ** OF? ** SF? ** ZF? ** CF? ** PF?)
                                               (fun initial x b => P initial ** AL ~= x ** OF? ** SF? ** CF? ** PF?)
                                               accumulate
                                               (fun x => x == value)).
  { repeat match goal with
             | [ H : is_true (only_last _ _ _) |- _ ] => idtac; rewrite only_last__only_last'/only_last' in H
             | [ H : is_true (_ && _) |- _ ] => apply andb_prop in H
             | [ H : _ = true |- _ ] => move/eqP in H
             | _ => progress destruct_head and
             | _ => by hyp_rewrite *
             | _ => done
           end. }
  { assumption. }
  { basic apply H_body; eassumption. }
  { attempt basic apply *.
    rewrite low_catB subB_eq0.
    repeat match goal with
             | _ => done
             | [ |- context[if ?x then _ else _] ] => case_eq x
             | _ => progress simpl
           end. }
Qed.

Example addB_until_zero_prog_safe ch o s z c p S al
: S |-- (Forall initial (x : BYTE) (xs : seq BYTE) (pf1 : only_last (fun t : BYTE => t == #0) x xs),
         (loopy_basic (AH ~= initial ** AL ~= al ** OSZCP o s z c p)
                      (accumulate_until_value_prog #0 (ADD AH, AL) ch)
                      (foldr catOP empOP (map (inOP (zeroExtend n8 ch)) (x::xs)))
                      ((AH ~= (foldl (fun x y => addB x y) initial (drop_last x xs)))
                         ** AL ~= (last x xs) ** OF? ** SF? ** ZF ~= true ** CF? ** PF?))).
Proof.
  specintros => *. admit.
(* basic apply (@accumulate_until_value_prog_safe #0 _ (fun x => AH ~= x)) => *; first assumption.
  basic apply *. *)
Qed.

Import Streams.

Definition stream_to_in_out (in_c out_c : BYTE) (ls : Stream BYTE) : OPred
  := map_opred_to_stream (In (zeroExtend n8 in_c)) (fun v => (Out (zeroExtend n8 out_c) v)::nil) ls.

Definition echo_once in_c out_c :=
  (IN in_c, AL;;
   OUT out_c, AL).

Definition echo_once_OP_spec (in_c out_c : BYTE) v := catOP (inOP (zeroExtend n8 in_c) v) (outOP (zeroExtend n8 out_c) v).

Example safe_echo_once al in_c out_c
: |-- Forall v, basic (AL ~= al)
                      (echo_once in_c out_c)
                      (echo_once_OP_spec in_c out_c v)
                      (AL ~= v).
Proof.
  specintros => v. rewrite /echo_once/echo_once_OP_spec.
  basic apply *.
  basic apply *.
Qed.

Instance: forall in_c out_c, instrrule (echo_once in_c out_c) := fun in_c out_c al => @safe_echo_once al in_c out_c.

Definition echo in_c out_c := while (TEST EAX, EAX) CC_O false (echo_once in_c out_c).

Lemma eq_opred_stream__echo_once in_c out_c s
: (catOP (echo_once_OP_spec in_c out_c (hd s)) (stream_to_in_out in_c out_c (tl s)))
    |-- (stream_to_in_out in_c out_c s).
Proof.
  rewrite /echo_once_OP_spec/stream_to_in_out.
  destruct s.
  rewrite !map_opred_to_stream_def //=.
  rewrite /inOP/outOP ?catOPA.
  do !(apply lorR2; f_cancel).
Qed.

Lemma echo_safe in_c out_c eax
: |-- (Forall (s : Stream BYTE),
       (loopy_basic (EAX ~= eax ** AL? ** OSZCP?)
                    (echo in_c out_c)
                    (stream_to_in_out in_c out_c s)
                    lfalse)).
Proof.
  rewrite /echo.
  eapply @while_rule_ind
  with (I_logic := fun _ b => false == b)
         (Otest := fun _ => empOP)
         (Obody := fun s => echo_once_OP_spec in_c out_c (hd s))
         (I_state := fun s _ => EAX ~= eax ** AL? ** SF? ** ZF? ** CF? ** PF?)
         (transition_body := @tl _)
         (O_after_test := fun s => default_PointedOPred
                                     (catOP (echo_once_OP_spec in_c out_c (hd s)) (stream_to_in_out in_c out_c (tl s))));
    do ![ progress rewrite -> ?empOPL, -> ?eq_opred_stream__echo_once
        | specintros => *
        | done
        | by ssimpl
        | basic apply *
        | progress simpl OPred_pred
        | progress move => *
        | progress rewrite /stateIsAny
        | reflexivity ].
Qed.

author: nbenton


text:
Load LFindLoad.
Load LFindLoad.
From adtind Require Import goal35.

From lfind Require Import LFind.
Lemma lfind_state  (x:natural) (y:natural) (z:natural) (IHx:@eq natural (mult (mult x y) z) (mult x (mult y z))):@eq natural (mult (plus (mult x y) y) z)
  (plus (mult x (mult y z)) (mult y z)).
Admitted.
From QuickChick Require Import QuickChick.
QCInclude "/home/yousef/lemmafinder/benchmark/_lfind_clam_lf_goal35_mult_assoc_102_distrib/".
QCInclude ".".
Extract Constant defNumTests => "50".
Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.

Open Scope string_scope.

Parameter print : natural -> string -> natural.
Extract Constant print => "Extract.print".
Definition collect_data  (x:natural) (y:natural) (z:natural) :=
 let lfind_var := "x:" ++ "(" ++ show x ++ ")"++ "|" ++"y:" ++ "(" ++ show y ++ ")"++ "|" ++"z:" ++ "(" ++ show z ++ ")"
 in let lfind_v := print x lfind_var
 in lfind_state lfind_v  y z.
QuickChick collect_data.
Success.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import Rsequence.
Require Import Rseries_def.

(** Basic facts *)

Lemma Rser_cv_unique: forall An l1 l2,
  Rser_cv An l1 -> Rser_cv An l2 -> l1 = l2.
Proof.
intros ; eapply Rseq_cv_unique ; eassumption.
Qed.

Lemma Rser_cv_ext: forall An Bn l, An == Bn ->
  (Rser_cv An l <-> Rser_cv Bn l).
Proof.
intros ; apply Rseq_cv_eq_compat, Rseq_sum_ext ; assumption.
Qed.

(** Compatibility with common operations *)

Lemma Rser_cv_scal_compat_l: forall An la (l : R),
  Rser_cv An la -> Rser_cv (l * An) (l * la).
Proof.
intros ; eapply Rseq_cv_eq_compat.
 apply Rseq_sum_scal_compat_l.
 apply Rseq_cv_mult_compat ; intuition.
Qed.

Lemma Rser_cv_scal_compat_r: forall An la (l : R),
  Rser_cv An la -> Rser_cv (An * l) (la * l).
Proof.
intros ; eapply Rseq_cv_eq_compat.
 apply Rseq_sum_scal_compat_r.
 apply Rseq_cv_mult_compat ; intuition.
Qed.

Lemma Rser_cv_opp_compat: forall An l,
  Rser_cv An l -> Rser_cv (- An) (- l).
Proof.
intros ; eapply Rseq_cv_eq_compat.
 apply Rseq_sum_opp_compat.
 apply Rseq_cv_opp_compat ; assumption.
Qed.

Lemma Rser_cv_plus_compat: forall An Bn la lb,
  Rser_cv An la -> Rser_cv Bn lb -> Rser_cv (An + Bn) (la + lb).
Proof.
intros ; eapply Rseq_cv_eq_compat.
 apply Rseq_sum_plus_compat.
 apply Rseq_cv_plus_compat ; assumption.
Qed.

Lemma Rser_cv_minus_compat: forall An Bn la lb,
  Rser_cv An la -> Rser_cv Bn lb -> Rser_cv (An - Bn) (la - lb).
Proof.
intros ; eapply Rseq_cv_eq_compat.
 apply Rseq_sum_minus_compat.
 apply Rseq_cv_minus_compat ; assumption.
Qed.

(** Series convergence shifting compatibility *)

Lemma Rser_cv_shift : forall An l, Rser_cv An l ->
  Rser_cv (Rseq_shift An) (l - (An O)).
Proof.
intros An l Hl ; eapply Rseq_cv_eq_compat.
 intro n ; apply Rseq_sum_shift_compat.
 apply Rseq_cv_minus_compat.
  apply Rseq_cv_shift_compat_reciprocal ; assumption.
  apply Rseq_constant_cv.
Qed.

Lemma Rser_cv_shift_rev : forall An l,
  Rser_cv (Rseq_shift An) l ->  Rser_cv An (l + An 0%nat).
Proof.
intros An l Hl ; apply Rseq_cv_shift_compat ; apply Rseq_cv_eq_compat with
 (Rseq_plus (Rseq_sum (Rseq_shift An)) (An O)).
 intro n ; unfold Rseq_plus, Rseq_constant ;
  rewrite (Rseq_sum_shift_compat An n) ; ring.
 apply Rseq_cv_plus_compat ; [assumption | apply Rseq_constant_cv].
Qed.

Lemma Rser_cv_shift_rev2: forall Un l,
  Rser_cv (Rseq_shift Un) (l - (Un O)) -> Rser_cv Un l.
Proof.
intros ; replace l with (l - Un O + Un O) by ring ;
 apply Rser_cv_shift_rev ; assumption.
Qed.

Lemma Rser_cv_shifts : forall k An l, Rser_cv An l ->
  Rser_cv (Rseq_shifts An (S k)) (l - Rseq_sum An k).
Proof.
intros k An l Hl ; eapply Rseq_cv_eq_compat.
 intro n ; apply Rseq_sum_shifts_compat.
 apply Rseq_cv_minus_compat.
  apply Rseq_cv_shifts_compat_reciprocal ; assumption.
  apply Rseq_constant_cv.
Qed.

Lemma Rser_cv_shifts_rev : forall k An l,
  Rser_cv (Rseq_shifts An (S k)) l ->  Rser_cv An (l + Rseq_sum An k).
Proof.
intros k An l Hl ; apply Rseq_cv_shifts_compat with (S k) ; apply Rseq_cv_eq_compat with
 (Rseq_plus (Rseq_sum (Rseq_shifts An (S k))) (Rseq_sum An k)).
 intro n ; unfold Rseq_plus, Rseq_constant ;
  rewrite (Rseq_sum_shifts_compat An k n) ; ring.
 apply Rseq_cv_plus_compat ; [assumption | apply Rseq_constant_cv].
Qed.

Lemma Rser_cv_sig_shift_rev: forall An,
  {l | Rser_cv (Rseq_shift An) l} -> {l | Rser_cv An l}.
Proof.
intros An [l Hl] ; exists (l + An O) ; apply Rser_cv_shift_rev ; assumption.
Qed.

Lemma Rser_cv_sig_shifts_rev: forall k An,
  {l | Rser_cv (Rseq_shifts An k) l} -> {l | Rser_cv An l}.
Proof.
intros [| k] An [l Hl].
 exists l ; eapply Rser_cv_ext ; [symmetry ; apply Rseq_shifts_0 | assumption].
 exists (l + Rseq_sum An k) ; apply Rser_cv_shifts_rev ; assumption.
Qed.

(** If a series converges absolutely, then it converges *)

Lemma Rser_abs_cv_cv : forall An, {l | Rser_abs_cv An l} -> {l | Rser_cv An l}.
Proof.
intros An Habs ; apply (cv_cauchy_2 An),
 cauchy_abs, cv_cauchy_1, Habs.
Qed.

(** If a series converges, its coefficients' sequence converges to zero *)

Lemma Rser_cv_zero : forall An l, Rser_cv An l -> Rseq_cv An 0.
Proof.
intros An l Hl ; apply Rseq_cv_shift_compat ;
 apply Rseq_cv_eq_compat with (Rseq_shift (Rseq_sum An) - Rseq_sum An)%Rseq.
 clear ; intro p ; unfold Rseq_shift, Rseq_minus ; rewrite Rseq_sum_simpl ; ring.
 replace 0 with (l - l) by ring ; apply Rseq_cv_minus_compat ;
 [apply Rseq_cv_shift_compat_reciprocal |] ; assumption.
Qed.

author: coqtail

repo: coqtail

save_path: github-repos/coq/coqtail-coqtail


text:
Require Export ZArith.
Require Export List.
Require Export Arith.
Require Export Zwf.
Require Export Relations.
Require Export Inverse_Image.

 (**
 Binary trees labeleld with integers

*)
Inductive Z_btree : Set :=
| Z_leaf : Z_btree
| Z_bnode : Z->Z_btree->Z_btree->Z_btree.

(**

Have a look at the  induction principles

Print Z_btree_ind.
Print Z_btree_rect.
 *)

(**
  Another definition : A binary node's sons are represented
 through a function.
*)
Inductive Z_fbtree : Set :=
  Z_fleaf : Z_fbtree
| Z_fnode : Z->(bool->Z_fbtree)->Z_fbtree.

(** even natural numbers *)

Inductive even : nat->Prop :=
  | O_even : even 0%nat
  | plus_2_even : forall n:nat, even n -> even (S (S n)).

Open Scope nat_scope.

(** perfect  binary trees (indexed by their height)
*)

Inductive htree (A:Set) : nat->Set :=
  hleaf : A -> htree A 0
| hnode : forall n:nat, A -> htree A n -> htree A n -> htree A (S n).

(** infinitely branching trees *)

Inductive inf_branch_tree (A:Set) : Set :=
  inf_leaf : inf_branch_tree A
| inf_node : A -> (nat -> inf_branch_tree A) -> inf_branch_tree A.

(** For compatibility with the book :
    have a look at Tpe Classes !
*)

Record group : Type :=
  {A : Type;
   op : A->A->A;
   sym : A->A;
   e : A;
   e_neutral_left : forall x:A, op e x = x;
   sym_op : forall x:A, op (sym x) x = e;
   op_assoc : forall x y z:A, op (op x y) z = op x (op y z);
   op_comm : forall x y:A, op x y = op y x}.

Fixpoint nat_simple_rec (A:Type)(exp1:A)(exp2:nat->A->A)(x:nat)
  : A :=
  match x with
  | O => exp1
  | S p => exp2 p (nat_simple_rec A exp1 exp2 p)
  end.

Definition example_codomain (b:bool) : Set :=
  match b with true => nat | false => bool end.

Definition example_dep_function (b:bool) : example_codomain b :=
  match b as x return example_codomain x with
  | true => 0
  | false => true
  end.

Inductive type_name (A B:Type) : nat -> nat -> Type := .

Definition bool_case
   (F:bool -> Type)(v1:F true)(v2:F false)(x:bool) :=
  match x return F x with true => v1 | false => v2 end.

Module redefine_nat_case.

Definition nat_case
  (F:nat -> Type)(exp1:F 0)(exp2:forall p:nat, F (S p))(n:nat) :=
  match n as x return F x with
  | O => exp1
  | S p => exp2 p
  end.

End redefine_nat_case.

Module Type nat_rect_type.
Parameter
nat_rect :
  forall f:nat->Type, f 0 ->(forall n:nat, f n -> f (S n))-> forall n:nat, f n.
End nat_rect_type.

Module nat_rect_module : nat_rect_type.

Fixpoint nat_rect (f:nat->Type)(exp1:f 0)
 (exp2:forall p:nat, f p -> f (S p))(n:nat){struct n} : f n :=
  match n as x return f x with
  | O => exp1
  | S p => exp2 p (nat_rect f exp1 exp2 p)
  end.

End nat_rect_module.

Definition mult2' :=
  nat_rect (fun n:nat => nat) 0 (fun p v:nat => S (S v)).

Module redefine_nat_ind.

Fixpoint nat_ind (P:nat->Prop)(exp1:P 0)
 (exp2:forall p:nat, P p -> P (S p))(n:nat){struct n} : P n :=
  match n as x return P x with
  | O => exp1
  | S p => exp2 p (nat_ind P exp1 exp2 p)
  end.

End redefine_nat_ind.

Module Type Z_btree_rect_type.
Parameter
Z_btree_rect :
  forall f:Z_btree->Type,
   f Z_leaf ->
   (forall (n:Z)(t1:Z_btree), f t1 ->
      forall t2:Z_btree, f t2 -> f (Z_bnode n t1 t2))->
   forall t:Z_btree, f t.
End Z_btree_rect_type.

Module Z_btree_rect_module : Z_btree_rect_type.

Fixpoint Z_btree_rect (f:Z_btree->Type)(exp1:f Z_leaf)
 (exp2:forall (n:Z)(t1:Z_btree), f t1 ->
        forall t2:Z_btree, f t2 -> f (Z_bnode n t1 t2))
 (t:Z_btree) : f t :=
  match t as x return f x with
  | Z_leaf => exp1
  | Z_bnode n t1 t2 =>
      exp2 n t1 (Z_btree_rect f exp1 exp2 t1) t2
        (Z_btree_rect f exp1 exp2 t2)
  end.

End Z_btree_rect_module.

Scheme le_ind' := Induction for le Sort Prop.

(**

Compute
  (forall (n:nat)(P:nat->Prop),
     (fun (n':nat)(P:forall m:nat, n' <= m -> Prop) =>
        P n' (le_n n')->
        (forall (m:nat)(h:n' <= m), P m h -> P (S m)(le_S n' m h))->
        forall (m:nat)(h:n' <= m), P m h) n
       (fun (m:nat)(_:n <= m) => P m)).
*)

Fixpoint even_ind_max (P:forall n:nat, even n -> Prop)
 (exp1:P 0 O_even)
 (exp2:forall (n:nat)(t:even n),
         P n t -> P (S (S n))(plus_2_even n t))(n:nat)(t:even n)
 {struct t} : P n t :=
  match t as x0 in (even x) return P x x0 with
  | O_even => exp1
  | plus_2_even p t' => exp2 p t' (even_ind_max P exp1 exp2 p t')
  end.

Fixpoint even_ind' (P:nat->Prop)(exp1:P 0)
 (exp2:forall n:nat, even n -> P n -> P (S (S n)))(n:nat)(t:even n)
 {struct t} : P n :=
  match t in (even x) return P x with
  | O_even => exp1
  | plus_2_even p t' => exp2 p t' (even_ind' P exp1 exp2 p t')
  end.

Definition clos_trans_ind' (A:Set)(R P:A->A->Prop)
 (exp1:forall x y:A, R x y -> P x y)
 (exp2:forall x y z:A,
         clos_trans A R x y ->
         P x y -> clos_trans A R y z -> P y z -> P x z)(x y:A)
 (p:clos_trans A R x y) : P x y.
Proof.
 induction p.
 -  intros;apply exp1;auto.
 -  intros;eapply exp2;eauto.
Defined.

Fixpoint clos_trans_ind'' (A:Set)(R P:A->A->Prop)
 (exp1:forall x y:A, R x y -> P x y)
 (exp2:forall x y z:A,
         clos_trans A R x y ->
         P x y -> clos_trans A R y z -> P y z -> P x z)(x y:A)
 (p:clos_trans A R x y){struct p} : P x y :=
 match p in (clos_trans _ _ _ x0) return P x x0 with
 | t_step  _ _ _ y' h => exp1 x y' h
 | t_trans _ _ _ y' z' h1 h2 =>
   exp2 x y' z' h1 (clos_trans_ind'' A R P exp1 exp2  x y' h1) h2
     (clos_trans_ind'' A R P exp1 exp2  y' z' h2)
  end.

Module even_ind_max_redefined.

 Scheme even_ind_max := Induction for even Sort Prop.

End even_ind_max_redefined.

Module nat_simple_rec_redefined.

Scheme nat_simple_rec := Minimality for nat Sort Set.

End nat_simple_rec_redefined.

Definition rich_minus (n m:nat) := {x : nat | x+m = n}.

Definition le_rich_minus : forall m n:nat, n <= m -> rich_minus m n.
 induction m as [ | n IHn].
 -  intros n Hle; exists 0.
    now  inversion Hle.
 -  intros p; case p.
     + intro Hle; exists (S n); auto with arith.
     + intros q Hle; case (IHn q).
       * inversion Hle;auto with arith.
       * intros x Hx; exists x; rewrite <- Hx; auto with arith.
Defined.

Inductive lfactor {A: Type} : list A -> list A -> Prop :=
  lf1 : forall u:list A, lfactor nil u
| lf2 : forall (a:A)(u v:list A),
       lfactor u v -> lfactor (cons a u)(cons a v).

Module redefine_eq_rec.

Definition eq_rect (A:Type)(x:A)(P:A->Type)(f:P x)(y:A)(e:x = y)
  : P y := match e in (_ = x) return P x with
           | refl_equal => f
           end.

Definition eq_rec {A:Type}(x:A)(P:A->Set) :
  P x -> forall y:A, x = y -> P y := eq_rect A x P.

End redefine_eq_rec.

Section update_def.
  Variables (A : Type)(A_eq_dec : forall x y:A, {x = y}+{x <> y}).
  Variables (B : A -> Type)(a : A)(v : B a)(f : forall x:A, B x).

  Definition update (x:A) : B x :=
    match A_eq_dec a x with
    | left h => eq_rect a B v x h
    | right h' => f x
    end.

End update_def.

(**
Check (fun eq_rect_eq
     :forall (U:Type)(p:U)(Q:U->Set)(x:Q p)(h:p = p),
                 x = eq_rec p Q x p h =>  False).

Check (fun update_eq
     :forall (A:Type)(eq_dec:forall x y:A, {x = y}+{x <> y})
                 (B:A->Type)(a:A)(v:B a)(f:forall x:A, B x),
                 update A eq_dec B a v f a = v =>  False).
*)

Inductive ntree (A:Type) : Type :=
  nnode : A -> nforest A -> ntree A
with nforest (A:Type) : Type :=
  nnil : nforest A | ncons : ntree A -> nforest A -> nforest A.
Open Scope Z_scope.

Fixpoint count (A:Type)(t:ntree A){struct t} : Z :=
  match t with
  | nnode _ a l => 1 + count_list A l
  end
 with count_list (A:Type)(l:nforest A){struct l} : Z :=
  match l with
  | nnil _ => 0
  | ncons _ t tl => count A t + count_list A tl
  end.

Module Type ntree_ind_type.

Parameter
ntree_ind :
  forall (A:Type)(P:ntree A -> Prop),
    (forall (a:A)(l:nforest A), P (nnode A a l))->
    forall t:ntree A, P t.

End ntree_ind_type.

Module ntree_ind_module.
Definition ntree_ind := ntree_ind.
End ntree_ind_module.

(**

Print ntree_ind_module.ntree_ind.
*)

Scheme ntree_ind2 :=
   Induction for ntree Sort Prop
 with nforest_ind2 :=
   Induction for nforest Sort Prop.

Inductive occurs (A:Type)(a:A) : ntree A -> Prop :=
| occurs_root : forall l, occurs A a (nnode A a l)
| occurs_branches :
   forall b l, occurs_forest A a l -> occurs A a (nnode A b l)
with occurs_forest (A:Type)(a:A) : nforest A -> Prop :=
  occurs_head :
   forall t tl, occurs A a t -> occurs_forest A a (ncons A t tl)
| occurs_tail :
   forall t tl,
    occurs_forest A a tl -> occurs_forest A a (ncons A t tl).

Fixpoint n_sum_values (t:ntree Z) : Z :=
  match t with
  | nnode _ z l => z + n_sum_values_l l
  end
 with n_sum_values_l (l:nforest Z) : Z :=
  match l with
  | nnil _ => 0
  | ncons _ t tl => n_sum_values t + n_sum_values_l tl
  end.

#[export] Hint Resolve occurs_branches occurs_root Zplus_le_compat : core.

Theorem greater_values_sum :
 forall t:ntree Z,
   (forall x:Z, occurs Z x t -> 1 <= x)-> count Z t <= n_sum_values t.
Proof.
 intros t; elim t using ntree_ind2 with
  (P0 := fun l:nforest Z =>
           (forall x:Z, occurs_forest Z x l -> 1 <= x)->
           count_list Z l <= n_sum_values_l l).
 -  intros z l Hl Hocc; lazy beta iota delta -[Zplus Z.le];
    fold count_list n_sum_values_l;   auto with *.

 -  auto with zarith.
 -  intros t1 Hrec1 tl Hrec2 Hocc; lazy beta iota delta -[Zplus Z.le];
  fold count count_list n_sum_values n_sum_values_l.
  apply Zplus_le_compat.
  apply Hrec1; intros; apply Hocc; apply occurs_head; auto.
  apply Hrec2; intros; apply Hocc; apply occurs_tail; auto.
Qed.

Inductive ltree (A:Type) : Type :=
    lnode : A -> list (ltree A)-> ltree A.

Section correct_ltree_ind.

Variables
  (A : Type)(P : ltree A -> Prop)(Q : list (ltree A)-> Prop).

Hypotheses
 (H : forall (a:A)(l:list (ltree A)), Q l -> P (lnode A a l))
 (H0 : Q nil)
 (H1 : forall t:ltree A, P t -> forall l:list (ltree A), Q l -> Q (cons t l)).

Fixpoint ltree_ind2 (t:ltree A) : P t :=
  match t as x return P x with
  | lnode _ a l =>
      H a l
        (((fix l_ind (l':list (ltree A)) : Q l' :=
             match l' as x return Q x with
             | nil => H0
             | cons t1 tl => H1 t1 (ltree_ind2 t1) tl (l_ind tl)
             end)) l)
  end.

End correct_ltree_ind.

author: coq-community

repo: coq-art

save_path: github-repos/coq/coq-community-coq-art