Update lemmas with new update function

1 files changed, 128 insertions, 35 deletions

diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 68d14fa..2c677c3 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -1156,20 +1156,22 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       rewrite eval_predf_negate. rewrite H0. auto.
   Qed.
 
-(*  Lemma sem_update_instr :
-    forall f i' i'' a sp p i,
+  Lemma sem_update_instr :
+    forall f i' i'' a sp p i p' f',
       sem (mk_ctx i sp ge) f (i', None) ->
       step_instr ge sp (Iexec i') a (Iexec i'') ->
-      sem (mk_ctx i sp ge) (snd (update (p, f) a)) (i'', None).
+      update (Some (p, f)) a = Some (p', f') ->
+      sem (mk_ctx i sp ge) f' (i'', None).
   Proof. Admitted.
 
   Lemma sem_update_instr_term :
-    forall f i' i'' a sp i cf p p',
+    forall f i' i'' a sp i cf p p' p'' f',
       sem (mk_ctx i sp ge) f (i', None) ->
       step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) ->
-      sem (mk_ctx i sp ge) (snd (update (p', f) a)) (i'', Some cf)
-           /\ falsy (is_ps i'') (fst (update (p', f) a)).
-  Proof. Admitted.*)
+      update (Some (p', f)) a = Some (p'', f') ->
+      sem (mk_ctx i sp ge) f' (i'', Some cf)
+           /\ eval_apred (mk_ctx i sp ge) p'' false.
+  Proof. Admitted.
 
   Lemma step_instr_lessdef :
     forall sp a i i' ti,
@@ -1225,28 +1227,98 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     constructor. auto.
   Qed.
 
-(*  Lemma falsy_update :
-    forall f a ps,
-      falsy ps (fst f) ->
-      falsy ps (fst (update f a)).
+  (* Inductive is_predicate_expr: expression -> Prop := *)
+  (* | is_predicate_expr_Epredset : *)
+  (*   forall c a, is_predicate_expr (Esetpred c a) *)
+  (* | is_predicate_expr_Ebase : *)
+  (*   forall p, is_predicate_expr (Ebase (Pred p)). *)
+
+  (* Inductive apred_wf: apred_op -> Prop := *)
+  (* | apred_wf_Plit: forall b p, *)
+  (*     is_predicate_expr p -> *)
+  (*     apred_wf (Plit (b, p)) *)
+  (* | apred_wf_Ptrue: apred_wf Ptrue *)
+  (* | apred_wf_Pfalse: apred_wf Pfalse *)
+  (* | apred_wf_Pand: forall a b, *)
+  (*   apred_wf a -> apred_wf b -> apred_wf (a ∧ b) *)
+  (* | apred_wf_Por: forall a b, *)
+  (*   apred_wf a -> apred_wf b -> apred_wf (a ∨ b). *)
+
+  Lemma apred_and_false1 :
+    forall A ctx a b c,
+      @eval_apred A ctx a false ->
+      @eval_apred A ctx b c ->
+      eval_apred ctx (a ∧ b) false.
+  Proof.
+    intros.
+    replace false with (false && c) by auto.
+    constructor; auto.
+  Qed.
+
+  Lemma apred_and_false2 :
+    forall A ctx a b c,
+      @eval_apred A ctx a c ->
+      eval_apred ctx b false ->
+      eval_apred ctx (a ∧ b) false.
   Proof.
-    destruct f; destruct a; inversion 1; subst; crush.
-    rewrite <- H1. constructor. unfold Option.default. destruct o0.
-    rewrite eval_predf_Pand. rewrite H0. crush. crush.
+    intros.
+    replace false with (c && false) by eauto with bool.
+    constructor; auto.
   Qed.
 
+  #[local] Opaque simplify.
+
+  Lemma apred_simplify:
+    forall A ctx a b,
+      @eval_apred A ctx a b ->
+      @eval_apred A ctx (simplify a) b.
+  Proof. Admitted.
+
+  Lemma exists_get_pred_eval :
+    forall A ctx f p,
+    exists c, @eval_apred A ctx (get_pred' f p) c.
+  Proof.
+    induction p; crush; try solve [econstructor; constructor; eauto].
+    destruct_match. inv Heqp0. econstructor.
+    unfold apredicated_to_apred_op.
+    Admitted. (*probably not provable.*)
+
+  Lemma falsy_update :
+    forall A f a ctx p f',
+      @eval_apred A ctx (fst f) false ->
+      update (Some f) a = Some (p, f') ->
+      eval_apred ctx p false.
+  Proof.
+    destruct f; destruct a; inversion 1; subst; crush;
+    destruct_match; simplify; auto;
+    unfold Option.bind, Option.bind2 in *;
+    repeat (destruct_match; try discriminate; []); simplify; auto.
+    apply apred_simplify. eapply apred_and_false2; eauto. admit.
+    apply apred_simplify. eapply apred_and_false2; eauto. admit.
+    constructor; auto.
+    constructor; auto.
+    constructor; auto.
+    constructor; auto.
+    constructor; auto.
+    rewrite H2.
+    apply apred_simplify. eapply apred_and_false2; eauto. admit.
+    apply apred_simplify. eapply apred_and_false2; eauto. admit.
+    Unshelve. all: exact true.
+  Admitted.
+
   Lemma abstr_fold_falsy :
-    forall x i0 sp cf i f,
-    sem (mk_ctx i0 sp ge) (snd f) (i, cf) ->
-    falsy (is_ps i) (fst f) ->
-    sem (mk_ctx i0 sp ge) (snd (fold_left update x f)) (i, cf).
+    forall x i0 sp cf i f p p' f',
+    sem (mk_ctx i0 sp ge) f (i, cf) ->
+    eval_apred (mk_ctx i0 sp ge) p false ->
+    fold_left update x (Some (p, f)) =  Some (p', f') ->
+    sem (mk_ctx i0 sp ge) f' (i, cf).
   Proof.
     induction x; crush.
     eapply IHx.
     destruct a; destruct f; crush;
       try solve [eapply app_predicated_sem; eauto; apply combined_falsy; auto].
-    now apply falsy_update.
-  Qed.*)
+    (* now apply falsy_update. *)
+  (* Qed. *) Admitted.
 
   Lemma state_lessdef_sem :
     forall i sp f i' ti cf,
@@ -1255,25 +1327,43 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'.
   Proof. Admitted.
 
+  Lemma update_Some :
+    forall x n y,
+      fold_left update x n = Some y ->
+      exists n', n = Some n'.
+  Proof.
+    induction x; crush.
+    econstructor; eauto.
+    exploit IHx; eauto; simplify.
+    unfold update, Option.bind2, Option.bind in H1.
+    repeat (destruct_match; try discriminate); econstructor; eauto.
+  Qed.
+
+  #[local] Opaque update.
+
   Lemma abstr_fold_correct :
-    forall sp x i i' i'' cf f f',
+    forall sp x i i' i'' cf f p f',
       SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) ->
       sem (mk_ctx i sp ge) (snd f) (i', None) ->
-      fold_left update x (Some f) = Some f' ->
+      fold_left update x (Some f) = Some (p, f') ->
       forall ti,
         state_lessdef i ti ->
-        exists ti', sem (mk_ctx ti sp ge) (snd f') (ti', Some cf)
+        exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf)
                /\ state_lessdef i'' ti'.
   Proof.
     induction x; simplify; inv H.
-    (*- destruct f; exploit IHx; eauto; eapply sem_update_instr; eauto.
-    - destruct f. inversion H5; subst.
-      exploit state_lessdef_sem; eauto; intros. inv H. inv H2.
-      exploit step_instr_lessdef_term; eauto; intros. inv H2. inv H4.
-      exploit sem_update_instr_term; eauto; intros. inv H4.
-      eexists; split. eapply abstr_fold_falsy; eauto.
-      auto.
-  Qed.*) Admitted.
+    - destruct f. exploit update_Some; eauto; intros. simplify.
+      rewrite H3 in H1. destruct x0.
+      exploit IHx; eauto. eapply sem_update_instr; eauto.
+    - destruct f.
+      exploit state_lessdef_sem; eauto; intros. simplify.
+      exploit step_instr_lessdef_term; eauto; intros. simplify.
+      inv H6. exploit update_Some; eauto; simplify. destruct x2.
+      exploit sem_update_instr_term; eauto; simplify.
+      eexists; split.
+      eapply abstr_fold_falsy; eauto.
+      rewrite H6 in H1. eauto. auto.
+  Qed.
 
   Lemma sem_regset_empty :
     forall A ctx, @sem_regset A ctx empty (ctx_rs ctx).
@@ -1309,9 +1399,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
         exists ti', sem (mk_ctx ti sp ge) x' (ti', Some cf)
                /\ state_lessdef i'' ti'.
   Proof.
-    (*unfold abstract_sequence. intros; eapply abstr_fold_correct; eauto.
+    unfold abstract_sequence. intros. unfold Option.map in H0.
+    destruct_match; try easy.
+    destruct p; simplify.
+    eapply abstr_fold_correct; eauto.
     simplify. eapply sem_empty.
-  Qed.*) Admitted.
+  Qed.
 
   Lemma abstr_check_correct :
     forall sp i i' a b cf ti,
@@ -1339,7 +1432,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf)
              /\ state_lessdef i' ti'.
   Proof.
-    (*unfold schedule_oracle; intros. simplify.
+    unfold schedule_oracle; intros. repeat (destruct_match; try discriminate). simplify.
     exploit abstr_sequence_correct; eauto; simplify.
     exploit abstr_check_correct; eauto. apply state_lessdef_refl. simplify.
     exploit abstr_seq_reverse_correct; eauto. apply state_lessdef_refl. simplify.
@@ -1347,7 +1440,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     econstructor; split; eauto.
     etransitivity; eauto.
     etransitivity; eauto.
-  Qed.*) Admitted.
+  Qed.
 
   Lemma step_cf_correct :
     forall cf ts s s' t,