mukeshtiwari

 A : Type
  O : Op A
  l : list A
  Hmon : mon O
  Hfin : forall a : A, In a l
  H : card l (iter O 0 full_ss) >= card l (iter O 1 full_ss) + 1
  ============================
  card l (iter O 1 full_ss) + 1 <= card l (iter O 0 full_ss)

mukeshtiwari

 Theorem  iter_fp_gfp {A: Type} (O: Op A) (l: list A):
    mon O -> (forall a: A, In a l) ->
    forall (n : nat), (pred_eeq (iter O (n + 1) full_ss) (iter O n full_ss)) \/
               (card l (iter O (n+1) full_ss) + (n + 1)) <= length l.
  Proof.
    intros Hmon Hfin n. induction n.
    destruct (iter_aux_dec O l Hmon Hfin 0).
    left. assumption.
    right. replace (0 + 1)%nat with 1 in *.
    transitivity (card l (iter O 0 full_ss))%nat.

mukeshtiwari

 A : Type
  k : nat
  O : (A -> bool) -> A -> bool
  Hmon : mon O
  l : list A
  Hin : forall a : A, In a l
  Hlen : length l <= k
  n : nat
  Hlel : k < n
  R : length (filter (iter O (k + 1) full_ss) l) + (k + 1) <= length l

mukeshtiwari

  A : Type
  k : nat
  O : (A -> bool) -> A -> bool
  Hmon : mon O
  l : list A
  Hin : forall a : A, In a l
  Hlen : length l <= k
  n : nat
  Hlel : k < n
  R : length (filter (iter O (k + 1) full_ss) l) + (k + 1) <= length l

mukeshtiwari

  c, d : cand
  k : nat
  H : Path k c d
  ============================
  Fixpoints.iter (O k) (length (all_pairs cand_all)) Fixpoints.empty_ss (c, d) = true

To 

  c, d : cand
  k : nat

mukeshtiwari

 Lemma monotone_operator_w : forall k, Fixpoints.mon (W k).
  Proof.
    intros k. unfold Fixpoints.mon. intros p1 p2 H.
    unfold W. unfold Fixpoints.pred_subset in *.
    intros a H1. apply andb_true_iff in H1.
    apply andb_true_iff. destruct H1 as [H2 H3].
    split. assumption. unfold mp in *.
    apply forallb_forall.
    
Goal: 

mukeshtiwari

  Definition pred (A: Type) := A -> bool.

  (* subset relation on boolean predicates *)
  Definition pred_subset {A: Type} (p1 p2: pred A) :=
    forall a: A, p1 a = true -> p2 a = true.

  (* extensional equality of boolean predicates *)
  Definition pred_eeq {A: Type} (p1 p2: pred A) :=
    pred_subset p1 p2 /\ pred_subset p2 p1.
    

mukeshtiwari

Definition pred (A: Type) := A -> bool.

Definition complement {A : Type} p : pred A := fun x => negb (p x).

Lemma remove_complement : forall (A : Type) (p : pred A),
      (complement (complement p)) = p.
Proof.
    intros A p. unfold complement. rewrite negb_involutive.

mukeshtiwari

  Theorem path_lfp : forall (c d : cand) (k : nat),
      Fixpoints.least_fixed_point
        (cand * cand) (all_pairs cand_all)
        (all_pairs_universal cand_all cand_fin) (O k) (monotone_operator k) (c, d) = true 
      <-> Path k c d.
  Proof.
    split. intros H. apply wins_evi. exists (length (all_pairs cand_all)). assumption.
    intros H. apply wins_evi in H. destruct H as [n H]. unfold Fixpoints.least_fixed_point.
    unfold Fixpoints.empty_ss. remember (length (all_pairs cand_all)) as v.    
    specialize (Fixpoints.iter_fin v (O k) (monotone_operator k)). intros.

mukeshtiwari

Lemma MStar'' : forall T (s : list T) (re : reg_exp T),
    s =~ Star re ->
    exists ss : list (list T),
      s = fold app ss []
      /\ forall s', In s' ss -> s' =~ re.
Proof.
  intros T s re H. remember (Star re) as re'. remember s as s'. induction H.
  exists []. simpl. intuition.
  inversion Heqre'.