From 996f75a7526591f89160b2df1d52cd5075696618 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 2 Jun 2023 15:48:06 +0100 Subject: Finished the propert version of from_predicated_sem_pred_expr2 --- src/hls/AbstrSemIdent.v | 122 +++++++++++++++++++++++++------- src/hls/GiblePargen.v | 13 +++- src/hls/GiblePargenproofBackward.v | 21 +++++- src/hls/GiblePargenproofCommon.v | 141 ++++++++++++++++++++++++++++++++++++- src/hls/GiblePargenproofEquiv.v | 18 +++++ src/hls/GiblePargenproofForward.v | 33 +++++---- 6 files changed, 304 insertions(+), 44 deletions(-) (limited to 'src/hls') diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index fdd7dcb..5ec9200 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -1065,16 +1065,14 @@ Proof. eapply H3; eauto. * constructor; eauto. constructor. left. replace true with (negb false) by auto. now apply sem_pexpr_negate. - eapply IHpe; auto. eapply predicated_cons; eauto. + eauto using predicated_cons. + intros * HPREDS **; cbn in *; unfold "→"; repeat destr. inv Heqp. inv H0. * constructor. left. constructor. replace false with (negb true) by auto. now apply sem_pexpr_negate. constructor; auto. - * constructor. right. - eapply IHpe; eauto. - eapply predicated_cons; eauto. + * constructor. right. eauto using predicated_cons. Qed. -Lemma from_predicated_sem_pred_expr2: +Lemma from_predicated_sem_pred_expr2': forall preds ps pe b b', (forall x, sem_pexpr ctx (get_forest_p' x preds) (ps !! x)) -> predicated_mutexcl pe -> @@ -1095,29 +1093,105 @@ Proof. * eapply sem_pred_det; eauto. reflexivity. * replace false with (negb true) in H4 by auto. apply sem_pexpr_negate2 in H4. eapply sem_pexpr_det in H4; eauto; [discriminate|reflexivity]. - + inv H1. - * exploit from_predicated_sem_pred_expr_true. - instantiate (2 := pe). instantiate (1 := preds). - intros. - assert (NE.In x (NE.cons (p, p0) pe)) by (constructor; tauto). - inv H. - assert ((p, p0) <> x). - { unfold not; intros. subst. inv H4. contradiction. } - specialize (H3 _ _ ltac:(constructor; left; auto) H2 H). - destruct x; cbn in *. - eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H7; eauto. - apply negb_inj; cbn. - rewrite <- eval_predf_negate. - eapply H3; eauto. - intros. eapply sem_pexpr_det in H0; now try eapply H1. - * eapply IHpe; auto. eapply predicated_cons; eauto. - + inv H4. inv H2; inv H1. + + inv H1; eauto using predicated_cons. + exploit from_predicated_sem_pred_expr_true. + instantiate (2 := pe). instantiate (1 := preds). + intros. + assert (NE.In x (NE.cons (p, p0) pe)) by (constructor; tauto). + inv H. + assert ((p, p0) <> x). + { unfold not; intros. subst. inv H4. contradiction. } + specialize (H3 _ _ ltac:(constructor; left; auto) H2 H). + destruct x; cbn in *. + eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H7; eauto. + apply negb_inj; cbn. + rewrite <- eval_predf_negate. + eapply H3; eauto. + intros. eapply sem_pexpr_det in H0; now try eapply H1. + + inv H4. inv H2; inv H1; eauto using predicated_cons. * replace true with (negb false) in H0 by auto. apply sem_pexpr_negate2 in H0. eapply sem_pexpr_det in H0; now try apply H8. - * eapply IHpe; eauto. eapply predicated_cons; eauto. * inv H0. eapply sem_pred_det in H9; now eauto. - * eapply IHpe; eauto. eapply predicated_cons; eauto. +Qed. + +Lemma from_predicated_inv_exists_true : + forall ps pe, + eval_predf ps (from_predicated_inv pe) = true -> + exists y, NE.In y pe /\ (eval_predf ps (fst y) = true). +Proof. + induction pe; cbn -[eval_predf]; intros; repeat destr; inv Heqp. + - exists (p, p0); intuition constructor. + - rewrite eval_predf_Por in H. apply orb_prop in H. inv H. + + exists (p, p0); intuition constructor; tauto. + + exploit IHpe; auto; simplify. + exists x; intuition constructor; tauto. +Qed. + +Lemma from_predicated_sem_pred_expr2: + forall preds ps pe b, + (forall x, sem_pexpr ctx (get_forest_p' x preds) (ps !! x)) -> + predicated_mutexcl pe -> + sem_pexpr ctx (from_predicated true preds pe) b -> + eval_predf ps (from_predicated_inv pe) = true -> + sem_pred_expr preds sem_pred ctx pe b. +Proof. + induction pe. + - cbn -[eval_predf]; intros; repeat destr. inv Heqp. inv H1. inv H6. + + replace true with (negb false) in H1 by auto. + apply sem_pexpr_negate2 in H1. + eapply sem_pexpr_eval_inv in H1; eauto. + now rewrite H1 in H2. + + inv H1. constructor; auto. eapply sem_pexpr_eval; eauto. + + inv H7. constructor; auto. eapply sem_pexpr_eval; eauto. + - cbn -[eval_predf]; intros; repeat destr. inv Heqp. + rewrite eval_predf_Por in H2. apply orb_prop in H2. inv H2. + + inv H1. inv H6. + * inv H1. inv H6. constructor; eauto using sem_pexpr_eval. + * (* contradiction, because eval_predf p true means that all other + implications in H1 are false, therefore sem_pexpr will evaluate to + true. *) + exploit from_predicated_sem_pred_expr_true. + -- instantiate (2 := pe). instantiate (1 := preds). + intros. destruct x. + assert (HIN1: NE.In (p, p0) (NE.cons (p, p0) pe)) + by (intuition constructor; tauto). + assert (HIN2: NE.In (p1, p2) (NE.cons (p, p0) pe)) + by (intuition constructor; tauto). + assert (HNEQ: (p, p0) <> (p1, p2)). + { unfold not; inversion 1; subst. clear H4. inv H0. inv H5. contradiction. } + cbn. eapply sem_pexpr_eval; eauto. + symmetry. rewrite <- negb_involutive. symmetry. + rewrite <- eval_predf_negate. rewrite <- negb_involutive. + f_equal; cbn. + inv H0. specialize (H4 _ _ HIN1 HIN2 HNEQ). cbn in H4. + eapply H4; auto. + -- intros. eapply sem_pexpr_det in H1; now eauto. + * inv H5. inv H2. + -- eapply sem_pexpr_negate2' in H1. eapply sem_pexpr_eval_inv in H; eauto. + now rewrite H in H3. + -- inv H1. constructor; eauto using sem_pexpr_eval. + + assert (eval_predf ps p = false). + { case_eq (eval_predf ps p); auto; intros HCASE; exfalso. + exploit from_predicated_inv_exists_true; eauto; simplify. + destruct x; cbn -[eval_predf] in *. + assert (HNEQ: (p, p0) <> (p1, p2)). + { unfold not; intros. inv H4. inv H0. inv H6. contradiction. } + assert (HIN2: NE.In (p1, p2) (NE.cons (p, p0) pe)) + by (intuition constructor; tauto). + assert (HIN1: NE.In (p, p0) (NE.cons (p, p0) pe)) + by (intuition constructor; tauto). + inv H0. specialize (H4 _ _ HIN1 HIN2 HNEQ). eapply H4 in HCASE. cbn in HCASE. + rewrite negate_correct in HCASE. now setoid_rewrite H5 in HCASE. + } + inv H1. inv H7. + * inv H1. + apply sem_pexpr_negate2' in H6. eapply sem_pexpr_eval_inv in H6; eauto. + now rewrite H2 in H6. + * eapply sem_pred_expr_cons_false; + eauto using sem_pexpr_eval, predicated_cons. + * inv H6. inv H4; eapply sem_pred_expr_cons_false; + eauto using sem_pexpr_eval, predicated_cons. Qed. End PROOF. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 91b0450..c1c5fdb 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -193,6 +193,12 @@ Fixpoint from_predicated (b: bool) (f: PTree.t pred_pexpr) (a: predicated pred_e (from_predicated b f r) end. +Fixpoint from_predicated_inv (a: predicated pred_expression): pred_op := + match a with + | NE.singleton (p, e) => p + | (p, e) ::| r => Por p (from_predicated_inv r) + end. + #[local] Open Scope monad_scope. Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) := @@ -262,12 +268,15 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest (merge (list_translation rl f))) (f #r Mem))); Some (pred, f #r Mem <- pruned) | RBsetpred p' c args p => + let predicated := seq_app + (pred_ret (PEsetpred c)) + (merge (list_translation args f)) in let new_pred := (from_pred_op f.(forest_preds) (dfltp p' ∧ pred) - → from_predicated true f.(forest_preds) (seq_app (pred_ret (PEsetpred c)) - (merge (list_translation args f)))) + → from_predicated true f.(forest_preds) predicated) ∧ (from_pred_op f.(forest_preds) (¬ (dfltp p') ∨ ¬ pred) → (f #p p)) in + do _ <- assert_ (check_mutexcl predicated); do _ <- assert_ (predicated_not_in_forest p f); do _ <- assert_ (is_initial_pred_and_notin f p pred); Some (pred, f #p p <- new_pred) diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 5a18efe..676c96d 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -93,10 +93,25 @@ Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list | RBexit p c => lst end. +Definition remember_expr_p (f : forest) (lst: list (option pred_op * predicated pred_expression)) (i : instr): + list (option pred_op * predicated pred_expression) := + match i with + | RBnop => lst + | RBop p op rl r => lst + | RBload p chunk addr rl r => lst + | RBstore p chunk addr rl r => lst + | RBsetpred p' c args p => (p', seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) :: lst + | RBexit p c => lst + end. + Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) := let '(p, f, l, lm) := s in Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i). +Definition update'' (s: pred_op * forest * list pred_expr * list pred_expr * list (option pred_op * predicated pred_expression)) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr * list (option pred_op * predicated pred_expression)) := + let '(p, f, l, lm, lp) := s in + Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i, remember_expr_p f lp i)) (update (p, f) i). + Lemma equiv_update: forall i p f l lm p' f' l' lm', mfold_left update' i (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -357,14 +372,16 @@ Proof. assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) by now inv H0. inversion_clear HPRED' as [? ? ? HPRED]. - destruct ti as [is_trs is_tps is_tm]. destr. inv H4. inv H1. + destruct ti as [is_trs is_tps is_tm]. do 2 destr. inv H4. inv H1. pose proof H as YH. specialize (YH src). rewrite forest_pred_gss in YH. inv YH; try inv H3. + inv H1. inv H6. replace false with (negb true) in H4 by auto. replace false with (negb true) in H8 by auto. eapply sem_pexpr_negate2 in H4. eapply sem_pexpr_negate2 in H8. destruct i. - exploit from_predicated_sem_pred_expr2; eauto; intros. + exploit from_predicated_sem_pred_expr2. + 3: { eauto. } + 3: { } exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify. inv H3. inv H15. clear H13. exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H3. diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 2dbdf12..0a09c23 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -233,11 +233,148 @@ Proof. - intros. cbn in H. eapply andb_prop in H. inv H. eapply IHa in H0. unfold predicated_not_inP in *; intros. inv H. inv H3; cbn in *; eauto. unfold not; intros. eapply predin_PredIn in H. now rewrite H in H1. -Qed. - +Qed. Lemma truthy_dec: forall ps a, truthy ps a \/ falsy ps a. Proof. destruct a; try case_eq (eval_predf ps p); intuition (constructor; auto). Qed. + +Definition all_mutexcl (f: forest) : Prop := + forall x, predicated_mutexcl (f #r x). + +(* Lemma map_mutexcl' : *) +(* forall A B (x: predicated A) (f: (pred_op * A) -> (pred_op * B)), *) +(* predicated_mutexcl x -> *) +(* (forall a pop, fst (f (pop, a)) ⇒ pop) -> *) +(* (forall a b, f a = f b -> a = b) -> *) +(* predicated_mutexcl (NE.map f x). *) +(* Proof. *) +(* induction x; cbn; intros. *) +(* - cbn. repeat constructor; intros. inv H2. inv H3. contradiction. *) +(* - constructor. intros. *) +(* assert (exists x0', x0 = f x0') by admit. *) +(* assert (exists y', y = f y') by admit. *) +(* simplify. unfold "⇒" in *; intros. *) +(* destruct x2, x1. *) +(* eapply H0 in H5. *) +(* inv H. *) +(* specialize (H6 (p, a0) (p0, a1)). *) +(* assert ((fst (p, a0)) ⇒ ¬ (fst (p0, a1))) by admit. *) +(* unfold "⇒" in H; simplify. *) +(* apply H in H5. *) + +Lemma map_deep_simplify : + forall A x (eqd: forall a b: pred_op * A, {a = b} + {a <> b}), + predicated_mutexcl x -> + predicated_mutexcl + (GiblePargenproofEquiv.NE.map (fun x : Predicate.pred_op * A => (deep_simplify peq (fst x), snd x)) x). +Proof. + intros. inv H. + assert (forall x0 y : pred_op * A, + GiblePargenproofEquiv.NE.In x0 + (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) -> + GiblePargenproofEquiv.NE.In y + (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) -> + x0 <> y -> fst x0 ⇒ ¬ fst y). + { intros. exploit NE.In_map2. eapply H. simplify. + exploit NE.In_map2. eapply H2. simplify. + specialize (H0 _ _ H4 H5). + destruct (eqd x1 x0); subst; try contradiction. + apply H0 in n. + unfold "⇒" in *; intros. rewrite negate_correct. + rewrite deep_simplify_correct. rewrite <- negate_correct. apply n. + erewrite <- deep_simplify_correct; eassumption. } + constructor; auto. + generalize dependent x. induction x; crush; [constructor|]. + inv H1. + assert (forall x0 y, GiblePargenproofEquiv.NE.In x0 x -> GiblePargenproofEquiv.NE.In y x -> x0 <> y -> fst x0 ⇒ ¬ fst y). + { intros. eapply H0; auto; constructor; tauto. } + assert (forall x0 y : pred_op * A, + GiblePargenproofEquiv.NE.In x0 + (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) -> + GiblePargenproofEquiv.NE.In y + (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) -> + x0 <> y -> fst x0 ⇒ ¬ fst y). + { intros. eapply H; auto; constructor; tauto. } + constructor; eauto. + unfold not; intros. + Abort. + +Lemma prune_predicated_mutexcl : + forall A (x: predicated A) y, + predicated_mutexcl x -> + prune_predicated x = Some y -> + predicated_mutexcl y. +Proof. + unfold prune_predicated; intros. + Admitted. +#[local] Hint Resolve prune_predicated_mutexcl : mte. + +Lemma app_predicated_mutexcl : + forall A p (x: predicated A) y, + predicated_mutexcl x -> + predicated_mutexcl y -> + predicated_mutexcl (app_predicated p x y). +Proof. Admitted. +#[local] Hint Resolve app_predicated_mutexcl : mte. + +Lemma seq_app_predicated_mutexcl : + forall A B (f: predicated (A -> B)) y, + predicated_mutexcl f -> + predicated_mutexcl y -> + predicated_mutexcl (seq_app f y). +Proof. Admitted. +#[local] Hint Resolve seq_app_predicated_mutexcl : mte. + +Lemma all_predicated_mutexcl: + forall f l, + all_mutexcl f -> + predicated_mutexcl (merge (list_translation l f)). +Proof. Admitted. +#[local] Hint Resolve all_predicated_mutexcl : mte. + +Lemma flap2_predicated_mutexcl : + forall A B C (f: predicated (A -> B -> C)) x y, + predicated_mutexcl f -> + predicated_mutexcl (flap2 f x y). +Proof. Admitted. +#[local] Hint Resolve flap2_predicated_mutexcl : mte. + +Lemma all_mutexcl_set : + forall f n r, + all_mutexcl f -> + predicated_mutexcl n -> + all_mutexcl f #r r <- n. +Proof. + unfold all_mutexcl; intros. + destruct (resource_eq x r); subst. + { now rewrite forest_reg_gss. } + now rewrite forest_reg_gso by auto. +Qed. +#[local] Hint Resolve all_mutexcl_set : mte. + +Lemma pred_ret_mutexcl : + forall A (a: A), predicated_mutexcl (pred_ret a). +Proof. + unfold pred_ret. repeat constructor; intros. inv H. inv H0. contradiction. +Qed. +#[local] Hint Resolve pred_ret_mutexcl : mte. + +Lemma all_mutexcl_maintained : + forall f p p' f' i, + all_mutexcl f -> + update (p, f) i = Some (p', f') -> + all_mutexcl f'. +Proof. + destruct i; cbn -[seq_app]; intros; unfold Option.bind in *; repeat destr; inv H0. + - trivial. + - apply prune_predicated_mutexcl in Heqo1; auto with mte. + - apply prune_predicated_mutexcl in Heqo0; auto with mte. + - apply prune_predicated_mutexcl in Heqo0; auto with mte. + apply app_predicated_mutexcl; auto with mte. + - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto. + - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn. + fold (get_forest x f). auto. +Qed. diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index a1bfa0c..9e58981 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -890,6 +890,24 @@ Section SEM_PRED_EXEC. + destruct b; try discriminate. constructor; eauto. Qed. + Lemma sem_pexpr_negate2' : + forall p b, + sem_pexpr ctx (¬ p) b -> + sem_pexpr ctx p (negb b). + Proof. + intros. rewrite <- negb_involutive in H. + auto using sem_pexpr_negate2. + Qed. + + Lemma sem_pexpr_negate' : + forall p b, + sem_pexpr ctx p (negb b) -> + sem_pexpr ctx (¬ p) b. + Proof. + intros. rewrite <- negb_involutive. + auto using sem_pexpr_negate. + Qed. + Lemma sem_pexpr_evaluable : forall f_p ps, (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index d340477..3d0f7d5 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -374,6 +374,7 @@ all be evaluable. Lemma sem_update_Isetpred: forall A (ctx: @ctx A) f pr p0 c args b rs m, + predicated_mutexcl (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) -> valid_mem (ctx_mem ctx) m -> sem ctx f (mk_instr_state rs pr m, None) -> Op.eval_condition c rs ## args m = Some b -> @@ -381,7 +382,9 @@ all be evaluable. sem_pexpr ctx (from_predicated true (forest_preds f) (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f)))) b. Proof. - intros. eapply from_predicated_sem_pred_expr. + intros * HPREDMUT **. eapply from_predicated_sem_pred_expr. + { inv H0. inv H10. eassumption. } + { auto. } pose proof (sem_merge_list _ ctx f rs pr m args H0). apply sem_pred_expr_ident2 in H3; simplify. eapply sem_pred_expr_seq_app_val; [eauto| |]. @@ -402,7 +405,7 @@ all be evaluable. Proof. intros * EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED. pose proof SEM as SEM2. - inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. destr. + inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. repeat destr. inversion_clear PRUNE. rename Heqo into PRUNE. inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT]. @@ -413,11 +416,12 @@ all be evaluable. + constructor; intros. destruct (peq x pred); subst. * rewrite Regmap.gss. rewrite forest_pred_gss. - cbn [update] in *. unfold Option.bind in *. destr. destr. inv UPD. + cbn [update] in *. unfold Option.bind in *. repeat destr. inv UPD. replace b with (b && true) by eauto with bool. apply sem_pexpr_Pand. destruct b. constructor. right. eapply sem_update_Isetpred; eauto. + { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. } constructor. constructor. replace false with (negb true) by auto. apply sem_pexpr_negate. inv TRUTHY. constructor. cbn. eapply sem_pexpr_eval. inv PRED. eauto. auto. @@ -425,6 +429,7 @@ all be evaluable. apply sem_pexpr_negate. eapply sem_pexpr_eval. inv PRED. eauto. auto. eapply sem_update_Isetpred; eauto. + { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. } constructor. constructor. constructor. replace true with (negb false) by auto. apply sem_pexpr_negate. eapply sem_pexpr_eval. inv PRED. eauto. inv TRUTHY. auto. cbn -[eval_predf]. @@ -503,10 +508,10 @@ all be evaluable. eapply sem_pred_expr_app_predicated_false. inv H3. auto. inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto. * inv H3. auto. - - unfold Option.bind in *. destr. destr. inv H2. + - unfold Option.bind in *. repeat destr. inv H2. constructor. * constructor; intros. rewrite forest_pred_reg. apply sem_pred_not_in. - inv H3. inv H8. auto. apply pred_not_in_forestP. unfold assert_ in Heqo. now destr. + inv H3. inv H8. auto. apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr. * constructor. intros. destruct (peq x pred); subst. rewrite forest_pred_gss. replace (ps !! pred) with (true && ps !! pred) by auto. assert (sem_pexpr state0 (¬ (from_pred_op (forest_preds f) p0 ∧ from_pred_op (forest_preds f) p')) true). @@ -521,9 +526,9 @@ all be evaluable. } rewrite forest_pred_gso by auto. inv H3. inv H9. auto. * rewrite forest_pred_reg. apply sem_pred_not_in. inv H3. auto. - apply pred_not_in_forestP. unfold assert_ in Heqo. now destr. + apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr. * apply sem_pred_not_in. inv H3; auto. cbn. - apply pred_not_in_forest_exitP. unfold assert_ in Heqo. now destr. + apply pred_not_in_forest_exitP. unfold assert_ in Heqo0. now destr. - unfold Option.bind in *. destr. inv H2. inv H3. constructor. * constructor. inv H8. auto. * constructor. intros. inv H9. eauto. @@ -578,10 +583,10 @@ all be evaluable. eapply sem_pred_expr_app_predicated_false. inv H1. auto. inv H1. inv H8. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool. * inv H1. auto. - - unfold Option.bind in *. destr. destr. inv H0. split; [|solve [auto]]. + - unfold Option.bind in *. repeat destr. inv H0. split; [|solve [auto]]. constructor. * constructor; intros. rewrite forest_pred_reg. apply sem_pred_not_in. - inv H1. inv H7. auto. apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr. + inv H1. inv H7. auto. apply pred_not_in_forestP. unfold assert_ in Heqo1. now destr. * constructor. intros. destruct (peq x p0); subst. rewrite forest_pred_gss. replace (ps !! p0) with (true && ps !! p0) by auto. assert (sem_pexpr state0 (¬ (from_pred_op (forest_preds f) (dfltp o) ∧ from_pred_op (forest_preds f) p')) true). @@ -596,9 +601,9 @@ all be evaluable. } rewrite forest_pred_gso by auto. inv H1. inv H8. auto. * rewrite forest_pred_reg. apply sem_pred_not_in. inv H1. auto. - apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr. + apply pred_not_in_forestP. unfold assert_ in Heqo1. now destr. * apply sem_pred_not_in. inv H1; auto. cbn. - apply pred_not_in_forest_exitP. unfold assert_ in Heqo0. now destr. + apply pred_not_in_forest_exitP. unfold assert_ in Heqo1. now destr. - unfold Option.bind in *. destr. inv H0. inv H1. split. -- constructor. * constructor. inv H7. auto. @@ -742,9 +747,9 @@ all be evaluable. Proof. intros * UPD STEP EVAL. destruct instr; cbn [update] in UPD; try solve [unfold Option.bind in *; try destr; inv UPD; inv STEP; auto]. - - unfold Option.bind in *. destr. destr. inv UPD. inv STEP; auto. cbn [is_ps] in *. - unfold is_initial_pred_and_notin in Heqo1. unfold assert_ in Heqo1. destr. destr. - destr. destr. destr. destr. subst. assert (~ PredIn p2 next_p). + - unfold Option.bind in *. repeat destr. inv UPD. inv STEP; auto. cbn [is_ps] in *. + unfold is_initial_pred_and_notin in Heqo2. unfold assert_ in Heqo2. repeat destr. + subst. assert (~ PredIn p2 next_p). unfold not; intros. apply negb_true_iff in Heqb0. apply not_true_iff_false in Heqb0. apply Heqb0. now apply predin_PredIn. rewrite eval_predf_not_PredIn; auto. - unfold Option.bind in *. destr. inv UPD. inv STEP. inv H3. cbn. -- cgit