mukeshtiwari

;some thing went wrong with my firefox update
(defn go-to-tripadv
  "returns tripadvisors urls for city"
  [city]
  (do
    (set-driver! {:browser :firefox})
    (get-url "https://www.tripadvisor.in")
    (wait-until #(= (title) "TripAdvisor: Read Reviews, Compare Prices & Book"))
    (input-text "#GEO_SCOPED_SEARCH_INPUT" city)
    (click "#GEO_SCOPE_CONTAINER .scopedSearchDisplay li")

mukeshtiwari

Module Evote.

  Require Import Notations.
  Require Import Coq.Lists.List.
  Require Import Coq.Arith.Le.
  Require Import Coq.Numbers.Natural.Peano.NPeano.
  Require Import Coq.Arith.Compare_dec.
  Require Import Coq.omega.Omega.
  Import ListNotations.

mukeshtiwari

 k : nat
  u, v : cand
  l : list (cand * cand)
  H1 : fold_left
         (fun (x : bool) (b : cand) => x && (bool_in (b, snd (u, v)) l || el k (fst (u, v), b)))
         cand_all true = true
  b : cand
  ============================
   In (b, snd (u, v)) l \/ edge (fst (u, v)) b <= k

mukeshtiwari

  Definition bool_in (p: (cand * cand)%type) (l: list (cand * cand)%type) :=
    existsb (fun q => (andb (cand_eqb (fst q) (fst p))) ((cand_eqb (snd q) (snd p)))) l. 
    
  Definition el (k: nat) (p: (cand * cand)%type) := Compare_dec.leb (edge (fst p) (snd p)) k.

  Lemma edge_prop : forall a b k, el k (a, b) = true -> edge a b <= k.
  Proof.
    intros a b k H; unfold el in H; simpl in H;
    apply leb_complete in H; assumption.
  Qed.

mukeshtiwari

Module Evote.

  Require Import Notations.
  Require Import Coq.Lists.List.
  Require Import Coq.Arith.Le.
  Require Import Coq.Numbers.Natural.Peano.NPeano.
  Require Import Coq.Arith.Compare_dec.
  Require Import Coq.omega.Omega.
  Require Import Bool.Sumbool.
  Require Import Bool.Bool.

mukeshtiwari

Theorem noduplicate : forall (l1 l2 : list bool), NoDup l1 -> NoDup l2 ->
                                            (forall a : bool, In a l1) -> length l2 <= length l1.

mukeshtiwari

 Theorem  iter_aux_new {A: Type} (O: (A -> bool) -> (A -> bool)) (l: list A):
    mon O ->
    (forall a: A, In a l) ->
    forall (n : nat), (forall a:A, iter O n nil_pred a = true <-> iter O (n+1) nil_pred a = true) \/
               card l (iter O n nil_pred) >= n.
  Proof.              
    intros Hmon Hfin n. specialize (iter_aux O l Hmon Hfin n); intros.
    destruct H as [H | H]. left. assumption.
    right. unfold mon in Hmon. unfold card in H; unfold card.
    generalize dependent n. 

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
  Hler : k >= n
  H : forall a : A, iter O k nil_pred a = true <-> iter O (k + 1) nil_pred a = true

mukeshtiwari

  Theorem iter_fin {A: Type} (k: nat) (O: (A -> bool) -> (A -> bool)) :
    mon O -> bounded_card A k ->
    forall n: nat, forall a: A, iter O n nil_pred a = true -> iter O k nil_pred a = true.
  Proof. 
  intros Hmon Hboun; unfold bounded_card in Hboun.
  destruct Hboun as [l [Hin Hlen]]. intros n.
  assert (Hle : k < n \/ k >= n) by omega.    
  destruct Hle as [Hlel | Hler]; swap 1 2.
  destruct (iter_aux_newagain O l Hmon Hin k). intros a Hiter.
  specialize (increasing O Hmon); intros. unfold pred_subset in H0.

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
  a : A
  H : iter O n nil_pred a = true