diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-02-11 20:43:58 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-02-11 20:43:58 +0000 |
| commit | e5db7d1259c32a886182c21201e6db3d567e7f96 (patch) | |
| tree | 0a0ded5ced2364f89b9af716a5259d6ee92f280b /src/hls/Abstr.v | |
| parent | 304762a8405d0e8f2edc3d0d9caaf063bddbb0ca (diff) | |
| download | vericert-e5db7d1259c32a886182c21201e6db3d567e7f96.tar.gz vericert-e5db7d1259c32a886182c21201e6db3d567e7f96.zip | |
Change evaluation of predicates and remove forest_evaluable
Diffstat (limited to 'src/hls/Abstr.v')
| -rw-r--r-- | src/hls/Abstr.v | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 410271f..ec45007 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -311,34 +311,38 @@ Inductive sem_pexpr (c: ctx) : pred_pexpr -> bool -> Prop := | sem_pexpr_Plit : forall p (b: bool) bres, sem_pred c p (if b then bres else negb bres) -> sem_pexpr c (Plit (b, p)) bres -| sem_pexpr_Pand_first : forall p1 p2, - sem_pexpr c p1 false -> +| sem_pexpr_Pand_false : forall p1 p2, + sem_pexpr c p1 false \/ sem_pexpr c p2 false -> sem_pexpr c (Pand p1 p2) false -| sem_pexpr_Pand_second : forall p1 p2 b, - sem_pexpr c p1 true -> - sem_pexpr c p2 b -> - sem_pexpr c (Pand p1 p2) b -| sem_pexpr_Por_first : forall p1 p2, +| sem_pexpr_Pand_true : forall p1 p2, sem_pexpr c p1 true -> + sem_pexpr c p2 true -> + sem_pexpr c (Pand p1 p2) true +| sem_pexpr_Por_true : forall p1 p2, + sem_pexpr c p1 true \/ sem_pexpr c p2 true -> sem_pexpr c (Por p1 p2) true -| sem_pexpr_Por_second : forall p1 p2 b, +| sem_pexpr_Por_false : forall p1 p2, sem_pexpr c p1 false -> - sem_pexpr c p2 b -> - sem_pexpr c (Por p1 p2) b. + sem_pexpr c p2 false -> + sem_pexpr c (Por p1 p2) false. Lemma sem_pexpr_Pand : forall ctx p1 p2 a b, sem_pexpr ctx p1 a -> sem_pexpr ctx p2 b -> sem_pexpr ctx (p1 ∧ p2) (a && b). -Proof. intros. destruct a; constructor; auto. Qed. +Proof. + intros. destruct a; cbn; try destruct b; solve [constructor; auto]. +Qed. Lemma sem_pexpr_Por : forall ctx p1 p2 a b, sem_pexpr ctx p1 a -> sem_pexpr ctx p2 b -> sem_pexpr ctx (p1 ∨ p2) (a || b). -Proof. intros. destruct a; constructor; auto. Qed. +Proof. + intros. destruct a; cbn; try destruct b; try solve [constructor; auto]. +Qed. (*| ``from_pred_op`` translates a ``pred_op`` into a ``pred_pexpr``. The main |