diff options
| author | Brian Campbell | 2018-07-07 15:17:20 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-07 15:17:20 +0100 |
| commit | 2a2f38f46735a81a921891bf0bf9e35a7cc4a347 (patch) | |
| tree | 0d7a403c0e40efa40ad49eb0906fe06c3e33d0c0 /lib | |
| parent | 7c36a2c621ce64e3a181bf72f7b0434f42450092 (diff) | |
Coq: eq_range should take proofs
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 | ||||
| -rw-r--r-- | lib/flow.sail | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 990817e6..db0339d8 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1368,6 +1368,8 @@ Definition abs_with_eq n : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.ab (* Similarly, for ranges (currently in MIPS) *) +Definition eq_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : bool := + (projT1 l) =? (projT1 r). Definition add_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : {x & ArithFact (n+o <= x <= m+p)} := build_ex ((projT1 l) + (projT1 r)). diff --git a/lib/flow.sail b/lib/flow.sail index c4ffd75a..304f14bc 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -27,7 +27,7 @@ val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom(' 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_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : 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 val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool |