diff options
Diffstat (limited to 'src/versions/standard/Int63/Int63Axioms_standard.v')
| -rw-r--r-- | src/versions/standard/Int63/Int63Axioms_standard.v | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v index 6bc1b3c..6a002ea 100644 --- a/src/versions/standard/Int63/Int63Axioms_standard.v +++ b/src/versions/standard/Int63/Int63Axioms_standard.v @@ -17,6 +17,7 @@ Require Import Bvector. Require Export BigNumPrelude. +Require Import Int63Lib. Require Export Int63Native. Require Export Int63Op. @@ -73,34 +74,34 @@ Axiom div_spec : forall x y, [|x / y|] = [|x|] / [|y|]. Axiom mod_spec : forall x y, [|x \% y|] = [|x|] mod [|y|]. (* Comparisons *) -Axiom eqb_refl : forall x, (x == x)%int63 = true. +Axiom eqb_refl : forall x, (x == x)%int = true. -Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> [|x|] < [|y|]. +Axiom ltb_spec : forall x y, (x < y)%int = true <-> [|x|] < [|y|]. -Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> [|x|] <= [|y|]. +Axiom leb_spec : forall x y, (x <= y)%int = true <-> [|x|] <= [|y|]. (** Iterators *) Axiom foldi_cont_gt : forall A B f from to cont, - (to < from)%int63 = true -> foldi_cont (A:=A) (B:=B) f from to cont = cont. + (to < from)%int = true -> foldi_cont (A:=A) (B:=B) f from to cont = cont. Axiom foldi_cont_eq : forall A B f from to cont, from = to -> foldi_cont (A:=A) (B:=B) f from to cont = f from cont. Axiom foldi_cont_lt : forall A B f from to cont, - (from < to)%int63 = true-> - foldi_cont (A:=A) (B:=B) f from to cont = - f from (fun a' => foldi_cont f (from+1) to cont a'). + (from < to)%int = true-> + foldi_cont (A:=A) (B:=B) f from to cont = + f from (fun a' => foldi_cont f (from + 1%int) to cont a'). Axiom foldi_down_cont_lt : forall A B f from downto cont, - (from < downto)%int63 = true -> foldi_down_cont (A:=A) (B:=B) f from downto cont = cont. + (from < downto)%int = true -> foldi_down_cont (A:=A) (B:=B) f from downto cont = cont. Axiom foldi_down_cont_eq : forall A B f from downto cont, from = downto -> foldi_down_cont (A:=A) (B:=B) f from downto cont = f from cont. Axiom foldi_down_cont_gt : forall A B f from downto cont, - (downto < from)%int63 = true-> - foldi_down_cont (A:=A) (B:=B) f from downto cont = + (downto < from)%int = true-> + foldi_down_cont (A:=A) (B:=B) f from downto cont = f from (fun a' => foldi_down_cont f (from-1) downto cont a'). (** Print *) @@ -117,11 +118,11 @@ Axiom head0_spec : forall x, 0 < [|x|] -> Axiom tail0_spec : forall x, 0 < [|x|] -> (exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]))%Z. -Axiom addc_def_spec : forall x y, (x +c y)%int63 = addc_def x y. +Axiom addc_def_spec : forall x y, (x +c y)%int = addc_def x y. Axiom addcarryc_def_spec : forall x y, addcarryc x y = addcarryc_def x y. -Axiom subc_def_spec : forall x y, (x -c y)%int63 = subc_def x y. +Axiom subc_def_spec : forall x y, (x -c y)%int = subc_def x y. Axiom subcarryc_def_spec : forall x y, subcarryc x y = subcarryc_def x y. |