diff options
Diffstat (limited to 'src/Smtpredicate.v')
| -rw-r--r-- | src/Smtpredicate.v | 5138 |
1 files changed, 5138 insertions, 0 deletions
diff --git a/src/Smtpredicate.v b/src/Smtpredicate.v new file mode 100644 index 0000000..3594d53 --- /dev/null +++ b/src/Smtpredicate.v @@ -0,0 +1,5138 @@ +Require Import Coq.Logic.Decidable. +Require Import Coq.Structures.Equalities. +Require Import Coq.Numbers.Cyclic.Int63.Int63. +Require Import Coq.Sorting.Sorted. +Require Import Coq.Classes.RelationClasses. + +Require Import TVSMT.Coqlib. +Require Import TVSMT.Maps. +Require Import TVSMT.Errors. +Require Import TVSMT.Sat. +Require Import TVSMT.Common. +Require Import TVSMT.Predicate. +Require Import TVSMT.Hashtree. +Import TVSMT.Predicate.PredicateNotation. + +Require SMTCoq.SMTCoq. +Import SMTCoq.SMT_terms. +Import SMTCoq.SMT_terms.Atom. +Import SMTCoq.SMT_terms.Form. +Import SMTCoq.Trace. + +#[local] Open Scope error_monad_scope. +#[local] Open Scope predicate. + +#[export] Hint Unfold is_true : smtpred. + +Local Notation predicate := (@pred positive). + +Parameter pred_verit_unsat : + PArray.array Atom.atom -> + PArray.array Form.form -> + PArray.array Int63.int -> + (PArray.array Form.form + * PArray.array Atom.atom + * PArray.array Int63.int + * option (PArray.array Int63.int) + * Checker_Ext.certif) +. + +Notation latom := Int63.int (only parsing). +Notation _llit := Int63.int (only parsing). +Notation lfargs := (list _llit) (only parsing). + +Inductive lform : Type := +| LFatom (_:latom) +| LFtrue +| LFfalse +| LFnot2 (_:Int63.int) (_:_llit) +| LFand (_:lfargs) +| LFor (_:lfargs) +| LFimp (_:lfargs) +| LFxor (_:_llit) (_:_llit) +| LFiff (_:_llit) (_:_llit) +| LFite (_:_llit) (_:_llit) (_:_llit) +(* Bit-blasting predicate (theory of bit vectors): + bbT a [l1;...;ln] means [l1;...;ln] is the bitwise representation of a + (in little endian) + WARNING: this is a slight infringement of stratification + *) +| LFbbT (_:latom) (_:list _llit) +(* TODO: replace [list _lit] with [fargs] *) +. + +Fixpoint of_list' {A} (i: Z) (a: PArray.array A) (l: list A) := + match l with + | nil => a + | el :: b => + of_list' (i+1) (PArray.set a (Int63.of_Z i) el) b + end. + +Definition of_list {A} (d: A) (l: list A) := + of_list' 0 (PArray.make (Int63.of_Z (Zlength l)) d) l. + +Definition lform_to_form (f: lform): form := + match f with + | LFatom a => Fatom a + | LFtrue => Ftrue + | LFfalse => Ffalse + | LFnot2 i l => Fnot2 i l + | LFand args => Fand (of_list (Int63.of_Z 0) args) + | LFor args => For (of_list (Int63.of_Z 0) args) + | LFimp args => Fimp (of_list (Int63.of_Z 0) args) + | LFxor l1 l2 => Fxor l1 l2 + | LFiff l1 l2 => Fiff l1 l2 + | LFite l1 l2 l3 => Fite l1 l2 l3 + | LFbbT a b => FbbT a b + end. + +Definition form_to_lform (f: form): lform := + match f with + | Fatom a => LFatom a + | Ftrue => LFtrue + | Ffalse => LFfalse + | Fnot2 i l => LFnot2 i l + | Fand args => LFand (Misc.to_list args) + | For args => LFor (Misc.to_list args) + | Fimp args => LFimp (Misc.to_list args) + | Fxor l1 l2 => LFxor l1 l2 + | Fiff l1 l2 => LFiff l1 l2 + | Fite l1 l2 l3 => LFite l1 l2 l3 + | FbbT a b => LFbbT a b + end. + +Definition int_dec: forall a b: Int63.int, {a = b} + {a <> b}. +Proof. + intros. + destruct (Int63.eqb a b) eqn:?; [left|right]. + now apply Int63.eqb_correct. + unfold not; intros. apply Int63.eqb_complete in H. + now rewrite H in Heqb0. +Defined. + +Definition form_eq_dec : + forall d1 d2: lform, {d1 = d2} + {d1 <> d2}. +Proof. + intros. + pose proof int_dec. + pose proof (list_eq_dec H). + decide equality. +Defined. + +Definition atom_eq_dec : + forall d1 d2: atom, {d1 = d2} + {d1 <> d2}. +Proof. + intros. destruct (eqb d1 d2) eqn:?. apply eqb_spec in Heqb. auto. + right. unfold not; intros. apply Typ.not_is_true_eq_false in Heqb. + apply Heqb. unfold is_true. apply eqb_spec. trivial. +Defined. + +Module AtomDec <: MiniDecidableType. + Definition t := atom. + Definition eq_dec := atom_eq_dec. +End AtomDec. +Module AtomHash := Make_UDT(AtomDec). +Module Import AH := HashTree(AtomHash). +Module Import AH_Prop := HashTreeProperties(AtomHash). + +Module FormDec <: MiniDecidableType. + Definition t := lform. + Definition eq_dec := form_eq_dec. +End FormDec. +Module FormHash := Make_UDT(FormDec). +Module Import FH := HashTree(FormHash). +Module Import FH_Prop := HashTreeProperties(FormHash). + +Definition pred_list: Type := (predicate * list (positive * predicate)). + +Definition to_equiv (p: list (positive * predicate)) := + map (fun x => equiv (Pbase (fst x)) (snd x)) p. + +Definition eval_pred_list (p: pred_list) (a: PTree.t bool): option bool := + eval_hash_pred + (Pand (fst p) + (fold_left Pand (to_equiv (snd p)) Ptrue)) a. + +Fixpoint unnest_predicate (fresh: positive) (p: predicate) + : (pred_list * positive) := + match p with + | Ptrue => (Ptrue, nil, fresh) + | Pfalse => (Pfalse, nil, fresh) + | Pundef => (Pundef, nil, fresh) + | Pbase p' => (Pbase p', nil, fresh) + | Pand p1 p2 => + let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in + let '(p2', p2l, fresh2) := unnest_predicate fresh1 p2 in + let nvar := Pbase fresh2 in + (nvar, (fresh2, (Pand p1' p2')) :: p2l ++ p1l, Pos.succ fresh2) + | Por p1 p2 => + let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in + let '(p2', p2l, fresh2) := unnest_predicate fresh1 p2 in + let nvar := Pbase fresh2 in + (nvar, (fresh2, (Por p1' p2')) :: p2l ++ p1l, Pos.succ fresh2) + | Pimp p1 p2 => + let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in + let '(p2', p2l, fresh2) := unnest_predicate fresh1 p2 in + let nvar := Pbase fresh2 in + (nvar, (fresh2, (Pimp p1' p2')) :: p2l ++ p1l, Pos.succ fresh2) + | Pnot p1 => + let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in + let nvar := Pbase fresh1 in + (nvar, (fresh1, Pnot p1') :: p1l, Pos.succ fresh1) + end. + +Notation form_t := (PArray.array SMT_terms.Form.form). +Notation atom_t := (PArray.array SMT_terms.Atom.atom). +Notation root_t := (PArray.array Int63.int) (only parsing). + +Fixpoint all_preds (tree: PTree.t unit) (p: predicate): PTree.t unit := + match p with + | Ptrue | Pfalse | Pundef => tree + | Pbase p' => PTree.set p' tt tree + | Pand p1 p2 | Por p1 p2 | Pimp p1 p2 => all_preds (all_preds tree p1) p2 + | Pnot p1 => all_preds tree p1 + end. + +Definition of_P (a: positive) := Int63.of_Z (Zpos a - 2). +Definition to_P (a: Int63.int) := Z.to_pos (Int63.to_Z a + 2). + +Definition P_of_P (a: positive) := Int63.of_Z ((Zpos a - 2) * 2). +Definition N_of_P (a: positive) := Int63.of_Z ((Zpos a - 2) * 2 + 1). + +Definition of_map {A} (l: PMap.t A): PArray.array A := + PTree.fold (fun st i a => PArray.set st (of_P i) a) + (snd l) + (PArray.make (Int63.of_pos (max_key (snd l))) (fst l)). + +Definition of_tree {A} (d: A) (l: PTree.t A): option (PArray.array A) := + let max := ((max_key l) + 1)%positive in + if Z.pos max <? Int63.wB then + Some (PTree.fold (fun st i a => PArray.set st (of_P i) a) + l (PArray.make (of_P max) d)) + else None. + +Lemma max_key_empty : + forall A (m: PTree.t A), + PTree.bempty m = true -> + max_key m = 1%positive. +Proof. + intros. + rewrite PTree.bempty_correct in H. + unfold max_key. + rewrite PTree.elements_extensional with (n:= PTree.Leaf); auto. + intros. rewrite PTree.gleaf; auto. +Qed. + +Lemma max_key_list_in : forall l, + ((fold_right Pos.max 1%positive l) = 1%positive /\ l = nil) + \/ (In (fold_right Pos.max 1%positive l) l /\ l <> nil). +Proof. + induction l ; intros. + - auto. + - inv IHl. + + inv H. right. simpl. + split; [lia | congruence]. + + inv H. right. simpl. + split; [| congruence]. + edestruct Pos.max_spec with (n:= a) (m:= (fold_right Pos.max 1%positive l)). + * inv H. rewrite H3. right. auto. + * inv H. rewrite H3. left. auto. +Qed. + +Lemma max_key_list_not_nil : forall A l (m: PTree.t A), + (l <> nil) -> + (forall k v, m ! k = Some v -> In k l) -> + (forall k, In k l -> exists v, m ! k = Some v) -> + exists x, m ! (fold_right Pos.max 1%positive l) = Some x. +Proof. + intros A l. + generalize (max_key_list_in l). + intros [HCASE | HCASE]; intros. + - inv HCASE. congruence. + - inv HCASE. + eapply H1; eauto. +Qed. + +Lemma PTree_bempty_false_exists : forall A (m: PTree.t A), + PTree.bempty m = false -> + exists x v, m ! x = Some v. +Proof. + induction m ; intros. + - simpl in *. congruence. + - simpl in *. + destruct o. + + exists xH. simpl. eauto. + + apply andb_false_iff in H. + inv H. + * exploit IHm1; eauto. intros [x [v HSOME]]. + exists (xO x). eauto. + * exploit IHm2; eauto. intros [x [v HSOME]]. + exists (xI x). eauto. +Qed. + +Lemma max_key_in : + forall A (m: PTree.t A), + PTree.bempty m = false -> + exists x, m ! (max_key m) = Some x. +Proof. + unfold max_key. + intros * BEMPTY. + eapply max_key_list_not_nil with (l := (map fst (PTree.elements m))). + - intro. apply map_eq_nil in H. + generalize (PTree_bempty_false_exists _ m BEMPTY); eauto. + intros [x [v HGET]]. + eapply PTree.elements_correct in HGET. + rewrite H in *. inv HGET. + - intros. + eapply PTree.elements_correct in H. + apply in_map_iff. exists (k,v). auto. + - intros. + apply in_map_iff in H. destruct H as [[kk v] [Hfst Helt]]. subst. + simpl. eapply PTree.elements_complete in Helt. + eauto. +Qed. + +Lemma max_key_ext1 : + forall A (m: PTree.t A) m', + (forall x, m ! x = m' ! x) -> + PTree.bempty m = false -> + (max_key m <= max_key m')%positive. +Proof. + intros * ALL BEMPTY. + pose proof (max_key_in _ m BEMPTY) as X. inversion X as [x IN]; clear X. + pose proof IN as Y. rewrite ALL in Y. + assert (BEMPTY2: PTree.bempty m' = false). + { apply not_true_iff_false; unfold not; intros BEMPTY2. + apply not_true_iff_false in BEMPTY. apply BEMPTY. + apply PTree.bempty_correct; intros. + rewrite ALL. eapply PTree.bempty_correct in BEMPTY2; eauto. + } + pose proof (max_key_in _ m' BEMPTY2) as XX. inversion XX as [y IN2]; clear XX. + eapply max_key_correct; eauto. +Qed. + +Lemma max_key_ext2 : + forall A (m: PTree.t A) m', + (forall x, m ! x = m' ! x) -> + PTree.bempty m' = false -> + (max_key m' <= max_key m)%positive. +Proof. + intros * ALL BEMPTY. + pose proof (max_key_in _ m' BEMPTY) as X. inversion X as [x IN]; clear X. + pose proof IN as Y. rewrite <- ALL in Y. + assert (BEMPTY2: PTree.bempty m = false). + { apply not_true_iff_false; unfold not; intros BEMPTY2. + apply not_true_iff_false in BEMPTY. apply BEMPTY. + apply PTree.bempty_correct; intros. + rewrite <- ALL. eapply PTree.bempty_correct in BEMPTY2; eauto. + } + pose proof (max_key_in _ m BEMPTY2) as XX. inversion XX as [y IN2]; clear XX. + eapply max_key_correct; eauto. +Qed. + +Lemma max_key_ext : + forall A (m: PTree.t A) m', + (forall x, m ! x = m' ! x) -> + max_key m' = max_key m. +Proof. + unfold max_key; intros; erewrite PTree.elements_extensional; eauto. +Qed. + +Lemma max_key_map_le : + forall A B (m: PTree.t A) (m': PTree.t B), + (forall x, m ! x <> None <-> m' ! x <> None) -> + PTree.bempty m = false -> + (max_key m <= max_key m')%positive. +Proof. + intros * ALL BEMPTY. + assert (BEMPTY2: PTree.bempty m' = false). + { apply not_true_iff_false; unfold not; intros BEMPTY2. + apply not_true_iff_false in BEMPTY. apply BEMPTY. + apply PTree.bempty_correct; intros. + case_eq (m ! x); intros; auto. + specialize (ALL x). rewrite H in *. + rewrite PTree.bempty_correct in BEMPTY2. + specialize (BEMPTY2 x). + intuition congruence. + } + pose proof (max_key_in _ m BEMPTY) as X. inversion X as [x INx]; clear X. + assert (Y : exists y, m' ! (max_key m) = Some y). + { case_eq (m' ! (max_key m)); intros; eauto. + specialize (ALL (max_key m)). intuition congruence. + } + inversion Y as [y INy]. + try solve [eapply max_key_correct; eauto]. +Qed. + +Lemma ptree_map_same_keys: forall A B (f: positive -> A -> B) m, + forall x, m ! x <> None <-> (PTree.map f m) ! x <> None. +Proof. + split; intros. + - intro. elim H. + rewrite PTree.gmap in H0. + case_eq (m ! x); intros; auto. + rewrite H1 in H0; auto. + simpl in H0. congruence. + - intro. elim H. + rewrite PTree.gmap. + rewrite H0. auto. +Qed. + +Lemma max_key_map : + forall A B (m: PTree.t A) (f: positive -> A -> B), + max_key m = max_key (PTree.map f m). +Proof. + intros *. destruct (PTree.bempty m) eqn:Heqb. + - assert (BEMPTY2: PTree.bempty (PTree.map f m) = true). + { apply PTree.bempty_correct; intros. + eapply PTree.bempty_correct in Heqb; eauto. + rewrite PTree.gmap; eauto. + rewrite Heqb. auto. + } + rewrite ! max_key_empty; auto. + - assert (BEMPTY2: PTree.bempty (PTree.map f m) = false). + { apply not_true_iff_false; intro BEMPTY2. + apply not_true_iff_false in Heqb. apply Heqb. + apply PTree.bempty_correct; intros. + eapply PTree.bempty_correct with (x:= x) in BEMPTY2; eauto. + rewrite PTree.gmap in BEMPTY2; eauto. + unfold option_map in *. destruct_match; easy. + } + eapply Pos.le_antisym; eauto. + + eapply max_key_map_le; eauto. + eapply ptree_map_same_keys; eauto. + + eapply max_key_map_le; eauto. + split. + * intros. eapply ptree_map_same_keys; eauto. + * intros. eapply ptree_map_same_keys in H; eauto. +Qed. + +Lemma gt_1_map_iff : + forall A B (m: PTree.t A) (f: positive -> A -> B), + gt_1 m <-> gt_1 (PTree.map f m). +Proof. + unfold gt_1 in *; simplify. + split. + - simplify. + rewrite PTree.gmap in *. unfold option_map in *. + destruct (m ! x) eqn:?. eapply H. eauto. easy. + - simplify. + eapply H; eauto. + rewrite PTree.gmap. unfold option_map in *. + rewrite H0. easy. +Qed. + +(* From Coq.micromega Require Import RingMicromega QMicromega EnvRing Tauto ZifyComparison ZifyBool ZifyInt63. *) +(* Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. *) + +Lemma bounded_lt : + forall a b n, a < b -> 0 <= a < n -> 0 <= b < n -> a mod n < b mod n. +Proof. + intros; rewrite !Z.mod_small; lia. Qed. + +Lemma max_key_set_le : forall A (m: PTree.t A) k v, + (max_key m <= max_key (PTree.set k v m))%positive. +Proof. + intros. + case_eq (Pos.leb (max_key m) (max_key (PTree.set k v m)))%positive; intros. + - apply Pos.leb_le; auto. + - apply Pos.leb_gt in H; auto. + apply Pos.lt_gt in H. + exploit max_not_present; eauto. + intros. + assert (k <= max_key (PTree.set k v m))%positive. + { eapply max_key_correct; eauto. + rewrite PTree.gss; auto. + } + case_eq (PTree.bempty m); intros. + + exploit max_key_empty; eauto. + intros. rewrite H3 in *. + lia. + + exploit (max_key_in _ m); eauto. + intros [vmk HSome]. + rewrite PTree.gso in H0. + * congruence. + * intro; subst. + rewrite PTree.gss in H0. + congruence. +Qed. + +Lemma PArray_length_fold_set : forall A B a f (t: PTree.t A) (g: A -> B), + PArray.length (PTree.fold (fun st i a => PArray.set st (f i) (g a)) t a) + = PArray.length a. +Proof. + intros. + eapply PTree_Properties.fold_rec; eauto. + intros. + rewrite PArray.length_set. + auto. +Qed. + +Lemma of_pos_rec_inj: forall p1 p2 + (PVALID: 0 <= Z.pos p1 < wB) + (KVALID: 0 <= Z.pos p2 < wB), + (φ (of_pos_rec size p1) = φ (of_pos_rec size p2))%int63 -> + p1 = p2. +Proof. + unfold wB. intros. + rewrite ! of_pos_rec_spec in H; auto. + rewrite ! Z.mod_small in H; try lia. +Qed. + +Lemma of_P_inj : forall k p + (PVALID: 0 <= Z.pos p - 2 < wB) + (KVALID: 0 <= Z.pos k - 2 < wB), + of_P k = of_P p -> k = p. +Proof. + unfold of_P, of_Z, wB, of_pos; intros. + do 2 destruct_match; try lia. + - generalize (of_pos_rec_spec size (Nat.le_refl _) p0). + rewrite Z.mod_small; auto. intros. + rewrite <- H in H0. + rewrite to_Z_0 in H0. + lia. + - generalize (of_pos_rec_spec size (Nat.le_refl _) p0). + rewrite Z.mod_small; auto. intros. + rewrite H in H0. + rewrite to_Z_0 in H0. + lia. + - generalize (of_pos_rec_spec size (Nat.le_refl _) p0). + generalize (of_pos_rec_spec size (Nat.le_refl _) p1). + rewrite !Z.mod_small; auto. intros. + assert (p0 = p1). + { eapply of_pos_rec_inj; eauto. + congruence. + } + lia. +Qed. + +Definition tree_a_wf (t: PTree.t atom) := + 1 < Zpos (max_key t) < wB + /\ gt_1 t + /\ t ! 2 = Some (Acop CO_xH) + /\ t ! 3 = Some (Auop UO_Zpos (of_P 2)) + /\ t ! 4 = Some (Auop UO_Zopp (of_P 3)) +. + +Definition tree_f_wf (t: PTree.t lform) := + 1 < Zpos (max_key t) + /\ (Zpos (max_key t) - 2) * 2 + 1 < wB + /\ gt_1 t + /\ t ! 2 = Some (LFtrue) + /\ t ! 3 = Some (LFfalse) +. + +(* Abstracting over the type of elements of the tree *) +Definition tree_key_wf A (t: PTree.t A) := + 1 < Zpos (max_key t) + /\ ((Zpos (max_key t) - 2) * 2 + 1 < wB + \/ Zpos (max_key t) < wB) + /\ gt_1 t. + +Lemma of_tree_of_P : + forall A d t p (v: A) a + (TAWF: tree_key_wf _ t), + gt_1 t -> + t ! p = Some v -> + of_tree d t = Some a -> + PArray.get a (of_P p) = v. +Proof. + unfold of_tree. + intros. destruct_match; try discriminate. inv H1. + assert + (X: 0 <= Z.pos (max_key t) - 1 <= + to_Z (PArray.length (PTree.fold (fun st i a => PArray.set st (of_P i) a) t + (PArray.make (of_P (max_key t + 1)) d)))). + { erewrite PArray_length_fold_set; eauto. + rewrite PArray.length_make. + unfold PArray.max_length. + unfold wB, size in Heqb. + inv TAWF. + destruct_match; try lia. + - unfold of_P. rewrite of_Z_spec. + rewrite Z.mod_small; try lia. + - rewrite Misc.max_int_wB. + unfold wB in *. lia. + } + unfold gt_1 in *. + generalize dependent H. + generalize dependent Heqb. + generalize dependent v. + generalize dependent p. + generalize dependent X. + apply PTree_Properties.fold_rec; eauto. intros. + - rewrite <- H in H1. + eapply H0; auto. + + erewrite max_key_ext; eauto. + + erewrite max_key_ext; eauto. + + intros. rewrite H in H3; eauto. + - intros. + now rewrite PTree.gempty in H0. + - intros. + destruct (peq k p); subst. + + rewrite PTree.gss in H2. inv H2. + rewrite PArray.get_set_same; auto. + apply Int63.ltb_spec. + rewrite PArray.length_set in X. + destruct X as [XX X]. + eapply Z.lt_le_trans; eauto. + * unfold of_P. rewrite of_Z_spec. + assert (p <= max_key (PTree.set p v0 m))%positive. + { eapply max_key_correct; eauto. + rewrite PTree.gss; auto. + } + rewrite Z.mod_small; try lia. + inv TAWF. inv H5. unfold gt_1 in *. + specialize (H7 _ _ H0). + apply max_key_correct with (hi:= p) in H0; eauto. + apply Pos2Z.pos_le_pos in H0. lia. + + rewrite PTree.gso in H2; auto. + rewrite PArray.get_set_other. + * apply H1; auto. + -- rewrite PArray.length_set in X. + destruct X as [XX X]. + split; [lia |]. + eapply Z.le_trans; eauto. + assert (max_key m <= max_key (PTree.set k v m))%positive + by (eapply max_key_set_le; eauto). + lia. + -- rewrite PArray.length_set in X. + assert (max_key m <= max_key (PTree.set k v m))%positive + by (eapply max_key_set_le; eauto). + rewrite Z.ltb_lt in *. + lia. + -- intros. eapply H3; eauto. + erewrite PTree.gso; eauto. + congruence. + * intro; subst. + eapply of_P_inj in H4; eauto. + apply Z.ltb_lt in Heqb. + rewrite PArray.length_set in X. + -- assert (1 < p)%positive. + { eapply H3; eauto. + rewrite PTree.gso; eauto. + } + assert (p <= max_key (PTree.set k v m))%positive. + { eapply max_key_correct; eauto. + rewrite PTree.gso; eauto. + } + lia. + -- assert (1 < k)%positive. + { eapply H3; eauto. + rewrite PTree.gss; auto. + } + assert (k <= max_key (PTree.set k v m))%positive. + { eapply max_key_correct; eauto. + rewrite PTree.gss; auto. + } + apply Z.ltb_lt in Heqb; auto. + rewrite PArray.length_set in X. + lia. +Qed. + +Definition to_smt_i ah p := + match p with + | Pbase p => match AH.find_tree (Aapp (of_P p) nil) ah with + | Some pi => + if (1 <? Zpos pi) && (Zpos pi <? wB) && (0 <=? Z.pos p - 2) && (Z.pos p - 2 <? wB) + then Some (of_P pi) + else None + | _ => None + end + | Ptrue => Some (Int63.of_Z 1) + | Pfalse => Some (Int63.of_Z 2) + | _ => None + end. + +Fixpoint get_index_acc {A} (dec: A -> A -> bool) (l : list A) + (a : A) (acc : nat) {struct l} : option nat := + match l with + | nil => None + | x :: m => if dec x a then Some acc else get_index_acc dec m a (acc + 1)%nat + end. + +Definition get_index {A} dec (l : list A) (a : A) := get_index_acc dec l a 0. + +Definition form_eqb (f1 f2: form) := + match f1, f2 with + | Fatom i1, Fatom i2 => Int63.eqb i1 i2 + | Ftrue, Ftrue => true + | Ffalse, Ffalse => true + | Fnot2 a1 b1, Fnot2 a2 b2 + | Fiff a1 b1, Fiff a2 b2 + | Fxor a1 b1, Fxor a2 b2 => Int63.eqb a1 a2 && Int63.eqb b1 b2 + | Fand args1, Fand args2 + | For args1, For args2 + | Fimp args1, Fimp args2 => list_beq Int63.eqb (Misc.to_list args1) (Misc.to_list args2) + | Fite a1 b1 c1, Fite a2 b2 c2 => Int63.eqb a1 a2 && Int63.eqb b1 b2 && Int63.eqb c1 c2 + | _, _ => false + end. + +Definition get_fi (lf: list form) (fresh: Z) (f: form): Z * Z * list form := + match get_index form_eqb lf f with Some i => (Z.of_nat i, fresh, lf) | _ => (fresh, Z.succ fresh, lf ++ f::nil) end. + +Definition get_ai (lf: list atom) (fresh: Z) (f: atom): Z * Z * list atom := + match get_index Atom.eqb lf f with Some i => (Z.of_nat i, fresh, lf) | _ => (fresh, Z.succ fresh, lf ++ f::nil) end. + +Definition to_smt_and hf ha p p1 p2 := + let (a1, ha1) := AH.hash_value 1%positive (Abop BO_Zlt p1 p2) ha in + let (a2, ha2) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p1) ha1 in + let (a3, ha3) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p2) ha2 in + let (i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a1)) hf in + let (i2, hf2) := FH.hash_value 1%positive (LFatom (of_P a2)) hf1 in + let (i3, hf3) := FH.hash_value 1%positive (LFatom (of_P a3)) hf2 in + let (i4, hf4) := FH.hash_value 1%positive (LFite (P_of_P i1) (P_of_P i2) (P_of_P i3)) hf3 in + (hf4, ha3, i4). + +Definition to_smt_or hf ha p p1 p2 := + let '(a1, ha1) := AH.hash_value 1%positive (Abop BO_Zlt p1 p2) ha in + let '(a2, ha2) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p2) ha1 in + let '(a3, ha3) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p1) ha2 in + let '(i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a1)) hf in + let '(i2, hf2) := FH.hash_value 1%positive (LFatom (of_P a2)) hf1 in + let '(i3, hf3) := FH.hash_value 1%positive (LFatom (of_P a3)) hf2 in + let '(i4, hf4) := FH.hash_value 1%positive (LFite (P_of_P i1) (P_of_P i2) (P_of_P i3)) hf3 in + (hf4, ha3, i4). + +Definition to_smt_imp hf ha p p1 p2 := + let '(a1, ha1) := AH.hash_value 1%positive (Abop BO_Zminus (of_P 3) p1) ha in + let '(a2, ha2) := AH.hash_value 1%positive (Abop BO_Zplus (of_P a1) p2) ha1 in + let '(a3, ha3) := AH.hash_value 1%positive (Abop BO_Zlt (of_P 3) (of_P a2)) ha2 in + let '(a4, ha4) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p (of_P 3)) ha3 in + let '(a5, ha5) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p (of_P a2)) ha4 in + let '(i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a3)) hf in + let '(i2, hf2) := FH.hash_value 1%positive (LFatom (of_P a4)) hf1 in + let '(i3, hf3) := FH.hash_value 1%positive (LFatom (of_P a5)) hf2 in + let '(i4, hf4) := FH.hash_value 1%positive (LFite (P_of_P i1) (P_of_P i2) (P_of_P i3)) hf3 in + (hf4, ha5, i4). + +Definition to_smt_not hf ha p p1 := + let '(a1, ha1) := AH.hash_value 1%positive (Auop UO_Zopp p1) ha in + let '(a2, ha2) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p (of_P a1)) ha1 in + let '(i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a2)) hf in + (hf1, ha2, i1). + +Definition to_smt_l (el: positive * predicate) (state: option (list Int63.int * FH.hash_tree * AH.hash_tree)) := + match state with + | Some (r, f, a) => + let to_smt_i := to_smt_i a in + match el with + | (p, Pand p1 p2) => + match to_smt_i (Pbase p), to_smt_i p1, to_smt_i p2 with + | Some p', Some p1', Some p2' => + let '(f', a', r') := to_smt_and f a p' p1' p2' in + Some (r++(P_of_P r'::nil), f', a') + | _, _, _ => None + end + | (p, Por p1 p2) => + match to_smt_i (Pbase p), to_smt_i p1, to_smt_i p2 with + | Some p', Some p1', Some p2' => + let '(f', a', r') := to_smt_or f a p' p1' p2' in + Some (r++(P_of_P r'::nil), f', a') + | _, _, _ => None + end + | (p, Pimp p1 p2) => + match to_smt_i (Pbase p), to_smt_i p1, to_smt_i p2 with + | Some p', Some p1', Some p2' => + let '(f', a', r') := to_smt_imp f a p' p1' p2' in + Some (r++(P_of_P r'::nil), f', a') + | _, _, _ => None + end + | (p, Pnot p1) => + match to_smt_i (Pbase p), to_smt_i p1 with + | Some p', Some p1' => + let '(f', a', r') := to_smt_not f a p' p1' in + Some (r++(P_of_P r'::nil), f', a') + | _, _ => None + end + | _ => None + end + | _ => None + end. + +Definition declare_atoms_with_bounds + (a: Z * list Int63.int * FH.hash_tree * AH.hash_tree) := + let '(num, cr, cf, ca) := a in + let (happ, ca_inter) := AH.hash_value 1%positive (Aapp (Int63.of_Z num) nil) ca in + let '((hlt1, hlt2), ca') := + AH.hash_value2 1%positive + (Abop BO_Zle (of_P 4) (of_P happ), + Abop BO_Zge (of_P 3) (of_P happ)) ca_inter in + let '((halt1, halt2), cf_inter) := + FH.hash_value2 1%positive (LFatom (of_P hlt1), LFatom (of_P hlt2)) cf in + let (hlfand, cf') := + FH.hash_value 1%positive (LFand (P_of_P halt1 :: P_of_P halt2 :: nil)) cf_inter in + (num + 1, cr ++ (P_of_P hlfand :: nil), cf', ca'). + +Definition check_tree_f_wf (f: PTree.t lform) := + let max := Z.pos (max_key f) in + (1 <? max) + && ((max - 2) * 2 + 1 <? wB) + && match f ! 1 with None => true | _ => false end + && match f ! 2 with Some LFtrue => true | _ => false end + && match f ! 3 with Some LFfalse => true | _ => false end. + +Definition check_tree_a_wf (a: PTree.t atom) := + let max := Z.pos (max_key a) in + (1 <? max) + && (max <? wB) + && match a ! 1 with None => true | _ => false end + && match a ! 2 with Some (Acop CO_xH) => true | _ => false end + && match a ! 3 with Some (Auop UO_Zpos v) => (v =? 0)%int63 | _ => false end + && match a ! 4 with Some (Auop UO_Zopp v) => (v =? 1)%int63 | _ => false end. + +Definition to_smt (max: positive) (p: pred_list): option (root_t * form_t * atom_t) := + let (p', pl) := p in + let '(_, init_forms) := FH.hash_value2 1%positive (LFtrue, LFfalse) FH.empty in + let (hpone, ia_inter1) := AH.hash_value 1%positive (Acop CO_xH) AH.empty in + let (hzone, ia_inter2) := AH.hash_value 1%positive (Auop UO_Zpos (of_P hpone)) ia_inter1 in + let (hzmone, init_atoms) := AH.hash_value 1%positive (Auop UO_Zopp (of_P hzone)) ia_inter2 in + let '(v, r_defs, form_defs, atom_defs) := + fold_right (fun _ => declare_atoms_with_bounds) + (0, nil, init_forms, init_atoms) + (repeat tt (Pos.to_nat max - 1)) + in + match + fold_right to_smt_l (Some (r_defs, form_defs, atom_defs)) pl, + to_smt_i atom_defs p' + with + | Some (r, f, a), Some p'' => + let '(a1, fin_a) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p'' (Int63.of_Z 1)) a in + let '(f1, fin_f) := FH.hash_value 1%positive (LFatom (of_P a1)) f in + let fin_r := r ++ (N_of_P f1)::nil in + match + of_tree Ftrue (PTree.map (fun _ => lform_to_form) fin_f), + of_tree (Acop CO_xH) fin_a + with + | Some fin_f', Some fin_a' => + if check_form fin_f' + && check_atom fin_a' + && check_tree_f_wf fin_f + && check_tree_a_wf fin_a + && (v <? wB) + && (Zlength fin_r <? wB) + then Some (of_list (Int63.of_Z 0) fin_r, fin_f', fin_a') + else None + | _, _ => None + end + | _, _ => None + end. + +Fixpoint check_list {A} (comp: A -> A -> bool) (a b: list A) := + match b, a with + | _, nil => true + | x::xs, y::ys => comp x y && check_list comp ys xs + | _, _ => false + end. + +Definition check_array {A} (comp: A -> A -> bool) a b := + check_list comp (Misc.to_list a) (Misc.to_list b). + +Definition single_form_not_bv f := + match f with + | Fatom _ | Ftrue | Ffalse | Fnot2 _ _ | Fand _ + | For _ | Fxor _ _ | Fiff _ _ | Fite _ _ _ => true + | FbbT _ _ | Fimp _ => false + end. + +Definition check_atoms_in_form (l: Int63.int) (f: form) := + match f with + | Fatom a => Int63.ltb a l + | _ => true + end. + +Definition check_local_form la f := + Form.check_form f + && Misc.aforallbi (fun i f' => single_form_not_bv f' + && check_atoms_in_form la f') f. + +Definition bool_typ_compdec := SMT_classes.Typ_compdec bool SMT_classes_instances.bool_compdec. +Definition Z_typ_compdec := SMT_classes.Typ_compdec Z SMT_classes_instances.Z_compdec. + +Definition t_i_empty := PArray.make (Int63.of_Z 0) Z_typ_compdec. + +Definition Ztrue := 1. +Definition Zfalse := -1. +Definition Zundef := 0. + +Definition Zand (a b: Z) := + if a <? b then a else b. + +Definition Zor (a b: Z) := + if a <? b then b else a. + +Definition Zimp (a b: Z) := + if 1 <? (1 - a + b) then 1 else (1 - a + b). + +Definition Znot (a: Z) := - a. + +Definition Zval (v: option bool): Z := + match v with + | Some true => 1 + | Some false => -1 + | None => 0 + end. + +Definition t_func_mk: Z -> tval t_i_empty := fun b => Tval t_i_empty (nil, Typ.TZ) b. + +(* Definition asgn_transl' (max: positive) (a: PTree.t bool) := *) +(* Misc.foldi (fun i na => PArray.set na i (t_func_mk (Zval (a!(to_P i))))) *) +(* (Int63.of_Z 0) (of_P max) *) +(* (PArray.make (of_P max) (t_func_mk 0)). *) + +Inductive asgn_transl_spec (a: PTree.t bool) (res: PArray.array (tval t_i_empty)) := +| asgn_transl_rule : + (forall i, 0 <= Z.pos i - 2 < wB -> PArray.get res (of_P i) = t_func_mk (Zval (a!i))) -> + PArray.default res = t_func_mk 0 /\ (forall i, exists n, PArray.get res i = t_func_mk n) -> + asgn_transl_spec a res. + +Definition asgn_transl (a: PTree.t bool) := + let max := max_key a in + PTree.fold (fun na i el => + PArray.set na (of_P i) (t_func_mk (Zval (Some el))) + ) a (PArray.make (of_P (max + 1)) (t_func_mk 0)). + +Lemma PArray_set_out_of_bound: forall A (a: PArray.array A) k d i, + (k <? PArray.length a = false)%int63 -> + PArray.get (PArray.set a k d) i = PArray.get a i. +Proof. + intros. + unfold PArray.set in *. + destruct a. simpl PArray.length in *. + destruct_match. + - auto. + - rewrite Misc.ltb_negb_geb in H. + rewrite negb_false_iff in H. + congruence. +Qed. + +Lemma PArray_default_fold_set : forall A B (m: PTree.t A) f (g: A -> B) array, + PArray.default (PTree.fold (fun st i a => PArray.set st (f i) (g a)) m array) = + PArray.default array. +Proof. + intros. + eapply PTree_Properties.fold_rec; eauto. + intros. rewrite PArray.default_set; auto. +Qed. + +Lemma asgn_transl_OOB: forall a k, + (k <? PArray.length (asgn_transl a) = false)%int63 -> + PArray.get (asgn_transl a) k = t_func_mk 0. +Proof. + unfold asgn_transl. + intros. + rewrite PArray.get_outofbound; auto. + rewrite PArray_default_fold_set; auto. +Qed. + +Lemma exists_asgn: + forall a, + forall (MAX: Z.pos (max_key a) - 2 < wB - 1), + (forall k x, a ! k = Some x -> (0 <= Z.pos k - 2 < wB)%int63) -> + exists res, asgn_transl_spec a res. +Proof. + intros. exists (asgn_transl a). + constructor. + intros i. + case_eq (of_P i <? PArray.length (asgn_transl a))%int63. + - unfold asgn_transl in *. + revert H. + eapply PTree_Properties.fold_rec; eauto. + + intros. rewrite <- H. + eapply H0; eauto. + intros. eapply H1; eauto. + rewrite <- H. eauto. + + intros. simpl. unfold Zval. rewrite PTree.gempty. + destruct_match; auto. + + unfold Zval. intros. + rewrite PArray.length_set in H3. + destruct (peq i k). + * subst. + rewrite PTree.gss. + rewrite PArray.get_set_same; auto. + * rewrite PTree.gso; auto. + rewrite PArray.get_set_other; auto. + -- eapply H1; eauto. + intros. eapply H2; eauto. + rewrite PTree.gso; eauto. + congruence. + -- intro. eapply of_P_inj in H5; eauto. + exploit (H2 k); eauto. + rewrite PTree.gss; eauto. + - intros. + rewrite PArray.get_outofbound; auto. + unfold asgn_transl. + rewrite PArray_default_fold_set. + rewrite PArray.default_make. + case_eq (a ! i); auto. intros b Haib. + unfold asgn_transl in H0. + rewrite PArray_length_fold_set in H0. + rewrite PArray.length_make in H0. + assert (0 <= Z.pos (max_key a) - 2 < wB). + { case_eq (PTree.bempty a); intros. + - rewrite PTree.bempty_correct in H2. + specialize (H2 i). + congruence. + - eapply max_key_in in H2. + destruct H2 as [x Hmax]. + eapply H in Hmax; eauto. + } + assert (i <= max_key a)%positive by (eapply max_key_correct; eauto). + case_eq (of_P (max_key a + 1) ≤? PArray.max_length)%int63; intros. + + rewrite H4 in H0. + rewrite Misc.ltb_negb_geb in H0. + rewrite negb_false_iff in H0. + unfold PArray.max_length in *. + unfold of_P in *. + rewrite ! leb_spec in *. + rewrite ! of_Z_spec in *. + rewrite Misc.max_int_wB in *. + rewrite ! Z.mod_small in *; try lia. + + rewrite H4 in *. + rewrite Misc.leb_negb_gtb in H4. + rewrite negb_false_iff in H4. + unfold PArray.max_length in *. + rewrite ! ltb_spec in *. + rewrite Misc.max_int_wB in *. + unfold of_P in *. + rewrite of_Z_spec in *. + rewrite Z.mod_small in *; try lia. + - unfold asgn_transl; intros. + eapply PTree_Properties.fold_rec; eauto; split; intros. + + auto. + + econstructor. rewrite PArray.get_make. auto. + + rewrite PArray.default_set. tauto. + + inv H2. + * destruct (int_dec (of_P k) i); subst. + ** destruct (of_P k <? PArray.length a0)%int63 eqn:?. + *** econstructor. rewrite PArray.get_set_same; eauto. + *** econstructor. rewrite PArray.get_outofbound. rewrite PArray.default_set. eassumption. + rewrite PArray.length_set. auto. + ** destruct (i <? PArray.length a0)%int63 eqn:?. + *** specialize (H4 i). inv H4. econstructor. rewrite PArray.get_set_other; eassumption. + *** econstructor. rewrite PArray.get_outofbound. rewrite PArray.default_set. eassumption. + rewrite PArray.length_set. auto. +Qed. + +Definition empty_tfunc := + PArray.make 0 (t_func_mk 0). + +Definition check_root_index (f: PArray.array form) (r: PArray.array Int63.int) := + forallb (fun x => to_Z (State.Lit.blit x) <? to_Z (PArray.length f)) (Misc.to_list r). + +Definition check_wt_extra a := + Misc.aforallbi (fun i a' => + match a' with + | Anop _ _ => false + | Aapp _ (_::_) => false + | _ => true + end) a. + +Fixpoint pred_in c p := + match p with + | Ptrue | Pfalse | Pundef => false + | Pbase c2 => (c =? c2)%positive + | Pand p1 p2 | Por p1 p2 | Pimp p1 p2 => pred_in c p1 || pred_in c p2 + | Pnot p' => pred_in c p' + end. + +Definition check_smt (p: predicate): bool := + let a_preds1 := + (max_hash_pred p + 1)%positive + in + let '(p', a_preds) := unnest_predicate a_preds1 p in + match to_smt a_preds p' with + | Some (d, forms, atoms) => + let '(nf, na, roots, used_roots, cert) := pred_verit_unsat atoms forms d in + check_array form_eqb forms nf + && check_array Atom.eqb atoms na + && check_local_form (PArray.length atoms) forms + && Atom.check_atom na + && Atom.wt _ empty_tfunc na + && check_wt_extra na + && (check_root_index forms d && negb (pred_in 1 p) && (Z.pos a_preds <? wB)) + && Checker_Ext.checker_ext na nf d used_roots cert + | None => false + end. + +Definition mutate1_p (p: predicate): predicate := + match p with + | Pand p1 p2 => Pand p2 p1 + | Por p1 p2 => Por p2 p1 + | Pimp (Pand p1 p2) b => Pimp (Pand p2 p1) b + | Pimp (Por p1 p2) b => Pimp (Por p2 p1) b + | Pimp b (Pand p1 p2) => Pimp b (Pand p2 p1) + | Pimp b (Por p1 p2) => Pimp b (Por p2 p1) + | Pnot (Pand p1 p2) => Pnot (Pand p2 p1) + | Pnot (Por p1 p2) => Pnot (Por p2 p1) + | p => p + end. + +Fixpoint has_Pbase (p: predicate) := + match p with + | Ptrue | Pfalse | Pundef => false + | Pbase _ => true + | Pand a b | Por a b | Pimp a b => has_Pbase a || has_Pbase b + | Pnot a => has_Pbase a + end. + +Definition check_smt_total (p: predicate): bool := + if check_smt p then true + else if check_smt (mutate1_p p) then true + else false. + + (** We need a higher level specification for this function so that everything is easier to prove. *) + + Definition upd_asgn := + fold_left + (fun a' el => + match eval_hash_pred (snd el) a' with + | Some p_b => PTree.set (fst el) p_b a' + | _ => a' + end). + + Inductive upd_asgn_spec: list (positive * predicate) -> PTree.t bool -> PTree.t bool -> Prop := + | upd_asgn_intros x : + upd_asgn_spec nil x x + | upd_asgn_cons_Some x xs t1 t2 b: + eval_hash_pred (snd x) t1 = Some b -> + upd_asgn_spec xs (PTree.set (fst x) b t1) t2 -> + upd_asgn_spec (x :: xs) t1 t2 + | upd_asgn_cons_None x xs t1 t2: + eval_hash_pred (snd x) t1 = None -> + upd_asgn_spec xs t1 t2 -> + upd_asgn_spec (x :: xs) t1 t2. + + (* #[local] Open Scope positive. *) + (* Compute PTree.get 3 (upd_asgn ((3, Pbase 2)::(2, Pbase 1)::nil) (PTree.set 1 false (PTree.empty _))). *) + + (* Lemma upd_asgn_cons : *) + (* forall p form r a, *) + (* (forall pb, pred_In pb form -> ~ In pb (map fst r)) -> *) + (* (upd_asgn ((p, form)::r) a) ! p = eval_hash_pred form a. *) + (* Proof. *) + + (* Lemma upd_asgn_cons_form : *) + (* forall p form r a, *) + (* eval_hash_pred (Pbase p) (upd_asgn ((p, form)::r) a) = eval_hash_pred form a. *) + (* Proof. *) + + (* Lemma wt_correct' : *) + (* v_type Typ.type (Typ.interp t_i_empty) (PArray.get (Atom.t_interp t_i_empty a' atoms) i) *) + + Ltac ldestruct_match := + match goal with + | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:? + end. + + Lemma wt_correct' : + forall a' a (atoms: atom_t) + (ATOMSNONOP: forall i x l, PArray.get atoms i <> Anop x l) + (ATOMSAPP: forall i n l, PArray.get atoms i = Aapp n l -> l = nil) + (GETA1: forall i, exists n, PArray.get a' i = t_func_mk n) + (GETA2: forall i, exists n, PArray.get a i = t_func_mk n), + forall i, + v_type Typ.type (Typ.interp t_i_empty) + (PArray.get (Atom.t_interp t_i_empty a atoms) i) = + v_type Typ.type (Typ.interp t_i_empty) (PArray.get (Atom.t_interp t_i_empty a' atoms) i). + Proof. + intros. generalize dependent i. + pose proof (Atom.length_t_interp t_i_empty a atoms) as Y1. + pose proof (Atom.length_t_interp t_i_empty a' atoms) as Y2. + generalize dependent Y2. + generalize dependent Y1. + apply Misc.foldi_ind2 with + (P := (fun x b b' => + PArray.length b = PArray.length atoms -> + PArray.length b' = PArray.length atoms -> + (forall i, + v_type Typ.type (Typ.interp t_i_empty) (PArray.get b i) + = v_type Typ.type (Typ.interp t_i_empty) (PArray.get b' i)))). + + apply Misc.leb_0. + + intros. rewrite PArray.get_make in *. crush. + + intros. + rewrite PArray.length_set in *. + pose proof H0 as LT1. apply Int63.ltb_spec in LT1. + pose proof H as LE2. apply Int63.leb_spec in LE2. + destruct (int_dec i i0); subst. + rewrite !PArray.get_set_same by (apply Int63.ltb_spec; try (rewrite H3); try rewrite H2; lia); auto. + specialize (H1 H2 H3). assert (EQ1:=H2). assert (EQ2:=H3). clear H2. clear H3. + destruct (PArray.get atoms i0) eqn:ATOMS; subst; simplify. + - unfold interp_cop; repeat destruct_match; subst; auto. + - assert (HEQ := H1 i). unfold interp_uop; destruct_match; unfold apply_unop; + repeat destruct_match; auto; + setoid_rewrite Heqb0 in HEQ; simplify; + setoid_rewrite Heqb in HEQ; simplify; subst; rewrite Heqc in Heqc0; discriminate. + - assert (HEQ1 := H1 i). assert (HEQ2 := H1 i1). + unfold interp_bop. destruct_match; + unfold apply_binop; repeat destruct_match; auto; + try (setoid_rewrite Heqb4 in HEQ2; setoid_rewrite Heqb2 in HEQ2; + setoid_rewrite Heqb3 in HEQ1; setoid_rewrite Heqb1 in HEQ1; + simplify; subst; try rewrite Heqc0 in *; try rewrite Heqc1 in *; + try rewrite Heqc2 in *; try rewrite Heqc3 in *; discriminate). + - assert (HEQ1 := H1 i). assert (HEQ2 := H1 i1). assert (HEQ3 := H1 i2). + unfold interp_top. destruct_match; subst. unfold apply_terop. + repeat destruct_match; auto; + setoid_rewrite Heqb4 in HEQ3; setoid_rewrite Heqb2 in HEQ1; setoid_rewrite Heqb3 in HEQ2; + setoid_rewrite Heqb1 in HEQ3; setoid_rewrite Heqb in HEQ1; setoid_rewrite Heqb0 in HEQ2; + simplify; subst; try rewrite Heqc4 in *; try rewrite Heqc3 in *; try rewrite Heqc2 in *; + try rewrite Heqc1 in *; try rewrite Heqc0 in *; try rewrite Heqc in *; discriminate. + - exfalso. eapply ATOMSNONOP; eassumption. + - assert (HEQ1 := H1 i). specialize (GETA1 i). specialize (GETA2 i). + inv GETA1. inv GETA2. + repeat destruct_match. assert (l = nil) by (eapply ATOMSAPP; eassumption); subst. + cbn [map]. unfold t_func_mk in *. unfold Tval in *. inv H2. simpl. + inv H3. auto. + - rewrite !PArray.get_set_other + by (auto; apply Int63.ltb_spec; try (rewrite H3); try rewrite H2; lia); + eauto. + Qed. + + Lemma wt_correct2 : + forall atoms a a' + (ATOMSNONOP: forall i x l, PArray.get atoms i <> Anop x l) + (ATOMSAPP: forall i n l, PArray.get atoms i = Aapp n l -> l = nil) + (GETA1: forall i, exists n, PArray.get a' i = t_func_mk n) + (GETA2: forall i, exists n, PArray.get a i = t_func_mk n), + is_true (wt t_i_empty a atoms) -> + is_true (wt t_i_empty a' atoms). + Proof. + unfold is_true, wt; intros. + apply Misc.aforallbi_spec; intros i LTB. + eapply Misc.aforallbi_spec in H; [|eassumption]. + unfold check_aux in *. + destruct (PArray.get atoms i) eqn:?; unfold get_type' in *. + - erewrite wt_correct'; eassumption. + - destruct_match. simplify. + setoid_rewrite wt_correct' with (a':=a); eauto. + rewrite H0. rewrite H1. auto. + - repeat destruct_match; simplify. + setoid_rewrite wt_correct' with (a':=a); eauto. + rewrite H1. rewrite H. rewrite H2. auto. + - repeat destruct_match; simplify. + setoid_rewrite wt_correct' with (a':=a); eauto. + rewrite H1. rewrite H0. rewrite H2. rewrite H3. auto. + - exfalso; eapply ATOMSNONOP; eauto. + - repeat destruct_match; crush. eapply ATOMSAPP in Heqa0; subst. simplify. + assert (GETB1:=GETA1). assert (GETB2:=GETA2). + specialize (GETA1 i0). specialize (GETA2 i0). inv GETA1. inv GETA2. + rewrite H in Heqf. rewrite H2 in Heqf0. unfold t_func_mk, Tval in *. + simplify. erewrite wt_correct'; eauto. + Qed. + + Lemma wf_empty_tfunc : + forall i, + exists n, PArray.get empty_tfunc i = t_func_mk n. + Proof. unfold empty_tfunc. intros. eexists. rewrite PArray.get_make. eauto. Qed. + + Lemma to_P_of_P : + forall p, 1 < Z.pos p < wB -> to_P (of_P p) = p. + Proof. + unfold to_P, of_P; intros * LT. + rewrite of_Z_spec. rewrite !Z.mod_small by lia. + assert (forall x, x - 2 + 2 = x) by lia. + rewrite H; auto. + Qed. + +Lemma not_int63_lt_0 : forall i, 0 <= Int63.to_Z i. +Proof. + intro i. + assert (~ Int63.to_Z i < 0). + { unfold not; intros. rewrite <- Int63.to_Z_0 in H. + apply Int63.ltb_spec in H. now apply Misc.ltb_0 in H. } + lia. +Qed. + + Lemma of_P_to_P : + forall p, of_P (to_P p) = p. + Proof. + unfold to_P, of_P; intros. rewrite Z2Pos.id. + assert (forall x, x + 2 - 2 = x) by lia. rewrite H. + now rewrite of_to_Z. + pose proof (not_int63_lt_0 p). lia. + Qed. + + Lemma wf_asgn_spec : + forall a a', + asgn_transl_spec a a' -> + forall i, exists n, PArray.get a' i = t_func_mk n. + Proof. inversion 1; intros. inv H1. eauto. Qed. + + Lemma wt_correct : + forall atoms a a' + (ATOMSNONOP: forall i x l, PArray.get atoms i <> Anop x l) + (ATOMSAPP: forall i n l, PArray.get atoms i = Aapp n l -> l = nil), + is_true (wt _ empty_tfunc atoms) -> + asgn_transl_spec a a' -> + is_true (wt _ a' atoms). + Proof. + intros. + pose proof (wf_asgn_spec _ _ H0). + pose proof wf_empty_tfunc. + eapply wt_correct2; eauto. + Qed. + +Section SMT_PROOF. + + Fixpoint Zeval (a: PTree.t bool) (p: predicate) := + match p with + | Ptrue => 1 + | Pfalse => -1 + | Pundef => 0 + | Pbase p' => Zval (a ! p') + | Pnot p' => Znot (Zeval a p') + | Pand p1 p2 => Zand (Zeval a p1) (Zeval a p2) + | Por p1 p2 => Zor (Zeval a p1) (Zeval a p2) + | Pimp p1 p2 => Zimp (Zeval a p1) (Zeval a p2) + end. + + Lemma Zeval_correct : + forall a p, + Zeval a p = Zval (eval_hash_pred p a). + Proof. + induction p; crush; + repeat (destruct_match; simplify); + try (rewrite IHp1; rewrite IHp2); + auto; rewrite IHp; auto; discriminate. + Qed. + +End SMT_PROOF. + +Lemma check_local_form_spec : + forall l f, + is_true (check_local_form l f) -> + (forall i a b, PArray.get f i <> FbbT a b) + /\ (forall i a, PArray.get f i <> Fimp a) + /\ (forall i a, PArray.get f i = Fatom a -> is_true (Int63.ltb a l)) + /\ is_true (check_form f). +Proof. + unfold check_local_form, is_true; simplify; auto. + - unfold not; intros. + destruct (Int63.ltb i (PArray.length f)) eqn:Heqb. + + eapply Misc.aforallbi_spec in H1; try eassumption. now rewrite H in H1. + + unfold check_form in H0. simplify. unfold is_Ffalse, is_Ftrue in *. + repeat (destruct_match; try discriminate). + rewrite PArray.get_outofbound in H; auto. now rewrite Heqf1 in H. + - unfold not; intros. + destruct (Int63.ltb i (PArray.length f)) eqn:Heqb. + + eapply Misc.aforallbi_spec in H1; try eassumption. now rewrite H in H1. + + unfold check_form in H0. simplify. unfold is_Ffalse, is_Ftrue in *. + repeat (destruct_match; try discriminate). + rewrite PArray.get_outofbound in H; auto. now rewrite Heqf1 in H. + - intros. + destruct (Int63.ltb i (PArray.length f)) eqn:Heqb. + + eapply Misc.aforallbi_spec in H1; try eassumption. simplify. + unfold check_atoms_in_form in H3. now rewrite H in H3. + + unfold check_form in H0. simplify. unfold is_Ffalse, is_Ftrue in *. + repeat (destruct_match; try discriminate). + rewrite PArray.get_outofbound in H by auto. now rewrite Heqf1 in H. +Qed. + +Lemma to_list_corr' : + forall A a, + (fun f b => + (forall i, (Int63.to_Z i < Int63.to_Z f) -> + PArray.get a i = nth (Z.to_nat (Int63.to_Z i)) (rev b) (PArray.default a)) + /\ Int63.to_Z f = Zlength b) + (PArray.length a) + (Misc.foldi (fun i (l : list A) => PArray.get a i :: l) + (Int63.of_Z 0) + (PArray.length a) nil). +Proof. + intros. apply Misc.foldi_ind; intros. + apply Int63.leb_spec. simplify; auto. + pose proof (not_int63_lt_0 (PArray.length a)). + rewrite Int63.to_Z_0. auto. + split; intros. simpl in H. rewrite Int63.to_Z_0 in H. + rewrite <- Int63.to_Z_0 in H. apply Int63.ltb_spec in H. + now apply Misc.ltb_0 in H. auto. + split; [|erewrite Misc.to_Z_add_1 by eassumption; + rewrite Zlength_cons; lia]. + cbn [rev]. intros. erewrite Misc.to_Z_add_1 in H2 by eassumption. + assert (Int63.to_Z i0 < Int63.to_Z i \/ Int63.to_Z i0 = Int63.to_Z i) by lia. + inv H3. rewrite app_nth1; auto. apply H1; lia. apply Nat2Z.inj_lt. + rewrite rev_length. + rewrite <- Zlength_correct. + rewrite Z_to_nat_max. + apply Int63.leb_spec in H. + apply Int63.ltb_spec in H0. + pose proof (not_int63_lt_0 i0). lia. + apply Int63.leb_spec in H. + apply Int63.ltb_spec in H0. simpl in H. + rewrite app_nth2; rewrite rev_length. + replace (Datatypes.length a0) with (Z.to_nat (Z.of_nat (Datatypes.length a0))) + by (now apply Nat2Z.id). + rewrite <- Zlength_correct. + rewrite <- Z2Nat.inj_sub. rewrite Zeq_minus by lia. + simpl. apply Int63.to_Z_inj in H4. + now subst. + rewrite Zlength_correct. lia. + zify. rewrite <- Zlength_correct. lia. +Qed. + +Lemma to_list_corr : + forall A (a: PArray.array A) i, + Int63.to_Z i < Int63.to_Z (PArray.length a) -> + PArray.get a i = nth (Z.to_nat (Int63.to_Z i)) (Misc.to_list a) (PArray.default a). +Proof. + intros; pose proof (to_list_corr' A a). + inv H0; auto. +Qed. + +Lemma check_list_correct : + forall A comp (a: list A) b i da db + (CHK : is_true (check_list comp a b)) + (LT : (i < (length a))%nat), + is_true (comp (nth i b db) (nth i a da)). +Proof. + unfold is_true; induction a; try solve[crush]. + intros. + simpl in CHK. destruct_match; try discriminate. + apply andb_prop in CHK. inv CHK. + simplify. destruct i. auto. + apply IHa; auto. lia. +Qed. + +Lemma Zlength_aux_concat: forall A (l1 l2: list A) (acc: Z), + Zlength_aux acc _ (l1 ++ l2) = Zlength_aux (Zlength_aux acc _ l1) _ l2. +Proof. + induction l1 ; intros; eauto. + simpl. + rewrite IHl1; eauto. +Qed. + +Lemma length_to_list : + forall A (a: PArray.array A), + Int63.to_Z (PArray.length a) = Zlength (Misc.to_list a). +Proof. + intros. unfold Misc.to_list. + eapply Misc.foldi_ind; eauto. + - apply Misc.leb_0. + - intros. unfold Zlength in *. simpl. + rewrite Zlength_aux_concat. + rewrite <- H1. simpl. + erewrite Misc.to_Z_add_1; eauto. +Qed. + +Lemma check_list_length : + forall A comp (l1: list A) l2, + is_true (check_list comp l1 l2) -> + Zlength l1 <= Zlength l2. +Proof. + induction l1; crush. rewrite Zlength_nil. rewrite Zlength_correct. lia. + destruct l2; crush. rewrite !Zlength_cons. + unfold is_true in H. simplify. eapply IHl1 in H1. lia. +Qed. + +Lemma check_array_length : + forall A comp (a: PArray.array A) b, + is_true (check_array comp a b) -> + Int63.to_Z (PArray.length a) <= Int63.to_Z (PArray.length b). +Proof. + intros. unfold check_array in *. + eapply check_list_length in H. rewrite !length_to_list; auto. +Qed. + +Lemma check_array_correct : + forall A comp (a: PArray.array A) b, + is_true (check_array comp a b) -> + forall i, + Int63.to_Z i < Int63.to_Z (PArray.length a) -> + is_true (comp (PArray.get b i) (PArray.get a i)). +Proof. + unfold check_array, is_true; intros * CHK i LT. + pose proof (not_int63_lt_0 i). + repeat rewrite to_list_corr. + apply check_list_correct; auto. zify. rewrite <- Zlength_correct. + rewrite <- length_to_list. lia. + lia. apply check_array_length in CHK. lia. +Qed. + +Section PROOF. + + Context (t_i: PArray.array SMT_classes.typ_compdec). + Context (t_func: PArray.array (tval t_i)). + + Definition bo_dec: + forall (a b: option bool), + {a = b} + {a <> b}. + Proof. pose proof bool_dec. decide equality. Qed. + + Lemma of_list'_length : forall A, + forall (b: list A) acc array, + PArray.length (of_list' acc array b) = PArray.length array. + Proof. + induction b; intros. + - reflexivity. + - simpl of_list'. + erewrite IHb; eauto. + rewrite PArray.length_set. auto. + Qed. + + Lemma of_list_Zlength : forall A (d: A) b, + Zlength b < wB -> + PArray.length (of_list d b) = of_Z (Z.of_nat (length b)). + Proof. + unfold of_list. + intros. rewrite of_list'_length; eauto. + rewrite PArray.length_make. + unfold PArray.max_length. + destruct_match. + - rewrite Zlength_correct. auto. + - rewrite Misc.leb_negb_gtb in Heqb0. + rewrite negb_false_iff in Heqb0. + eapply ltb_spec in Heqb0. + rewrite of_Z_spec in Heqb0. + rewrite Z.mod_small in Heqb0; try lia. + + rewrite Misc.max_int_wB in Heqb0. lia. + + split; auto. rewrite Zlength_correct. lia. + Qed. + + Opaque PArray.set. + + Lemma Zlength_aux_pos : forall A (b: list A) acc, + acc >= 0 -> + Zlength_aux acc A b >= 0. + Proof. + induction b; intros. + - auto. + - simpl. eapply IHb; eauto. + lia. + Qed. + + Lemma Zlength_pos : forall A (b: list A), + Zlength b >= 0. + Proof. + unfold Zlength. + intros. eapply Zlength_aux_pos; eauto. + lia. + Qed. + + Lemma of_list'_idx_preserve : forall A (b: list A) idx array, + forall i, + (0 <= idx)%Z -> + (i <? of_Z idx = true)%int63 -> + (0 <= idx + (Zlength b) < wB)%Z -> + (PArray.get (of_list' idx array b) i) = PArray.get array i. + Proof. + induction b; intros. + - auto. + - simpl of_list'. + rewrite Zlength_cons in *. + erewrite IHb; eauto. + + rewrite PArray.get_set_other; eauto. + intro ; subst. eelim Misc.not_ltb_refl; eauto. + + lia. + + rewrite ltb_spec in *. rewrite of_Z_spec in *. + assert (Zlength b >= 0) by (eapply Zlength_pos; eauto). + rewrite ! Z.mod_small in *; try lia. + + lia. + Qed. + + Opaque PArray.set. + + Lemma to_list_of_list'3 : + forall A (l: list A) arr x y, + y + Zlength l < wB -> + to_Z x < y -> + to_Z x < to_Z (PArray.length arr) -> + PArray.get (of_list' y arr l) x = PArray.get arr x. + Proof. + induction l; crush. + erewrite IHl. rewrite PArray.get_set_other; auto. + - unfold not; intros. assert (forall x y, x = y -> to_Z x = to_Z y) by (intros; now subst). + apply H3 in H2. rewrite of_Z_spec in H2. rewrite Z.mod_small in H2; subst. lia. + pose proof (not_int63_lt_0 x). split. lia. rewrite Zlength_cons in H. + pose proof (Zlength_pos _ l). lia. + - rewrite Zlength_cons in H. lia. + - lia. + - rewrite PArray.length_set. auto. + Qed. + + Lemma to_list_of_list'2 : + forall A l (d: A) x0 v a + (PARRR: to_Z x0 < to_Z (PArray.length a)) + (XXXXX: v + Zlength l < wB), + PArray.default a = d -> + to_Z (PArray.length a) <= Zlength l + v -> + v <= to_Z x0 -> + PArray.get (of_list' v a l) x0 = nth ((Z.to_nat (to_Z x0 - v))) l d. + Proof. + induction l; intros. + - simpl. assert ((x0 <? 0)%int63 = false). + { destruct ((x0 <? 0)%int63) eqn:?; auto. pose proof (not_int63_lt_0 x0). apply Int63.ltb_spec in Heqb. + replace (to_Z 0) with 0 in Heqb by auto. lia. + } rewrite Zlength_nil in H0. pose proof (not_int63_lt_0 (PArray.length a)). + rewrite PArray.get_outofbound. rewrite H. destruct_match; auto. + apply not_true_is_false. unfold not; intros. apply Int63.ltb_spec in H4. lia. + - simpl. destruct_match. + assert (forall x y, x = y -> Z.of_nat x = Z.of_nat y) by (intros; subst; auto). + apply H2 in Heqn. rewrite Z_to_nat_max in Heqn. + rewrite Zlength_cons in H0. unfold Z.succ in H0. + { replace (Z.max (to_Z x0 - v) 0) with (to_Z x0 - v) in Heqn by lia. + assert (to_Z x0 = v) by lia. subst. + rewrite of_to_Z. erewrite to_list_of_list'3; try lia. + rewrite PArray.get_set_same; auto. + apply Int63.ltb_spec. auto. + rewrite Zlength_cons in XXXXX. lia. + rewrite PArray.length_set; auto. + } + rewrite IHl with (d:=d). + assert (Z.to_nat (to_Z x0 - (v + 1)) = n). + { assert (forall a b, a = b -> (a - 1)%nat = (b - 1)%nat) by lia. + apply H2 in Heqn. + assert ((S n - 1)%nat = n) by lia. rewrite H3 in Heqn. rewrite <- Heqn. + lia. + } rewrite H2. auto. + rewrite PArray.length_set. lia. rewrite Zlength_cons in XXXXX. lia. + rewrite PArray.default_set. auto. + rewrite PArray.length_set. rewrite Zlength_cons in H0. lia. + lia. + Qed. + Transparent PArray.set. + + Lemma to_list_of_list' : + forall A l (d: A) x0, + Zlength l < wB -> + to_Z x0 < Zlength l -> + PArray.get (of_list d l) x0 = nth (Z.to_nat (Int63.to_Z x0)) l d. + Proof. + unfold of_list. intros. + replace (to_Z x0) with (to_Z x0 - 0) by lia. + pose proof (Zlength_pos _ l). + apply to_list_of_list'2. + rewrite PArray.length_make. + assert ((of_Z (Zlength l) <=? PArray.max_length)%int63 = true). + apply Int63.leb_spec. rewrite of_Z_spec. rewrite Z.mod_small by lia. + unfold PArray.max_length. rewrite Misc.max_int_wB. lia. rewrite H2. + rewrite of_Z_spec. rewrite Z.mod_small by lia. auto. + lia. + rewrite PArray.default_make; auto. + rewrite PArray.length_make. + assert ((of_Z (Zlength l) <=? PArray.max_length)%int63 = true). + apply Int63.leb_spec. rewrite of_Z_spec. rewrite Z.mod_small by lia. + unfold PArray.max_length. rewrite Misc.max_int_wB. lia. rewrite H2. + rewrite of_Z_spec. rewrite Z.mod_small by lia. auto. lia. + pose proof (not_int63_lt_0 x0). lia. + Qed. + + Lemma to_list_of_list2 : (* lemmes nth of_list' *) + forall A (d: A) (b: list A) x, + Zlength b < wB -> + In x (Misc.to_list (of_list d b)) -> + In x b. + Proof. + intros. apply Misc.In_to_list in H0. simplify. + rewrite to_list_of_list'. apply nth_In. + apply Int63.ltb_spec in H0. rewrite of_list_Zlength in H0 by auto. + rewrite of_Z_spec in H0. rewrite Z.mod_small in H0. + assert (Z.of_nat (Z.to_nat φ (x0)%int63) < Z.of_nat (Datatypes.length b)). + { rewrite Z_to_nat_max. + pose proof (not_int63_lt_0 x0). + lia. + } + lia. + simplify. lia. + rewrite <- Zlength_correct; auto. + auto. + apply Int63.ltb_spec in H0. rewrite of_list_Zlength in H0; auto. + rewrite <- Zlength_correct in H0. rewrite Int63.of_Z_spec in H0. + rewrite Z.mod_small in H0; auto. + pose proof (Zlength_pos _ b). lia. + Qed. + + Lemma of_pos_rec_unfold_xO : forall n p, + of_pos_rec (S n) (xO p) = (of_pos_rec n p << 1)%int63. + Proof. + intros. reflexivity. + Qed. + + Lemma is_even_of_pos : + forall p a, + (Z.pos a - 2) * 2 = Z.pos p -> + is_even (of_pos p) = true. + Proof. + destruct p. + - lia. + - intros. + unfold of_pos, size. + rewrite of_pos_rec_unfold_xO. + eapply is_even_lsl_1. + - lia. + Qed. + + Lemma is_pos_P_of_P: + forall a, + 0 <= (Zpos a - 2) * 2 < wB -> + State.Lit.is_pos (P_of_P a) = true. + Proof. + unfold State.Lit.is_pos, P_of_P. + intros. + unfold of_Z. case_eq ((Z.pos a - 2) * 2); intros; try lia. + - apply Bva_checker.is_even_0. + - eapply is_even_of_pos; eauto. + Qed. + + Lemma of_pos_rec_unfold_xI : forall n p, + of_pos_rec (S n) (xI p) = (of_pos_rec n p << 1 lor 1)%int63. + Proof. + intros. reflexivity. + Qed. + + Lemma is_even_of_pos_false : + forall p a, + (Z.pos a - 2) * 2 + 1 = Z.pos p -> + is_even (of_pos p) = false. + Proof. + destruct p. + - intros. unfold of_pos, size. + rewrite of_pos_rec_unfold_xI. + rewrite Misc.is_even_or. + rewrite andb_false_r; auto. + - lia. + - intros. auto. + Qed. + + Lemma is_neg_N_of_P: + forall a, + 0 <= (Zpos a - 2) * 2 + 1 < wB -> + State.Lit.is_pos (N_of_P a) = false. + Proof. + unfold State.Lit.is_pos, N_of_P. + intros. + unfold of_Z. case_eq ((Z.pos a - 2) * 2 + 1); intros; try lia. + eapply is_even_of_pos_false; eauto. + Qed. + + Lemma blit_N_of_P: + forall a, + 1 < Z.pos a -> + (Z.pos a - 2) * 2 + 1 < wB -> + State.Lit.blit (N_of_P a) = of_P a. + Proof. + unfold State.Lit.blit, of_P, N_of_P; intros. + apply to_Z_inj. + rewrite lsr_spec. + replace (to_Z (1)%int63) with 1 by crush. + replace (2 ^ 1) with 2 by lia. + rewrite !of_Z_spec. + rewrite !Z.mod_small by lia. + rewrite Z.div_add_l by lia. + assert (X: 1 / 2 = 0) by auto. + rewrite X. rewrite Z.add_0_r. auto. + Qed. + + Lemma blit_P_of_P: + forall a, + 1 < Z.pos a -> + (Z.pos a - 2) * 2 < wB -> + State.Lit.blit (P_of_P a) = of_P a. + Proof. + unfold State.Lit.blit, of_P, P_of_P; intros. + apply to_Z_inj. + rewrite lsr_spec. + replace (to_Z (1)%int63) with 1 by crush. + replace (2 ^ 1) with 2 by lia. + rewrite !of_Z_spec. + rewrite !Z.mod_small by lia. + rewrite Z_div_mult by lia. auto. + Qed. + + Lemma in_tree_lt_array : + forall d tree f x y, + tree_key_wf _ tree -> + of_tree d (PTree.map (fun _ : positive => lform_to_form) tree) = Some f -> + tree ! x = Some y -> + is_true (of_P x <? PArray.length f)%int63. + Proof. + intros. + unfold of_tree in *. + destruct_match; try congruence. + inv H0. rewrite PArray_length_fold_set. + rewrite PArray.length_make. + unfold PArray.max_length in *. + erewrite <- max_key_map in *; eauto. + destruct_match. + + pose proof (max_key_correct _ _ _ _ H1). + unfold of_P, is_true, tree_key_wf, gt_1 in *. + rewrite ltb_spec. + rewrite Z.ltb_lt in *. + rewrite ! of_Z_spec. + inv H. inv H3. specialize (H4 x y H1). + rewrite ! Z.mod_small; try lia. + + pose proof (max_key_correct _ _ _ _ H1). + unfold of_P, is_true, tree_key_wf, gt_1 in *. + rewrite ltb_spec. + rewrite ! of_Z_spec. + rewrite Z.ltb_lt in *. + rewrite Misc.max_int_wB. + rewrite ! Z.mod_small; try lia. + inv H. inv H3. specialize (H4 x y H1). lia. + Qed. + + Lemma of_tree_default : + forall A (d: A) f y, + of_tree d f = Some y -> + PArray.default y = d. + Proof. + intros. unfold of_tree in *. destruct_match; try discriminate; simplify. + rewrite PArray_default_fold_set; auto. + Qed. + + Lemma hash_value_in : + forall max f ht h ht', + hash_value max f ht = (h, ht') -> + ht' ! h = Some f. + Proof. + unfold hash_value. intros. + destruct_match. + - inv H. eapply find_tree_correct; eauto. + - inv H. rewrite PTree.gss. auto. + Qed. + + Lemma AHhash_value_in : + forall max f ht h ht', + AH.hash_value max f ht = (h, ht') -> + ht' ! h = Some f. + Proof. + unfold AH.hash_value; intros. + destruct_match. + - inv H. eapply AH.find_tree_correct; eauto. + - inv H. rewrite PTree.gss. auto. + Qed. + + Lemma pos_of_tree_max_key : + forall A (d: A) h11 h6 x h, + tree_a_wf h11 -> + (max_key h6 <= max_key h11)%positive -> + h11 ! h = h6 ! h -> + AH.find_tree x h6 = Some h -> + 1 < Z.pos h < wB. + Proof. + intros. eapply AH.find_tree_Some in H2. + pose proof H2. rewrite <- H1 in H3. + eapply max_key_correct in H2. + unfold tree_a_wf in *. inversion H as [RANGE [PROP [SOME1 [SOME2 SOME3]]]]. + apply PROP in H3. lia. + Qed. + + Definition match_one {A} (f: PTree.t A) lf := + forall y z, lf ! y = Some z -> f ! y = Some z. + + Definition match_all {A} (f: PTree.t A) lf := + Forall (match_one f) lf. + +Lemma match_one_refl : + forall A x, @match_one A x x. +Proof. unfold match_one; auto. Qed. + +Instance match_one_Reflexive {A} : Reflexive (@match_one A). +Proof. unfold Reflexive. auto using match_one_refl. Qed. + +Lemma match_one_trans : + forall A x y z, @match_one A x y -> match_one y z -> match_one x z. +Proof. unfold match_one; auto. Qed. + +Instance match_one_Transitive {A} : Transitive (@match_one A). +Proof. unfold Transitive. eauto using match_one_trans. Qed. + + Lemma tree_a_wf_lt : + forall h x y, + tree_a_wf h -> + h ! x = Some y -> + 0 <= Z.pos x - 2 < wB. + Proof. + unfold tree_a_wf; intros. pose proof H0 as X. apply max_key_correct in H0. + unfold gt_1 in *. inv H. inv H2. apply H in X. + all: lia. + Qed. + + Section PROOF_MORE. + + Context (f: form_t) (a: atom_t) (f_t: PTree.t lform) (a_t: PTree.t atom). + + Context (CHKF: is_true (check_form f)). + Context (CHKA: is_true (check_atom a)). + Context (WFF: tree_f_wf f_t). + Context (WFA: tree_a_wf a_t). + + Context (GENF: of_tree Ftrue (PTree.map (fun _ => lform_to_form) f_t) = Some f). + Context (GENA: of_tree (Acop CO_xH) a_t = Some a). + + Context (la: PTree.t bool). + Context (la_arr: PArray.array (tval t_i_empty)). + + Context (MATCH_LA: forall i : positive, 0 <= Z.pos i - 2 < wB -> + PArray.get la_arr (of_P i) = t_func_mk (Zval la ! i)). + + Lemma match_one_hash_value : + forall max x h h' y y', + hash_value max y h = (y', h') -> + match_one x h' -> + match_one x h. + Proof. + unfold match_one. + intros. + eapply H0; eauto. + eapply hash_constant; eauto. + Qed. + + Lemma AHmatch_one_hash_value : + forall max x h h' y y', + AH.hash_value max y h = (y', h') -> + match_one x h' -> + match_one x h. + Proof. + unfold match_one. + intros. + eapply H0; eauto. + eapply AH.hash_constant; eauto. + Qed. + + Lemma gt_1_map : + gt_1 (PTree.map (fun _ : positive => lform_to_form) f_t). + Proof. + inversion WFF; unfold gt_1 in *; simplify. + rewrite PTree.gmap in H1. unfold option_map in *. + destruct (f_t ! x) eqn:?. eapply H0. eauto. easy. + Qed. + + Lemma gt_1_a : + gt_1 a_t. + Proof. inversion WFA; crush. Qed. + + Lemma in_tree_bounded : + forall t p y, + t ! p = Some y -> + match_one f_t t -> + 0 <= (Z.pos p - 2) * 2 + 1 < wB. + Proof. + intros. unfold match_one in *. apply H0 in H. + pose proof H. apply max_key_correct in H. + unfold tree_f_wf in WFF. inversion WFF as [X1 [X2 [X3 X4]]]. + unfold gt_1 in X3. + apply X3 in H1. + lia. + Qed. + + Lemma in_tree_bounded2 : + forall t p y, + t ! p = Some y -> + match_one f_t t -> + 0 <= (Z.pos p - 2) * 2 < wB. + Proof. + intros. unfold match_one in *. apply H0 in H. + pose proof H. apply max_key_correct in H. + unfold tree_f_wf in WFF. inversion WFF as [X1 [X2 [X3 X4]]]. + unfold gt_1 in X3. + apply X3 in H1. + lia. + Qed. + + Lemma in_tree_bounded3 : + forall t p y, + t ! p = Some y -> + match_one f_t t -> + 0 <= Z.pos p - 2 < wB. + Proof. + intros. unfold match_one in *. apply H0 in H. + pose proof H. apply max_key_correct in H. + unfold tree_f_wf in WFF. inversion WFF as [X1 [X2 [X3 X4]]]. + unfold gt_1 in X3. + apply X3 in H1. + lia. + Qed. + + Lemma in_tree_bounded4 : + forall t p y, + t ! p = Some y -> + match_one a_t t -> + 0 <= Z.pos p - 2 < wB. + Proof. + intros. unfold match_one in *. apply H0 in H. + pose proof H. apply max_key_correct in H. + unfold tree_a_wf in WFA. inversion WFA as [X1 [X2 [X3 X4]]]. + unfold gt_1 in X2. + apply X2 in H1. + lia. + Qed. + + Lemma tree_f_wf_tree_key_wf: forall f_t, + tree_f_wf f_t -> + tree_key_wf _ f_t. + Proof. + clear. intros. + inversion H as [X1 [X2 [X3 [X4 X5]]]]. + unfold tree_key_wf. + repeat split; try lia. + auto. + Qed. + + Lemma tree_a_wf_tree_key_wf: forall f_t, + tree_a_wf f_t -> + tree_key_wf _ f_t. + Proof. + clear. intros. + inversion H as [X1 [X2 [X3 [X4 X5]]]]. + unfold tree_key_wf. + repeat split; try lia. + auto. + Qed. + + Lemma tree_key_wf_map : forall A B f_t (f: positive -> A -> B), + tree_key_wf _ f_t -> + tree_key_wf _ (PTree.map f f_t). + Proof. + clear. intros. + inversion H as [X1 [X2 X3]]. + unfold tree_key_wf. + repeat split; try (erewrite <- max_key_map; eauto). + rewrite <- gt_1_map_iff; eauto. + Qed. + + #[local] Hint Resolve gt_1_map : to_smt. + #[local] Hint Resolve gt_1_a : to_smt. + #[local] Hint Resolve in_tree_bounded : to_smt. + #[local] Hint Resolve in_tree_bounded2 : to_smt. + #[local] Hint Resolve in_tree_bounded3 : to_smt. + #[local] Hint Resolve in_tree_bounded4 : to_smt. + + Lemma of_tree_of_P_2 : + forall t p v, + t ! p = Some v -> + match_one f_t t -> + PArray.get f (of_P p) = (lform_to_form v). + Proof. + unfold match_one; intros. + eapply of_tree_of_P; eauto with to_smt. + - eapply tree_key_wf_map; eauto. + eapply tree_f_wf_tree_key_wf; eauto. + - rewrite PTree.gmap. apply H0 in H. rewrite H. auto. + Qed. + + Lemma of_tree_of_P_2_hv : + forall t p v x h, + hash_value x v h = (p, t) -> + match_one f_t t -> + PArray.get f (of_P p) = (lform_to_form v). + Proof. + intros; apply hash_value_in in H; auto. + eapply of_tree_of_P_2; eassumption. + Qed. + + Lemma AHof_tree_of_P_2 : + forall t p v, + t ! p = Some v -> + match_one a_t t -> + PArray.get a (of_P p) = v. + Proof. + intros. pose proof H0. unfold match_one in H0; intros. + pose proof H. apply H0 in H. + eapply of_tree_of_P; eauto with to_smt. + eapply tree_a_wf_tree_key_wf; eauto. + Qed. + + Lemma AHof_tree_of_P_2_hv : + forall t p v x h, + AH.hash_value x v h = (p, t) -> + match_one a_t t -> + PArray.get a (of_P p) = v. + Proof. + unfold match_one; intros. apply AHhash_value_in in H. + pose proof H. apply H0 in H. + eapply of_tree_of_P; eauto with to_smt. + eapply tree_a_wf_tree_key_wf; eauto. + Qed. + + Lemma is_true_Atom_wf : + is_true (Atom.wf a). + Proof. + unfold is_true in *. unfold check_atom in CHKA. repeat (destruct_match; try discriminate; []); auto. + Qed. + + Lemma is_true_Form_wf : + is_true (wf f). + Proof. + unfold is_true in *. unfold check_form in CHKF. repeat (destruct_match; try discriminate; []); crush. + Qed. + + Lemma is_true_default_a : + PArray.default a = Acop CO_xH. + Proof. + unfold is_true in *. unfold check_atom in CHKA. repeat (destruct_match; try discriminate; []); auto. + Qed. + + Lemma gt_1_in : + forall h h1 y, + h ! h1 = Some y -> + match_one f_t h -> + 1 < Z.pos h1. + Proof. + intros. unfold match_one in H0. apply H0 in H. + inv WFF. unfold gt_1 in *. + inv H2. inv H4. inv H5. + apply H2 in H. lia. + Qed. + + Lemma gt_1_in2 : + forall h h1 y, + h ! h1 = Some y -> + match_one f_t h -> + (Z.pos h1 - 2) * 2 < wB. + Proof. + intros. unfold match_one in H0. apply H0 in H. + inv WFF. apply max_key_correct in H. lia. + Qed. + + Lemma gt_1_in3 : + forall h h1 y, + h ! h1 = Some y -> + match_one f_t h -> + (Z.pos h1 - 2) * 2 + 1 < wB. + Proof. + intros. unfold match_one in H0. apply H0 in H. + inv WFF. apply max_key_correct in H. lia. + Qed. + + #[local] Hint Resolve gt_1_in : to_smt. + #[local] Hint Resolve gt_1_in2: to_smt. + #[local] Hint Resolve gt_1_in3: to_smt. + + Lemma blit_lt_length : + forall h1 h y, + h ! h1 = Some y -> + match_one f_t h -> + is_true (State.Lit.blit (P_of_P h1) <? PArray.length f)%int63. + Proof. + intros. rewrite blit_P_of_P; eauto with to_smt. + eapply in_tree_lt_array; eauto with to_smt. + eapply tree_f_wf_tree_key_wf; eauto. + Qed. + + Lemma blit_lt_length2 : + forall h1 h y max h', + hash_value max y h' = (h1, h) -> + match_one f_t h -> + is_true (State.Lit.blit (P_of_P h1) <? PArray.length f)%int63. + Proof. + intros. eapply hash_value_in in H; eauto using blit_lt_length. + Qed. + + Lemma blit_lt_length_N : + forall h1 h y, + h ! h1 = Some y -> + match_one f_t h -> + is_true (State.Lit.blit (N_of_P h1) <? PArray.length f)%int63. + Proof. + intros. rewrite blit_N_of_P; eauto with to_smt. + eapply in_tree_lt_array; eauto with to_smt. + eapply tree_f_wf_tree_key_wf; eauto. + Qed. + + Lemma blit_lt_length_N2 : + forall h1 h y max h', + hash_value max y h' = (h1, h) -> + match_one f_t h -> + is_true (State.Lit.blit (N_of_P h1) <? PArray.length f)%int63. + Proof. + intros. eapply hash_value_in in H; eauto using blit_lt_length_N. + Qed. + + Lemma lt_pos_in : + forall h1 y h, + h ! h1 = Some y -> + match_one f_t h -> + 0 <= (Z.pos h1 - 2) * 2 < wB. + Proof. + intros. inversion WFF as [BOUNDS [MAXKEY [GT [S2 S3]]]]. unfold gt_1 in GT. + unfold match_one in *. apply H0 in H. pose proof H as X. apply GT in H. + apply max_key_correct in X. lia. + Qed. + + Lemma lt_pos_in2 : + forall h1 y h max h', + hash_value max y h' = (h1, h) -> + match_one f_t h -> + 0 <= (Z.pos h1 - 2) * 2 < wB. + Proof. + intros. eapply hash_value_in in H. eapply lt_pos_in; eauto. + Qed. + + #[local] Hint Resolve is_true_Atom_wf : to_smt. + #[local] Hint Resolve is_true_Form_wf : to_smt. + #[local] Hint Resolve is_true_default_a : to_smt. + #[local] Hint Resolve blit_lt_length2 : to_smt. + #[local] Hint Resolve lt_pos_in2 : to_smt. + #[local] Hint Resolve blit_lt_length_N2 : to_smt. + #[local] Hint Resolve tree_a_wf_tree_key_wf : to_smt. + #[local] Hint Resolve tree_f_wf_tree_key_wf : to_smt. + + #[local] Opaque Z.sub. + + Lemma to_smt_i_correct : + forall h p i, + match_one a_t h -> + to_smt_i h p = Some i -> + Atom.interp_aux t_i_empty la_arr (PArray.get (Atom.t_interp t_i_empty la_arr a)) (PArray.get a i) + = Bval _ Typ.TZ (Zval (eval_hash_pred p la)). + Proof. + intros * MATCH TO_SMT. + unfold to_smt_i in TO_SMT. + destruct_match; try discriminate; simplify. + unfold tree_a_wf in WFA. inversion WFA as [BOUND [PROP [AT1 [AT2 AT3]]]]. + replace (of_pos 1) with (of_P 3) by auto. + erewrite ! of_tree_of_P; try eassumption; try lia; simpl. + rewrite Atom.t_interp_wf by auto with to_smt. + erewrite ! of_tree_of_P; try eassumption; try lia; auto. + repeat split; auto; try lia. + repeat split; auto; try lia. + unfold tree_a_wf in WFA. inversion WFA as [BOUND [PROP [AT1 [AT2 AT3]]]]. + replace (of_pos 2) with (of_P 4) by auto. + erewrite ! of_tree_of_P; try eassumption; try lia; simpl. + rewrite Atom.t_interp_wf by auto with to_smt. + erewrite ! of_tree_of_P; try eassumption; try lia; simpl. + rewrite Atom.t_interp_wf by auto with to_smt. + erewrite ! of_tree_of_P; try eassumption; try lia; simpl. auto. + repeat split; auto; try lia. + repeat split; auto; try lia. + repeat split; auto; try lia. + + repeat (destruct_match; try discriminate; []). simplify. + apply AH.find_tree_correct in Heqo. + erewrite ! AHof_tree_of_P_2; try eassumption; try lia; simpl. + destruct_match. + rewrite MATCH_LA in Heqt. + destruct (la ! p0) eqn:?; [destruct b|]; simplify; unfold t_func_mk, Tval in Heqt; + symmetry in Heqt; inv Heqt; eapply Eqdep.EqdepTheory.inj_pair2 in H5; subst; auto. + lia. + Qed. + + Lemma interp_eval_pred : + forall h13 h11 h6 p0 i h8 h10 h9 h12, + match_one f_t h13 -> + match_one a_t h11 -> + match_one a_t h6 -> + eval_hash_pred p0 la <> Some true -> + to_smt_i h6 p0 = Some i -> + AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) i (Int63.of_pos 1)) h8 = (h10, h11) -> + hash_value 1%positive (LFatom (of_P h10)) h9 = (h12, h13) -> + State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) + (N_of_P h12) = true. + Proof. + intros * M1 M2 M3 EVAL TOSMT HASH1 HASH2. unfold State.Lit.interp. + unfold State.Var.interp, interp_state_var. + pose proof HASH1 as IN1. eapply AHhash_value_in in IN1. + pose proof HASH2 as IN2. eapply hash_value_in in IN2. + rewrite is_neg_N_of_P by eauto with to_smt. + rewrite t_interp_wf by eauto with to_smt. + rewrite blit_N_of_P by eauto with to_smt. + erewrite ! of_tree_of_P_2 by eauto with to_smt; simpl. + unfold interp_form_hatom, interp_hatom. + rewrite Atom.t_interp_wf by eauto with to_smt. + erewrite ! AHof_tree_of_P_2 by eauto with to_smt; simpl. + rewrite !Atom.t_interp_wf by eauto with to_smt. + erewrite to_smt_i_correct by eauto with to_smt. + replace (of_pos 1) with (of_P 3) by auto. + inversion WFA as [X1 [X2 [X3 [X4 X5]]]]. + erewrite of_tree_of_P; + [idtac|idtac|eauto with to_smt|eauto with to_smt|eauto with to_smt]. + simpl. rewrite !Atom.t_interp_wf by eauto with to_smt. + erewrite of_tree_of_P; + [idtac|idtac|eauto with to_smt|eauto with to_smt|eauto with to_smt]. + simpl. + destruct (eval_hash_pred p0 la) eqn:?; [destruct b|]; try discriminate; auto. + eapply tree_a_wf_tree_key_wf; eauto. + eapply tree_a_wf_tree_key_wf; eauto. + Qed. + + Lemma eval_hash_pred_Pand_lt : + forall la p1 p2, + Zval (eval_hash_pred (p1 ∧ p2) la) = + if Zval (eval_hash_pred p1 la) <? Zval (eval_hash_pred p2 la) + then Zval (eval_hash_pred p1 la) else Zval (eval_hash_pred p2 la). + Proof. + intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|]; + destruct (eval_hash_pred p2 la0) eqn:B; try destruct b; + simplify; rewrite !A; rewrite !B; auto. + Qed. + + Lemma eval_hash_pred_Por_lt : + forall la p1 p2, + Zval (eval_hash_pred (p1 ∨ p2) la) = + if Zval (eval_hash_pred p1 la) <? Zval (eval_hash_pred p2 la) + then Zval (eval_hash_pred p2 la) else Zval (eval_hash_pred p1 la). + Proof. + intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|]; + destruct (eval_hash_pred p2 la0) eqn:B; try destruct b; + simplify; rewrite !A; rewrite !B; auto. + Qed. + + Lemma eval_hash_pred_Pimp_lt : + forall la p1 p2, + Zval (eval_hash_pred (p1 → p2) la) = + if 1 <? 1 - Zval (eval_hash_pred p1 la) + Zval (eval_hash_pred p2 la) + then 1 else 1 - Zval (eval_hash_pred p1 la) + Zval (eval_hash_pred p2 la). + Proof. + intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|]; + destruct (eval_hash_pred p2 la0) eqn:B; try destruct b; + simplify; rewrite !A; rewrite !B; auto. + Qed. + + Lemma eval_hash_pred_Pnot_lt : + forall la p1, + Zval (eval_hash_pred (¬ p1) la) = - Zval (eval_hash_pred p1 la). + Proof. + intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|]; + simplify; rewrite !A; auto. + Qed. + + Lemma to_smt_and_correct : + forall h fa0 i p1_1 i0 p1_2 i1 h0 h9 h8 h1, + to_smt_and h0 h i i0 i1 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one a_t h8 -> + to_smt_i h (Pbase fa0) = Some i -> + to_smt_i h p1_1 = Some i0 -> + to_smt_i h p1_2 = Some i1 -> + eval_hash_pred (equiv (Pbase fa0) (p1_1 ∧ p1_2)) la = Some true -> + State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) + (P_of_P h1) = true. + Proof. + intros * SMTAND M1 M2 SMT1 SMT2 SMT3 EVAL. unfold State.Lit.interp. + unfold to_smt_and in SMTAND. repeat ldestruct_match; []. inversion SMTAND; clear SMTAND; subst. + assert (match_one f_t h15) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h13) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h11) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h0) by (eapply match_one_hash_value; eauto). + assert (match_one a_t h5) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto). + rewrite is_pos_P_of_P by eauto with to_smt. + unfold State.Var.interp. unfold interp_state_var. + rewrite t_interp_wf by eauto with to_smt. + rewrite blit_P_of_P. + erewrite of_tree_of_P_2_hv; try eassumption. simpl. + unfold State.Lit.interp, State.Var.interp. + rewrite !is_pos_P_of_P by eauto with to_smt. + rewrite !t_interp_wf by eauto with to_smt. + rewrite !blit_P_of_P. + erewrite !of_tree_of_P_2_hv; try eassumption; simpl. + unfold interp_form_hatom, interp_hatom. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !AHof_tree_of_P_2_hv; try eassumption; simpl. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !to_smt_i_correct by eassumption. simpl. + apply eval_equiv in EVAL. + replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto. + rewrite EVAL. + rewrite !eval_hash_pred_Pand_lt. + destruct_match; apply Typ.i_eqb_refl. + all: match goal with + | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v => + apply hash_value_in in H; eauto with to_smt + | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ => + apply hash_value_in in H; eauto with to_smt + end. + Qed. + + Lemma to_smt_and_match_one : + forall h i i0 i1 h0 h9 h8 h1, + to_smt_and h0 h i i0 i1 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one f_t h0. + Proof. + unfold to_smt_and; intros * SMTAND M1. + repeat ldestruct_match; []. inversion SMTAND; clear SMTAND; subst. + repeat (eapply match_one_hash_value; try eassumption). + Qed. + + Lemma to_smt_and_match_one2 : + forall h i i0 i1 h0 h9 h8 h1, + to_smt_and h0 h i i0 i1 = (h9, h8, h1) -> + match_one a_t h8 -> + match_one a_t h. + Proof. + unfold to_smt_and; intros * SMTAND M1. + repeat ldestruct_match; []. inversion SMTAND; clear SMTAND; subst. + repeat (eapply AHmatch_one_hash_value; try eassumption). + Qed. + + Lemma to_smt_or_correct : + forall h fa0 i p1_1 i0 p1_2 i1 h0 h9 h8 h1, + to_smt_or h0 h i i0 i1 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one a_t h8 -> + to_smt_i h (Pbase fa0) = Some i -> + to_smt_i h p1_1 = Some i0 -> + to_smt_i h p1_2 = Some i1 -> + eval_hash_pred (equiv (Pbase fa0) (p1_1 ∨ p1_2)) la = Some true -> + State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) + (P_of_P h1) = true. + Proof. + intros * SMTOR M1 M2 SMT1 SMT2 SMT3 EVAL. unfold State.Lit.interp. + unfold to_smt_or in SMTOR. repeat ldestruct_match; []. inversion SMTOR; clear SMTOR; subst. + assert (match_one f_t h15) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h13) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h11) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h0) by (eapply match_one_hash_value; eauto). + assert (match_one a_t h5) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto). + rewrite is_pos_P_of_P by eauto with to_smt. + unfold State.Var.interp. unfold interp_state_var. + rewrite t_interp_wf by eauto with to_smt. + rewrite blit_P_of_P. + erewrite of_tree_of_P_2_hv; try eassumption. simpl. + unfold State.Lit.interp, State.Var.interp. + rewrite !is_pos_P_of_P by eauto with to_smt. + rewrite !t_interp_wf by eauto with to_smt. + rewrite !blit_P_of_P. + erewrite !of_tree_of_P_2_hv; try eassumption; simpl. + unfold interp_form_hatom, interp_hatom. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !AHof_tree_of_P_2_hv; try eassumption; simpl. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !to_smt_i_correct by eassumption. simpl. + apply eval_equiv in EVAL. + replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto. + rewrite EVAL. + rewrite !eval_hash_pred_Por_lt. + destruct_match; apply Typ.i_eqb_refl. + all: match goal with + | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v => + apply hash_value_in in H; eauto with to_smt + | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ => + apply hash_value_in in H; eauto with to_smt + end. + Qed. + + Lemma to_smt_or_match_one : + forall h i i0 i1 h0 h9 h8 h1, + to_smt_or h0 h i i0 i1 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one f_t h0. + Proof. + unfold to_smt_or; intros * SMTOR M1. + repeat ldestruct_match; []. inversion SMTOR; clear SMTOR; subst. + repeat (eapply match_one_hash_value; try eassumption). + Qed. + + Lemma to_smt_or_match_one2 : + forall h i i0 i1 h0 h9 h8 h1, + to_smt_or h0 h i i0 i1 = (h9, h8, h1) -> + match_one a_t h8 -> + match_one a_t h. + Proof. + unfold to_smt_or; intros * SMTOR M1. + repeat ldestruct_match; []. inversion SMTOR; clear SMTOR; subst. + repeat (eapply AHmatch_one_hash_value; try eassumption). + Qed. + + Lemma to_smt_imp_correct : + forall h fa0 i p1_1 i0 p1_2 i1 h0 h9 h8 h1, + to_smt_imp h0 h i i0 i1 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one a_t h8 -> + to_smt_i h (Pbase fa0) = Some i -> + to_smt_i h p1_1 = Some i0 -> + to_smt_i h p1_2 = Some i1 -> + eval_hash_pred (equiv (Pbase fa0) (p1_1 → p1_2)) la = Some true -> + State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) + (P_of_P h1) = true. + Proof. + intros * SMTIMP M1 M2 SMT1 SMT2 SMT3 EVAL. unfold State.Lit.interp. + unfold to_smt_imp in SMTIMP. repeat ldestruct_match; []. inversion SMTIMP; clear SMTIMP; subst. + assert (match_one f_t h19) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h17) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h15) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h0) by (eapply match_one_hash_value; eauto). + assert (match_one a_t h11) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h7) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h5) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto). + rewrite is_pos_P_of_P by eauto with to_smt. + unfold State.Var.interp. unfold interp_state_var. + rewrite t_interp_wf by eauto with to_smt. + rewrite blit_P_of_P. + erewrite of_tree_of_P_2_hv by eassumption. simpl. + unfold State.Lit.interp, State.Var.interp. + rewrite !is_pos_P_of_P by eauto with to_smt. + rewrite !t_interp_wf by eauto with to_smt. + rewrite !blit_P_of_P. + erewrite !of_tree_of_P_2_hv by eassumption; simpl. + unfold interp_form_hatom, interp_hatom. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !AHof_tree_of_P_2_hv by eassumption; simpl. + rewrite !Atom.t_interp_wf by auto with to_smt. + inversion WFA as [WFA1 [WFA2 [WFA3 [WFA4 WFA5]]]]. + erewrite !of_tree_of_P by + (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia). + simpl. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !of_tree_of_P by + (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia). + erewrite !AHof_tree_of_P_2_hv by eassumption. + erewrite !to_smt_i_correct by eassumption. cbn [Atom.interp_aux]. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !AHof_tree_of_P_2_hv by eassumption. + erewrite !to_smt_i_correct by eassumption. cbn [Atom.interp_aux]. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !of_tree_of_P by + (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia). + cbn [Atom.interp_aux]. + rewrite !Atom.t_interp_wf by auto with to_smt. + erewrite !of_tree_of_P by + (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia). + erewrite !to_smt_i_correct by eassumption. + cbn -[Z.sub]. + apply eval_equiv in EVAL. + replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto. + rewrite EVAL. + rewrite !eval_hash_pred_Pimp_lt. + destruct_match; auto using Z.eqb_refl. + all: match goal with + | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v => + apply hash_value_in in H; eauto with to_smt + | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ => + apply hash_value_in in H; eauto with to_smt + end. + Qed. + + Lemma to_smt_imp_match_one : + forall h i i0 i1 h0 h9 h8 h1, + to_smt_imp h0 h i i0 i1 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one f_t h0. + Proof. + unfold to_smt_imp; intros * SMTIMP M1. + repeat ldestruct_match; []. inversion SMTIMP; clear SMTIMP; subst. + repeat (eapply match_one_hash_value; try eassumption). + Qed. + + Lemma to_smt_imp_match_one2 : + forall h i i0 i1 h0 h9 h8 h1, + to_smt_imp h0 h i i0 i1 = (h9, h8, h1) -> + match_one a_t h8 -> + match_one a_t h. + Proof. + unfold to_smt_imp; intros * SMTIMP M1. + repeat ldestruct_match; []. inversion SMTIMP; clear SMTIMP; subst. + repeat (eapply AHmatch_one_hash_value; try eassumption). + Qed. + + Lemma to_smt_not_correct : + forall h fa0 i p1_1 i0 h0 h9 h8 h1, + to_smt_not h0 h i i0 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one a_t h8 -> + to_smt_i h (Pbase fa0) = Some i -> + to_smt_i h p1_1 = Some i0 -> + eval_hash_pred (equiv (Pbase fa0) (¬ p1_1)) la = Some true -> + State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) + (P_of_P h1) = true. + Proof. + intros * SMTNOT M1 M2 SMT1 SMT2 EVAL. unfold State.Lit.interp. + unfold to_smt_not in SMTNOT. repeat ldestruct_match; []. inversion SMTNOT; clear SMTNOT; subst. + assert (match_one f_t h0) by (eapply match_one_hash_value; eauto). + assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto). + rewrite is_pos_P_of_P by eauto with to_smt. + unfold State.Var.interp. unfold interp_state_var. + rewrite t_interp_wf by eauto with to_smt. + rewrite blit_P_of_P. + erewrite of_tree_of_P_2_hv by eassumption. cbn. + unfold interp_form_hatom. unfold interp_hatom. + rewrite Atom.t_interp_wf by eauto with to_smt. + erewrite !AHof_tree_of_P_2_hv by eassumption. cbn. + rewrite Atom.t_interp_wf by eauto with to_smt. + inversion WFA as [WFA1 [WFA2 [WFA3 [WFA4 WFA5]]]]. + erewrite !to_smt_i_correct by eassumption. + rewrite Atom.t_interp_wf by eauto with to_smt. + erewrite !AHof_tree_of_P_2_hv by eassumption. cbn. + rewrite Atom.t_interp_wf by eauto with to_smt. + erewrite !to_smt_i_correct by eassumption. cbn. + apply eval_equiv in EVAL. + replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto. + rewrite EVAL. + rewrite !eval_hash_pred_Pnot_lt. + auto using Z.eqb_refl. + all: match goal with + | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v => + apply hash_value_in in H; eauto with to_smt + | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ => + apply hash_value_in in H; eauto with to_smt + end. + Qed. + + Lemma to_smt_not_match_one : + forall h i i0 h0 h9 h8 h1, + to_smt_not h0 h i i0 = (h9, h8, h1) -> + match_one f_t h9 -> + match_one f_t h0. + Proof. + unfold to_smt_not; intros * SMTNOT M1. + repeat ldestruct_match; []. inversion SMTNOT; clear SMTNOT; subst. + repeat (eapply match_one_hash_value; try eassumption). + Qed. + + Lemma to_smt_not_match_one2 : + forall h i i0 h0 h9 h8 h1, + to_smt_not h0 h i i0 = (h9, h8, h1) -> + match_one a_t h8 -> + match_one a_t h. + Proof. + unfold to_smt_not; intros * SMTNOT M1. + repeat ldestruct_match; []. inversion SMTNOT; clear SMTNOT; subst. + repeat (eapply AHmatch_one_hash_value; try eassumption). + Qed. + + Lemma fold_to_smt_l_correct : + forall l l0 h7 h6 l1 h9 h8 x, + match_one f_t h9 -> match_one a_t h8 -> + fold_right to_smt_l (Some (l0, h7, h6)) l = Some (l1, h9, h8) -> + (forall y, In y l0 -> State.Lit.interp (interp_state_var + (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) y = true) -> + eval_hash_pred (fold_left Pand (to_equiv l) T) la = Some true -> + In x l1 -> + State.Lit.interp (interp_state_var + (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) x = true. + Proof. + induction l as [|a0 l' IHl]; intros * M1 M2 TO_SMT_L PREV_LIST EVAL_FOLD IN. simplify; eauto. + simpl in EVAL_FOLD. + apply eval_hash_pred_fold_Pand4 in EVAL_FOLD. inversion EVAL_FOLD as [EVAL_FOLD' EVAL_A0]. + destruct a0 as [fa0 sa0]. cbn [fst snd] in *. + simpl in TO_SMT_L. unfold to_smt_l in TO_SMT_L. fold to_smt_l in TO_SMT_L. + repeat (destruct_match; try discriminate; []). + destruct_match; try discriminate; + repeat (destruct_match; try discriminate; []); inversion TO_SMT_L; subst; + [ assert (match_one f_t h0) by (eapply to_smt_and_match_one; eauto); + assert (match_one a_t h) by (eapply to_smt_and_match_one2; eauto) + | assert (match_one f_t h0) by (eapply to_smt_or_match_one; eauto); + assert (match_one a_t h) by (eapply to_smt_or_match_one2; eauto) + | assert (match_one f_t h0) by (eapply to_smt_imp_match_one; eauto); + assert (match_one a_t h) by (eapply to_smt_imp_match_one2; eauto) + | assert (match_one f_t h0) by (eapply to_smt_not_match_one; eauto); + assert (match_one a_t h) by (eapply to_smt_not_match_one2; eauto) ]. + all: apply in_app_or in IN; inversion IN as [INL | INP]; clear IN; [solve [eauto]|]; + inversion INP as [EQ | NIL]; clear INP; [|solve [inversion NIL]]; subst. + - eapply to_smt_and_correct; eauto. now rewrite <- eval_hash_pred_T_Pand. + - eapply to_smt_or_correct; eauto. now rewrite <- eval_hash_pred_T_Pand. + - eapply to_smt_imp_correct; eauto. now rewrite <- eval_hash_pred_T_Pand. + - eapply to_smt_not_correct; eauto. now rewrite <- eval_hash_pred_T_Pand. + Qed. + + Lemma gt_1_fold_init : + forall (lx: list unit) v' l0 init_forms init_atoms v l1 form_defs atom_defs, + fold_right (fun _ => declare_atoms_with_bounds) + (v', l0, init_forms, init_atoms) + lx = (v, l1, form_defs, atom_defs) -> + 0 <= v' -> 0 <= v. + Proof. + induction lx; crush. + remember (fold_right (fun _ : unit => declare_atoms_with_bounds) + (v', l0, init_forms, init_atoms) lx) as folds. + symmetry in Heqfolds. destruct folds as [[[A1 A2] A3] A4]. + eapply IHlx in Heqfolds; eauto. unfold declare_atoms_with_bounds in H. + repeat (destruct_match; []). simplify. lia. + Qed. + + Lemma fold_init_correct : + forall (lx: list unit) l1 x init_forms init_atoms form_defs atom_defs l0 v v', + match_one f_t form_defs -> match_one a_t atom_defs -> + fold_right (fun _ => declare_atoms_with_bounds) + (v', l0, init_forms, init_atoms) + lx = (v, l1, form_defs, atom_defs) -> + (forall y, In y l0 -> + State.Lit.interp (interp_state_var + (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) y = true) -> + In x l1 -> 0 <= v' -> v < wB -> + State.Lit.interp (interp_state_var + (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) x = true. + Proof. + induction lx; crush. assert (VPRIME := H4). clear H4. assert (VPRIME2 := H5). clear H5. + remember (fold_right (fun _ : unit => declare_atoms_with_bounds) (v', l0, init_forms, init_atoms) lx) as folds. + symmetry in Heqfolds. destruct folds as [[[V R] F] A]. simpl in H1. + repeat (destruct_match; []). simplify. + eapply in_app in H3. inv H3. eapply IHlx in Heqfolds; eauto; try lia. + assert (match_one f_t h4) by (eapply match_one_hash_value; eauto). + assert (match_one f_t h10) by (eapply match_one_hash_value; eauto). + eapply match_one_hash_value; eauto. + assert (match_one a_t h14) by (eapply AHmatch_one_hash_value; eauto). + assert (match_one a_t h0) by (eapply AHmatch_one_hash_value; eauto). + eapply AHmatch_one_hash_value; eauto. + assert (F1: match_one f_t h4) by (eapply match_one_hash_value; eauto). + assert (F2: match_one f_t h10) by (eapply match_one_hash_value; eauto). + assert (A1: match_one a_t h14) by (eapply AHmatch_one_hash_value; eauto). + assert (A2: match_one a_t h0) by (eapply AHmatch_one_hash_value; eauto). + inv H1; [|inv H3]. + unfold State.Lit.interp. + rewrite is_pos_P_of_P by eauto with to_smt. + unfold State.Var.interp. unfold interp_state_var. + rewrite t_interp_wf by eauto with to_smt. + rewrite blit_P_of_P. + erewrite of_tree_of_P_2_hv by eassumption. cbn. + unfold State.Lit.interp. + rewrite !is_pos_P_of_P by eauto with to_smt. + unfold State.Var.interp. rewrite !t_interp_wf by eauto with to_smt. + rewrite !blit_P_of_P. + erewrite !of_tree_of_P_2_hv by eassumption. cbn. + unfold interp_form_hatom, interp_hatom. + rewrite !Atom.t_interp_wf by eauto with to_smt. + erewrite !AHof_tree_of_P_2_hv by eassumption. cbn. + inversion WFA as [WFA1 [WFA2 [WFA3 [WFA4 WFA5]]]]. + rewrite !Atom.t_interp_wf by eauto with to_smt. + erewrite !AHof_tree_of_P_2 by (try eassumption; reflexivity). cbn. + rewrite !Atom.t_interp_wf by eauto with to_smt. + erewrite !AHof_tree_of_P_2 by (try eassumption; reflexivity). cbn. + rewrite !Atom.t_interp_wf by eauto with to_smt. + erewrite !AHof_tree_of_P_2 by (try eassumption; reflexivity). cbn. + erewrite !AHof_tree_of_P_2_hv by eassumption. cbn. + repeat (destruct_match; []). repeat (ldestruct_match; []). + assert (0 <= V). + { eapply gt_1_fold_init; eauto. } + replace (of_Z V) with (of_P (Z.to_pos (V + 2))) in Heqt by + (unfold of_P; f_equal; rewrite Z2Pos.id by lia; lia). + rewrite MATCH_LA in Heqt. + destruct (la ! (Z.to_pos (V + 2))). destruct b. + unfold t_func_mk, Tval in Heqt. cbn in Heqt. + symmetry in Heqt. inv Heqt. eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. + simpl in Heqb. unfold Bval in Heqb. symmetry in Heqb. inv Heqb. + eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. auto. + unfold t_func_mk, Tval in Heqt. cbn in Heqt. + symmetry in Heqt. inv Heqt. eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. + simpl in Heqb. unfold Bval in Heqb. symmetry in Heqb. inv Heqb. + eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. auto. + unfold t_func_mk, Tval in Heqt. cbn in Heqt. + symmetry in Heqt. inv Heqt. eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. + simpl in Heqb. unfold Bval in Heqb. symmetry in Heqb. inv Heqb. + eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. auto. + all: try match goal with + | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v => + apply hash_value_in in H; eauto with to_smt + | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ => + apply hash_value_in in H; eauto with to_smt + end. + rewrite Z2Pos.id; lia. + Qed. + +End PROOF_MORE. + + Definition pl_leq {A} (a b: positive * A): Prop := + ((fst a) <= (fst b))%positive. + + Definition pl_lt {A} (a b: positive * A): Prop := + ((fst a) < (fst b))%positive. + + Definition pl_eq {A} (a b: positive * A): Prop := + fst a = fst b. + + Lemma pl_lt_trans : + forall A (a b c: positive * A), pl_lt a b -> pl_lt b c -> pl_lt a c. + Proof. unfold pl_lt; lia. Qed. + + Lemma pl_lt_irrefl : + forall A (a: positive * A), ~ pl_lt a a. + Proof. unfold pl_lt; lia. Qed. + + Lemma pl_lt_asymm : + forall A (a b: positive * A), pl_lt a b -> pl_lt b a -> False. + Proof. unfold pl_lt; lia. Qed. + + Definition Sorted := Sorted (@pl_lt predicate). + + Lemma pl_leq_refl : + forall A (a: positive * A), pl_leq a a. + Proof. unfold pl_leq; reflexivity. Qed. + + Lemma pl_leq_trans : + forall A (a b c: positive * A), pl_leq a b -> pl_leq b c -> pl_leq a c. + Proof. unfold pl_leq; intros; lia. Qed. + + Lemma pl_eq_refl : + forall A (a: positive * A), pl_eq a a. + Proof. unfold pl_leq; reflexivity. Qed. + + Lemma pl_eq_symm : + forall A (a b: positive * A), pl_eq a b -> pl_eq b a. + Proof. unfold pl_eq; intros; lia. Qed. + + Lemma pl_eq_trans : + forall A (a b c: positive * A), pl_eq a b -> pl_eq b c -> pl_eq a c. + Proof. unfold pl_eq; intros; lia. Qed. + + #[global] Instance Reflexive_pl_leq {A} : Reflexive (@pl_leq A). + Proof. unfold Reflexive. apply pl_leq_refl. Qed. + + #[global] Instance Transitive_pl_leq {A} : Transitive (@pl_leq A). + Proof. unfold Transitive. apply pl_leq_trans. Qed. + + #[global] Instance PreOrder_pl_leq {A} : PreOrder (@pl_leq A) := {}. + + #[global] Instance Reflexive_pl_eq {A} : Reflexive (@pl_eq A). + Proof. unfold Reflexive. apply pl_eq_refl. Qed. + + #[global] Instance Symmetric_pl_eq {A} : Symmetric (@pl_eq A). + Proof. unfold Symmetric. apply pl_eq_symm. Qed. + + #[global] Instance Transitive_pl_eq {A} : Transitive (@pl_eq A). + Proof. unfold Transitive. apply pl_eq_trans. Qed. + + #[global] Instance Equivalence_pl_eq {A} : Equivalence (@pl_eq A) := {}. + + #[global] Instance Antisymmetric_pl_leq {A} : Antisymmetric (positive * A) pl_eq pl_leq. + Proof. unfold Antisymmetric, pl_eq, pl_leq; lia. Qed. + + #[global] Instance PartialOrder_pl_leq {A} : PartialOrder (@pl_eq A) (@pl_leq A). + Proof. + unfold PartialOrder, relation_equivalence, predicate_equivalence. crush. + unfold relation_conjunction, predicate_intersection. simplify. unfold pl_eq, pl_leq, Basics.flip. + split. lia. lia. + Qed. + + #[global] Instance Irreflexive_pl_lt {A} : Irreflexive (@pl_lt A). + Proof. unfold Irreflexive, Reflexive, complement. apply pl_lt_irrefl. Qed. + + #[global] Instance Asymmetric_pl_lt {A} : Asymmetric (@pl_lt A). + Proof. unfold Asymmetric. apply pl_lt_asymm. Qed. + + #[global] Instance Transitive_pl_lt {A} : Transitive (@pl_lt A). + Proof. unfold Transitive. apply pl_lt_trans. Qed. + + #[global] Instance StrictOrder_pl_lt {A} : StrictOrder (@pl_lt A) := {}. + + Lemma eval_hash_pred_upd_asgn : + forall l p a, + Forall (fun x => (max_hash_pred p < fst x)%positive) l -> + eval_hash_pred p (upd_asgn l a) = eval_hash_pred p a. + Proof. + induction l as [| c l IHl]; try solve [crush]. + intros * FORALL. + inversion FORALL as [|? ? EL FORALL2]; subst; clear FORALL. + unfold upd_asgn. cbn [fold_left]. destruct_match; + replace ((fold_left + (fun (a' : PTree.t bool) (el : positive * hash_pred) => + match eval_hash_pred (snd el) a' with + | Some p_b => PTree.set (fst el) p_b a' + | None => a' + end) l a)) with (upd_asgn l a) in * by auto; eauto. + rewrite IHl; auto. + rewrite eval_hash_pred_gso; auto. + Qed. + + Lemma upd_asgn_not_in : + forall l c1 a, + ~ In c1 (map fst l) -> + (upd_asgn l a) ! c1 = a ! c1. + Proof. + induction l as [| c l IHl ]; try solve [crush]. + intros * NOTIN. simplify. + assert (fst c <> c1). + { unfold not; intros. subst. apply NOTIN; tauto. } + assert (~ In c1 (map fst l)). + { unfold not; intros. apply NOTIN; tauto. } + destruct_match; auto. + erewrite IHl; eauto. rewrite PTree.gso; auto. + Qed. + + Definition equiv_list_wf l := + Sorted l /\ Forall (fun x => (max_hash_pred (snd x) < fst x)%positive) l. + + Lemma equiv_list_wf_inv : + forall l a, + equiv_list_wf (a :: l) -> + equiv_list_wf l /\ Forall (pl_lt a) l /\ (max_hash_pred (snd a) < fst a)%positive. + Proof. + unfold equiv_list_wf; intros * S. inversion S as [A B]. + split; split. + - inversion A; auto. + - inversion B; auto. + - apply Sorted_StronglySorted in A. inversion A; auto. + unfold Relations_1.Transitive. apply pl_lt_trans. + - inversion B; auto. + Qed. + + Lemma equiv_list_wf_nil : + equiv_list_wf nil. + Proof. + unfold equiv_list_wf; split; auto; apply Sorted_nil. + Qed. + + Lemma sorted_not_in : + forall A l c1 (c2: A), + Forall (pl_lt (c1, c2)) l -> + ~ In c1 (map fst l). + Proof. + unfold not; intros. + eapply list_in_map_inv in H0. inv H0. inv H1. + eapply Forall_forall in H; eauto. + destruct x. simpl in H. unfold pl_lt in H. simpl in H. lia. + Qed. + + Lemma upd_asgn_set_sorted : + forall l a x, + Forall (Pos.lt x) (map fst l) -> + (upd_asgn l a) ! x = a ! x. + Proof. + induction l; auto. + intros. cbn. inv H. erewrite IHl; auto. + destruct_match; auto; now rewrite PTree.gso by lia. + Qed. + + Lemma eval_hash_pred_equiv_asgn : + forall l p a, + eval_hash_pred p a = Some true -> + equiv_list_wf l -> + Forall (fun x => a ! (fst x) = None) l -> + Forall (fun x => (max_hash_pred p < fst x)%positive) l -> + eval_hash_pred (fold_left Pand (to_equiv l) p) (upd_asgn l a) = Some true. + Proof. + induction l as [|c l IHl]; [crush|]. intros p a EVAL WF FORALL MAX. + destruct c as [c1 c2]. simpl. + inversion FORALL as [| ? ? NONE FORALL2]; subst; cbn [fst snd] in *; clear FORALL. + inversion MAX as [| ? ? MAXC MAX2]; subst; cbn [fst snd] in *; clear MAX. + eapply equiv_list_wf_inv in WF. inversion WF as [WF2 [FRL MHP]]; subst; clear WF. + cbn [snd fst] in *. destruct_match. + - rewrite IHl; eauto. + apply pand_true2; [|rewrite eval_hash_pred_gso by lia; auto]. + apply eval_equiv2. symmetry; rewrite eval_hash_pred_gso by crush. + rewrite Heqo. crush. symmetry; apply PTree.gss. + apply Forall_forall; intros. repeat match goal with H: Forall _ _ |- _ => eapply Forall_forall in H; eauto end. + unfold pl_lt in *. simplify. rewrite PTree.gso by lia. auto. + apply Forall_forall; intros. repeat match goal with H: Forall _ _ |- _ => eapply Forall_forall in H; eauto end. + unfold pl_lt in *. simplify. lia. + - eapply IHl; eauto. apply pand_true2. + apply eval_equiv2. rewrite Heqo. + simpl. auto. auto. + apply Forall_forall; intros. repeat match goal with H: Forall _ _ |- _ => eapply Forall_forall in H; eauto end. + unfold pl_lt in *. simplify. lia. + Qed. + +#[local] Opaque max_key. +#[local] Opaque Z.sub. +#[local] Opaque PTree.get. + +Lemma check_tree_f_wf_correct : + forall f, + check_tree_f_wf f = true -> tree_f_wf f. +Proof. + unfold check_tree_f_wf, tree_f_wf. + simplify; auto. + unfold gt_1; intros. + assert ((x = 1 \/ 1 < x)%positive) by lia. + inv H5; auto. rewrite H0 in H3. discriminate. + repeat (destruct_match; try discriminate; []); auto. + repeat (destruct_match; try discriminate; []); auto. +Qed. + +Lemma check_tree_a_wf_correct : + forall a, + check_tree_a_wf a = true -> tree_a_wf a. +Proof. + unfold check_tree_a_wf, tree_a_wf. + simplify; auto. + unfold gt_1; intros. + assert ((x = 1 \/ 1 < x)%positive) by lia. + inv H6; auto. rewrite H in H4. discriminate. + repeat (destruct_match; try discriminate; []); auto. + repeat (destruct_match; try discriminate; []); auto. + subst. apply Int63.eqb_spec in H2. apply Int63.eqb_spec in H1. subst. + auto. + repeat (destruct_match; try discriminate; []); auto. + subst. apply Int63.eqb_spec in H2. apply Int63.eqb_spec in H1. subst. + auto. +Qed. + +#[local] Transparent max_key. +#[local] Transparent Z.sub. +#[local] Transparent PTree.get. + +Lemma to_smt_l_match_one2 : + forall a y l0 h0 h r' f' a', + to_smt_l a (Some (l0, h0, h)) = Some (r', f', a') -> + match_one y a' -> + match_one y h. +Proof. + destruct a. destruct p0; simplify; try discriminate; + repeat (destruct_match; try discriminate; []); simplify; + eauto using to_smt_and_match_one2, to_smt_or_match_one2, + to_smt_imp_match_one2, to_smt_not_match_one2. +Qed. + +Lemma to_smt_l_match_one : + forall a y l0 h0 h r' f' a', + to_smt_l a (Some (l0, h0, h)) = Some (r', f', a') -> + match_one y f' -> + match_one y h0. +Proof. + destruct a. destruct p0; simplify; try discriminate; + repeat (destruct_match; try discriminate; []); simplify; + eauto using to_smt_and_match_one, to_smt_or_match_one, + to_smt_imp_match_one, to_smt_not_match_one. +Qed. + +Lemma to_smt_l_fold_match_one2 : + forall l y r f a r' f' a', + fold_right to_smt_l (Some (r, f, a)) l = Some (r', f', a') -> + match_one y a' -> + match_one y a. +Proof. + induction l; crush. remember (fold_right to_smt_l (Some (r, f, a0)) l) as folds. + destruct folds; [|crush]; []. + symmetry in Heqfolds. + destruct p. destruct p. eapply IHl; eauto. + eapply to_smt_l_match_one2; eauto. +Qed. + +Lemma to_smt_l_fold_match_one : + forall l y r f a r' f' a', + fold_right to_smt_l (Some (r, f, a)) l = Some (r', f', a') -> + match_one y f' -> + match_one y f. +Proof. + induction l; crush. remember (fold_right to_smt_l (Some (r, f, a0)) l) as folds. + destruct folds; [|crush]; []. + symmetry in Heqfolds. + destruct p. destruct p. eapply IHl; eauto. + eapply to_smt_l_match_one; eauto. +Qed. + +#[local] Opaque Z.sub. + +Lemma valid_to_smt : + forall p r f a la max la_arr, + ~ (is_true (Euf_Checker.valid la_arr a f r)) -> + asgn_transl_spec la la_arr -> + to_smt max p = Some (r, f, a) -> + eval_hash_pred (fold_left Pand (to_equiv (snd p)) T) la = Some true -> + eval_pred_list p la = Some true. +Proof. + intros. + destruct (bo_dec (eval_pred_list p la) (Some true)); auto. + exfalso. eapply H. inv H0. inv H4. assert (DEFAULT1:=H0). + assert (DEFAULT2:=H5). clear H5. clear H0. + unfold to_smt in H1. repeat (destruct_match; try discriminate; []). + simplify. + unfold is_true. + unfold eval_pred_list in n. cbn [fst snd] in *. + apply pand_false in n; auto; []. + unfold Euf_Checker.valid. + rewrite Misc.afold_left_and. + apply forallb_forall. intros. + eapply to_list_of_list2 in H4; [|lia]. + apply in_app_or in H4. + (* These are all easy properties that need a bit of extra checking code inside of to_smt. *) + assert (tree_a_wf h11) by (now apply check_tree_a_wf_correct). + assert (tree_f_wf h13) by (now apply check_tree_f_wf_correct). + assert (match_one h11 h8) by (now (eapply AHmatch_one_hash_value; eauto)). + assert (match_one h13 h9) by (now (eapply match_one_hash_value; eauto)). + inv H4. + - eapply fold_to_smt_l_correct; eauto. + (* This is a proof that all the variables will only be between -1 and 1, which are the only + values allowed by Zval anyways, so there can't be larger values in the context. *) + assert (forall y : Int63.int, + In y l0 -> + State.Lit.interp + (interp_state_var (interp_form_hatom t_i_empty la_arr a) + (interp_form_hatom_bv t_i_empty la_arr a) f) y = + true). + { intros. eapply fold_init_correct with (form_defs := h7) (atom_defs := h6). + auto. auto. eassumption. eassumption. auto. auto. eauto. + eapply to_smt_l_fold_match_one; eauto. eapply to_smt_l_fold_match_one2; eauto. + eapply Heqp5. inversion 1. auto. lia. lia. + } auto. + - inv H13; [|inv H4]. eapply interp_eval_pred with (h6 := h6) (h11 := h11) (h13 := h13); eauto; + try reflexivity; eapply to_smt_l_fold_match_one2; eauto. +Qed. + +#[local] Transparent Z.sub. + + Lemma upd_asgn_get : + forall l y x a, + (upd_asgn l a) ! y = None -> + (upd_asgn (l ++ (y, x) :: nil) a) ! y = eval_hash_pred x (upd_asgn l a). + Proof. + intros. + unfold upd_asgn; rewrite fold_left_app; cbn [fold_left]. + cbn [fst snd]; destruct_match; auto; apply PTree.gss. + Qed. + + Lemma list_app_cons : + forall A l1 l2 (a: A), + (l1 ++ a :: nil) ++ l2 = l1 ++ a :: l2. + Proof. induction l1; crush. Qed. + + Lemma upd_asgn_app : + forall l1 l2 a, + upd_asgn (l1 ++ l2) a = upd_asgn l2 (upd_asgn l1 a). + Proof. intros; unfold upd_asgn; now rewrite fold_left_app. Qed. + + Lemma upd_asgn_pred_In : + forall p a l1 a0, + ~ pred_In (fst a) p -> + eval_hash_pred p (upd_asgn (l1 ++ a :: nil) a0) = eval_hash_pred p (upd_asgn l1 a0). + Proof. + induction p; try solve [crush]. + + intros. simpl. rewrite upd_asgn_app. simpl. destruct_match; auto. + destruct (peq (fst a0) a); subst. + - exfalso; apply H. constructor. + - apply PTree.gso; auto. + + simplify. rewrite IHp2. rewrite IHp1; auto. + unfold not; intros; apply H. constructor; auto. + unfold not; intros; apply H. apply pred_In_Pand2; auto. + + simplify. rewrite IHp2. rewrite IHp1; auto. + unfold not; intros; apply H. constructor; auto. + unfold not; intros; apply H. apply pred_In_Por2; auto. + + simplify. rewrite IHp2. rewrite IHp1; auto. + unfold not; intros; apply H. constructor; auto. + unfold not; intros; apply H. apply pred_In_Pimp2; auto. + + simplify. rewrite IHp; auto. + unfold not; intros; apply H. constructor; auto. + Qed. + + Lemma upd_asgn_app1 : + forall l2 l1 p a, + Forall (fun x => ~ pred_In (fst x) p) l2 -> + eval_hash_pred p (upd_asgn (l1 ++ l2) a) = eval_hash_pred p (upd_asgn l1 a). + Proof. + induction l2. + - intros. now rewrite app_nil_r. + - intros. rewrite <- list_app_cons. inv H. + rewrite IHl2; auto. + rewrite upd_asgn_pred_In; auto. + Qed. + + Lemma eval_hash_pred_upd_asgn_set : + forall l2 p a a0 a0', + ~ pred_In a p -> + Forall (fun x => a <> (fst x) /\ ~ pred_In a (snd x)) l2 -> + (forall x, x <> a -> a0 ! x = a0' ! x) -> + eval_hash_pred p (upd_asgn l2 a0) = eval_hash_pred p (upd_asgn l2 a0'). + Proof. + induction l2; intros. + crush. eapply eval_hash_pred_except; eauto. + inversion H0 as [| ? ? [NEQ PRED] FRL ]; subst. + simpl. + assert (eval_hash_pred (snd a) a0' = eval_hash_pred (snd a) a1). + { eapply eval_hash_pred_except; eauto. intros. symmetry. eapply H1. auto. } + setoid_rewrite H2. + destruct_match; setoid_rewrite Heqo; eauto. + eapply IHl2; eauto; intros. + destruct (peq x (fst a)); subst. + now rewrite !PTree.gss. + rewrite !PTree.gso by auto; eauto. + Qed. + + Lemma eval_hash_pred_upd_asgn_set2 : + forall l2 p a a0 y, + ~ pred_In a p -> + Forall (fun x => a <> (fst x) /\ ~ pred_In a (snd x)) l2 -> + eval_hash_pred p (upd_asgn l2 (PTree.set a y a0)) + = eval_hash_pred p (upd_asgn l2 a0). + Proof. + intros; eapply eval_hash_pred_upd_asgn_set; eauto. + intros; now apply PTree.gso. + Qed. + + Lemma upd_asgn_app2 : + forall l1 l2 p a, + Forall (fun y => Forall (fun x => fst y <> fst x /\ ~ pred_In (fst y) (snd x)) l2) l1 -> + (forall x, In x l1 -> ~ pred_In (fst x) p) -> + eval_hash_pred p (upd_asgn (l1 ++ l2) a) = eval_hash_pred p (upd_asgn l2 a). + Proof. + induction l1; auto. + intros; simpl. + inv H. + rewrite IHl1; auto. + destruct_match; auto. + apply eval_hash_pred_upd_asgn_set2; auto. + Qed. + + Lemma sorted_rev : + forall A R l (b: A) a, + LocallySorted (Basics.flip R) (l ++ (b :: a :: nil)) -> + R a b. + Proof. + induction l; crush. + inv H. auto. inv H. + assert (forall A (a b: list A), nil = a ++ b -> a = nil /\ b = nil). + { induction a1; crush. } + apply H in H2. crush. + eapply IHl. rewrite <- H1. auto. + Qed. + + Lemma sorted_rev2 : + forall A R l (b: A) a, + LocallySorted (Basics.flip R) (l ++ b :: nil) -> + R a b -> + LocallySorted (Basics.flip R) (l ++ (b :: a :: nil)). + Proof. + induction l; crush. + constructor. constructor. auto. + inv H. + assert (forall A (a b: list A), nil = a ++ b -> a = nil /\ b = nil). + { induction a1; crush. } + apply H in H3. crush. + replace (a :: l ++ b :: a0 :: nil) with ((a :: l ++ b :: nil) ++ a0 :: nil). + rewrite <- H2. + replace ((a :: b0 :: l0) ++ a0 :: nil) with (a :: b0 :: (l0 ++ a0 :: nil)). + constructor; auto. + replace (b0 :: l0 ++ a0 :: nil) with ((b0 :: l0) ++ a0 :: nil). + rewrite H2. + replace ((l ++ b :: nil) ++ a0 :: nil) with (l ++ b :: a0 :: nil). + eapply IHl; eauto. rewrite <- H2. auto. + rewrite list_app_cons. auto. + rewrite app_comm_cons. auto. + rewrite app_comm_cons. auto. + rewrite <- app_comm_cons. + rewrite list_app_cons. auto. + Qed. + + Lemma sorted_rev3 : + forall A R l, + Sorted.LocallySorted R l -> + Sorted.LocallySorted (Basics.flip R) (@rev A l). + Proof. + induction l; crush. inv H. constructor. + inv H. crush. constructor. + crush. + replace ((rev l0 ++ b :: nil) ++ a :: nil) with (rev l0 ++ b :: a :: nil). + eapply sorted_rev2; eauto. + now rewrite list_app_cons. + Qed. + + Lemma sorted_rev4 : + forall A R l, + Sorted.Sorted R l -> + Sorted.Sorted (Basics.flip R) (@rev A l). + Proof. + intros. apply Sorted_LocallySorted_iff. + apply sorted_rev3. apply Sorted_LocallySorted_iff. auto. + Qed. + + Lemma unnest_predicate_lt_fresh : + forall p p' fresh fresh' lp, + unnest_predicate fresh p = (p', lp, fresh') -> + (fresh <= fresh')%positive. + Proof. + induction p; crush; repeat (destruct_match; []); simplify; + try (pose proof (IHp1 _ _ _ _ Heqp); pose proof (IHp2 _ _ _ _ Heqp4); lia). + apply IHp in Heqp0; lia. + Qed. + + Lemma unnest_predicate_lt_in_list : + forall p p' fresh fresh' lp, + unnest_predicate fresh p = (p', lp, fresh') -> + Forall (fun x => (fresh <= fst x < fresh')%positive) lp. + Proof. + induction p; crush; repeat (destruct_match; []); simplify. + - pose proof (IHp1 _ _ _ _ Heqp). + pose proof (IHp2 _ _ _ _ Heqp4). + constructor; cbn. + + apply unnest_predicate_lt_fresh in Heqp4. + apply unnest_predicate_lt_fresh in Heqp. lia. + + apply Forall_app; split; apply Forall_forall; intros. + * eapply Forall_forall in H0; eauto. + apply unnest_predicate_lt_fresh in Heqp. lia. + * eapply Forall_forall in H; eauto. + apply unnest_predicate_lt_fresh in Heqp4. lia. + - pose proof (IHp1 _ _ _ _ Heqp). + pose proof (IHp2 _ _ _ _ Heqp4). + constructor; cbn. + + apply unnest_predicate_lt_fresh in Heqp4. + apply unnest_predicate_lt_fresh in Heqp. lia. + + apply Forall_app; split; apply Forall_forall; intros. + * eapply Forall_forall in H0; eauto. + apply unnest_predicate_lt_fresh in Heqp. lia. + * eapply Forall_forall in H; eauto. + apply unnest_predicate_lt_fresh in Heqp4. lia. + - pose proof (IHp1 _ _ _ _ Heqp). + pose proof (IHp2 _ _ _ _ Heqp4). + constructor; cbn. + + apply unnest_predicate_lt_fresh in Heqp4. + apply unnest_predicate_lt_fresh in Heqp. lia. + + apply Forall_app; split; apply Forall_forall; intros. + * eapply Forall_forall in H0; eauto. + apply unnest_predicate_lt_fresh in Heqp. lia. + * eapply Forall_forall in H; eauto. + apply unnest_predicate_lt_fresh in Heqp4. lia. + - pose proof (IHp _ _ _ _ Heqp0). + constructor; cbn. + + apply unnest_predicate_lt_fresh in Heqp0. lia. + + apply Forall_forall; intros. eapply Forall_forall in H; eauto. + lia. + Qed. + + Lemma unnest_predicate_lt_in_list5 : + forall p p' fresh fresh' lp, + unnest_predicate fresh p = (p', lp, fresh') -> + (max_hash_pred p < fresh)%positive -> + (max_hash_pred p' < fresh')%positive. + Proof. induction p; crush; repeat (destruct_match; []); crush. Qed. + + Lemma unnest_predicate_lt_in_list2 : + forall p p' fresh fresh' lp, + unnest_predicate fresh p = (p', lp, fresh') -> + (max_hash_pred p < fresh)%positive -> + Forall (fun x => (max_hash_pred (snd x) < fst x)%positive) lp. + Proof. + induction p; crush; repeat (destruct_match; []); simplify. + - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). + pose proof (IHp1 _ _ _ _ Heqp ltac:(lia)) as X. + pose proof (IHp2 _ _ _ _ Heqp4 ltac:(lia)) as Y. + pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp ltac:(lia)). + pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp4 ltac:(lia)). + constructor; cbn; [lia|]. + apply Forall_app; split; eapply Forall_forall; intros. + + eapply Forall_forall in Y; eauto. + + eapply Forall_forall in X; eauto. + - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). + pose proof (IHp1 _ _ _ _ Heqp ltac:(lia)) as X. + pose proof (IHp2 _ _ _ _ Heqp4 ltac:(lia)) as Y. + pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp ltac:(lia)). + pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp4 ltac:(lia)). + constructor; cbn; [lia|]. + apply Forall_app; split; eapply Forall_forall; intros. + + eapply Forall_forall in Y; eauto. + + eapply Forall_forall in X; eauto. + - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). + pose proof (IHp1 _ _ _ _ Heqp ltac:(lia)) as X. + pose proof (IHp2 _ _ _ _ Heqp4 ltac:(lia)) as Y. + pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp ltac:(lia)). + pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp4 ltac:(lia)). + constructor; cbn; [lia|]. + apply Forall_app; split; eapply Forall_forall; intros. + + eapply Forall_forall in Y; eauto. + + eapply Forall_forall in X; eauto. + - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp0). + pose proof (IHp _ _ _ _ Heqp0 ltac:(lia)) as X. + pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp0 ltac:(lia)). + constructor; cbn; [lia|auto]. + Qed. + + Lemma unnest_predicate_lt_in_list4 : + forall p p' fresh fresh' lp y, + unnest_predicate fresh p = (p', lp, fresh') -> + pred_In y p' -> + In y (map fst lp) \/ pred_In y p. + Proof. + induction p; crush; repeat (destruct_match; []); simplify. + - inv H0. tauto. + - inv H0. tauto. + - inv H0. tauto. + - inv H0. tauto. + Qed. + + Lemma unnest_predicate_lt_in_list3 : + forall p p' fresh fresh' lp, + unnest_predicate fresh p = (p', lp, fresh') -> + Forall (fun x => forall y, pred_In y (snd x) -> In y (map fst lp) \/ pred_In y p) lp. + Proof. + induction p; crush; repeat (destruct_match; []); simplify. + - pose proof (IHp1 _ _ _ _ Heqp). + pose proof (IHp2 _ _ _ _ Heqp4). + constructor; intros; cbn [snd] in *. + + inv H1. + * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp H4). + inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto. + right. now apply pred_In_Pand1. + * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp4 H4). + inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto. + right. now apply pred_In_Pand2. + + apply Forall_app; split. + * apply Forall_forall; intros. eapply Forall_forall in H0; eauto. + rewrite map_app. apply H0 in H2. inv H2. + left. right. apply in_app; tauto. + right. now apply pred_In_Pand2. + * apply Forall_forall; intros. eapply Forall_forall in H; eauto. + rewrite map_app. apply H in H2. inv H2. + left. right. apply in_app; tauto. + right. now apply pred_In_Pand1. + - pose proof (IHp1 _ _ _ _ Heqp). + pose proof (IHp2 _ _ _ _ Heqp4). + constructor; intros; cbn [snd] in *. + + inv H1. + * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp H4). + inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto. + right. now apply pred_In_Por1. + * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp4 H4). + inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto. + right. now apply pred_In_Por2. + + apply Forall_app; split. + * apply Forall_forall; intros. eapply Forall_forall in H0; eauto. + rewrite map_app. apply H0 in H2. inv H2. + left. right. apply in_app; tauto. + right. now apply pred_In_Por2. + * apply Forall_forall; intros. eapply Forall_forall in H; eauto. + rewrite map_app. apply H in H2. inv H2. + left. right. apply in_app; tauto. + right. now apply pred_In_Por1. + - pose proof (IHp1 _ _ _ _ Heqp). + pose proof (IHp2 _ _ _ _ Heqp4). + constructor; intros; cbn [snd] in *. + + inv H1. + * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp H4). + inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto. + right. now apply pred_In_Pimp1. + * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp4 H4). + inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto. + right. now apply pred_In_Pimp2. + + apply Forall_app; split. + * apply Forall_forall; intros. eapply Forall_forall in H0; eauto. + rewrite map_app. apply H0 in H2. inv H2. + left. right. apply in_app; tauto. + right. now apply pred_In_Pimp2. + * apply Forall_forall; intros. eapply Forall_forall in H; eauto. + rewrite map_app. apply H in H2. inv H2. + left. right. apply in_app; tauto. + right. now apply pred_In_Pimp1. + - pose proof (IHp _ _ _ _ Heqp0). + constructor; intros; cbn [snd] in *. + + inv H0. + pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp0 H3). + inv H0. tauto. + right. now apply pred_In_Pnot. + + apply Forall_forall; intros. eapply Forall_forall in H0; eauto. + apply H0 in H1. inv H1; [tauto|]. + right. now apply pred_In_Pnot. + Qed. + + Lemma unnest_predicate_sorted : + forall p p' lp fresh' fresh, + unnest_predicate fresh p = (p', lp, fresh') -> + Sorted.Sorted (Basics.flip pl_lt) lp. + Proof. + induction p; crush; try apply Sorted_nil; + repeat (destruct_match; []); simplify. + - constructor. + eapply SetoidList.SortA_app with (eqA := eq); auto. + eapply IHp2; eassumption. + eapply IHp1; eassumption. + intros. apply SetoidList.InA_alt in H; simplify. + apply SetoidList.InA_alt in H0; simplify. + unfold Basics.flip. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4). + eapply Forall_forall in H; [|eassumption]. + eapply Forall_forall in H0; [|eassumption]. + destruct x, x0; unfold pl_lt; cbn [snd fst] in *; lia. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4). + apply SetoidList.InfA_app. + + apply SetoidList.InA_InfA with (eqA := eq); auto; intros. + apply SetoidList.InA_alt in H1; simplify. + eapply Forall_forall in H0; [|eassumption]. + unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia. + + apply SetoidList.InA_InfA with (eqA := eq); auto; intros. + apply SetoidList.InA_alt in H1; simplify. + eapply Forall_forall in H; [|eassumption]. + unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). lia. + - constructor. + eapply SetoidList.SortA_app with (eqA := eq); auto. + eapply IHp2; eassumption. + eapply IHp1; eassumption. + intros. apply SetoidList.InA_alt in H; simplify. + apply SetoidList.InA_alt in H0; simplify. + unfold Basics.flip. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4). + eapply Forall_forall in H; [|eassumption]. + eapply Forall_forall in H0; [|eassumption]. + destruct x, x0; unfold pl_lt; cbn [snd fst] in *; lia. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4). + apply SetoidList.InfA_app. + + apply SetoidList.InA_InfA with (eqA := eq); auto; intros. + apply SetoidList.InA_alt in H1; simplify. + eapply Forall_forall in H0; [|eassumption]. + unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia. + + apply SetoidList.InA_InfA with (eqA := eq); auto; intros. + apply SetoidList.InA_alt in H1; simplify. + eapply Forall_forall in H; [|eassumption]. + unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). lia. + - constructor. + eapply SetoidList.SortA_app with (eqA := eq); auto. + eapply IHp2; eassumption. + eapply IHp1; eassumption. + intros. apply SetoidList.InA_alt in H; simplify. + apply SetoidList.InA_alt in H0; simplify. + unfold Basics.flip. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4). + eapply Forall_forall in H; [|eassumption]. + eapply Forall_forall in H0; [|eassumption]. + destruct x, x0; unfold pl_lt; cbn [snd fst] in *; lia. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4). + apply SetoidList.InfA_app. + + apply SetoidList.InA_InfA with (eqA := eq); auto; intros. + apply SetoidList.InA_alt in H1; simplify. + eapply Forall_forall in H0; [|eassumption]. + unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia. + + apply SetoidList.InA_InfA with (eqA := eq); auto; intros. + apply SetoidList.InA_alt in H1; simplify. + eapply Forall_forall in H; [|eassumption]. + unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). lia. + - constructor. + eapply IHp; eassumption. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp0). + apply SetoidList.InA_InfA with (eqA := eq); auto; intros. + apply SetoidList.InA_alt in H0; simplify. + eapply Forall_forall in H; [|eassumption]. + unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia. + Qed. + + Lemma to_equiv_rev : + forall l, rev (to_equiv l) = to_equiv (rev l). + Proof. unfold to_equiv; intros. rewrite map_rev. auto. Qed. + + Lemma unnest_predicate_sorted_app : + forall p1 p l p0 p3 p4 l0 fresh p2, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + Sorted.Sorted (Basics.flip pl_lt) l -> + Sorted.Sorted (Basics.flip pl_lt) l0 -> + Sorted.Sorted (Basics.flip pl_lt) (l0 ++ l). + Proof. + intros * NEST1 NEST2 SORT1 SORT2. + apply SetoidList.SortA_app with (eqA := eq); auto. + intros. + apply SetoidList.InA_alt in H. + apply SetoidList.InA_alt in H0. simplify. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2). + eapply Forall_forall in H; [|eassumption]. + eapply Forall_forall in H1; [|eassumption]. + unfold Basics.flip, pl_lt. lia. + Qed. + + Lemma unnest_predicate_equiv_list : + forall p p0 p1 p2 p3 p4 l l0 fresh, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + (Pos.max (max_hash_pred p1) (max_hash_pred p2) < fresh)%positive -> + equiv_list_wf (rev (l0 ++ l)). + Proof. + intros * NEST1 NEST2 MAX. + unfold equiv_list_wf. split. unfold Sorted. + pose proof (unnest_predicate_sorted _ _ _ _ _ NEST1). + pose proof (unnest_predicate_sorted _ _ _ _ _ NEST2). + replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by (unfold Basics.flip; auto). + apply sorted_rev4. + eapply unnest_predicate_sorted_app; eauto. + apply Forall_rev; apply Forall_app; split; + eapply unnest_predicate_lt_in_list2; eauto. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + lia. lia. + Qed. + + Lemma pred_in_fold : + forall A l p y, + @pred_In A p (fold_left Pand l y) -> + (exists i, In i l /\ pred_In p i) \/ pred_In p y. + Proof. + induction l. + intros. simplify. tauto. + intros. simpl in *. apply IHl in H. + inv H; simplify. left. econstructor. + constructor. right. eauto. auto. + inv H0; try tauto. + do 2 econstructor; split; try eassumption; tauto. + Qed. + + Lemma max_hash_pred_lt : + forall p l, + pred_In l p -> + (l <= max_hash_pred p)%positive. + Proof. + induction p; intros; try inv H; crush; + try (apply IHp1 in H2; lia); + apply IHp2 in H2; lia. + Qed. + + Lemma unnest_predicate_not_in : + forall p p0 p1 p2 p3 p4 l l0 fresh y, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + (Pos.max (max_hash_pred p1) (max_hash_pred p2) < fresh)%positive -> + Forall (fun x : positive * hash_pred => + ~ pred_In (fst x) (fold_left Pand (to_equiv (l0 ++ l)) T)) + ((p4, y) :: nil). + Proof. + intros * NEST1 NEST2 MAX. + constructor; [|constructor]. cbn [fst]. unfold not; intros. + apply pred_in_fold in H. inv H; inv H0; + simplify. unfold to_equiv in H0. apply map_in_some in H0. simplify. + apply in_app_or in H0; inv H0. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TEMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2). + eapply Forall_forall in H0; [|eassumption]. + eapply Forall_forall in H2; [|eassumption]. destruct x0. cbn [snd fst] in *. + apply max_hash_pred_lt in H1. unfold equiv in H1. + unfold max_hash_pred in H1. fold max_hash_pred in H1. lia. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1). + eapply Forall_forall in H0; [|eassumption]. + eapply Forall_forall in H2; [|eassumption]. destruct x0. cbn [snd fst] in *. + apply max_hash_pred_lt in H1. unfold equiv in H1. + unfold max_hash_pred in H1. fold max_hash_pred in H1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + Qed. + + Lemma unnest_predicate_not_in4 : + forall p p0 p1 l fresh y, + unnest_predicate fresh p1 = (p, l, p0) -> + (max_hash_pred p1 < fresh)%positive -> + Forall (fun x : positive * hash_pred => + ~ pred_In (fst x) (fold_left Pand (to_equiv l) T)) + ((p0, y) :: nil). + Proof. + intros * NEST1 MAX. + constructor; [|constructor]. cbn [fst]. unfold not; intros. + apply pred_in_fold in H. inv H; inv H0; + simplify. unfold to_equiv in H0. apply map_in_some in H0. simplify. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1). + eapply Forall_forall in H; [|eassumption]. + eapply Forall_forall in H2; [|eassumption]. destruct x0. cbn [snd fst] in *. + apply max_hash_pred_lt in H1. unfold equiv in H1. + unfold max_hash_pred in H1. fold max_hash_pred in H1. lia. + Qed. + + Lemma unnest_predicate_in_pred : + forall fresh p1 p l p0, + unnest_predicate fresh p1 = (p, l, p0) -> + (max_hash_pred p1 < fresh)%positive -> + ~ pred_In p0 p. + Proof. + destruct p1; unfold not; intros. + - inv H. inv H1. + - inv H. inv H1. + - inv H. inv H1. + - inv H. crush. inv H1. lia. + - simplify. repeat (destruct_match; []). simplify. + inv H1. lia. + - simplify. repeat (destruct_match; []). simplify. + inv H1. lia. + - simplify. repeat (destruct_match; []). simplify. + inv H1. lia. + - simplify. repeat (destruct_match; []). simplify. + inv H1. lia. + Qed. + + Lemma unnest_predicate_in_pred2 : + forall fresh p1 p l p0, + unnest_predicate fresh p1 = (p, l, p0) -> + (max_hash_pred p1 < fresh)%positive -> + (max_hash_pred p < p0)%positive. + Proof. + intros. + destruct p1; crush. + - repeat (destruct_match; []); simplify; lia. + - repeat (destruct_match; []); simplify; lia. + - repeat (destruct_match; []); simplify; lia. + - repeat (destruct_match; []); simplify; lia. + Qed. + + Lemma unnest_predicate_forall_none : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 ∧ p2) < fresh)%positive -> + Forall (fun x : positive * predicate => a ! (fst x) = None) (rev (l0 ++ l)). + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + apply Forall_forall; intros. apply GTMAX. + unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as X3. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as X4. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as X2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as Y1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y2. + apply in_rev in H. apply in_app in H. inv H. + eapply Forall_forall in X1; eauto; []. + eapply Forall_forall in X2; eauto; []. lia. + eapply Forall_forall in Y1; eauto; []. + eapply Forall_forall in Y2; eauto; []. lia. + Qed. + + Lemma unnest_predicate_forall_gt1 : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 ∧ p2) < fresh)%positive -> + Forall (fun x : positive * predicate => (1 < fst x)%positive) (rev (l0 ++ l)). + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + apply Forall_forall; intros. + unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as X3. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as X4. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as X2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as Y1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y2. + apply in_rev in H. apply in_app in H. inv H. + eapply Forall_forall in X1; eauto; []. + eapply Forall_forall in X2; eauto; []. lia. + eapply Forall_forall in Y1; eauto; []. + eapply Forall_forall in Y2; eauto; []. lia. + Qed. + + Lemma unnest_predicate_not_in3 : + forall p1 p0 l fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred p1 < fresh)%positive -> + ~ In p0 (map fst (rev l)). + Proof. + intros * NEST1 EVAL1 GTMAX MAXHASH. + unfold not; intros. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + apply map_in_some in H. simplify. + eapply in_rev in H. + eapply Forall_forall in H0; eauto. + eapply Forall_forall in H1; eauto. + destruct x; cbn [fst snd max_hash_pred] in *. + lia. + Qed. + + Lemma unnest_predicate_not_in2 : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 ∧ p2) < fresh)%positive -> + ~ In p4 (map fst (rev l ++ rev l0)). + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + unfold not; intros. + + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2). + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1). + apply map_in_some in H. simplify. + apply in_app_or in H. inv H. + eapply in_rev in H4. + eapply Forall_forall in H2; eauto. + eapply Forall_forall in H3; eauto. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). + destruct x; cbn [fst snd] in *. lia. + eapply in_rev in H4. + eapply Forall_forall in H0; eauto. + eapply Forall_forall in H1; eauto. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + destruct x; cbn [fst snd] in *. lia. + Qed. + + Lemma eval_equiv_added : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 ∧ p2) < fresh)%positive -> + eval_hash_pred (equiv (Pbase p4) (p ∧ p3)) (upd_asgn (rev l ++ rev l0 ++ (p4, p ∧ p3) :: nil) a) = Some true. + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + apply eval_equiv2. rewrite eval_hash_pred_get. + rewrite app_assoc. + rewrite upd_asgn_get. + symmetry. rewrite upd_asgn_app1; auto. + constructor; [|constructor]; simpl. + pose proof NEST1 as X1. pose proof NEST2 as X2. + eapply unnest_predicate_in_pred2 in X1. + eapply unnest_predicate_in_pred2 in X2. + + 2: { unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + + 2: { unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). + unfold not; intros. apply max_hash_pred_lt in H1. + cbn [max_hash_pred] in H1. lia. + + rewrite upd_asgn_not_in. eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + eapply unnest_predicate_not_in2; eauto. + Qed. + + Lemma eval_equiv_added_Por : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 ∨ p2) < fresh)%positive -> + eval_hash_pred (equiv (Pbase p4) (p ∨ p3)) (upd_asgn (rev l ++ rev l0 ++ (p4, p ∨ p3) :: nil) a) = Some true. + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + apply eval_equiv2. rewrite eval_hash_pred_get. + rewrite app_assoc. + rewrite upd_asgn_get. + symmetry. rewrite upd_asgn_app1; auto. + constructor; [|constructor]; simpl. + pose proof NEST1 as X1. pose proof NEST2 as X2. + eapply unnest_predicate_in_pred2 in X1. + eapply unnest_predicate_in_pred2 in X2. + + 2: { unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + + 2: { unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). + unfold not; intros. apply max_hash_pred_lt in H1. + cbn [max_hash_pred] in H1. lia. + + rewrite upd_asgn_not_in. eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + eapply unnest_predicate_not_in2; eauto. + Qed. + + Lemma eval_equiv_added_Pimp : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 → p2) < fresh)%positive -> + eval_hash_pred (equiv (Pbase p4) (p → p3)) (upd_asgn (rev l ++ rev l0 ++ (p4, p → p3) :: nil) a) = Some true. + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + apply eval_equiv2. rewrite eval_hash_pred_get. + rewrite app_assoc. + rewrite upd_asgn_get. + symmetry. rewrite upd_asgn_app1; auto. + constructor; [|constructor]; simpl. + pose proof NEST1 as X1. pose proof NEST2 as X2. + eapply unnest_predicate_in_pred2 in X1. + eapply unnest_predicate_in_pred2 in X2. + + 2: { unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + + 2: { unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). + unfold not; intros. apply max_hash_pred_lt in H1. + cbn [max_hash_pred] in H1. lia. + + rewrite upd_asgn_not_in. eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + eapply unnest_predicate_not_in2; eauto. + Qed. + + Lemma unnest_predicate_correct_Pand : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 ∧ p2) < fresh)%positive -> + eval_hash_pred (p1 ∧ p2) a = + eval_hash_pred (Pbase p4 ∧ fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∧ p3))) + (upd_asgn (rev (l0 ++ l) ++ (p4, p ∧ p3) :: nil) a). + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + assert (eval_hash_pred (fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∧ p3))) + (upd_asgn (rev l ++ rev l0 ++ (p4, p ∧ p3) :: nil) a) = Some true). + { apply eval_hash_pred_fold_Pand2 with (x := T). + rewrite app_assoc. + rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in; eauto]. + replace (rev l ++ rev l0) with (rev (l0 ++ l)) by (rewrite rev_app_distr; auto). + apply fold_left_Pand_rev. + rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + eapply unnest_predicate_equiv_list; eauto. + eapply unnest_predicate_forall_none; eauto. + eapply unnest_predicate_forall_gt1; eauto. + rewrite eval_hash_pred_T_Pand. + eapply eval_equiv_added; eauto. + } + assert (eval_hash_pred (p1 ∧ p2) a = eval_hash_pred (Pbase p4) + (upd_asgn ((rev l ++ rev l0) ++ (p4, p ∧ p3) :: nil) a)). + { rewrite eval_hash_pred_get. + rewrite upd_asgn_get. + 2: { rewrite upd_asgn_not_in by (eapply unnest_predicate_not_in2; eauto). + eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + apply eval_hash_pred_pand. + { rewrite EVAL1. unfold eval_pred_list. cbn [snd fst]. + rewrite upd_asgn_app1. + { rewrite eval_hash_pred_T_Pand2; auto. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + { unfold equiv_list_wf, Sorted; split. + { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. } + { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. cbn [max_hash_pred] in *; lia. } } + { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } + { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } } + { apply Forall_rev. apply Forall_forall; intros. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + eapply Forall_forall in H1; eauto. eapply Forall_forall in H2; eauto. + unfold not; intros. apply max_hash_pred_lt in H5. destruct x; cbn [fst snd] in *. + unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST1). + pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST2). + lia. + } } + { rewrite EVAL2. unfold eval_pred_list. cbn [snd fst]. + rewrite upd_asgn_app2. + { rewrite eval_hash_pred_T_Pand2; auto. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + { unfold equiv_list_wf, Sorted; split. + { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. } + { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + cbn [max_hash_pred] in *; lia. } } + { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } + { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } } + { apply Forall_rev. apply Forall_forall; intros. + apply Forall_rev. apply Forall_forall; intros. split. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + destruct x, x0. cbn [fst snd] in *. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + cbn [fst snd] in *. lia. + + pose proof (unnest_predicate_lt_in_list3 _ _ _ _ _ NEST2) as X. + unfold not; intros Y. eapply Forall_forall in X; eauto. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + destruct x, x0. cbn [fst snd] in *. + unfold max_hash_pred in *; fold max_hash_pred in *. + exploit unnest_predicate_in_pred2; eauto. lia; intros. + exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros. + pose proof Y as YY. apply X in YY. inv YY. + eapply map_in_some in H4; simplify. destruct x; simplify. + eapply max_hash_pred_lt in Y. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2) as X22. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y22. + eapply Forall_forall in X22; eauto. eapply Forall_forall in Y22; eauto. + cbn [fst snd] in *. + cbn [max_hash_pred] in *. + lia. lia. + eapply max_hash_pred_lt in H4. lia. + } + { intros. apply in_rev in H0. destruct x; cbn [fst snd] in *. + unfold not; intros Y. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + cbn [max_hash_pred fst snd] in *. + exploit unnest_predicate_in_pred2; eauto. lia; intros. intros. + exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros. + exploit unnest_predicate_lt_in_list4. eapply NEST2. eauto. intros. inv H3. + eapply map_in_some in H4; simplify. + destruct x. + cbn [max_hash_pred fst snd] in *. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + cbn [max_hash_pred fst snd] in *. + eapply max_hash_pred_lt in Y. lia. + eapply max_hash_pred_lt in H4. lia. + } } } + symmetry; rewrite eval_hash_pred_T_Pand2; rewrite rev_app_distr; + try solve [rewrite <- app_assoc; auto]; auto. + Qed. + + Lemma unnest_predicate_correct_Por : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 ∨ p2) < fresh)%positive -> + eval_hash_pred (p1 ∨ p2) a = + eval_hash_pred (Pbase p4 ∧ fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∨ p3))) + (upd_asgn (rev (l0 ++ l) ++ (p4, p ∨ p3) :: nil) a). + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + assert (eval_hash_pred (fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∨ p3))) + (upd_asgn (rev l ++ rev l0 ++ (p4, p ∨ p3) :: nil) a) = Some true). + { apply eval_hash_pred_fold_Pand2 with (x := T). + rewrite app_assoc. + rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in; eauto]. + replace (rev l ++ rev l0) with (rev (l0 ++ l)) by (rewrite rev_app_distr; auto). + apply fold_left_Pand_rev. + rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + eapply unnest_predicate_equiv_list; eauto. + eapply unnest_predicate_forall_none; eauto. + eapply unnest_predicate_forall_gt1; eauto. + rewrite eval_hash_pred_T_Pand. + eapply eval_equiv_added_Por; eauto. + } + assert (eval_hash_pred (p1 ∨ p2) a = eval_hash_pred (Pbase p4) + (upd_asgn ((rev l ++ rev l0) ++ (p4, p ∨ p3) :: nil) a)). + { rewrite eval_hash_pred_get. + rewrite upd_asgn_get. + 2: { rewrite upd_asgn_not_in by (eapply unnest_predicate_not_in2; eauto). + eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + apply eval_hash_pred_por. + { rewrite EVAL1. unfold eval_pred_list. cbn [snd fst]. + rewrite upd_asgn_app1. + { rewrite eval_hash_pred_T_Pand2; auto. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + { unfold equiv_list_wf, Sorted; split. + { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. } + { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. cbn [max_hash_pred] in *; lia. } } + { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } + { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } } + { apply Forall_rev. apply Forall_forall; intros. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + eapply Forall_forall in H1; eauto. eapply Forall_forall in H2; eauto. + unfold not; intros. apply max_hash_pred_lt in H5. destruct x; cbn [fst snd] in *. + unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST1). + pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST2). + lia. + } } + { rewrite EVAL2. unfold eval_pred_list. cbn [snd fst]. + rewrite upd_asgn_app2. + { rewrite eval_hash_pred_T_Pand2; auto. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + { unfold equiv_list_wf, Sorted; split. + { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. } + { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + cbn [max_hash_pred] in *; lia. } } + { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } + { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } } + { apply Forall_rev. apply Forall_forall; intros. + apply Forall_rev. apply Forall_forall; intros. split. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + destruct x, x0. cbn [fst snd] in *. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + cbn [fst snd] in *. lia. + + pose proof (unnest_predicate_lt_in_list3 _ _ _ _ _ NEST2) as X. + unfold not; intros Y. eapply Forall_forall in X; eauto. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + destruct x, x0. cbn [fst snd] in *. + unfold max_hash_pred in *; fold max_hash_pred in *. + exploit unnest_predicate_in_pred2; eauto. lia; intros. + exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros. + pose proof Y as YY. apply X in YY. inv YY. + eapply map_in_some in H4; simplify. destruct x; simplify. + eapply max_hash_pred_lt in Y. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2) as X22. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y22. + eapply Forall_forall in X22; eauto. eapply Forall_forall in Y22; eauto. + cbn [fst snd] in *. + cbn [max_hash_pred] in *. + lia. lia. + eapply max_hash_pred_lt in H4. lia. + } + { intros. apply in_rev in H0. destruct x; cbn [fst snd] in *. + unfold not; intros Y. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + cbn [max_hash_pred fst snd] in *. + exploit unnest_predicate_in_pred2; eauto. lia; intros. intros. + exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros. + exploit unnest_predicate_lt_in_list4. eapply NEST2. eauto. intros. inv H3. + eapply map_in_some in H4; simplify. + destruct x. + cbn [max_hash_pred fst snd] in *. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + cbn [max_hash_pred fst snd] in *. + eapply max_hash_pred_lt in Y. lia. + eapply max_hash_pred_lt in H4. lia. + } } } + symmetry; rewrite eval_hash_pred_T_Pand2; rewrite rev_app_distr; + try solve [rewrite <- app_assoc; auto]; auto. + Qed. + +Lemma unnest_predicate_correct_Pimp : + forall p1 p2 p0 p3 l0 l p4 fresh p a, + unnest_predicate fresh p1 = (p, l, p0) -> + unnest_predicate p0 p2 = (p3, l0, p4) -> + eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) -> + eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) -> + (forall y, (fresh <= y)%positive -> a ! y = None) -> + (max_hash_pred (p1 → p2) < fresh)%positive -> + eval_hash_pred (p1 → p2) a = + eval_hash_pred (Pbase p4 ∧ fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p → p3))) + (upd_asgn (rev (l0 ++ l) ++ (p4, p → p3) :: nil) a). + Proof. + intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH. + assert (eval_hash_pred (fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p → p3))) + (upd_asgn (rev l ++ rev l0 ++ (p4, p → p3) :: nil) a) = Some true). + { apply eval_hash_pred_fold_Pand2 with (x := T). + rewrite app_assoc. + rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in; eauto]. + replace (rev l ++ rev l0) with (rev (l0 ++ l)) by (rewrite rev_app_distr; auto). + apply fold_left_Pand_rev. + rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + eapply unnest_predicate_equiv_list; eauto. + eapply unnest_predicate_forall_none; eauto. + eapply unnest_predicate_forall_gt1; eauto. + rewrite eval_hash_pred_T_Pand. + eapply eval_equiv_added_Pimp; eauto. + } + assert (eval_hash_pred (p1 → p2) a = eval_hash_pred (Pbase p4) + (upd_asgn ((rev l ++ rev l0) ++ (p4, p → p3) :: nil) a)). + { rewrite eval_hash_pred_get. + rewrite upd_asgn_get. + 2: { rewrite upd_asgn_not_in by (eapply unnest_predicate_not_in2; eauto). + eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia. + } + apply eval_hash_pred_pimp. + { rewrite EVAL1. unfold eval_pred_list. cbn [snd fst]. + rewrite upd_asgn_app1. + { rewrite eval_hash_pred_T_Pand2; auto. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + { unfold equiv_list_wf, Sorted; split. + { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. } + { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. + cbn [max_hash_pred] in *; lia. } } + { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } + { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } } + { apply Forall_rev. apply Forall_forall; intros. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)). + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + eapply Forall_forall in H1; eauto. eapply Forall_forall in H2; eauto. + unfold not; intros. apply max_hash_pred_lt in H5. destruct x; cbn [fst snd] in *. + unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST1). + pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST2). + lia. + } } + { rewrite EVAL2. unfold eval_pred_list. cbn [snd fst]. + rewrite upd_asgn_app2. + { rewrite eval_hash_pred_T_Pand2; auto. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + { unfold equiv_list_wf, Sorted; split. + { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. } + { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + cbn [max_hash_pred] in *; lia. } } + { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } + { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2. + all: eauto. intros. cbn. rewrite rev_app_distr in H0. + apply Forall_app in H0; crush. } } + { apply Forall_rev. apply Forall_forall; intros. + apply Forall_rev. apply Forall_forall; intros. split. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + destruct x, x0. cbn [fst snd] in *. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + cbn [fst snd] in *. lia. + + pose proof (unnest_predicate_lt_in_list3 _ _ _ _ _ NEST2) as X. + unfold not; intros Y. eapply Forall_forall in X; eauto. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + destruct x, x0. cbn [fst snd] in *. + unfold max_hash_pred in *; fold max_hash_pred in *. + exploit unnest_predicate_in_pred2; eauto. lia; intros. + exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros. + pose proof Y as YY. apply X in YY. inv YY. + eapply map_in_some in H4; simplify. destruct x; simplify. + eapply max_hash_pred_lt in Y. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2) as X22. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y22. + eapply Forall_forall in X22; eauto. eapply Forall_forall in Y22; eauto. + cbn [fst snd] in *. + cbn [max_hash_pred] in *. + lia. lia. + eapply max_hash_pred_lt in H4. lia. + } + { intros. apply in_rev in H0. destruct x; cbn [fst snd] in *. + unfold not; intros Y. + cbn [max_hash_pred] in *. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1. + eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto. + cbn [max_hash_pred fst snd] in *. + exploit unnest_predicate_in_pred2; eauto. lia; intros. intros. + exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros. + exploit unnest_predicate_lt_in_list4. eapply NEST2. eauto. intros. inv H3. + eapply map_in_some in H4; simplify. + destruct x. + cbn [max_hash_pred fst snd] in *. + pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2. + eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto. + cbn [max_hash_pred fst snd] in *. + eapply max_hash_pred_lt in Y. lia. + eapply max_hash_pred_lt in H4. lia. + } } } + symmetry; rewrite eval_hash_pred_T_Pand2; rewrite rev_app_distr; + try solve [rewrite <- app_assoc; auto]; auto. + Qed. + + Lemma upd_asgn_nil : + forall a, upd_asgn nil a = a. + Proof. crush. Qed. + + #[local] Opaque eval_hash_pred. + #[local] Opaque upd_asgn. + + Lemma unnest_predicate_correct : + forall a p fresh p' lp fresh', + (max_hash_pred p < fresh)%positive -> + unnest_predicate fresh p = (p', lp, fresh') -> + (forall y : positive, (fresh <= y)%positive -> a ! y = None) -> + eval_hash_pred p a = eval_pred_list (p', lp) (upd_asgn (rev lp) a). + Proof. + induction p; try solve [crush]. + - unfold eval_pred_list. simplify. + rewrite eval_hash_pred_T_Pand3. + rewrite upd_asgn_nil. auto. + - simplify. + destruct (unnest_predicate fresh p1) eqn:?. destruct p. + destruct (unnest_predicate p0 p2) eqn:?. destruct p3. + unfold eval_pred_list. simplify. + pose proof Heqp as X1. pose proof Heqp3 as X2. + pose proof X2 as X3. + pose proof X1 as X4. + apply IHp1 in X1; [|lia|auto]. + apply unnest_predicate_lt_fresh in X2. + apply unnest_predicate_lt_fresh in X4. + apply IHp2 in X3; [|lia|intros; eapply H1; lia]. + eapply unnest_predicate_correct_Pand; eauto. + - simplify. + destruct (unnest_predicate fresh p1) eqn:?. destruct p. + destruct (unnest_predicate p0 p2) eqn:?. destruct p3. + unfold eval_pred_list. simplify. + pose proof Heqp as X1. pose proof Heqp3 as X2. + pose proof X2 as X3. + pose proof X1 as X4. + apply IHp1 in X1; [|lia|auto]. + apply unnest_predicate_lt_fresh in X2. + apply unnest_predicate_lt_fresh in X4. + apply IHp2 in X3; [|lia|intros; eapply H1; lia]. + eapply unnest_predicate_correct_Por; eauto. + - simplify. + destruct (unnest_predicate fresh p1) eqn:?. destruct p. + destruct (unnest_predicate p0 p2) eqn:?. destruct p3. + unfold eval_pred_list. simplify. + pose proof Heqp as X1. pose proof Heqp3 as X2. + pose proof X2 as X3. + pose proof X1 as X4. + apply IHp1 in X1; [|lia|auto]. + apply unnest_predicate_lt_fresh in X2. + apply unnest_predicate_lt_fresh in X4. + apply IHp2 in X3; [|lia|intros; eapply H1; lia]. + eapply unnest_predicate_correct_Pimp; eauto. + - simplify. repeat destruct_match; simplify. + unfold eval_pred_list; simplify. + pose proof Heqp0 as X1. + pose proof Heqp0 as X2. + apply IHp in X1; [|lia|auto]. + apply unnest_predicate_lt_fresh in X2. + symmetry; rewrite eval_hash_pred_T_Pand2; [symmetry|]. + + rewrite eval_hash_pred_get. + rewrite upd_asgn_get; + [|rewrite upd_asgn_not_in; auto; + eapply unnest_predicate_not_in3; eauto]; []. + apply eval_hash_pred_pnot. rewrite X1. unfold eval_pred_list. + simplify. + rewrite eval_hash_pred_T_Pand2; auto; []. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + * unfold equiv_list_wf; split. + ** unfold Sorted. + replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. + ** apply Forall_rev; eapply unnest_predicate_lt_in_list2; eauto. + * apply Forall_rev. apply Forall_forall; intros. apply H1. + apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto. + lia. + * apply Forall_rev. apply Forall_forall; intros. simplify. + apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto. + lia. + + apply eval_hash_pred_fold_Pand2 with (x := T). + * rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in4; eauto]; []. + apply fold_left_Pand_rev. rewrite to_equiv_rev. + apply eval_hash_pred_equiv_asgn; auto. + ** unfold equiv_list_wf; split. + *** unfold Sorted. + replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + apply sorted_rev4. eapply unnest_predicate_sorted; eauto. + *** apply Forall_rev; eapply unnest_predicate_lt_in_list2; eauto. + ** apply Forall_rev. apply Forall_forall; intros. apply H1. + apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto. + lia. + ** apply Forall_rev. apply Forall_forall; intros. simplify. + apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto. + lia. + * rewrite eval_hash_pred_T_Pand. + apply eval_equiv2. rewrite eval_hash_pred_get. + rewrite upd_asgn_get. + ** symmetry. rewrite upd_asgn_app1; auto. + constructor; [|constructor]; simpl. + pose proof Heqp0 as NEST1. + pose proof NEST1 as Y1. + eapply unnest_predicate_in_pred2 in Y1. + *** pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). + unfold not; intros. apply max_hash_pred_lt in H2. + cbn [max_hash_pred] in H2. lia. + *** unfold max_hash_pred in *; fold max_hash_pred in *. + pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). lia. + ** rewrite upd_asgn_not_in; auto. eapply unnest_predicate_not_in3; eauto. + Qed. + +#[local] Transparent eval_hash_pred. +#[local] Transparent upd_asgn. + +Lemma interp_aux_correct : + forall a ba f h1 h2, + (forall l, h1 <> Fimp l) -> + is_true (form_eqb h1 h2) -> + interp_aux a ba f h1 = interp_aux a ba f h2. +Proof. + unfold is_true. intros * IMP **. + destruct h1; unfold form_eqb in *; try destruct_match; crush; auto. + - apply Int63.eqb_spec in H; subst; auto. + - apply Int63.eqb_spec in H0; subst; + apply Int63.eqb_spec in H1; subst; auto. + - apply list_beq_spec in H. subst. + rewrite !Misc.afold_left_and. rewrite H. auto. + exact Int63.eqb_spec. + - apply list_beq_spec in H. subst. + rewrite !Misc.afold_left_or. rewrite H. auto. + exact Int63.eqb_spec. + - apply Int63.eqb_spec in H0. apply Int63.eqb_spec in H1. subst; auto. + - apply Int63.eqb_spec in H0. apply Int63.eqb_spec in H1. subst; auto. + - apply Int63.eqb_spec in H. apply Int63.eqb_spec in H1. apply Int63.eqb_spec in H2. subst; auto. +Qed. + +Lemma form_eqb_symm : + forall f1 f2, + is_true (form_eqb f1 f2) -> + is_true (form_eqb f2 f1). +Proof. + unfold is_true, form_eqb. intros. repeat destruct_match; try discriminate; auto; + repeat match goal with + | H: Int63.eqb _ _ = true |- _ => apply Int63.eqb_spec in H + | |- Int63.eqb _ _ = true => apply Int63.eqb_spec + | H: list_beq _ _ _ = true |- _ => apply list_beq_spec in H; [|exact Int63.eqb_spec] + | |- list_beq _ _ _ = true => apply list_beq_spec; [exact Int63.eqb_spec|] + | H: _ && _ = true |- _ => simplify + | |- _ && _ = true => apply andb_true_intro; split + end; subst; auto. +Qed. + +Lemma t_interp_check_form : (* First array might be shorter, but it's ok *) + forall a ba f1 f2 l, + is_true (check_array form_eqb f1 f2) -> + is_true (check_local_form l f1) -> + forall i, + to_Z i < to_Z (PArray.length f1) -> + PArray.get (t_interp a ba f1) i = PArray.get (t_interp a ba f2) i. +Proof. + intros * TRUE CHK. + pose proof (check_array_length _ _ _ _ TRUE) as BOUNDS. + pose proof (length_t_interp a ba f1) as Y. + pose proof (length_t_interp a ba f2) as Z. + revert Y. + unfold t_interp. + apply Misc.foldi_ind with (P := + fun iter fol => + PArray.length fol = PArray.length f1 -> + forall i, + to_Z i < to_Z iter -> + PArray.get fol i = PArray.get _ i + ); intros. + + apply Misc.leb_0. + + pose proof (not_int63_lt_0 i). replace (to_Z 0) with 0 in H0 by auto. lia. + + rewrite PArray.length_set in H2. specialize (H1 H2). + erewrite Misc.to_Z_add_1 in H3 by eassumption. + destruct (int_dec i i0); subst. + - rewrite PArray.get_set_same by (now rewrite H2). + revert H1. revert Z. unfold t_interp. + assert (W: to_Z i0 < to_Z (PArray.length f2)). + { apply Int63.ltb_spec in H0. lia. } revert W. + apply Misc.foldi_ind with (P := + fun iter fol => + to_Z i0 < to_Z iter -> + PArray.length fol = PArray.length f2 -> + (forall i, to_Z i < to_Z i0 -> + PArray.get a0 i = PArray.get fol i) -> + _ = PArray.get fol i0 + ); intros. + * apply Misc.leb_0. + * pose proof (not_int63_lt_0 i0). replace (to_Z 0) with 0 in H1 by auto. lia. + * rewrite PArray.length_set in H7. erewrite Misc.to_Z_add_1 in H6 by eassumption. + destruct (int_dec i0 i); subst. rewrite PArray.get_set_same by (now rewrite H7). + rewrite lt_form_interp_form_aux with (f2 := PArray.get a1) (i := i). + erewrite interp_aux_correct; auto. + eapply check_local_form_spec; eauto. + apply form_eqb_symm. eapply check_array_correct; eauto. + apply Int63.ltb_spec in H0. auto. + intros. rewrite H8. rewrite PArray.get_set_other; auto. + unfold not; intros; subst. apply Int63.ltb_spec in H9. lia. + apply Int63.ltb_spec in H9; auto. + unfold check_local_form, is_true in *. simplify. + unfold check_form in *. simplify. unfold wf in *. + eapply Misc.aforallbi_spec in H12; eauto. + rewrite PArray.get_set_other by auto. eapply H5; auto. + assert (to_Z i <> to_Z i0) by (unfold not; intros; apply n; now apply to_Z_inj). + lia. intros. rewrite H8; auto. rewrite PArray.get_set_other. auto. + unfold not; intros. subst. lia. + - rewrite PArray.get_set_other by auto. eapply H1. + assert (to_Z i <> to_Z i0) by (unfold not; intros; apply n; now apply to_Z_inj). + lia. +Qed. + +(* Lemma a_interp_check_form : *) +(* forall t_i (t_func: PArray.array (tval t_i)) a ba a1 a2, *) +(* is_true (check_array Atom.eqb a1 a2) -> *) +(* is_true (check_array Bool.eqb (Atom.t_interp t_i t_func a1) (Atom.t_interp t_i t_func a2)). *) + +(* Misc.foldi_ind2: *) +(* forall (A B : Type) (P : Int63.int -> A -> B -> Prop) (f1 : Int63.int -> A -> A) *) +(* (f2 : Int63.int -> B -> B) (from to : Int63.int) (a1 : A) (a2 : B), *) +(* Int63.leb from to = true -> *) +(* P from a1 a2 -> *) +(* (forall (i : Int63.int) (a3 : A) (a4 : B), *) +(* Int63.leb from i = true -> Int63.ltb i to = true -> P i a3 a4 -> P (Int63.add i 1) (f1 i a3) (f2 i a4)) -> *) +(* P to (Misc.foldi f1 from to a1) (Misc.foldi f2 from to a2) *) + +Definition ind_S A a_init j (to: Int63.int) (fold1: PArray.array A) := + PArray.get fold1 j = PArray.get a_init j. + +Lemma ind_S_nochange : + forall a2 j from to a_init, + Int63.to_Z j < Int63.to_Z from <= Int63.to_Z to -> + ind_S _ a_init j to (Misc.foldi + (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) => + PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i))) from to a_init). +Proof. + intros. apply Misc.foldi_ind. apply Int63.leb_spec. lia. now unfold ind_S. + intros. unfold ind_S. rewrite PArray.get_set_other. + unfold ind_S in H2. auto. apply Int63.leb_spec in H0. + unfold not. intros. assert (Int63.to_Z i = Int63.to_Z j) by (now subst). + lia. +Qed. + +Lemma foldi_array_get_constant : + forall a2 j from to a_init, + Int63.to_Z j < Int63.to_Z from <= Int63.to_Z to -> + PArray.get (Misc.foldi + (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) => + PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i))) from to a_init) j = PArray.get a_init j. +Proof. apply ind_S_nochange; auto. Qed. + +Definition interp_ind_S t_i j (to: Int63.int) (fold1: PArray.array (bval t_i)) fold2 := + PArray.get fold1 j = PArray.get fold2 j. + +(* (Misc.foldi *) +(* (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) => *) +(* PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i))) (Int63.of_Z 0) *) +(* (PArray.length a2) (PArray.make (PArray.length a2) (interp_cop t_i CO_xH))) *) + +Lemma get_t_interp : + forall a1 a2 j, + is_true (Atom.wf a1) -> + is_true (check_array Atom.eqb a1 a2) -> + Int63.to_Z j < Int63.to_Z (PArray.length a1) -> + PArray.get (Atom.t_interp t_i t_func a1) j = + PArray.get (Atom.t_interp t_i t_func a2) j. +Proof. + intros * WF CHECK BOUNDS. unfold Atom.t_interp. + pose proof (check_array_length _ _ _ _ CHECK) as ABOUNDS. + pose proof (check_array_correct _ _ _ _ CHECK). + generalize dependent j. + assert (TMP: forall (A: Prop), + A /\ ((Int63.to_Z (PArray.length (Misc.foldi + (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) => + PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a1 i))) (Int63.of_Z 0) + (PArray.length a1) (PArray.make (PArray.length a1) (interp_cop t_i CO_xH))))) + = Int63.to_Z (PArray.length a1)) -> A) by tauto. apply TMP. clear TMP. + apply Misc.foldi_ind with + (P := fun iter fol => + (forall j, + Int63.to_Z j < Int63.to_Z iter -> + PArray.get fol j = + PArray.get + (Misc.foldi + (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) => + PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i))) + (Int63.of_Z 0) + (PArray.length a2) (PArray.make (PArray.length a2) (interp_cop t_i CO_xH))) j) /\ + Int63.to_Z (PArray.length fol) = Int63.to_Z (PArray.length a1) + ). + + apply Int63.leb_spec; simpl. + pose proof (not_int63_lt_0 (PArray.length a1)). + rewrite Int63.to_Z_0. auto. + + split. + + intros j BOUNDS0. pose proof (not_int63_lt_0 j). simpl in BOUNDS0. rewrite Int63.to_Z_0 in BOUNDS0. lia. + auto. + + intros i a ILEB ILTB [HIND ARRLEN]; split. + + intros j BOUNDS1. + erewrite Misc.to_Z_add_1 in BOUNDS1 by eassumption. + apply Int63.ltb_spec in ILTB. + apply Int63.leb_spec in ILEB. + assert (X: Int63.to_Z j < Int63.to_Z i \/ Int63.to_Z j = Int63.to_Z i) by lia. + inversion X as [X1|X1]. rewrite PArray.get_set_other. + rewrite HIND; auto; try lia. + unfold not; intro EQ. assert (Int63.to_Z j = Int63.to_Z i) by (now subst). lia. + assert (j = i) by (now apply Int63.to_Z_inj). subst. + rewrite PArray.get_set_same. 2: { apply Int63.ltb_spec. lia. } + generalize dependent HIND. + assert (X2: Int63.to_Z i < Int63.to_Z (PArray.length a2)) by lia. + generalize X2. + assert (TMP: forall (A: Prop), + A /\ ((Int63.to_Z (PArray.length (Misc.foldi + (fun (i0 : Int63.int) (t_a : PArray.array (bval t_i)) => + PArray.set t_a i0 (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i0))) + (Int63.of_Z 0) (PArray.length a2) (PArray.make (PArray.length a2) (interp_cop t_i CO_xH))))) + = Int63.to_Z (PArray.length a2)) -> A) by tauto. apply TMP. clear TMP. + apply Misc.foldi_ind with + (P := fun iter fol => + (Int63.to_Z i < Int63.to_Z iter -> + (forall j : Int63.int, + Int63.to_Z j < Int63.to_Z i -> + PArray.get a j = PArray.get fol j) -> + Atom.interp_aux t_i t_func (PArray.get a) (PArray.get a1 i) = PArray.get fol i) + /\ Int63.to_Z (PArray.length fol) = Int63.to_Z (PArray.length a2) + ). + + apply Int63.leb_spec. lia. + + split. intros BOUNDS2. + pose proof (not_int63_lt_0 i). lia. auto. + + intros i0 a0 ILEB1 ILTB1 HIND2. split. + intros BOUNDS3 HHIND. + erewrite Misc.to_Z_add_1 in BOUNDS3 by eassumption. + assert (A: Int63.to_Z i < Int63.to_Z i0 \/ Int63.to_Z i = Int63.to_Z i0) by lia. + inversion A as [A1|A1]; clear A; subst. + rewrite PArray.get_set_other. eapply HIND2. lia. + intros j BOUNDS4. rewrite HHIND. rewrite PArray.get_set_other; auto. + unfold not; intros EQ. assert (U: Int63.to_Z j = Int63.to_Z i0) by (now subst). lia. lia. + unfold not; intros EQ. assert (U: Int63.to_Z i = Int63.to_Z i0) by (now subst). lia. + assert (U: i = i0) by (now apply Int63.to_Z_inj). subst. + rewrite PArray.get_set_same by (apply Int63.ltb_spec; lia). + assert (EQ: PArray.get a2 i0 = PArray.get a1 i0). + { apply Atom.eqb_spec. apply check_array_correct; auto. } + + rewrite EQ in *. + apply lt_interp_aux with (i := i0). intros j ILTB2. + rewrite HHIND. apply Int63.ltb_spec in ILTB2. rewrite PArray.get_set_other. + auto. unfold not; intros EQ1. assert (U: Int63.to_Z i0 = Int63.to_Z j) by (now subst). lia. + apply Int63.ltb_spec in ILTB2. + auto. + unfold Atom.wf in WF. eapply Misc.aforallbi_spec in WF. eassumption. + apply Int63.ltb_spec. lia. + rewrite PArray.length_set. lia. + rewrite PArray.length_set. lia. +Qed. + +Lemma interp_form_hatom_preserved : + forall a1 a2 x, + is_true (Atom.wf a1) -> + is_true (check_array Atom.eqb a1 a2) -> + Int63.to_Z x < Int63.to_Z (PArray.length a1) -> + interp_form_hatom t_i t_func a1 x = interp_form_hatom t_i t_func a2 x. +Proof. + unfold interp_form_hatom. unfold interp_hatom. intros. + erewrite get_t_interp; auto. +Qed. + +(* Definition F f2 := *) +(* (fun i fol => *) +(* (forall x, 0 <= Int63.to_Z x < Int63.to_Z i -> *) +(* PArray.get fol x *) +(* = PArray.get *) +(* (Misc.foldi *) +(* (fun (i : Int63.int) (t_b : PArray.array bool) => *) +(* PArray.set t_b i *) +(* (interp_aux (interp_form_hatom t_i t_func a1) *) +(* (interp_form_hatom_bv t_i t_func a1) *) +(* (PArray.get t_b) (PArray.get f2 i))) *) +(* (Int63.of_Z 0) (PArray.length f2) *) +(* (PArray.make (PArray.length f2) true)) x)). *) + +Definition form_atom f P := + forall i a, PArray.get f i = Fatom a -> P a. + +Definition single_form_atom f P := + forall a, f = Fatom a -> P a. + +Lemma lt_form_interp_single_form_atom : + forall a1 a2 b f h, + single_form_atom h (fun j => a1 j = a2 j) -> + interp_aux a1 b f h = interp_aux a2 b f h. +Proof. + destruct h;simpl;intros; trivial. auto. +Qed. + +Lemma lt_form_interp_not_bv : + forall b1 b2 a f h, + is_true (single_form_not_bv h) -> + interp_aux a b1 f h = interp_aux a b2 f h. +Proof. + destruct h;simpl;intros; trivial. discriminate. +Qed. + +Lemma check_single_form_not_bv : + forall f1 l x, + is_true (check_local_form l f1) -> + to_Z x < to_Z (PArray.length f1) -> + is_true (single_form_not_bv (PArray.get f1 x)). +Proof. + unfold check_local_form, is_true; simplify. + eapply Misc.aforallbi_spec in H2; [|apply Int63.ltb_spec; eassumption]. + crush. +Qed. + +Lemma is_true_lt_form : + forall a b f1 x, + to_Z a < to_Z b -> + is_true (lt_form a (PArray.get f1 x)) -> + is_true (lt_form b (PArray.get f1 x)). +Proof. + unfold is_true, lt_form; intros. destruct_match; auto. + - apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia. + - apply Misc.aforallbi_spec; intros. eapply Misc.aforallbi_spec in H0; eauto. + apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia. + - apply Misc.aforallbi_spec; intros. eapply Misc.aforallbi_spec in H0; eauto. + apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia. + - apply Misc.aforallbi_spec; intros. eapply Misc.aforallbi_spec in H0; eauto. + apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia. + - simplify. apply Int63.ltb_spec in H1. apply Int63.ltb_spec in H2. + apply andb_true_intro. split; apply Int63.ltb_spec; lia. + - simplify. apply Int63.ltb_spec in H1. apply Int63.ltb_spec in H2. + apply andb_true_intro. split; apply Int63.ltb_spec; lia. + - simplify. apply Int63.ltb_spec in H2. apply Int63.ltb_spec in H3. + apply Int63.ltb_spec in H0. + apply andb_true_intro; split; [apply andb_true_intro;split|]; + apply Int63.ltb_spec; lia. + - apply forallb_forall; intros. eapply forallb_forall in H0; try eassumption. + apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia. +Qed. + +Lemma get_t_interp_form : + forall a1 a2 f1, + is_true (check_array Atom.eqb a1 a2) -> + is_true (check_local_form (PArray.length a1) f1) -> + is_true (Atom.wf a1) -> + forall x, + Int63.to_Z x < Int63.to_Z (PArray.length f1) -> + (PArray.get (t_interp (interp_form_hatom t_i t_func a2) (interp_form_hatom_bv t_i t_func a2) f1) x + = PArray.get (t_interp (interp_form_hatom t_i t_func a1) (interp_form_hatom_bv t_i t_func a1) f1) x). +Proof. + intros * TRUE LOCAL WFA. + pose proof (length_t_interp (interp_form_hatom t_i t_func a1) + (interp_form_hatom_bv t_i t_func a1) f1) as Y1. + pose proof (length_t_interp (interp_form_hatom t_i t_func a2) + (interp_form_hatom_bv t_i t_func a2) f1) as Y2. + revert Y1. revert Y2. + unfold t_interp. + apply Misc.foldi_ind2 with (P := + fun i a b => + PArray.length a = PArray.length f1 -> + PArray.length b = PArray.length f1 -> + forall x, + to_Z x < to_Z (PArray.length f1) -> + PArray.get a x = PArray.get b x + ). + - apply Misc.leb_0. + - intros. now rewrite PArray.get_make. + - intros. rewrite PArray.length_set in H2. rewrite PArray.length_set in H3. + specialize (H1 H2 H3). + destruct (int_dec i x); subst. + + symmetry. rewrite !PArray.get_set_same + by (try rewrite H3 in *; try rewrite H2 in *; apply Int63.ltb_spec; lia); auto. + erewrite lt_form_interp_not_bv; [|eapply check_single_form_not_bv; eauto]. + erewrite lt_form_interp_single_form_atom. + 2: { unfold single_form_atom; intros. + rewrite interp_form_hatom_preserved with (a2 := a2). eauto. + auto. auto. apply check_local_form_spec in LOCAL; simplify. + eapply Int63.ltb_spec. eapply H7; eauto. } + erewrite lt_form_interp_form_aux. eauto. intros. symmetry. eapply H1; eauto. + apply Int63.ltb_spec in H5. eauto. + unfold is_true in LOCAL. unfold check_local_form in LOCAL. simplify. unfold check_form in H5. + simplify. unfold wf in H8. eapply Misc.aforallbi_spec in H8; eauto. + eapply is_true_lt_form; eauto. + + rewrite !PArray.get_set_other by auto; auto. +Qed. + +Lemma valid_same_corr : + forall r a1 a2 f1 f2, + ~ is_true (Euf_Checker.valid t_func a2 f2 r) -> + is_true (check_array Atom.eqb a1 a2) -> + is_true (check_array form_eqb f1 f2) -> + is_true (check_local_form (PArray.length a1) f1) -> + is_true (Atom.wf a1) -> + Forall (fun x => Int63.to_Z (State.Lit.blit x) < Int63.to_Z (PArray.length f1)) + (Misc.to_list r) -> + ~ is_true (Euf_Checker.valid t_func a1 f1 r). +Proof. + unfold is_true. intros * VAL CHKA CHKF LOCAL WFA LT. + unfold not in *. intros * VAL2; apply VAL. + unfold Euf_Checker.valid in *. rewrite Misc.afold_left_and in *. + rewrite forallb_forall in *; intros x IN. + pose proof IN as VAL3. + apply VAL2 in VAL3. + rewrite Forall_forall in LT. + pose proof IN as VAL4. + apply LT in VAL4. + unfold interp_state_var. + unfold State.Lit.interp. + unfold State.Var.interp. + pose proof CHKF as INTERP. + eapply t_interp_check_form in INTERP; eauto. + rewrite <- INTERP. + now rewrite get_t_interp_form with (a1 := a1). +Qed. + +End PROOF. + +Lemma restrict_a : + forall p a a', + (forall y, (y <= max_hash_pred p)%positive -> a ! y = a' ! y) -> + eval_hash_pred p a = eval_hash_pred p a'. +Proof. + induction p; crush. + - now rewrite H by lia. + - erewrite IHp1. erewrite IHp2. eauto. + intros. eapply H. lia. + intros. eapply H. lia. + - erewrite IHp1. erewrite IHp2. eauto. + intros. eapply H. lia. + intros. eapply H. lia. + - erewrite IHp1. erewrite IHp2. eauto. + intros. eapply H. lia. + intros. eapply H. lia. + - erewrite IHp. eauto. + intros. eapply H. lia. +Qed. + +Definition nuke_asgn p (a: PTree.t bool) := + PTree.fold (fun b i a => + if (i <=? max_hash_pred p)%positive then PTree.set i a b else b + ) a (PTree.empty bool). + +Lemma eval_hash_pred_ext: + forall m m': PTree.t bool, + (forall x : PTree.elt, m ! x = m' ! x) -> + forall p, + eval_hash_pred p m = eval_hash_pred p m'. +Proof. + intros. eapply restrict_a; eauto. +Qed. + +Lemma nuke_asgn_spec : + forall p a, + exists a', + eval_hash_pred p a = eval_hash_pred p a' + /\ (forall y, (max_hash_pred p < y)%positive -> a' ! y = None). +Proof. + intros. exists (nuke_asgn p a). + revert p. revert a. + split. + - eapply restrict_a; eauto. + intros. unfold nuke_asgn. + eapply PTree_Properties.fold_rec; eauto. + + intros. rewrite <- H0; auto. + + intros. + case_eq ((k <=? max_hash_pred p)%positive); intros. + * destruct (peq k y). + -- subst. rewrite ! PTree.gss; auto. + -- rewrite ! PTree.gso; auto. + * rewrite POrderedType.Positive_as_DT.leb_gt in H3. + assert (k <> y) by lia. + rewrite PTree.gso; auto. + - unfold nuke_asgn. + eapply PTree_Properties.fold_rec; eauto; intros. + + unfold PTree.empty. rewrite PTree.gleaf; auto. + + destruct_match. + * rewrite POrderedType.Positive_as_DT.leb_le in Heqb. + assert (k <> y) by lia. + rewrite PTree.gso; auto. + * eapply H1; eauto. +Qed. + +Lemma nuke_1 : + forall p a x, + ~ pred_In x p -> + eval_hash_pred p a = eval_hash_pred p (PTree.remove x a). +Proof. + induction p; crush. + - assert (a <> x) by (unfold not; intros; subst; apply H; constructor). + rewrite PTree.gro; auto. + - assert (~ pred_In x p1) by (unfold not; intros; apply H; apply pred_In_Pand1; auto). + assert (~ pred_In x p2) by (unfold not; intros; apply H; apply pred_In_Pand2; auto). + erewrite IHp1; [|eassumption]; erewrite IHp2; eauto. + - assert (~ pred_In x p1) by (unfold not; intros; apply H; apply pred_In_Por1; auto). + assert (~ pred_In x p2) by (unfold not; intros; apply H; apply pred_In_Por2; auto). + erewrite IHp1; [|eassumption]; erewrite IHp2; eauto. + - assert (~ pred_In x p1) by (unfold not; intros; apply H; apply pred_In_Pimp1; auto). + assert (~ pred_In x p2) by (unfold not; intros; apply H; apply pred_In_Pimp2; auto). + erewrite IHp1; [|eassumption]; erewrite IHp2; eauto. + - assert (~ pred_In x p) by (unfold not; intros; apply H; constructor; auto). + erewrite IHp; eauto. +Qed. + +Lemma check_atom_to_smt : + forall a p d forms atoms, + to_smt a p = Some (d, forms, atoms) -> + is_true (check_atom atoms). +Proof. + intros. unfold to_smt in *. repeat (destruct_match; try discriminate; []). + crush. +Qed. + +Lemma check_wt_extra_spec : + forall a, + is_true (check_atom a) -> + is_true (check_wt_extra a) -> + (forall i x l, PArray.get a i <> Anop x l) + /\ (forall i n l, PArray.get a i = Aapp n l -> l = nil). +Proof. + unfold check_wt_extra, is_true; intros. + split; intros. + - unfold not; intros. exploit PArray.get_not_default_lt. rewrite H1. + unfold check_atom in H. destruct (PArray.default a); try discriminate. + intros. eapply Misc.aforallbi_spec in H0; eauto. + rewrite H1 in H0. discriminate. + - unfold not; intros. exploit PArray.get_not_default_lt. rewrite H1. + unfold check_atom in H. destruct (PArray.default a); try discriminate. + intros. eapply Misc.aforallbi_spec in H0; eauto. + rewrite H1 in H0. destruct_match; crush. +Qed. + +Lemma pred_in_correct : + forall p c, + pred_in c p = true -> + pred_In c p. +Proof. + induction p; crush; subst. + - constructor. + - apply orb_prop in H. inv H; auto using pred_In_Pand1, pred_In_Pand2. + - apply orb_prop in H. inv H; auto using pred_In_Por1, pred_In_Por2. + - apply orb_prop in H. inv H; auto using pred_In_Pimp1, pred_In_Pimp2. + - constructor; auto. +Qed. + +Lemma pred_in_complete : + forall p c, + pred_In c p -> + pred_in c p = true. +Proof. + induction p; crush; subst; try solve [inv H]. + - inv H. apply Pos.eqb_refl. + - apply orb_true_intro. inv H; intuition. + - apply orb_true_intro. inv H; intuition. + - apply orb_true_intro. inv H; intuition. + - inv H. auto. +Qed. + +Lemma max_key_upd_asgn : + forall l a x, + Forall (fun y => Z.pos y < x) (map fst l) -> + (Z.pos (max_key a) < x) -> + (Z.pos (max_key (upd_asgn l a)) < x). +Proof. + induction l; crush. + inv H. destruct_match. eapply IHl; auto. + - assert (exists y, (PTree.set (fst a) b a0) ! (max_key (PTree.set (fst a) b a0)) = Some y). + { apply max_key_in. + destruct (PTree.bempty (PTree.set (fst a) b a0)) eqn:?; auto. + exfalso. apply PTree.bempty_correct with (x := (fst a)) in Heqb0. rewrite PTree.gss in Heqb0. discriminate. + } + simplify. destruct (peq (max_key (PTree.set (fst a) b a0)) (fst a)). + + lia. + + rewrite PTree.gso in H1; auto. + assert (forall x y, ~ y <= x -> x < y) by lia. + apply H; unfold not; intros. + assert (Z.pos (max_key a0) < Z.pos (max_key (PTree.set (fst a) b a0))) by lia. + pose proof (max_not_present _ (max_key (PTree.set (fst a) b a0)) a0). + rewrite H6 in H1 by lia. discriminate. + - eapply IHl; eauto. +Qed. + +Theorem valid_check_smt : + forall p a, + check_smt p = true -> eval_hash_pred p a = Some true. +Proof. + intros * CHK. unfold check_smt in CHK. repeat (destruct_match; try discriminate; []). + apply andb_prop in CHK; inversion CHK as [CHK1 H0]; clear CHK. + apply andb_prop in CHK1; inversion CHK1 as [CHK6 CHKROOT]; clear CHK1. + apply andb_prop in CHK6; inversion CHK6 as [CHK2 CHK_EXTRA]; clear CHK6. + apply andb_prop in CHK2; inversion CHK2 as [CHK3 H2]; clear CHK2. + apply andb_prop in CHK3; inversion CHK3 as [CHK4 H3]; clear CHK3. + apply andb_prop in CHK4; inversion CHK4 as [CHK5 H4]; clear CHK4. + apply andb_prop in CHK5; inversion CHK5 as [H H5]; clear CHK5. + apply andb_prop in CHKROOT; inversion CHKROOT as [CHKROOT2 P1LT]; clear CHKROOT. + apply andb_prop in CHKROOT2; inversion CHKROOT2 as [CHKROOT3 NOTPREDIN]; clear CHKROOT2. + simplify. destruct p0. + exploit nuke_asgn_spec. intros. inv H1. inv H6. rewrite H1. + assert (NOTPRED: ~ pred_In 1%positive p). + { unfold not; intros HH. apply pred_in_complete in HH. rewrite HH in NOTPREDIN. discriminate. } + erewrite nuke_1; eauto. + assert (ALLEQ: forall y, (max_hash_pred p < y)%positive -> (PTree.remove 1 x) ! y = None). + { intros. destruct (peq 1 y); subst. rewrite PTree.grs. auto. rewrite PTree.gro; auto. } + erewrite unnest_predicate_correct; try eassumption; try lia; [|intros; eapply ALLEQ; lia]. + pose proof (exists_asgn (upd_asgn (rev l) (PTree.remove 1 x))) as X. + assert (ASSUMP1: Z.pos (max_key (upd_asgn (rev l) (PTree.remove 1 x))) - 2 < wB - 1). + { assert (forall l a x, + Forall (fun y => Z.pos y < x) (map fst l) -> + (Z.pos (max_key a) < x) -> + (Z.pos (max_key (upd_asgn l a)) < x)). + { apply max_key_upd_asgn; auto. } + assert (Z.pos (max_key (upd_asgn (rev l) (PTree.remove 1 x))) < wB). + { assert (GTWB: Z.pos p1 < wB) by assumption. eapply H6. apply Forall_forall; intros. + apply map_in_some in H8. inv H8. + inv H9. destruct x1 in *. apply in_rev in H8. + apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto. + cbn [fst snd] in *. lia. + assert ((max_key (PTree.remove 1 x) <= max_hash_pred p)%positive). + { assert (~ (max_hash_pred p < max_key (PTree.remove 1 x))%positive -> (max_key (PTree.remove 1 x) <= max_hash_pred p)%positive) by lia. + apply H8. unfold not; intros. pose proof H9. apply ALLEQ in H9. + destruct (PTree.bempty (PTree.remove 1 x)) eqn:?. + - rewrite max_key_empty in * by auto. lia. + - exploit max_key_in; try eassumption. intros. inv H11. rewrite H12 in H9. discriminate. + } + assert (max_hash_pred p < p1)%positive. + { eapply unnest_predicate_lt_fresh in Heqp0. lia. } + lia. + } + lia. + } + assert (ASSUMP2: (forall (k : positive) (x0 : bool), + (upd_asgn (rev l) (PTree.remove 1 x)) ! k = Some x0 -> 0 <= Z.pos k - 2 < wB)). + { intros. pose proof H6 as XXX. apply max_key_correct in H6. + destruct (in_dec peq k (map fst l)). + { apply map_in_some in i. inv i. inv H8. destruct x1; cbn [fst] in *. + apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto. + cbn [fst] in *. lia. + } + { assert (~ In k (map fst (rev l))). + { unfold not; intros; apply n. rewrite map_rev in H8. apply in_rev in H8. auto. } + rewrite upd_asgn_not_in in XXX by auto. + assert (k = 1%positive \/ (1 < k)%positive) by lia. inv H9. rewrite PTree.grs in XXX. discriminate. + lia. + } + } + assert (X2 := X). clear X. + pose proof (X2 ASSUMP1 ASSUMP2) as X. + inversion X as [res ASGN]; clear X. + assert (ASSUMP3: forall (i : Int63.int) (x0 : nop) (l0 : list Int63.int), + PArray.get a5 i <> Anop x0 l0) by (eapply check_wt_extra_spec; eauto). + assert (ASSUMP4: forall (i n : Int63.int) (l0 : list Int63.int), + PArray.get a5 i = Aapp n l0 -> l0 = nil) by (eapply check_wt_extra_spec; eauto). + eapply wt_correct in H2; try eassumption. + pose proof (Checker_Ext.checker_ext_correct _ _ _ _ _ H0) as X. + assert (XX: is_true (Atom.wf a0)) by + (apply check_atom_to_smt in Heqo; unfold check_atom in *; + destruct (PArray.default a0); try discriminate; + destruct c0; crush). + eapply valid_same_corr in X; try eassumption. + eapply valid_to_smt; try eassumption. + simpl. eapply fold_left_Pand_rev. + rewrite to_equiv_rev. eapply eval_hash_pred_equiv_asgn; auto. + unfold equiv_list_wf, Sorted; split. + replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto. + eapply sorted_rev4. eapply unnest_predicate_sorted; eauto. + apply Forall_rev; eapply unnest_predicate_lt_in_list2; eauto; lia. + apply Forall_rev; apply Forall_forall; intros. eapply ALLEQ. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp0) as Y. eapply Forall_forall in Y; eauto. lia. + apply Forall_rev; apply Forall_forall; intros. simpl. + pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp0) as Y. eapply Forall_forall in Y; eauto. lia. + apply Forall_forall; intros. unfold check_root_index in CHKROOT3. + eapply forallb_forall in CHKROOT3; eauto. + lia. +Qed. + +Lemma mutate_eval_correct : + forall p a, + eval_hash_pred (mutate1_p p) a = eval_hash_pred p a. +Proof. + unfold mutate1_p; intros. + repeat (destruct_match; crush). +Qed. + +Theorem valid_check_smt_total : + forall p a, + check_smt_total p = true -> eval_hash_pred p a = Some true. +Proof. + unfold check_smt_total; intros. + destruct_match; auto using valid_check_smt. + rewrite <- mutate_eval_correct. + destruct_match; auto using valid_check_smt. + discriminate. +Qed. |