Library EVMOpSem.Lem.lem_num

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import coqharness.

Open Scope nat_scope.
Open Scope string_scope.

Require Import lem_bool.
Require Export lem_bool.
Require Import lem_basic_classes.
Require Export lem_basic_classes.

Require Import Coq.Numbers.BinNums.
Require Export Coq.Numbers.BinNums.
Require Import Coq.ZArith.BinInt.
Require Export Coq.ZArith.BinInt.
Require Import Coq.ZArith.Zpower.
Require Export Coq.ZArith.Zpower.
Require Import Coq.ZArith.Zdiv.
Require Export Coq.ZArith.Zdiv.
Require Import Coq.ZArith.Zmax.
Require Export Coq.ZArith.Zmax.
Require Import Coq.Reals.Rsqrt_def.
Require Export Coq.Reals.Rsqrt_def.
Require Import NArith.
Require Export NArith.

Require Import Coq.QArith.Qabs.
Require Export Coq.QArith.Qabs.
Require Import Coq.QArith.Qminmax.
Require Export Coq.QArith.Qminmax.
Require Import Coq.QArith.Qround.
Require Export Coq.QArith.Qround.
Require Import Coq.Reals.ROrderedType.
Require Export Coq.Reals.ROrderedType.
Require Import Coq.Reals.Rbase.
Require Export Coq.Reals.Rbase.
Require Import Coq.Reals.Rfunctions.
Require Export Coq.Reals.Rfunctions.




Class NumNegate (a: Type): Type := {
  numNegate: a ->a
}.
Notation " X '~' Y" := (numNegate X Y) (at level 70, no associativity).

Class NumAbs (a: Type): Type := {
  abs: a ->a
}.

Class NumAdd (a: Type): Type := {
  numAdd: a ->a ->a
}.
Notation " X '+' Y" := (numAdd X Y) (at level 50, left associativity).

Class NumMinus (a: Type): Type := {
  numMinus: a ->a ->a
}.
Notation " X '-' Y" := (numMinus X Y) (at level 50, left associativity).

Class NumMult (a: Type): Type := {
  numMult: a ->a ->a
}.
Notation " X '*' Y" := (numMult X Y) (at level 40, left associativity).

Class NumPow (a: Type): Type := {
  numPow: a -> nat ->a
}.
Notation " X '**' Y" := (numPow X Y) (at level 70, no associativity).

Class NumDivision (a: Type): Type := {
  numDivision: a ->a ->a
}.
Notation " X '/' Y" := (numDivision X Y) (at level 40, left associativity).

Class NumIntegerDivision (a: Type): Type := {
  numIntegerDivision: a ->a ->a
}.
Notation " X 'div' Y" := (numIntegerDivision X Y) (at level 70, no associativity).

Class NumRemainder (a: Type): Type := {
  numRemainder: a ->a ->a
}.
Notation " X 'mod' Y" := (numRemainder X Y) (at level 40, no associativity).

Class NumSucc (a: Type): Type := {
  succ: a ->a
}.

Class NumPred (a: Type): Type := {
  pred: a ->a
}.



Require Import DecidableClass.
Definition beq_nat := fun (a b: nat)=> decide (a=b).
Instance x141_Eq : Eq nat := {
   isEqual := beq_nat;
   isInequal n1 n2 := negb (beq_nat n1 n2)
}.







Instance x140_Ord : Ord nat := {
   compare := (genericCompare nat_ltb beq_nat);
   isLess := nat_ltb;
   isLessEqual := nat_lteb;
   isGreater := nat_gtb;
   isGreaterEqual := nat_gteb
}.

Instance x139_SetType : SetType nat := {
   setElemCompare := (genericCompare nat_ltb beq_nat)
}.


Instance x138_NumAdd : NumAdd nat := {
   numAdd := Coq.Init.Peano.plus
}.


Instance x137_NumMinus : NumMinus nat := {
   numMinus := Coq.Init.Peano.minus
}.


Instance x136_NumSucc : NumSucc nat := {
   succ := S
}.


