diff options
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 7 | ||||
| -rw-r--r-- | lib/coq/Sail2_state.v | 7 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 4 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 27 |
4 files changed, 36 insertions, 9 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index dfc7fc46..9f40e0df 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -567,7 +567,6 @@ Definition slice {m} (v : mword m) lo len `{ArithFact (0 <=? len)} : mword len : else zeros len else autocast (subrange_vec_dec v (lo + len - 1) lo). -(* Lemma slice_is_ok m (v : mword m) lo len (H1 : 0 <= lo) (H2 : 0 < len) (H3: lo + len < m) : slice v lo len = autocast (subrange_vec_dec v (lo + len - 1) lo). @@ -580,9 +579,9 @@ destruct (sumbool_of_bool _). + exfalso. unbool_comparisons. omega. - + f_equal. - f_equal. -*) + + repeat replace_ArithFact_proof. + reflexivity. +Qed. Import ListNotations. Definition count_leading_zeros {N : Z} (x : mword N) `{ArithFact (N >=? 1)} diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index 51a8e5fd..7c751bc7 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -30,15 +30,12 @@ Fixpoint foreachS {A RV Vars E} (xs : list A) (vars : Vars) (body : A -> Vars -> foreachS xs vars body end. -(* This uses the same subproof as the prompt version to get around proof relevance issues - in Sail2_state_lemmas. TODO: if we switch to boolean properties this shouldn't be - necessary. *) Fixpoint foreach_ZS_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <=? z <=? to)), Vars -> monadS rv Vars e) {struct n} : monadS rv Vars e. exact ( match sumbool_of_bool (from + off <=? to) with left LE => match n with | O => returnS vars - | S n => body (from + off) (foreach_ZM_up'_subproof _ _ _ _ _ _ LE) vars >>$= fun vars => foreach_ZS_up' rv e Vars from to step (off + step) n _ (foreach_ZM_up'_subproof0 _ _ _ _) vars body + | S n => body (from + off) _ vars >>$= fun vars => foreach_ZS_up' rv e Vars from to step (off + step) n _ _ vars body end | right _ => returnS vars end). @@ -49,7 +46,7 @@ exact ( match sumbool_of_bool (to <=? from + off) with left LE => match n with | O => returnS vars - | S n => body (from + off) (foreach_ZM_down'_subproof _ _ _ _ _ _ LE) vars >>$= fun vars => foreach_ZS_down' _ _ _ from to step (off - step) n _ (foreach_ZM_down'_subproof0 _ _ _ _) vars body + | S n => body (from + off) _ vars >>$= fun vars => foreach_ZS_down' _ _ _ from to step (off - step) n _ _ vars body end | right _ => returnS vars end). diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v index 39406208..5f409e22 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -730,6 +730,8 @@ induction (S (Z.abs_nat (from - to))); intros. reflexivity. * simpl. rewrite_liftState. + destruct (sumbool_of_bool (from + off <=? to)); auto. + repeat replace_ArithFact_proof. reflexivity. Qed. Hint Rewrite liftState_foreach_ZM_up : liftState. @@ -751,6 +753,8 @@ induction (S (Z.abs_nat (from - to))); intros. reflexivity. * simpl. rewrite_liftState. + destruct (sumbool_of_bool (to <=? from + off)); auto. + repeat replace_ArithFact_proof. reflexivity. Qed. Hint Rewrite liftState_foreach_ZM_down : liftState. diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 9e53e577..be27d255 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -38,6 +38,33 @@ unfold ArithFact in *. apply fact. Defined. +Lemma ArithFact_irrelevant (P : bool) (p q : ArithFact P) : p = q. +destruct p,q. +f_equal. +apply Eqdep_dec.UIP_dec. +apply Bool.bool_dec. +Qed. + +Ltac replace_ArithFact_proof := + match goal with |- context[?x] => + match tt with + | _ => is_var x; fail 1 + | _ => + match type of x with ArithFact ?P => + let pf := fresh "pf" in + generalize x as pf; intro pf; + repeat multimatch goal with |- context[?y] => + match type of y with ArithFact P => + match y with + | pf => idtac + | _ => rewrite <- (ArithFact_irrelevant P pf y) + end + end + end + end + end + end. + (* Allow setoid rewriting through ArithFact *) Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. |