diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
| commit | f8bd8cde25321a3a4a3195bf9189416194b3732e (patch) | |
| tree | 7773d41eebb8ad6e26d545cc81ad51d24d2bd6a4 /src/hls/Abstr.v | |
| parent | c35404c110b7616b30eeb48fc4051dcb33d84f40 (diff) | |
| download | vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.tar.gz vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.zip | |
Clean up proofs
Diffstat (limited to 'src/hls/Abstr.v')
| -rw-r--r-- | src/hls/Abstr.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 07a9649..5ce7c0a 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1463,6 +1463,11 @@ Proof. rewrite RTree.gso; auto. Qed. +Lemma forest_reg_pred: + forall (f : forest) w dst dst', + (f #r dst <- w) #p dst' = f #p dst'. +Proof. auto. Qed. + Lemma forest_reg_gss: forall (f : forest) w dst, (f #r dst <- w) #r dst = w. @@ -1482,6 +1487,11 @@ Proof. rewrite PTree.gso; auto. Qed. +Lemma forest_pred_reg: + forall (f : forest) w dst dst', + (f #p dst <- w) #r dst' = f #r dst'. +Proof. auto. Qed. + Lemma forest_pred_gss: forall (f : forest) w dst, (f #p dst <- w) #p dst = w. |