diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-02 15:48:06 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-02 15:48:06 +0100 |
| commit | 996f75a7526591f89160b2df1d52cd5075696618 (patch) | |
| tree | e9445a811275e88fe350d560b8a0bfab35cdc8d5 /src/hls/GiblePargenproofEquiv.v | |
| parent | 385ac7a100a202886784ceecc1fa6c4836958f0b (diff) | |
| download | vericert-996f75a7526591f89160b2df1d52cd5075696618.tar.gz vericert-996f75a7526591f89160b2df1d52cd5075696618.zip | |
Finished the propert version of from_predicated_sem_pred_expr2
Diffstat (limited to 'src/hls/GiblePargenproofEquiv.v')
| -rw-r--r-- | src/hls/GiblePargenproofEquiv.v | 18 |
1 files changed, 18 insertions, 0 deletions
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) -> |