diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-25 17:53:22 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-25 17:53:22 +0100 |
| commit | e9f748f8e302f4d9977661e9c51ddaf5410bdec6 (patch) | |
| tree | 01c04d7e5770d4e927da40052f17eff48e7d8079 /src/hls/GiblePargenproofBackward.v | |
| parent | 9134c30e5c9a46299aacc94dd5664308bd554303 (diff) | |
| download | vericert-e9f748f8e302f4d9977661e9c51ddaf5410bdec6.tar.gz vericert-e9f748f8e302f4d9977661e9c51ddaf5410bdec6.zip | |
Finish mutual exclusivity check
Diffstat (limited to 'src/hls/GiblePargenproofBackward.v')
| -rw-r--r-- | src/hls/GiblePargenproofBackward.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 4b14234..43e97a6 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -361,7 +361,7 @@ Proof. exploit from_predicated_sem_pred_expr2. 3: eauto. { eauto. } - { unfold assert_ in Heqo. clear Heqo2. destr. now eapply check_mutexcl_correct. } + { unfold assert_ in Heqo. clear Heqo2. destr. eauto using check_mutexcl_correct. } { unfold assert_ in Heqo2. repeat destr. unfold sat_pred_simple in Heqo3. destruct (sat_pred_tseytin (¬ from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))))); [destruct s; discriminate|]. rewrite <- negb_involutive. symmetry. rewrite <- negb_involutive. rewrite <- eval_predf_negate. f_equal. eauto. @@ -406,7 +406,7 @@ Proof. exploit from_predicated_sem_pred_expr2. 3: eauto. { eauto. } - { unfold assert_ in Heqo. clear Heqo2. destr. now apply check_mutexcl_correct. } + { unfold assert_ in Heqo. clear Heqo2. destr. eauto using check_mutexcl_correct. } { unfold assert_ in Heqo2. repeat destr. unfold sat_pred_simple in Heqo3. destruct (sat_pred_tseytin (¬ from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))))); [destruct s; discriminate|]. rewrite <- negb_involutive. symmetry. rewrite <- negb_involutive. rewrite <- eval_predf_negate. f_equal. eauto. |