Instance x135_NumPred : NumPred nat := {
   pred := Coq.Init.Peano.pred
}.


Instance x134_NumMult : NumMult nat := {
   numMult := Coq.Init.Peano.mult
}.


Instance x133_NumIntegerDivision : NumIntegerDivision nat := {
   numIntegerDivision := Nat.div
}.

Instance x132_NumDivision : NumDivision nat := {
   numDivision := Nat.div
}.


Instance x131_NumRemainder : NumRemainder nat := {
   numRemainder := Nat.modulo
}.



Definition gen_pow {a : Type} (one : a) (mul : a -> a -> a) (b : a) (e : nat ) : a:=
  if nat_ltb e( 0%nat) then one else
  if ( beq_nat e( 0%nat)) then one else gen_pow_aux mul one b e.

Instance x130_NumPow : NumPow nat := {
   numPow := nat_power
}.




Instance x129_OrdMaxMin : OrdMaxMin nat := {
   max := nat_max;
   min := nat_min
}.



Instance x127_Eq : Eq nat := {
   isEqual := beq_nat;
   isInequal n1 n2 := negb (beq_nat n1 n2)
}.







Instance x126_Ord : Ord nat := {
   compare := (genericCompare nat_ltb beq_nat);
   isLess := nat_ltb;
   isLessEqual := nat_lteb;
   isGreater := nat_gtb;
   isGreaterEqual := nat_gteb
}.

Instance x125_SetType : SetType nat := {
   setElemCompare := (genericCompare nat_ltb beq_nat)
}.


Instance x124_NumAdd : NumAdd nat := {
   numAdd := Coq.Init.Peano.plus
}.


Instance x123_NumMinus : NumMinus nat := {
   numMinus := Coq.Init.Peano.minus
}.


Instance x122_NumSucc : NumSucc nat := {
   succ := S
}.


Instance x121_NumPred : NumPred nat := {
   pred := Coq.Init.Peano.pred
}.


Instance x120_NumMult : NumMult nat := {
   numMult := Coq.Init.Peano.mult
}.


Instance x119_NumPow : NumPow nat := {
   numPow := nat_power
}.


Instance x118_NumIntegerDivision : NumIntegerDivision nat := {
   numIntegerDivision := Nat.div
}.

Instance x117_NumDivision : NumDivision nat := {
   numDivision := Nat.div
}.


Instance x116_NumRemainder : NumRemainder nat := {
   numRemainder := Nat.modulo
}.




Instance x115_OrdMaxMin : OrdMaxMin nat := {
   max := nat_max;
   min := nat_min
}.



Instance x113_Eq : Eq Z := {
   isEqual := Z.eqb;
   isInequal n1 n2 := negb (Z.eqb n1 n2)
}.







Instance x112_Ord : Ord Z := {
   compare := (genericCompare int_ltb Z.eqb);
   isLess := int_ltb;
   isLessEqual := int_lteb;
   isGreater := int_gtb;
   isGreaterEqual := int_gteb
}.

Instance x111_SetType : SetType Z := {
   setElemCompare := (genericCompare int_ltb Z.eqb)
}.


Instance x110_NumNegate : NumNegate Z := {
   numNegate := (fun i=>(Coq.ZArith.BinInt.Z.sub Z0 i))
}.


Instance x109_NumAbs : NumAbs Z := {
   abs := (fun input=>(Z.pred (Z.pos (P_of_succ_nat (Z.abs_nat input)))))
}.


Instance x108_NumAdd : NumAdd Z := {
   numAdd := Coq.ZArith.BinInt.Z.add
}.


Instance x107_NumMinus : NumMinus Z := {
   numMinus := Coq.ZArith.BinInt.Z.sub
}.


