From 5afebe369cea7f2746dec7c64514822562e9100e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 2 Feb 2021 11:22:59 +0100 Subject: begin synthesizing select --- riscV/ExtValues.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'riscV/ExtValues.v') 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. -- cgit