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
  a : A
  m : nat
  H : iter O (S m) nil_pred a = true

mukeshtiwari

We can prove 
A
A -> B
-------
B

but not 

B 
A -> B

mukeshtiwari

(* equality on boolean predicates on a finite type is decidable *)
  Lemma pred_eq_dec_aux {A: Type} (l: list A) :
    forall (p1 p2: A -> bool), {forall a, In a l -> p1 a = p2 a} + {~(forall a, In a l -> p1 a = p2 a)}.
  Proof.
    induction l as [| x xs IHxs].
    (* nil case *)
    intros p1 p2. left.
    intros a Hin. inversion Hin.
    (* list of the form x:xs *)
    intros p1 p2.

mukeshtiwari

 (* all pairs that can be formed from a list *)
  Fixpoint all_pairs {A: Type} (l: list A): list (A * A) :=
    match l with
    |   [] => []
    |    c::cs => (c, c)::(all_pairs cs) ++ (map (fun x => (c, x)) cs) 
                                         ++ (map (fun x => (x, c)) cs)
    end.


  A : Type

mukeshtiwari

Definition bounded_card (A: Type) (n: nat) :=  exists l, (forall a: A, In a l) /\ length l <= n.

Fixpoint all_pairs {A: Type} (l: list A): list (A * A) :=
    match l with
    | [] => []
    | c::cs => (c, c) :: (all_pairs cs)
                     ++  (map (fun x => (c, x)) cs) 
                     ++ (map (fun x => (x, c)) cs)
    end.
    

mukeshtiwari

Definition bounded_card (A: Type) (n: nat) := 
exists l, (forall a: A, In a l) /\ length l <= n.




 Lemma length_cand : forall {A : Type} n , 
      Fixpoints.bounded_card A n -> Fixpoints.bounded_card (A * A) (n * n).
  Proof.

mukeshtiwari

 Lemma length_pair : forall {A : Type} (n : nat) (l : list A),
      length l <= n -> length (all_pairs l) <= n * n.
  Proof.
    intros. induction l.
    auto with arith.
    simpl. repeat rewrite app_length.
    repeat rewrite map_length.

  A : Type
  n : nat

mukeshtiwari

  Lemma length_pair : forall {A : Type} (n : nat) (l : list A),
      length l <= n -> length (all_pairs l) <= n * n.
  Proof.
    intros A n l. generalize dependent n. induction l.
    intros n H. auto with arith.
    intros n H. destruct n.
    inversion H.
    simpl. simpl in H.
    repeat rewrite app_length. repeat rewrite map_length.

mukeshtiwari

Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr => true
  | Char _ => true
  | App re1 re2 | Union re1 re2 => orb (re_not_empty re1) (re_not_empty re2)
  | Star re => re_not_empty re
  end.

Lemma re_not_empty_correct : forall T (re : reg_exp T),

mukeshtiwari

Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr => true
  | Char _ => true
  | App re1 re2 => andb (re_not_empty re1) (re_not_empty re2)
  | Union re1 re2 => orb (re_not_empty re1) (re_not_empty re2)
  | Star re => true (* always match empty string *)
  end.