Instance x106_NumSucc : NumSucc Z := {
   succ := (fun n=> Coq.ZArith.BinInt.Z.add n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x105_NumPred : NumPred Z := {
   pred := (fun n=> Coq.ZArith.BinInt.Z.sub n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x104_NumMult : NumMult Z := {
   numMult := Coq.ZArith.BinInt.Z.mul
}.


Instance x103_NumPow : NumPow Z := {
   numPow := Coq.ZArith.Zpower.Zpower_nat
}.


Instance x102_NumIntegerDivision : NumIntegerDivision Z := {
   numIntegerDivision := Z.div
}.

Instance x101_NumDivision : NumDivision Z := {
   numDivision := Z.div
}.


Instance x100_NumRemainder : NumRemainder Z := {
   numRemainder := Coq.ZArith.Zdiv.Zmod
}.




Instance x99_OrdMaxMin : OrdMaxMin Z := {
   max := Z.max;
   min := Z.min
}.




Instance x97_Eq : Eq Z := {
   isEqual := Z.eqb;
   isInequal n1 n2 := negb (Z.eqb n1 n2)
}.







Instance x96_Ord : Ord Z := {
   compare := (genericCompare int_ltb Z.eqb);
   isLess := int_ltb;
   isLessEqual := int_lteb;
   isGreater := int_gtb;
   isGreaterEqual := int_gteb
}.

Instance x95_SetType : SetType Z := {
   setElemCompare := (genericCompare int_ltb Z.eqb)
}.


Instance x94_NumNegate : NumNegate Z := {
   numNegate := (fun i=>(Coq.ZArith.BinInt.Z.sub Z0 i))
}.


Definition int32Abs (i : Z ) : Z := (if int_lteb((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) i then i else (Coq.ZArith.BinInt.Z.sub Z0 i)).

Instance x93_NumAbs : NumAbs Z := {
   abs := int32Abs
}.


Instance x92_NumAdd : NumAdd Z := {
   numAdd := Coq.ZArith.BinInt.Z.add
}.


Instance x91_NumMinus : NumMinus Z := {
   numMinus := Coq.ZArith.BinInt.Z.sub
}.



Instance x90_NumSucc : NumSucc Z := {
   succ := (fun n=> Coq.ZArith.BinInt.Z.add n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x89_NumPred : NumPred Z := {
   pred := (fun n=> Coq.ZArith.BinInt.Z.sub n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x88_NumMult : NumMult Z := {
   numMult := Coq.ZArith.BinInt.Z.mul
}.


Instance x87_NumPow : NumPow Z := {
   numPow := Coq.ZArith.Zpower.Zpower_nat
}.


Instance x86_NumIntegerDivision : NumIntegerDivision Z := {
   numIntegerDivision := Z.div
}.

Instance x85_NumDivision : NumDivision Z := {
   numDivision := Z.div
}.


Instance x84_NumRemainder : NumRemainder Z := {
   numRemainder := Coq.ZArith.Zdiv.Zmod
}.




Instance x83_OrdMaxMin : OrdMaxMin Z := {
   max := Z.max;
   min := Z.min
}.




Instance x81_Eq : Eq Z := {
   isEqual := Z.eqb;
   isInequal n1 n2 := negb (Z.eqb n1 n2)
}.







Instance x80_Ord : Ord Z := {
   compare := (genericCompare int_ltb Z.eqb);
   isLess := int_ltb;
   isLessEqual := int_lteb;
   isGreater := int_gtb;
   isGreaterEqual := int_gteb
}.

Instance x79_SetType : SetType Z := {
   setElemCompare := (genericCompare int_ltb Z.eqb)
}.


Instance x78_NumNegate : NumNegate Z := {
   numNegate := (fun i=>(Coq.ZArith.BinInt.Z.sub Z0 i))
}.


Definition int64Abs (i : Z ) : Z := (if int_lteb((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) i then i else (Coq.ZArith.BinInt.Z.sub Z0 i)).

Instance x77_NumAbs : NumAbs Z := {
   abs := int64Abs
}.


Instance x76_NumAdd : NumAdd Z := {
   numAdd := Coq.ZArith.BinInt.Z.add
}.


Instance x75_NumMinus : NumMinus Z := {
   numMinus := Coq.ZArith.BinInt.Z.sub
}.



Instance x74_NumSucc : NumSucc Z := {
   succ := (fun n=> Coq.ZArith.BinInt.Z.add n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x73_NumPred : NumPred Z := {
   pred := (fun n=> Coq.ZArith.BinInt.Z.sub n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x72_NumMult : NumMult Z := {
   numMult := Coq.ZArith.BinInt.Z.mul
}.


Instance x71_NumPow : NumPow Z := {
   numPow := Coq.ZArith.Zpower.Zpower_nat
}.


Instance x70_NumIntegerDivision : NumIntegerDivision Z := {
   numIntegerDivision := Z.div
}.

Instance x69_NumDivision : NumDivision Z := {
   numDivision := Z.div
}.


Instance x68_NumRemainder : NumRemainder Z := {
   numRemainder := Coq.ZArith.Zdiv.Zmod
}.




Instance x67_OrdMaxMin : OrdMaxMin Z := {
   max := Z.max;
   min := Z.min
}.




Instance x65_Eq : Eq Z := {
   isEqual := Z.eqb;
   isInequal n1 n2 := negb (Z.eqb n1 n2)
}.







Instance x64_Ord : Ord Z := {
   compare := (genericCompare int_ltb Z.eqb);
   isLess := int_ltb;
   isLessEqual := int_lteb;
   isGreater := int_gtb;
   isGreaterEqual := int_gteb
}.

Instance x63_SetType : SetType Z := {
   setElemCompare := (genericCompare int_ltb Z.eqb)
}.


Instance x62_NumNegate : NumNegate Z := {
   numNegate := (fun i=>(Coq.ZArith.BinInt.Z.sub Z0 i))
}.


Instance x61_NumAbs : NumAbs Z := {
   abs := (fun input=>(Z.pred (Z.pos (P_of_succ_nat (Z.abs_nat input)))))
}.


Instance x60_NumAdd : NumAdd Z := {
   numAdd := Coq.ZArith.BinInt.Z.add
}.


Instance x59_NumMinus : NumMinus Z := {
   numMinus := Coq.ZArith.BinInt.Z.sub
}.


Instance x58_NumSucc : NumSucc Z := {
   succ := (fun n=> Coq.ZArith.BinInt.Z.add n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x57_NumPred : NumPred Z := {
   pred := (fun n=> Coq.ZArith.BinInt.Z.sub n((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))
}.


Instance x56_NumMult : NumMult Z := {
   numMult := Coq.ZArith.BinInt.Z.mul
}.


Instance x55_NumPow : NumPow Z := {
   numPow := Coq.ZArith.Zpower.Zpower_nat
}.


Instance x54_NumIntegerDivision : NumIntegerDivision Z := {
   numIntegerDivision := Z.div
}.

Instance x53_NumDivision : NumDivision Z := {
   numDivision := Z.div
}.


Instance x52_NumRemainder : NumRemainder Z := {
   numRemainder := Coq.ZArith.Zdiv.Zmod
}.




Instance x51_OrdMaxMin : OrdMaxMin Z := {
   max := Z.max;
   min := Z.min
}.





Instance x49_Eq : Eq Q := {
   isEqual := Qeq_bool;
   isInequal n1 n2 := negb (Qeq_bool n1 n2)
}.







Instance x48_Ord : Ord Q := {
   compare := (genericCompare Qlt_bool Qeq_bool);
   isLess := Qlt_bool;
   isLessEqual := Qle_bool;
   isGreater := Qgt_bool;
   isGreaterEqual := Qge_bool
}.

Instance x47_SetType : SetType Q := {
   setElemCompare := (genericCompare Qlt_bool Qeq_bool)
}.


Instance x46_NumAdd : NumAdd Q := {
   numAdd := Qplus
}.


Instance x45_NumMinus : NumMinus Q := {
   numMinus := Qminus
}.



Instance x44_NumNegate : NumNegate Q := {
   numNegate := (fun n=> Qminus((inject_Z (Z.pred (Z.pos (P_of_succ_nat 0%nat))))) n)
}.



Instance x43_NumAbs : NumAbs Q := {
   abs := (fun n=>(if Qgt_bool n((inject_Z (Z.pred (Z.pos (P_of_succ_nat 0%nat))))) then n else Qminus((inject_Z (Z.pred (Z.pos (P_of_succ_nat 0%nat))))) n))
}.


Instance x42_NumSucc : NumSucc Q := {
   succ := (fun n=> Qplus n((inject_Z (Z.pred (Z.pos (P_of_succ_nat 1%nat))))))
}.


Instance x41_NumPred : NumPred Q := {
   pred := (fun n=> Qminus n((inject_Z (Z.pred (Z.pos (P_of_succ_nat 1%nat))))))
}.


Instance x40_NumMult : NumMult Q := {
   numMult := Qmult
}.


Instance x39_NumDivision : NumDivision Q := {
   numDivision := Qdiv
}.


Definition rationalFromFrac (n : Z ) (d : Z ) : Q := Qdiv ((inject_Z n)) ((inject_Z d)).





Instance x38_NumPow : NumPow Q := {
   numPow := (fun r e=>(Qpower r (Z.of_nat e)))
}.




Instance x37_OrdMaxMin : OrdMaxMin Q := {
   max := Qmax;
   min := Qmin
}.




Instance x35_Eq : Eq R := {
   isEqual := Reqb;
   isInequal n1 n2 := negb (Reqb n1 n2)
}.







Instance x34_Ord : Ord R := {
   compare := (genericCompare Rlt_bool Reqb);
   isLess := Rlt_bool;
   isLessEqual := Rle_bool;
   isGreater := Rgt_bool;
   isGreaterEqual := Rge_bool
}.

Instance x33_SetType : SetType R := {
   setElemCompare := (genericCompare Rlt_bool Reqb)
}.


Instance x32_NumAdd : NumAdd R := {
   numAdd := Rplus
}.


Instance x31_NumMinus : NumMinus R := {
   numMinus := Rminus
}.



Instance x30_NumNegate : NumNegate R := {
   numNegate := Ropp
}.



Instance x29_NumAbs : NumAbs R := {
   abs := Rabs
}.


Instance x28_NumSucc : NumSucc R := {
   succ := (fun n=> Rplus n((IZR (Z.pred (Z.pos (P_of_succ_nat 1%nat))))))
}.


Instance x27_NumPred : NumPred R := {
   pred := (fun n=> Rminus n((IZR (Z.pred (Z.pos (P_of_succ_nat 1%nat))))))
}.


Instance x26_NumMult : NumMult R := {
   numMult := Rmult
}.


Instance x25_NumDivision : NumDivision R := {
   numDivision := Rdiv
}.


Definition realFromFrac (n : Z ) (d : Z ) : R := Rdiv ((IZR n)) ((IZR d)).



Instance x24_NumPow : NumPow R := {
   numPow := pow
}.





Instance x23_OrdMaxMin : OrdMaxMin R := {
   max := Rmax;
   min := Rmin
}.

















Definition int32FromInteger (i : Z ) : Z := (
  let abs_int32 := (Z.pred (Z.pos (P_of_succ_nat (Z.abs_nat i)))) in
  if ( int_ltb i((Z.pred (Z.pos (P_of_succ_nat 0%nat))))) then ((Coq.ZArith.BinInt.Z.sub Z0 abs_int32)) else abs_int32
).

Definition int32FromInt (i : Z ) : Z := int32FromInteger ( i).

Definition int32FromInt64 (i : Z ) : Z := int32FromInteger ( i).



Definition int64FromInteger (i : Z ) : Z := (
  let abs_int64 := (Z.pred (Z.pos (P_of_succ_nat (Z.abs_nat i)))) in
  if ( int_ltb i((Z.pred (Z.pos (P_of_succ_nat 0%nat))))) then ((Coq.ZArith.BinInt.Z.sub Z0 abs_int64)) else abs_int64
).

Definition int64FromInt (i : Z ) : Z := int64FromInteger ( i).

Definition int64FromInt32 (i : Z ) : Z := int64FromInteger ( i).