diff options
Diffstat (limited to 'src/Predicate.v')
| -rw-r--r-- | src/Predicate.v | 1242 |
1 files changed, 1242 insertions, 0 deletions
diff --git a/src/Predicate.v b/src/Predicate.v new file mode 100644 index 0000000..1ff9831 --- /dev/null +++ b/src/Predicate.v @@ -0,0 +1,1242 @@ +Require Import Coq.Structures.Equalities. + +Require Import TVSMT.Coqlib. +Require Import TVSMT.Maps. +Require Import TVSMT.Errors. +Require Import TVSMT.Sat. +Require Import TVSMT.Common. +Require Import TVSMT.Hashtree. + +Local Open Scope error_monad_scope. +Local Open Scope positive. + +(** The [predicate] type defines the path predicates that are used in the [Ieta] and [Igamma] + instructions. *) +Inductive pred {A}: Type := +| Ptrue : pred +| Pfalse : pred +| Pundef : pred +| Pbase : A -> pred +| Pand : pred -> pred -> pred +| Por : pred -> pred -> pred +| Pimp : pred -> pred -> pred +| Pnot : pred -> pred. + +Module PredicateNotation. + + Declare Scope predicate. + + Notation "A ∧ B" := (Pand A B) (at level 20, left associativity) : predicate. + Notation "A ∨ B" := (Por A B) (at level 25, left associativity) : predicate. + Notation "A → B" := (Pimp A B) (at level 30, right associativity) : predicate. + Notation "¬ A" := (Pnot A) (at level 15) : predicate. + Notation "⟂" := (Pfalse) : predicate. + Notation "'T'" := (Ptrue) : predicate. + Notation "○" := (Pundef) : predicate. + +End PredicateNotation. + +Import PredicateNotation. +Local Open Scope predicate. +Local Open Scope bool. +Local Open Scope positive. + +Module ThreeValued(Base: UsualDecidableTypeBoth). + +Definition A := Base.t. +Definition el_dec: forall a b: A, {a = b} + {a <> b} := Base.eq_dec. + +Module Import AH := HashTree(Base). +Module Import AH_Prop := HashTreeProperties(Base). + +Section EVAL. + +Context (eval: A -> option bool). + +Definition predicate := @pred A. + +(* This evaluation follows Łukasiewicz logic. *) +Fixpoint eval_predicate (p: predicate) : option bool := + match p with + | T => Some true + | ⟂ => Some false + | ○ => None + | ¬ p => + match eval_predicate p with + | None => None + | Some b => Some (negb b) + end + | Pbase c => + match eval c with + | Some p => Some p + | None => None + end + | p1 ∧ p2 => + match eval_predicate p1, eval_predicate p2 with + | Some p1', Some p2' => Some (p1' && p2') + | Some false, None => Some false + | None, Some false => Some false + | _, _ => None + end + | p1 ∨ p2 => + match eval_predicate p1, eval_predicate p2 with + | Some p1', Some p2' => Some (p1' || p2') + | Some true, None => Some true + | None, Some true => Some true + | _, _ => None + end + | p1 → p2 => + match eval_predicate p1, eval_predicate p2 with + | Some p1', Some p2' => Some (negb p1' || p2') + | None, Some false => None + | Some true, None => None + | _, _ => Some true + end + end. + +Definition equiv {A} (a b: @pred A) := + Pand (Pimp a b) (Pimp b a). + +Definition hash_pred := @pred positive. + +Definition hash_tree := PTree.t A. + +Lemma comp_list_dec : + forall (a b: list positive), + {a = b} + {a <> b}. +Proof. generalize Pos.eq_dec. decide equality. Defined. + +Lemma hash_pred_dec : + forall (a b: hash_pred), + {a = b} + {a <> b}. +Proof. generalize Pos.eq_dec. generalize bool_dec. repeat decide equality. Defined. + +Lemma predicate_dec : + forall (a b: predicate), + {a = b} + {a <> b}. +Proof. generalize el_dec. generalize bool_dec. repeat decide equality. Defined. + +Definition find_tree (el: A) (h: hash_tree) : option positive := + match + filter (fun x => match x with (a, b) => if el_dec el b then true else false end) + (PTree.elements h) with + | (p, _) :: nil => Some p + | _ => None + end. + +Definition combine_option {A} (a b: option A) : option A := + match a, b with + | Some a', _ => Some a' + | _, Some b' => Some b' + | _, _ => None + end. + +Definition max_key {A} (t: PTree.t A) := + fold_right Pos.max 1 (map fst (PTree.elements t)). + +Fixpoint hash_predicate (p: predicate) (h: PTree.t A) + : hash_pred * PTree.t A := + match p with + | T => (T, h) + | ⟂ => (⟂, h) + | ○ => (○, h) + | ¬ p => let (p', t) := hash_predicate p h in (¬ p', t) + | Pbase c => + match find_tree c h with + | Some p => (Pbase p, h) + | None => + let nkey := max_key h + 1 in + (Pbase nkey, PTree.set nkey c h) + end + | p1 ∧ p2 => + let (p1', t1) := hash_predicate p1 h in + let (p2', t2) := hash_predicate p2 t1 in + (p1' ∧ p2', t2) + | p1 ∨ p2 => + let (p1', t1) := hash_predicate p1 h in + let (p2', t2) := hash_predicate p2 t1 in + (p1' ∨ p2', t2) + | p1 → p2 => + let (p1', t1) := hash_predicate p1 h in + let (p2', t2) := hash_predicate p2 t1 in + (p1' → p2', t2) + end. + +Fixpoint eval_hash_pred (p: hash_pred) (a: PTree.t bool) : option bool := + match p with + | T => Some true + | ⟂ => Some false + | ○ => None + | ¬ p => + match eval_hash_pred p a with + | Some b => Some (negb b) + | None => None + end + | Pbase k => a ! k + | p1 ∧ p2 => + match eval_hash_pred p1 a, eval_hash_pred p2 a with + | Some p1', Some p2' => Some (p1' && p2') + | Some false, None => Some false + | None, Some false => Some false + | _, _ => None + end + | p1 ∨ p2 => + match eval_hash_pred p1 a, eval_hash_pred p2 a with + | Some p1', Some p2' => Some (p1' || p2') + | Some true, None => Some true + | None, Some true => Some true + | _, _ => None + end + | p1 → p2 => + match eval_hash_pred p1 a, eval_hash_pred p2 a with + | Some p1', Some p2' => Some (negb p1' || p2') + | None, Some false => None + | Some true, None => None + | _, _ => Some true + end + end. + +(** The [predicate] type defines the path predicates that are used in the [Ieta] and [Igamma] + instructions. *) +Inductive pred_bin {A}: Type := +| PBtrue : pred_bin +| PBfalse : pred_bin +| PBbase : (bool * A) -> pred_bin +| PBand : pred_bin -> pred_bin -> pred_bin +| PBor : pred_bin -> pred_bin -> pred_bin. + +Definition hash_pred_bin : Type := @pred_bin positive * @pred_bin positive. + +Fixpoint eval_hash_pred_bin1 (p1: @pred_bin positive) (m: PMap.t bool) : bool := + match p1 with + | PBtrue => true + | PBfalse => false + | PBbase (b, p) => if b then m!!p else negb m!!p + | PBand p1 p2 => eval_hash_pred_bin1 p1 m && eval_hash_pred_bin1 p2 m + | PBor p1 p2 => eval_hash_pred_bin1 p1 m || eval_hash_pred_bin1 p2 m + end. + +Definition eval_hash_pred_bin (p1: hash_pred_bin) (m: PMap.t bool) : (bool * bool) := + (eval_hash_pred_bin1 (fst p1) m, eval_hash_pred_bin1 (snd p1) m). + +Fixpoint negate (h: @pred_bin positive) : @pred_bin positive := + match h with + | PBtrue => PBfalse + | PBfalse => PBtrue + | PBbase (b, p) => PBbase (negb b, p) + | PBand p1 p2 => PBor (negate p1) (negate p2) + | PBor p1 p2 => PBand (negate p1) (negate p2) + end. + +Fixpoint conv_hash_pred (p: hash_pred) (h: PTree.t positive) (fresh: positive): + (hash_pred_bin * PTree.t positive * positive) := + match p with + | Ptrue => ((PBfalse, PBtrue), h, fresh) + | Pfalse => ((PBfalse, PBfalse), h, fresh) + | Pundef => ((PBtrue, PBfalse), h, fresh) + | Pnot p => let '((p1, p2), h', fresh') := conv_hash_pred p h fresh in + ((p1, negate p2), h', fresh') + | Pand p1 p2 => + let '((p1s, p1'), h', fresh') := conv_hash_pred p1 h fresh in + let '((p2s, p2'), h'', fresh'') := conv_hash_pred p2 h' fresh' in + ((PBor (PBand p1' p2s) (PBor (PBand p1s p2s) (PBand p1s p2')), + PBand p1' p2'), h'', fresh'') + | Por p1 p2 => + let '((p1s, p1'), h', fresh') := conv_hash_pred p1 h fresh in + let '((p2s, p2'), h'', fresh'') := conv_hash_pred p2 h' fresh' in + ((PBor (PBand (negate p1') p2s) (PBor (PBand (negate p2') p1s) (PBand p1s p2s)), + PBor p1' p2'), h'', fresh'') + | Pimp p1 p2 => + let '((p1s, p1'), h', fresh') := conv_hash_pred p1 h fresh in + let '((p2s, p2'), h'', fresh'') := conv_hash_pred p2 h' fresh' in + ((PBor (PBand (negate p1s) (PBand p1' p2s)) (PBand (negate p2s) (PBand (negate p2') p1s)), + PBor p1s (PBor (negate p1') p2')), h'', fresh'') + | Pbase k => + ((PBbase (true, fresh), PBbase (true, k)), PTree.set k fresh h, fresh+1) + end. + +Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := + match a with + | nil => nil + | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b) + end. + +Definition simplify' {A} (p: @pred A) := + match p with + | A ∧ T => A + | T ∧ A => A + | _ ∧ ⟂ => ⟂ + | ⟂ ∧ _ => ⟂ + | ○ ∧ ○ => ○ + | A ∨ ⟂ => A + | ⟂ ∨ A => A + | _ ∨ T => T + | T ∨ _ => T + | ○ ∨ ○ => ○ + | T → A => A + | ⟂ → _ => T + | _ → T => T + | ○ → ○ => T + | ¬ T => ⟂ + | ¬ ⟂ => T + | ¬ ○ => ○ + | A => A + end. + +Fixpoint simplify {A} (dec: forall a b: @pred A, {a = b} + {a <> b} ) (p: @pred A) := + match p with + | A ∧ B => + let A' := simplify dec A in + let B' := simplify dec B in + if dec A' B' then A' else simplify' (A' ∧ B') + | A ∨ B => + let A' := simplify dec A in + let B' := simplify dec B in + if dec A' B' then A' else simplify' (A' ∨ B') + | A → B => + let A' := simplify dec A in + let B' := simplify dec B in + if dec A' B' then A' else simplify' (A' → B') + | ¬ p => simplify' (¬ (simplify dec p)) + | T => T + | ⟂ => ⟂ + | ○ => ○ + | Pbase a => Pbase a + end. + +Fixpoint sat_hash_pred_bin1' (p: @pred_bin positive) (a: asgn) : bool := + match p with + | PBtrue => true + | PBfalse => false + | PBbase (b, p') => if b then a (Pos.to_nat p') else negb (a (Pos.to_nat p')) + | PBand p1 p2 => sat_hash_pred_bin1' p1 a && sat_hash_pred_bin1' p2 a + | PBor p1 p2 => sat_hash_pred_bin1' p1 a || sat_hash_pred_bin1' p2 a + end. + +Fixpoint sat_hash_pred_bin1 (p: @pred_bin positive) (a: PMap.t bool) : bool := + match p with + | PBtrue => true + | PBfalse => false + | PBbase (b, p') => if b then a !! p' else negb (a !! p') + | PBand p1 p2 => sat_hash_pred_bin1 p1 a && sat_hash_pred_bin1 p2 a + | PBor p1 p2 => sat_hash_pred_bin1 p1 a || sat_hash_pred_bin1 p2 a + end. + +Definition sat_hash_pred_bin (p: hash_pred_bin) (a: PMap.t bool) : bool := + negb (sat_hash_pred_bin1 (fst p) a) && sat_hash_pred_bin1 (snd p) a. + +Definition conv_tree (p: PTree.t positive) (assigns: PTree.t bool) : PMap.t bool := + PTree.fold (fun m i a => + match assigns ! i with + | Some true => PMap.set a false (PMap.set i true m) + | Some false => PMap.set a false (PMap.set i false m) + | None => PMap.set a true (PMap.set i false m) + end) p (PMap.init false). + +Definition interp_bin (b: bool * bool): option bool := + match b with | (true, _) => None | (_, b) => Some b end. + +Fixpoint max_hash_pred (p: hash_pred) := + match p with + | T | ⟂ | ○ => 1 + | Pbase k => k + | p1 ∧ p2 | p1 ∨ p2 | p1 → p2 => Pos.max (max_hash_pred p1) (max_hash_pred p2) + | ¬ p' => max_hash_pred p' + end. + +Definition eval_through_bin (p: hash_pred) (a: PTree.t bool) := + let '(p', h, f) := conv_hash_pred p (PTree.empty _) (max_hash_pred p + 1) in + let m := conv_tree h a in + interp_bin (sat_hash_pred_bin1 (fst p') m, sat_hash_pred_bin1 (snd p') m). + +(*Compute eval_hash_pred (Pand (Por (Pbase 1) (Pbase 2)) (Pbase 3)) + (PTree.set 1 true (PTree.set 3 true (PTree.empty _))). +Compute eval_through_bin (Pand (Por (Pbase 1) (Pbase 2)) (Pbase 3)) + (PTree.set 1 true (PTree.set 3 true (PTree.empty _))).*) + +Lemma satFormula_concat: + forall a b agn, + satFormula a agn -> + satFormula b agn -> + satFormula (a ++ b) agn. +Proof. induction a; crush. Qed. + +Lemma satFormula_concat2: + forall a b agn, + satFormula (a ++ b) agn -> + satFormula a agn /\ satFormula b agn. +Proof. + induction a; simplify; + try apply IHa in H1; crush. +Qed. + +Lemma satClause_concat: + forall a a1 a0, + satClause a a1 -> + satClause (a0 ++ a) a1. +Proof. induction a0; crush. Qed. + +Lemma satClause_concat2: + forall a a1 a0, + satClause a0 a1 -> + satClause (a0 ++ a) a1. +Proof. + induction a0; crush. + inv H; crush. +Qed. + +Lemma satClause_concat3: + forall a b c, + satClause (a ++ b) c -> + satClause a c \/ satClause b c. +Proof. + induction a; crush. + inv H; crush. + apply IHa in H0; crush. + inv H0; crush. +Qed. + +Lemma satFormula_mult': + forall p2 a a0, + satFormula p2 a0 \/ satClause a a0 -> + satFormula (map (fun x : list lit => a ++ x) p2) a0. +Proof. + induction p2; crush. + - inv H. inv H0. apply satClause_concat. auto. + apply satClause_concat2; auto. + - apply IHp2. + inv H; crush; inv H0; crush. +Qed. + +Lemma satFormula_mult2': + forall p2 a a0, + satFormula (map (fun x : list lit => a ++ x) p2) a0 -> + satClause a a0 \/ satFormula p2 a0. +Proof. + induction p2; crush. + apply IHp2 in H1. inv H1; crush. + apply satClause_concat3 in H0. + inv H0; crush. +Qed. + +Lemma satFormula_mult: + forall p1 p2 a, + satFormula p1 a \/ satFormula p2 a -> + satFormula (mult p1 p2) a. +Proof. + induction p1; crush. + apply satFormula_concat; crush. + inv H. inv H0. + apply IHp1. auto. + apply IHp1. auto. + apply satFormula_mult'; + inv H; crush. +Qed. + +Lemma satFormula_mult2: + forall p1 p2 a, + satFormula (mult p1 p2) a -> + satFormula p1 a \/ satFormula p2 a. +Proof. + induction p1; crush. + apply satFormula_concat2 in H; crush. + apply IHp1 in H0. + inv H0; crush. + apply satFormula_mult2' in H1. inv H1; crush. +Qed. + +Fixpoint trans_pred (p: @pred_bin positive) : + {fm: formula | forall a, sat_hash_pred_bin1' p a = true <-> satFormula fm a}. + refine + (match p with + | PBtrue => exist _ nil _ + | PBfalse => exist _ (nil :: nil) _ + | PBbase (b, p') => exist _ (((b, Pos.to_nat p') :: nil) :: nil) _ + | PBand p1 p2 => + match trans_pred p1, trans_pred p2 with + | exist p1' _, exist p2' _ => exist _ (p1' ++ p2') _ + end + | PBor p1 p2 => + match trans_pred p1, trans_pred p2 with + | exist p1' _, exist p2' _ => exist _ (mult p1' p2') _ + end + end); split; crush. + - destruct_match; subst. tauto. simplify. tauto. + - inv H0; crush. destruct_match; crush. subst. apply negb_true_iff. crush. + - apply satFormula_concat. apply i; auto. apply i0; auto. + - apply satFormula_concat2 in H. simplify. apply andb_true_intro. + split. apply i in H0. auto. + apply i0 in H1. auto. + - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto. + apply i0 in H0. auto. + - apply orb_true_intro. + apply satFormula_mult2 in H. inv H. apply i in H0. auto. + apply i0 in H0. auto. +Qed. + +Definition sat_pred (bound: nat) (p: @pred_bin positive) : + option ({al : alist | sat_hash_pred_bin1' p (interp_alist al) = true} + + {forall a : asgn, sat_hash_pred_bin1' p a = false}). + refine + ( match trans_pred p with + | exist fm _ => + match boundedSat bound fm with + | Some (inleft (exist a _)) => Some (inleft (exist _ a _)) + | Some (inright _) => Some (inright _) + | None => None + end + end ). + - apply i in s1. auto. + - intros. specialize (n a). specialize (i a). + destruct (sat_hash_pred_bin1' p a). exfalso. + apply n. apply i. auto. auto. +Qed. + +Lemma negate_correct : + forall h a, sat_hash_pred_bin1' (negate h) a = negb (sat_hash_pred_bin1' h a). +Proof. + induction h; crush. + - repeat destruct_match; subst; crush; symmetry; apply negb_involutive. + - rewrite negb_andb; crush. + - rewrite negb_orb; crush. +Qed. + +Lemma sat_implication : + forall h h' a, + sat_hash_pred_bin1' (PBand (negate h) h') a = false -> + sat_hash_pred_bin1' h' a = true -> + sat_hash_pred_bin1' h a = true. +Proof. + intros. simplify. rewrite negate_correct in H. + rewrite H0 in H. rewrite andb_true_r in H. crush. +Qed. + +Fixpoint trans_pred_simple (p: @pred_bin positive) := + match p with + | PBtrue => nil + | PBfalse => nil :: nil + | PBbase (b, p') => ((b, Pos.to_nat p') :: nil) :: nil + | PBand p1 p2 => + match trans_pred_simple p1, trans_pred_simple p2 with + | p1', p2' => (p1' ++ p2') + end + | PBor p1 p2 => + match trans_pred_simple p1, trans_pred_simple p2 with + | p1', p2' => (mult p1' p2') + end + end. + +(*Compute trans_pred_simple (PBand (PBbase (false, 1)) (PBbase (true, 3))).*) + +Definition sat_pred_simple (bound: nat) (p: @pred_bin positive) := + boundedSatSimple bound (trans_pred_simple p). + +Definition sat_hash_pred_simple (bound: nat) (p: hash_pred_bin) := + match sat_pred_simple bound (PBor (fst p) (negate (snd p))) with + | Some None => Some None + | Some (Some a) => Some (Some a) + | None => None + end. + +Definition sat_hpred_simple bound (p: hash_pred) := + let '(p', h, f) := conv_hash_pred p (PTree.empty _) (max_hash_pred p + 1) in + sat_hash_pred_simple bound p'. + +Lemma max_key_correct' : + forall l hi, In hi l -> hi <= fold_right Pos.max 1 l. +Proof. + induction l; crush. + inv H. lia. + destruct (Pos.max_dec a (fold_right Pos.max 1 l)); rewrite e. + - apply Pos.max_l_iff in e. + assert (forall a b c, a <= c -> c <= b -> a <= b) by lia. + eapply H; eauto. + - apply IHl; auto. +Qed. + +Definition bar (p1: lit): lit := (negb (fst p1), (snd p1)). + +Definition stseytin_or (cur p1 p2: lit) : formula := + (bar cur :: p1 :: p2 :: nil) + :: (cur :: bar p1 :: nil) + :: (cur :: bar p2 :: nil) :: nil. + +Definition stseytin_and (cur p1 p2: lit) : formula := + (cur :: bar p1 :: bar p2 :: nil) + :: (bar cur :: p1 :: nil) + :: (bar cur :: p2 :: nil) :: nil. + +Fixpoint xtseytin (next: nat) (p: @pred_bin positive) {struct p} : (nat * lit * formula) := + match p with + | PBbase (b, p') => (next, (b, Pos.to_nat p'), nil) + | PBtrue => + ((next+1)%nat, (true, next), ((true, next)::nil)::nil) + | PBfalse => + ((next+1)%nat, (true, next), ((false, next)::nil)::nil) + | PBor p1 p2 => + let '(m1, n1, f1) := xtseytin next p1 in + let '(m2, n2, f2) := xtseytin m1 p2 in + ((m2+1)%nat, (true, m2), stseytin_or (true, m2) n1 n2 ++ f1 ++ f2) + | PBand p1 p2 => + let '(m1, n1, f1) := xtseytin next p1 in + let '(m2, n2, f2) := xtseytin m1 p2 in + ((m2+1)%nat, (true, m2), stseytin_and (true, m2) n1 n2 ++ f1 ++ f2) + end. + +Lemma stseytin_and_correct : + forall cur p1 p2 fm c, + stseytin_and cur p1 p2 = fm -> + satLit cur c -> + satLit p1 c /\ satLit p2 c -> + satFormula fm c. +Proof. + intros. + unfold stseytin_and in *. rewrite <- H. + unfold satLit in *. destruct p1. destruct p2. destruct cur. + simpl in *|-. cbn. unfold satLit. cbn. crush. +Qed. + +Lemma stseytin_or_correct : + forall cur p1 p2 fm c, + stseytin_or cur p1 p2 = fm -> + satLit cur c -> + satLit p1 c \/ satLit p2 c -> + satFormula fm c. +Proof. + intros. + unfold stseytin_or in *. rewrite <- H. inv H1. + unfold satLit in *. destruct p1. destruct p2. destruct cur. + simpl in *|-. cbn. unfold satLit. cbn. crush. + unfold satLit in *. destruct p1. destruct p2. destruct cur. + simpl in *|-. cbn. unfold satLit. cbn. crush. +Qed. + +Fixpoint max_predicate (p: @pred_bin positive) : positive := + match p with + | PBbase (b, p) => p + | PBtrue => 1 + | PBfalse => 1 + | PBand a b => Pos.max (max_predicate a) (max_predicate b) + | PBor a b => Pos.max (max_predicate a) (max_predicate b) + end. + +Definition tseytin_simple (p: @pred_bin positive) : formula := + let m := Pos.to_nat (max_predicate p + 1) in + let '(m, n, fm) := xtseytin m p in + (n::nil) :: fm. + +Definition sat_pred_simple_tseytin (p: @pred_bin positive) : option (option alist) := + match boundedSatSimple 10000%nat (tseytin_simple p) with + | Some (Some a) => Some (Some a) + | Some None => Some None + | None => None + end. + +Definition sat_hash_pred_simple_tseytin (p: hash_pred_bin) := + match sat_pred_simple_tseytin (PBor (fst p) (negate (snd p))) with + | Some None => Some None + | Some (Some a) => Some (Some a) + | None => None + end. + +Definition sat_hpred_simple_tseytin (p: hash_pred) := + let '(p', h, f) := conv_hash_pred p (PTree.empty _) (max_hash_pred p + 1) in + sat_hash_pred_simple_tseytin p'. + +(*Compute sat_hpred_simple_tseytin ((Pbase 1 ∨ Pbase 2) → (Pbase 1 ∨ Pbase 2)). +Compute sat_hpred_simple 1000%nat (simplify ((Pbase 1 ∨ Pbase 2) → (Pbase 1 ∨ Pbase 2))).*) + +Lemma max_key_correct : + forall A h_tree hi (c: A), + h_tree ! hi = Some c -> + hi <= max_key h_tree. +Proof. + unfold max_key. intros. apply PTree.elements_correct in H. + apply max_key_correct'. + eapply in_map with (f := fst) in H. auto. +Qed. + +Lemma hash_constant : + forall p h h_tree hi c h_tree', + h_tree ! hi = Some c -> + hash_predicate p h_tree = (h, h_tree') -> + h_tree' ! hi = Some c. +Proof. + induction p; crush. + - repeat (destruct_match; crush); subst. + pose proof H as X. apply max_key_correct in X. + rewrite PTree.gso by lia; auto. + - repeat (destruct_match; crush). exploit IHp1; eauto. + - repeat (destruct_match; crush). exploit IHp1; eauto. + - repeat (destruct_match; crush). exploit IHp1; eauto. + - repeat (destruct_match; crush). exploit IHp; eauto. +Qed. + +Lemma find_tree_correct : + forall c h_tree p, + find_tree c h_tree = Some p -> + h_tree ! p = Some c. +Proof. + intros. + unfold find_tree in H. destruct_match; crush. + destruct_match; simplify. + destruct_match; crush. + assert (In (p, a) (filter + (fun x : positive * A => + let (_, b) := x in if el_dec c b then true else false) (PTree.elements h_tree))). + { rewrite Heql. constructor. auto. } + apply filter_In in H. simplify. destruct_match; crush. subst. + apply PTree.elements_complete; auto. +Qed. + +Lemma find_tree_unique : + forall c h_tree p p', + find_tree c h_tree = Some p -> + h_tree ! p' = Some c -> + p = p'. +Proof. + intros. + unfold find_tree in H. + repeat (destruct_match; crush; []). + assert (In (p, a) (filter + (fun x : positive * A => + let (_, b) := x in if el_dec c b then true else false) (PTree.elements h_tree))). + { rewrite Heql. constructor. auto. } + apply filter_In in H. simplify. + destruct (Pos.eq_dec p p'); auto. + exfalso. + destruct_match; subst; crush. + assert (In (p', a) (PTree.elements h_tree) /\ (fun x : positive * A => + let (_, b) := x in if el_dec a b then true else false) (p', a) = true). + { split. apply PTree.elements_correct. auto. rewrite Heqs. auto. } + apply filter_In in H. rewrite Heql in H. inv H. simplify. crush. crush. +Qed. + +Lemma hash_predicate_hash_le : + forall p n p' n', + hash_predicate p n = (p', n') -> + (PTree_Properties.cardinal n <= PTree_Properties.cardinal n')%nat. +Proof. + induction p; crush. + - repeat (destruct_match; crush). + assert (n ! (max_key n + 1) = None). + { destruct (n ! (max_key n + 1)) eqn:?; auto. + apply max_key_correct in Heqo0. lia. } + exploit PTree_Properties.cardinal_set; eauto. + instantiate (1 := a); intros. lia. + - repeat (destruct_match; crush). + apply IHp1 in Heqp. apply IHp2 in Heqp0. lia. + - repeat (destruct_match; crush). + apply IHp1 in Heqp. apply IHp2 in Heqp0. lia. + - repeat (destruct_match; crush). + apply IHp1 in Heqp. apply IHp2 in Heqp0. lia. + - repeat (destruct_match; crush). + apply IHp in Heqp0. lia. +Qed. + +Lemma hash_predicate_hash_len : + forall p n p' n', + hash_predicate p n = (p', n') -> + PTree_Properties.cardinal n = PTree_Properties.cardinal n' -> + n = n'. +Proof. + induction p; crush. + - repeat (destruct_match; crush). + assert (n ! (max_key n + 1) = None). + { destruct (n ! (max_key n + 1)) eqn:?; auto. + apply max_key_correct in Heqo0. lia. } + exploit PTree_Properties.cardinal_set; eauto. + instantiate (1 := a); intros. lia. + - repeat (destruct_match; crush). + pose proof Heqp as X; apply hash_predicate_hash_le in X. + pose proof Heqp0 as X0; apply hash_predicate_hash_le in X0. + exploit IHp1; eauto. lia. intros; subst. + exploit IHp2; eauto. + - repeat (destruct_match; crush). + pose proof Heqp as X; apply hash_predicate_hash_le in X. + pose proof Heqp0 as X0; apply hash_predicate_hash_le in X0. + exploit IHp1; eauto. lia. intros; subst. + exploit IHp2; eauto. + - repeat (destruct_match; crush). + pose proof Heqp as X; apply hash_predicate_hash_le in X. + pose proof Heqp0 as X0; apply hash_predicate_hash_le in X0. + exploit IHp1; eauto. lia. intros; subst. + exploit IHp2; eauto. + - repeat (destruct_match; crush). + pose proof Heqp0 as X; apply hash_predicate_hash_le in X. + exploit IHp; eauto. +Qed. + +Inductive pred_In {A} : A -> @pred A -> Prop := +| pred_In_Pbase : forall a, pred_In a (Pbase a) +| pred_In_Pand1 : forall c p1 p2, pred_In c p1 -> pred_In c (p1 ∧ p2) +| pred_In_Pand2 : forall c p1 p2, pred_In c p2 -> pred_In c (p1 ∧ p2) +| pred_In_Por1 : forall c p1 p2, pred_In c p1 -> pred_In c (p1 ∨ p2) +| pred_In_Por2 : forall c p1 p2, pred_In c p2 -> pred_In c (p1 ∨ p2) +| pred_In_Pimp1 : forall c p1 p2, pred_In c p1 -> pred_In c (p1 → p2) +| pred_In_Pimp2 : forall c p1 p2, pred_In c p2 -> pred_In c (p1 → p2) +| pred_In_Pnot : forall c p, pred_In c p -> pred_In c (¬ p). + +Lemma pred_In_dec : + forall A (c: A) p, + (forall a b : A, { a = b } + { a <> b }) -> + { pred_In c p } + { ~ pred_In c p }. +Proof. + induction p; crush. + - right. unfold not. intros. inv H. + - right. unfold not. intros. inv H. + - right. unfold not. intros. inv H. + - destruct (X c a); subst. + { left. constructor. } + { right. unfold not. intros. inv H. auto. } + - pose proof X as X1. pose proof X as X2. + apply IHp1 in X1. apply IHp2 in X2. + inv X1; inv X2. left. constructor. tauto. + left. constructor. auto. + left. apply pred_In_Pand2. auto. + right. unfold not. intros. inv H1; auto. + - pose proof X as X1. pose proof X as X2. + apply IHp1 in X1. apply IHp2 in X2. + inv X1; inv X2. left. constructor. tauto. + left. constructor. auto. + left. apply pred_In_Por2. auto. + right. unfold not. intros. inv H1; auto. + - pose proof X as X1. pose proof X as X2. + apply IHp1 in X1. apply IHp2 in X2. + inv X1; inv X2. left. constructor. tauto. + left. constructor. auto. + left. apply pred_In_Pimp2. auto. + right. unfold not. intros. inv H1; auto. + - pose proof X as X1. apply IHp in X1. + inv X1. left. constructor. tauto. + right. unfold not. intros. inv H0; auto. +Qed. + +Lemma pred_In_hash : + forall p n p' n' c, + hash_predicate p n = (p', n') -> + pred_In c p -> + exists t, n' ! t = Some c /\ pred_In t p'. +Proof. + induction p; simplify. + - inv H0. + - inv H0. + - inv H0. + - repeat (destruct_match; crush; []); subst. + destruct_match; simplify. + { inv H0. apply find_tree_correct in Heqo. + econstructor; ecrush core. constructor. } + { inv H0. econstructor. rewrite PTree.gss. crush. constructor. } + - repeat (destruct_match; crush; []). inv H0. + exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto. + constructor; auto. + exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pand2. auto. + - repeat (destruct_match; crush; []). inv H0. + exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto. + constructor; auto. + exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Por2. auto. + - repeat (destruct_match; crush; []). inv H0. + exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto. + constructor; auto. + exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pimp2. auto. + - repeat (destruct_match; crush; []). inv H0. exploit IHp; eauto; simplify. + econstructor; simplify; eauto. econstructor; auto. +Qed. + +Lemma hash_pred_In' : + forall p h t c n n', + hash_predicate p n = (h, n') -> + n ! t = None -> + n' ! t = Some c -> + pred_In c p. +Proof. + induction p; crush. + - repeat (destruct_match); subst; crush. + destruct (Pos.eq_dec t (max_key n + 1)); subst. + { rewrite PTree.gss in H1. simplify. constructor. } + { rewrite PTree.gso in H1; crush. } + - repeat (destruct_match); subst; crush. + destruct (t0 ! t) eqn:?. + { pose proof Heqo as X. eapply hash_constant in X; eauto. simplify. + constructor. eapply IHp1; eauto. } + { apply pred_In_Pand2; eapply IHp2; eauto. } + - repeat (destruct_match); subst; crush. + destruct (t0 ! t) eqn:?. + { pose proof Heqo as X. eapply hash_constant in X; eauto. simplify. + constructor. eapply IHp1; eauto. } + { apply pred_In_Por2; eapply IHp2; eauto. } + - repeat (destruct_match); subst; crush. + destruct (t0 ! t) eqn:?. + { pose proof Heqo as X. eapply hash_constant in X; eauto. simplify. + constructor. eapply IHp1; eauto. } + { apply pred_In_Pimp2; eapply IHp2; eauto. } + - repeat (destruct_match); subst; crush. + exploit IHp; eauto; intros. econstructor; auto. +Qed. + +Lemma hash_pred_In : + forall p h p' h' c n, + hash_predicate p (PTree.empty _) = (h, n) -> + hash_predicate p' n = (h', n) -> + pred_In c p' -> pred_In c p. +Proof. + intros. exploit pred_In_hash; eauto. simplify. + eapply hash_pred_In'; eauto. apply PTree.gempty. +Qed. + +Lemma pred_In_hash2 : + forall p h n n' t, + hash_predicate p n = (h, n') -> + pred_In t h -> + exists c, n' ! t = Some c /\ pred_In c p. +Proof. + induction p; simplify. + - inv H0. + - inv H0. + - inv H0. + - repeat (destruct_match; crush; []); subst. + destruct_match; simplify. + { inv H0. apply find_tree_correct in Heqo. + econstructor; ecrush core. constructor. } + { inv H0. econstructor. rewrite PTree.gss. crush. constructor. } + - repeat (destruct_match; crush; []). inv H0. + exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto. + constructor; auto. + exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pand2. auto. + - repeat (destruct_match; crush; []). inv H0. + exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto. + constructor; auto. + exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Por2. auto. + - repeat (destruct_match; crush; []). inv H0. + exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto. + constructor; auto. + exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pimp2. auto. + - repeat (destruct_match; crush; []). inv H0. + exploit IHp; eauto; simplify; repeat econstructor; ecrush core. +Qed. + +Lemma hash_constant2 : + forall p n h n' v c c', + hash_predicate p n = (h, n') -> + n ! v = Some c -> + n' ! v = Some c' -> + c = c'. +Proof. + intros. + eapply hash_constant in H; eauto. rewrite H1 in H. crush. +Qed. + +Lemma pred_not_in_Pand : + forall A (c: A) p1 p2, + ~ pred_In c (p1 ∧ p2) -> + ~ pred_In c p1 /\ ~ pred_In c p2. +Proof. + intros. split. + - unfold not in *. intros. apply H. constructor. auto. + - unfold not in *. intros. apply H. apply pred_In_Pand2. auto. +Qed. + +Lemma pred_not_in_Por : + forall A (c: A) p1 p2, + ~ pred_In c (p1 ∨ p2) -> + ~ pred_In c p1 /\ ~ pred_In c p2. +Proof. + intros. split. + - unfold not in *. intros. apply H. constructor. auto. + - unfold not in *. intros. apply H. apply pred_In_Por2. auto. +Qed. + +Lemma simplify'_correct : + forall h a, + eval_hash_pred (simplify' h) a = eval_hash_pred h a. +Proof. destruct h; crush; repeat (destruct_match; crush). Qed. + +Lemma eval_hash_pred_Pand_destr : + forall p1 p2 p1' p2' a, + eval_hash_pred p1 a = eval_hash_pred p1' a -> + eval_hash_pred p2 a = eval_hash_pred p2' a -> + eval_hash_pred (Pand p1 p2) a = eval_hash_pred (Pand p1' p2') a. +Proof. intros. simpl. rewrite H in *. rewrite H0 in *. auto. Qed. + +Lemma eval_hash_pred_Pand_symm : + forall p1 p2 a, + eval_hash_pred (Pand p1 p2) a = eval_hash_pred (Pand p2 p1) a. +Proof. simplify. repeat destruct_match; auto. Qed. + +Lemma eval_hash_pred_Por_symm : + forall p1 p2 a, + eval_hash_pred (Por p1 p2) a = eval_hash_pred (Por p2 p1) a. +Proof. simplify. repeat destruct_match; auto. Qed. + +Lemma eval_hash_pred_Por_destr : + forall p1 p2 p1' p2' a, + eval_hash_pred p1 a = eval_hash_pred p1' a -> + eval_hash_pred p2 a = eval_hash_pred p2' a -> + eval_hash_pred (Por p1 p2) a = eval_hash_pred (Por p1' p2') a. +Proof. intros. simpl. rewrite H in *. rewrite H0 in *. auto. Qed. + +Lemma eval_hash_pred_Pand_refl : + forall p1 a, + eval_hash_pred (Pand p1 p1) a = eval_hash_pred p1 a. +Proof. intros. simpl. repeat destruct_match; auto. Qed. + +Lemma eval_hash_pred_Por_refl : + forall p1 a, + eval_hash_pred (Por p1 p1) a = eval_hash_pred p1 a. +Proof. intros. simpl. repeat destruct_match; auto. Qed. + + Lemma pand_false : + forall a b l, + eval_hash_pred (Pand a b) l <> Some true -> + eval_hash_pred b l = Some true -> + eval_hash_pred a l <> Some true. +Proof. simplify. repeat destruct_match; crush. Qed. + +Lemma pand_true : + forall a b l, + eval_hash_pred (Pand a b) l = Some true -> + eval_hash_pred a l = Some true /\ eval_hash_pred b l = Some true. +Proof. simplify; repeat destruct_match; crush. Qed. + +Lemma pand_true2 : + forall a b l, + eval_hash_pred b l = Some true -> + eval_hash_pred a l = Some true -> + eval_hash_pred (Pand a b) l = Some true. +Proof. simplify; repeat destruct_match; crush. Qed. + +Lemma eval_hash_pred_fold_Pand : + forall l x la, + eval_hash_pred (fold_left Pand l x) la = Some true -> + eval_hash_pred x la = Some true. +Proof. + induction l as [| el l' IHl ]; [tauto|]. + intros * EVAL. cbn in *. + eapply IHl in EVAL. eapply pand_true in EVAL; tauto. +Qed. + +Lemma eval_hash_pred_fold_Pand2 : + forall l x la y, + eval_hash_pred (fold_left Pand l x) la = Some true -> + eval_hash_pred y la = Some true -> + eval_hash_pred (fold_left Pand l y) la = Some true. +Proof. + induction l as [| el l' IHl ]; [tauto|]. + intros * EVAL EVALY. cbn in *. + pose proof EVAL as EVAL2. + apply eval_hash_pred_fold_Pand in EVAL. + eapply IHl; eauto. apply pand_true2; apply pand_true in EVAL; tauto. +Qed. + +Lemma eval_hash_pred_fold_Pand3 : + forall l x la, + eval_hash_pred (fold_left Pand l x) la = Some true -> + eval_hash_pred (fold_left Pand l T) la = Some true. +Proof. eauto using eval_hash_pred_fold_Pand2. Qed. + +Lemma eval_hash_pred_fold_Pand4 : + forall l x la, + eval_hash_pred (fold_left Pand l x) la = Some true -> + eval_hash_pred (fold_left Pand l T) la = Some true /\ eval_hash_pred x la = Some true. +Proof. + intros; split; + eauto using eval_hash_pred_fold_Pand3, eval_hash_pred_fold_Pand. +Qed. + +Lemma eval_equiv2 : + forall a b la, + eval_hash_pred a la = eval_hash_pred b la -> + eval_hash_pred (equiv a b) la = Some true. +Proof. + unfold equiv; intros. unfold eval_hash_pred in *. fold eval_hash_pred in *. + repeat destruct_match; try discriminate; crush. +Qed. + +Lemma eval_equiv : + forall a b la, + eval_hash_pred (equiv a b) la = Some true -> + eval_hash_pred a la = eval_hash_pred b la. +Proof. + unfold equiv; intros. unfold eval_hash_pred in *. fold eval_hash_pred in *. + repeat destruct_match; try discriminate; crush. +Qed. + +Lemma eval_hash_pred_T_Pand : + forall a l, + eval_hash_pred (Pand T a) l = eval_hash_pred a l. +Proof. + intros; unfold eval_hash_pred; fold eval_hash_pred; + destruct_match; auto. +Qed. + +Lemma fold_and_forall : + forall p a pt, + eval_hash_pred (fold_left Pand p pt) a = Some true -> + Forall (fun x => eval_hash_pred x a = Some true) p. +Proof. + induction p; crush. + constructor. + - apply eval_hash_pred_fold_Pand in H. eapply pand_true; eauto. + - eapply IHp. eauto. +Qed. + +Lemma fold_and_forall2 : + forall p a pt, + eval_hash_pred pt a = Some true -> + Forall (fun x => eval_hash_pred x a = Some true) p -> + eval_hash_pred (fold_left Pand p pt) a = Some true. +Proof. + induction p; crush. inv H0. + eapply IHp; eauto. + apply pand_true2; eauto. +Qed. + +Lemma fold_and_forall3 : + forall p a, + Forall (fun x => eval_hash_pred x a = Some true) p <-> + eval_hash_pred (fold_left Pand p T) a = Some true. +Proof. + intros; split; intros. + eapply fold_and_forall2; eauto. + eapply fold_and_forall; eauto. +Qed. + +Lemma eval_hash_pred_gso2 : + forall p x y b, + ~ pred_In y p -> + eval_hash_pred p (PTree.set y b x) = eval_hash_pred p x. +Proof. + induction p; try solve [crush]. + - intros * MAX. cbn in *. rewrite PTree.gso; auto. unfold not; intros. + apply MAX; subst; constructor. + - intros. cbn in H. simplify. erewrite !IHp1. + erewrite !IHp2. auto. unfold not in *; intros; apply H; now apply pred_In_Pand2. + unfold not in *; intros; apply H; now constructor. + - intros. cbn in H. simplify. erewrite !IHp1. + erewrite !IHp2. auto. unfold not in *; intros; apply H; now apply pred_In_Por2. + unfold not in *; intros; apply H; now constructor. + - intros. cbn in H. simplify. erewrite !IHp1. + erewrite !IHp2. auto. unfold not in *; intros; apply H; now apply pred_In_Pimp2. + unfold not in *; intros; apply H; now constructor. + - intros. cbn in H. simplify. erewrite !IHp. auto. + unfold not in *; intros; apply H; now constructor. +Qed. + +Lemma eval_hash_pred_gso : + forall p x y b, + (max_hash_pred p < y)%positive -> + eval_hash_pred p (PTree.set y b x) = eval_hash_pred p x. +Proof. + induction p; try solve [crush]. + - intros * MAX. cbn in *. now rewrite PTree.gso by lia. + - intros. cbn in H. simplify. erewrite !IHp1 by lia. + now erewrite !IHp2 by lia. + - intros. cbn in H. simplify. erewrite !IHp1 by lia. + now erewrite !IHp2 by lia. + - intros. cbn in H. simplify. erewrite !IHp1 by lia. + now erewrite !IHp2 by lia. + - intros. cbn in H. simplify. now erewrite !IHp by lia. +Qed. + +Lemma eval_hash_pred_get : + forall p a, + eval_hash_pred (Pbase p) a = a ! p. +Proof. crush. Qed. + +Lemma eval_hash_pred_except : + forall p a a0 a0', + ~ pred_In a p -> + (forall x : positive, x <> a -> a0 ! x = a0' ! x) -> + eval_hash_pred p a0 = eval_hash_pred p a0'. +Proof. + induction p; crush. + - destruct (peq a0 a); subst. + + exfalso. apply H. constructor. + + now rewrite H0 by auto. + - erewrite IHp1; eauto. + erewrite IHp2; eauto. + unfold not; intros; apply H. apply pred_In_Pand2; auto. + unfold not; intros; apply H. constructor; auto. + - erewrite IHp1; eauto. + erewrite IHp2; eauto. + unfold not; intros; apply H. apply pred_In_Por2; auto. + unfold not; intros; apply H. constructor; auto. + - erewrite IHp1; eauto. + erewrite IHp2; eauto. + unfold not; intros; apply H. apply pred_In_Pimp2; auto. + unfold not; intros; apply H. constructor; auto. + - erewrite IHp; eauto. + unfold not; intros; apply H. constructor; auto. +Qed. + +Lemma eval_hash_pred_pand : + forall p p1 p2 p3 a a', + eval_hash_pred p1 a = eval_hash_pred p a' -> + eval_hash_pred p2 a = eval_hash_pred p3 a' -> + eval_hash_pred (p1 ∧ p2) a = eval_hash_pred (p ∧ p3) a'. +Proof. simplify; rewrite !H; now rewrite !H0. Qed. + +Lemma eval_hash_pred_por : + forall p p1 p2 p3 a a', + eval_hash_pred p1 a = eval_hash_pred p a' -> + eval_hash_pred p2 a = eval_hash_pred p3 a' -> + eval_hash_pred (p1 ∨ p2) a = eval_hash_pred (p ∨ p3) a'. +Proof. simplify; rewrite !H; now rewrite !H0. Qed. + +Lemma eval_hash_pred_pimp : + forall p p1 p2 p3 a a', + eval_hash_pred p1 a = eval_hash_pred p a' -> + eval_hash_pred p2 a = eval_hash_pred p3 a' -> + eval_hash_pred (p1 → p2) a = eval_hash_pred (p → p3) a'. +Proof. simplify; rewrite !H; now rewrite !H0. Qed. + +Lemma eval_hash_pred_pnot : + forall p p' a a', + eval_hash_pred p a = eval_hash_pred p' a' -> + eval_hash_pred (¬ p) a = eval_hash_pred (¬ p') a'. +Proof. simplify; now rewrite !H. Qed. + +Lemma fold_left_Pand_rev : + forall l b, + eval_hash_pred (fold_left Pand (rev l) T) b = Some true -> + eval_hash_pred (fold_left Pand l T) b = Some true. +Proof. + intros. + apply fold_and_forall3. + apply fold_and_forall3 in H. + apply Forall_forall; intros. + now eapply Forall_forall in H; [|rewrite <- in_rev; eassumption]. +Qed. + +Lemma fold_left_Pand_rev2 : + forall l b, + eval_hash_pred (fold_left Pand l T) b = Some true -> + eval_hash_pred (fold_left Pand (rev l) T) b = Some true. +Proof. + intros. + apply fold_and_forall3. + apply fold_and_forall3 in H. + apply Forall_forall; intros. + now eapply Forall_forall in H; [|rewrite in_rev; eassumption]. +Qed. + +Lemma eval_hash_pred_T_Pand2 : + forall a b l, + eval_hash_pred b l = Some true -> + eval_hash_pred (Pand a b) l = eval_hash_pred a l. +Proof. + intros; unfold eval_hash_pred; fold eval_hash_pred. + repeat (destruct_match; crush). +Qed. + +Lemma eval_hash_pred_T_Pand3: + forall b a, + eval_hash_pred (b ∧ T) a = eval_hash_pred b a. +Proof. + unfold eval_hash_pred; crush. + repeat (destruct_match; crush). +Qed. + +End EVAL. + +End ThreeValued. |