keep_learning.v

Require Import List Arith.


Axiom cand : Type.
Axiom cand_eqb : cand -> cand -> bool.
Axiom edge : cand -> cand -> nat.

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.

Lemma boolin_prop :  forall a b l, bool_in (a, b) l = true -> In (a, b) l.
Proof. Admitted.

Axiom cand_all : list cand.

Lemma fold_left_andb' : 
  forall (A : Type) (f : A -> bool) l a, fold_left (fun x y => andb x (f y)) l a = true -> 
         a = true /\ List.Forall (fun a => f a = true) l.
Proof.
  induction l; simpl; intros.
  - auto.
  - apply IHl in H. destruct H.
    apply Bool.andb_true_iff in H. 
    intuition.
Qed.

Lemma fold_left_andb : 
  forall (A : Type) (f : A -> bool) l a, fold_left (fun x y => andb x (f y)) l a = true -> 
         List.Forall (fun a => f a = true) l.
Proof. apply fold_left_andb'. Qed.

Axiom cand_fin : forall c, In c cand_all.

Lemma fold_left_true :
  forall (p : cand * cand) (l : list (cand * cand)) (k : nat), 
    fold_left (fun (x : bool) (b : cand)
               => andb x (orb (bool_in (b, snd p) l)
                             (el k (fst p, b)))) cand_all true = true ->
    forall c , (bool_in (c, snd p) l) = true \/  (el k (fst p, c)) = true.
Proof.
  intros.
  apply fold_left_andb in H.
  rewrite Forall_forall in H.
  rewrite <- Bool.orb_true_iff.
  apply H.
  apply cand_fin.
Qed.