diff options
Diffstat (limited to 'riscV/SelectOpproof.v')
-rw-r--r-- | riscV/SelectOpproof.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 7f7474b6..c313fbaf 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -962,6 +962,25 @@ Proof. * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption. - inv H. TrivialExists. + cbn. constructor. + { econstructor. + { constructor. + { econstructor. eassumption. cbn. rewrite H3. reflexivity. } + constructor. econstructor. constructor. eassumption. + constructor. cbn. reflexivity. + constructor. econstructor. constructor. eassumption. constructor. + cbn. reflexivity. constructor. + } + constructor. + } + constructor. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + destruct b. + * rewrite ExtValues.select01_long_true. + apply ExtValues.float_bits_normalize. + * rewrite ExtValues.select01_long_false. + apply ExtValues.float_bits_normalize. + - inv H. TrivialExists. + + cbn. constructor. { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. } constructor. eassumption. constructor. eassumption. constructor. + cbn. f_equal. rewrite ExtValues.normalize_select01. |