diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 11:22:59 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 11:22:59 +0100 |
| commit | 5afebe369cea7f2746dec7c64514822562e9100e (patch) | |
| tree | f69f28af83fee03013ebfa41be43eb78f9435381 /riscV/ExtValues.v | |
| parent | 5dfa2de0e1ba0acd36584983afefd9af1f5c2262 (diff) | |
| download | compcert-kvx-5afebe369cea7f2746dec7c64514822562e9100e.tar.gz compcert-kvx-5afebe369cea7f2746dec7c64514822562e9100e.zip | |
begin synthesizing select
Diffstat (limited to 'riscV/ExtValues.v')
| -rw-r--r-- | riscV/ExtValues.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v index 81688ca6..3f283cdc 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -83,3 +83,21 @@ Proof. destruct (Int.eq i Int.one); trivial. destruct (Int.eq i Int.zero); trivial. Qed. + +Lemma select01_long_true: + forall vt vf, + select01_long Vtrue vt vf = vt. +Proof. + intros. unfold select01_long. cbn. + rewrite Int.eq_true. reflexivity. +Qed. + +Lemma select01_long_false: + forall vt vf, + select01_long Vfalse vt vf = vf. +Proof. + intros. unfold select01_long. cbn. + rewrite Int.eq_true. + rewrite Int.eq_false. reflexivity. + cbv. discriminate. +Qed. |