diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-02-12 21:09:37 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-02-12 21:09:37 +0000 |
| commit | 5ac129169e5613eee1c9ee1e69ba34eb6ee69ee7 (patch) | |
| tree | dc64e62c8b24989fa64e2733c3d6a262cb2448c8 | |
| parent | 6452ba3029054ef26fc12cde7e05861bd58fdacb (diff) | |
| download | vericert-5ac129169e5613eee1c9ee1e69ba34eb6ee69ee7.tar.gz vericert-5ac129169e5613eee1c9ee1e69ba34eb6ee69ee7.zip | |
Finish eval_predf_update_true
| -rw-r--r-- | src/hls/GiblePargenproof.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 7667ac2..b85224f 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -2129,12 +2129,15 @@ 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. inv UPD. inv STEP; auto. cbn [is_ps] in *. admit. + - 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 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. rewrite eval_predf_simplify. rewrite eval_predf_Pand. rewrite eval_predf_negate. destruct i'; cbn in *. rewrite H0. auto. - Admitted. (* TODO: This only needs the addition of the property that any - setpreds will not contain the predicate in the name. *) + Qed. Lemma forest_evaluable_regset : forall A f (ctx: @ctx A) n x, |