diff options
| author | Brian Campbell | 2018-06-21 12:00:49 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-22 15:26:32 +0100 |
| commit | b550177c4987f6d20500818a6d6d091bb09b0871 (patch) | |
| tree | dbbb62d8ab8f82a7ff4332cf638662c9243da50a /lib | |
| parent | 5184f151330d3b1a28c0fdfc5ccbcbe203e0b5be (diff) | |
Coq: project away range types in comparisons
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 9 | ||||
| -rw-r--r-- | lib/flow.sail | 16 |
2 files changed, 17 insertions, 8 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 23e7f486..7c70f88b 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -22,6 +22,15 @@ Defined. Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} := existT _ n H. +(* Project away range constraints in comparisons *) +Definition ltb_range_l {P} (l : sigT P) r := Z.ltb (projT1 l) r. +Definition leb_range_l {P} (l : sigT P) r := Z.leb (projT1 l) r. +Definition gtb_range_l {P} (l : sigT P) r := Z.gtb (projT1 l) r. +Definition geb_range_l {P} (l : sigT P) r := Z.geb (projT1 l) r. +Definition ltb_range_r {P} l (r : sigT P) := Z.ltb l (projT1 r). +Definition leb_range_r {P} l (r : sigT P) := Z.leb l (projT1 r). +Definition gtb_range_r {P} l (r : sigT P) := Z.gtb l (projT1 r). +Definition geb_range_r {P} l (r : sigT P) := Z.geb l (projT1 r). Definition ii := Z. Definition nn := nat. diff --git a/lib/flow.sail b/lib/flow.sail index b698b597..c4ffd75a 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -18,14 +18,14 @@ val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) - val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool -val lt_range_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val lteq_range_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val gt_range_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val gteq_range_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val lt_atom_range = {coq: "Z.ltb", _: "lt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val lteq_atom_range = {coq: "Z.leb", _: "lteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val gt_atom_range = {coq: "Z.gtb", _: "gt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val gteq_atom_range = {coq: "Z.geb", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val lt_range_atom = {coq: "ltb_range_l", _: "lt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val lteq_range_atom = {coq: "leb_range_l", _: "lteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val gt_range_atom = {coq: "gtb_range_l", _: "gt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val gteq_range_atom = {coq: "geb_range_l", _: "gteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val lt_atom_range = {coq: "ltb_range_r", _: "lt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val gt_atom_range = {coq: "gtb_range_r", _: "gt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool |