From a47d709fd9251f58032444fde27a3ad7e947c26d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 2 Feb 2021 13:33:43 +0100 Subject: Pselectd --- riscV/SelectOpproof.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'riscV/SelectOpproof.v') diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 7f7474b6..c313fbaf 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -960,6 +960,25 @@ Proof. destruct b. * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption. * 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. } -- cgit