diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-02-05 21:56:12 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-02-05 21:56:12 +0000 |
| commit | 304762a8405d0e8f2edc3d0d9caaf063bddbb0ca (patch) | |
| tree | 59eb9026b86268659298ad228d9478bb17340787 /src/hls/Abstr.v | |
| parent | a79914b49d81e6be31dd936b4c70a5a01ab498e2 (diff) | |
| download | vericert-304762a8405d0e8f2edc3d0d9caaf063bddbb0ca.tar.gz vericert-304762a8405d0e8f2edc3d0d9caaf063bddbb0ca.zip | |
Switch to half lazy evaluation
Diffstat (limited to 'src/hls/Abstr.v')
| -rw-r--r-- | src/hls/Abstr.v | 36 |
1 files changed, 28 insertions, 8 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index f67627d..410271f 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -311,14 +311,34 @@ 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 : forall p1 p2 b1 b2, - sem_pexpr c p1 b1 -> - sem_pexpr c p2 b2 -> - sem_pexpr c (Pand p1 p2) (b1 && b2) -| sem_pexpr_Por : forall p1 p2 b1 b2, - sem_pexpr c p1 b1 -> - sem_pexpr c p2 b2 -> - sem_pexpr c (Por p1 p2) (b1 || b2). +| sem_pexpr_Pand_first : forall p1 p2, + sem_pexpr c p1 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 c p1 true -> + sem_pexpr c (Por p1 p2) true +| sem_pexpr_Por_second : forall p1 p2 b, + sem_pexpr c p1 false -> + sem_pexpr c p2 b -> + sem_pexpr c (Por p1 p2) b. + +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. + +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. (*| ``from_pred_op`` translates a ``pred_op`` into a ``pred_pexpr``. The main |