diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-07-11 15:45:59 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-07-11 16:25:09 +0100 |
commit | 93117b6e766c25c5aeecdc20a963d5114fb91e59 (patch) | |
tree | 60e77f4d09548b3fa077d96e7d0e26fd8b0ad1ef /src/hls/GiblePargenproofForward.v | |
parent | 6cdb6490437b9e609afbf5e8749b24d31c02fce1 (diff) | |
download | vericert-93117b6e766c25c5aeecdc20a963d5114fb91e59.tar.gz vericert-93117b6e766c25c5aeecdc20a963d5114fb91e59.zip |
Add equivalence classes
Diffstat (limited to 'src/hls/GiblePargenproofForward.v')
-rw-r--r-- | src/hls/GiblePargenproofForward.v | 99 |
1 files changed, 0 insertions, 99 deletions
diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 946a243..48fe922 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -273,105 +273,6 @@ all be evaluable. + auto. Qed. - Lemma sem_pexpr_not_in : - forall G (ctx: @ctx G) p0 ps p e b, - ~ PredIn p p0 -> - sem_pexpr ctx (from_pred_op ps p0) b -> - sem_pexpr ctx (from_pred_op (PTree.set p e ps) p0) b. - Proof. - induction p0; auto; intros. - - cbn. destruct p. unfold get_forest_p'. - assert (p0 <> p) by - (unfold not; intros; apply H; subst; constructor). - rewrite PTree.gso; auto. - - cbn in *. - assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by - (split; unfold not; intros; apply H; constructor; tauto). - inversion_clear X as [X1 X2]. - inv H0. inv H4. - specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto. - specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto. - constructor; auto. - - cbn in *. - assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by - (split; unfold not; intros; apply H; constructor; tauto). - inversion_clear X as [X1 X2]. - inv H0. inv H4. - specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto. - specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto. - constructor; auto. - Qed. - - Lemma sem_pred_not_in : - forall A B G (ctx: @ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l v p e ps, - sem_pred_expr ps s ctx l v -> - predicated_not_inP p l -> - sem_pred_expr (PTree.set p e ps) s ctx l v. - Proof. - induction l. - - intros. unfold predicated_not_inP in H0. - destruct a. constructor. apply sem_pexpr_not_in. - eapply H0. econstructor. inv H. auto. inv H. auto. - - intros. inv H. constructor. unfold predicated_not_inP in H0. - eapply sem_pexpr_not_in. eapply H0. constructor. left. eauto. - auto. auto. - apply sem_pred_expr_cons_false. apply sem_pexpr_not_in. eapply H0. - constructor. tauto. auto. auto. - eapply IHl. eauto. eapply predicated_not_inP_cons; eauto. - Qed. - - Lemma pred_fold_true' : - forall A l pred y, - fold_left (fun a (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true -> - y = true. - Proof. - induction l; crush. - exploit IHl; try eassumption; intros. - eapply andb_prop in H0; tauto. - Qed. - - Lemma pred_fold_true : - forall A pred l p y, - fold_left (fun (a : bool) (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true -> - y = true -> - list_norepet (map fst l) -> - In p l -> - predicated_not_in pred (snd p) = true. - Proof. - induction l; crush. - inv H1. inv H2. - - cbn in *. now eapply pred_fold_true' in H. - - cbn in *; eapply IHl; try eassumption. - eapply pred_fold_true'; eauto. - Qed. - - Lemma pred_not_in_forestP : - forall pred f, - predicated_not_in_forest pred f = true -> - forall x, predicated_not_inP pred (f #r x). - Proof. - unfold predicated_not_in_forest, predicated_not_in_pred_expr; intros. - destruct (RTree.get x (forest_regs f)) eqn:?. - - eapply andb_prop in H. inv H. rewrite PTree.fold_spec in H0. - unfold RTree.get in Heqo. - exploit pred_fold_true. eauto. auto. apply PTree.elements_keys_norepet. - apply PTree.elements_correct; eauto. - intros. eapply predicated_not_inP_equiv. unfold "#r". - unfold RTree.get. rewrite Heqo. auto. - - unfold "#r". rewrite Heqo. unfold predicated_not_inP; intros. - inv H0. inversion 1. - Qed. - - Lemma pred_not_in_forest_exitP : - forall pred f, - predicated_not_in_forest pred f = true -> - predicated_not_inP pred (forest_exit f). - Proof. - intros. - eapply predicated_not_inP_equiv. unfold predicated_not_in_forest in H. - eapply andb_prop in H; tauto. - Qed. - 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))) -> |