Library EVMOpSem.Lem.lem_basic_classes

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 Coq.Strings.Ascii.
Require Export Coq.Strings.Ascii.



Class Eq (a: Type): Type := {
  isEqual: a ->a -> bool;
  isInequal: a ->a -> bool
}.
Notation " X '=' Y" := (isEqual X Y) (at level 70, no associativity).
Notation " X '<>' Y" := (isInequal X Y) (at level 70, no associativity).



Definition unsafe_structural_inequality {a : Type} (x : a) (y : a) : bool := negb (classical_boolean_equivalence x y).

Definition orderingIsLess (r : ordering ) : bool := (match ( r) with LT => true | _ => false end).
Definition orderingIsGreater (r : ordering ) : bool := (match ( r) with GT => true | _ => false end).
Definition orderingIsEqual (r : ordering ) : bool := (match ( r) with EQ => true | _ => false end).

Definition ordering_cases {a : Type} (r : ordering ) (lt : a) (eq : a) (gt : a) : a:=
  if orderingIsLess r then lt else
  if orderingIsEqual r then eq else gt.


Instance x19_Eq : Eq ordering := {
   isEqual := (fun left right=>(ordering_equal left right));
   isInequal x y := negb ((ordering_equal x y))
}.

Class Ord (a: Type): Type := {
  compare: a ->a -> ordering;
  isLess: a ->a -> bool;
  isLessEqual: a ->a -> bool;
  isGreater: a ->a -> bool;
  isGreaterEqual: a ->a -> bool
}.
Notation " X '<' Y" := (isLess X Y) (at level 70, no associativity).
Notation " X '<=' Y" := (isLessEqual X Y) (at level 70, no associativity).
Notation " X '>' Y" := (isGreater X Y) (at level 70, no associativity).
Notation " X '>=' Y" := (isGreaterEqual X Y) (at level 70, no associativity).






Definition genericCompare {a : Type} (less: a -> a -> bool ) (equal: a -> a -> bool ) (x : a) (y : a) : ordering :=
  if less x y then
    LT
  else if equal x y then
    EQ
  else
    GT.

Definition ordCompare {a : Type} `{Eq a} `{Ord a} (x : a) (y : a) : ordering :=
  if ( isLess x y) then LT else
  if (x = y) then EQ else GT.

Class OrdMaxMin (a: Type): Type := {
  max: a ->a ->a;
  min: a ->a ->a
}.


Definition minByLessEqual {a : Type} (le : a -> a -> bool ) (x : a) (y : a) : a:= if (le x y) then x else y.

Definition maxByLessEqual {a : Type} (le : a -> a -> bool ) (x : a) (y : a) : a:= if (le y x) then x else y.





Class SetType (a: Type): Type := {
  setElemCompare: a ->a -> ordering
}.



Instance x18_Eq : Eq bool := {
   isEqual := Bool.eqb;
   isInequal x y := negb (Bool.eqb x y)
}.

Definition boolCompare (b1 : bool ) (b2 : bool ) : ordering := match ( (b1, b2)) with
  | (true, true) => EQ
  | (true, false) => GT
  | (false, true) => LT
  | (false, false) => EQ
end.

Instance x17_SetType : SetType bool := {
   setElemCompare := boolCompare
}.



Instance x16_Eq : Eq ascii := {
   isEqual := (fun left right=>(char_equal left right));
   isInequal left right := negb ((char_equal left right))
}.



Instance x15_Eq : Eq string := {
   isEqual := (fun left right=>(string_equal left right));
   isInequal l r := negb ((string_equal l r))
}.



Instance x14_Eq{a b: Type} `{Eq a} `{Eq b}: Eq ((a * b) % type):= {
   isEqual := ((fun left right=>(tuple_equal_by (fun x y => x = y) (fun x y => x = y) left right)));
   isInequal x y := negb (((tuple_equal_by (fun x y => x = y) (fun x y => x = y) x y)))
}.


Definition pairCompare {a b : Type} (cmpa : a -> a -> ordering ) (cmpb : b -> b -> ordering ) (p : (a*b) % type) (p0 : (a*b) % type) : ordering :=
  match ( (cmpa,cmpb,p,p0)) with ( cmpa, cmpb, (a1, b1), (a2, b2)) =>
    match ( cmpa a1 a2) with | LT => LT | GT => GT | EQ => cmpb b1 b2 end end.

Definition pairLess {a b : Type} `{Ord a} `{Ord b} (p : (b*a) % type) (p0 : (b*a) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2), (y1, y2)) =>
    ( isLess x1 y1) || (( isLessEqual x1 y1) && ( isLess x2 y2)) end.
Definition pairLessEq {a b : Type} `{Ord a} `{Ord b} (p : (b*a) % type) (p0 : (b*a) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2), (y1, y2)) =>
    ( isLess x1 y1) || (( isLessEqual x1 y1) && ( isLessEqual x2 y2)) end.

Definition pairGreater {a b : Type} `{Ord a} `{Ord b} (x12 : (a*b) % type) (y12 : (a*b) % type) : bool := pairLess y12 x12.
Definition pairGreaterEq {a b : Type} `{Ord a} `{Ord b} (x12 : (a*b) % type) (y12 : (a*b) % type) : bool := pairLessEq y12 x12.

Instance x13_Ord{a b: Type} `{Ord a} `{Ord b}: Ord ((a * b) % type):= {
   compare := pairCompare compare compare;
   isLess := pairLess;
   isLessEqual := pairLessEq;
   isGreater := pairGreater;
   isGreaterEqual := pairGreaterEq
}.

Instance x12_SetType{a b: Type} `{SetType a} `{SetType b}: SetType ((a * b) % type):= {
   setElemCompare := pairCompare setElemCompare setElemCompare
}.


Definition tripleEqual {a b c : Type} `{Eq a} `{Eq b} `{Eq c} (p : (a*b*c) % type) (p0 : (a*b*c) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2, x3), (y1, y2, y3)) =>
    ( ((tuple_equal_by (fun x y => x = y)
          ((fun (left : (b*c) % type) (right : (b*c) % type)=>
              (tuple_equal_by (fun x y => x = y) (fun x y => x = y) left
                 right))) (x1, (x2, x3)) (y1, (y2, y3))))) end.

Instance x11_Eq{a b c: Type} `{Eq a} `{Eq b} `{Eq c}: Eq ((a * b * c) % type):= {
   isEqual := tripleEqual;
   isInequal x y := negb (tripleEqual x y)
}.


Definition tripleCompare {a b c : Type} (cmpa : a -> a -> ordering ) (cmpb : b -> b -> ordering ) (cmpc : c -> c -> ordering ) (p : (a*b*c) % type) (p0 : (a*b*c) % type) : ordering :=
  match ( (cmpa,cmpb,cmpc,p,p0)) with
      ( cmpa, cmpb, cmpc, (a1, b1, c1), (a2, b2, c2)) =>
    pairCompare cmpa (pairCompare cmpb cmpc) (a1, (b1, c1)) (a2, (b2, c2))
  end.

Definition tripleLess {a b c : Type} `{Ord a} `{Ord b} `{Ord c} (p : (a*b*c) % type) (p0 : (a*b*c) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2, x3), (y1, y2, y3)) =>
    pairLess (x1, (x2, x3)) (y1, (y2, y3)) end.
Definition tripleLessEq {a b c : Type} `{Ord a} `{Ord b} `{Ord c} (p : (a*b*c) % type) (p0 : (a*b*c) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2, x3), (y1, y2, y3)) =>
    pairLessEq (x1, (x2, x3)) (y1, (y2, y3)) end.

Definition tripleGreater {a b c : Type} `{Ord a} `{Ord b} `{Ord c} (x123 : (c*b*a) % type) (y123 : (c*b*a) % type) : bool := tripleLess y123 x123.
Definition tripleGreaterEq {a b c : Type} `{Ord a} `{Ord b} `{Ord c} (x123 : (c*b*a) % type) (y123 : (c*b*a) % type) : bool := tripleLessEq y123 x123.

Instance x10_Ord{a b c: Type} `{Ord a} `{Ord b} `{Ord c}: Ord ((a * b * c) % type):= {
   compare := tripleCompare compare compare compare;
   isLess := tripleLess;
   isLessEqual := tripleLessEq;
   isGreater := tripleGreater;
   isGreaterEqual := tripleGreaterEq
}.

Instance x9_SetType{a b c: Type} `{SetType a} `{SetType b} `{SetType c}: SetType ((a * b * c) % type):= {
   setElemCompare := tripleCompare setElemCompare setElemCompare setElemCompare
}.


Definition quadrupleEqual {a b c d : Type} `{Eq a} `{Eq b} `{Eq c} `{Eq d} (p : (a*b*c*d) % type) (p0 : (a*b*c*d) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2, x3, x4), (y1, y2, y3, y4)) =>
    ( ((tuple_equal_by (fun x y => x = y)
          ((fun (left : (b*((c*d) % type)) % type) (right : (b*((c*d) % type)) % type)=>
              (tuple_equal_by (fun x y => x = y)
                 ((fun (left : (c*d) % type) (right : (c*d) % type)=>
                     (tuple_equal_by (fun x y => x = y) (fun x y => x = y)
                        left right))) left right))) (x1, (x2, (x3, x4)))
          (y1, (y2, (y3, y4)))))) end.

Instance x8_Eq{a b c d: Type} `{Eq a} `{Eq b} `{Eq c} `{Eq d}: Eq ((a * b * c * d) % type):= {
   isEqual := quadrupleEqual;
   isInequal x y := negb (quadrupleEqual x y)
}.


Definition quadrupleCompare {a b c d : Type} (cmpa : a -> a -> ordering ) (cmpb : b -> b -> ordering ) (cmpc : c -> c -> ordering ) (cmpd : d -> d -> ordering ) (p : (a*b*c*d) % type) (p0 : (a*b*c*d) % type) : ordering :=
  match ( (cmpa,cmpb,cmpc,cmpd,p,p0)) with
      ( cmpa, cmpb, cmpc, cmpd, (a1, b1, c1, d1), (a2, b2, c2, d2)) =>
    pairCompare cmpa (pairCompare cmpb (pairCompare cmpc cmpd))
      (a1, (b1, (c1, d1))) (a2, (b2, (c2, d2))) end.

Definition quadrupleLess {a b c d : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} (p : (a*b*c*d) % type) (p0 : (a*b*c*d) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2, x3, x4), (y1, y2, y3, y4)) =>
    pairLess (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4))) end.
Definition quadrupleLessEq {a b c d : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} (p : (a*b*c*d) % type) (p0 : (a*b*c*d) % type) : bool :=
  match ( (p,p0)) with ( (x1, x2, x3, x4), (y1, y2, y3, y4)) =>
    pairLessEq (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4))) end.

Definition quadrupleGreater {a b c d : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} (x1234 : (d*c*b*a) % type) (y1234 : (d*c*b*a) % type) : bool := quadrupleLess y1234 x1234.
Definition quadrupleGreaterEq {a b c d : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} (x1234 : (d*c*b*a) % type) (y1234 : (d*c*b*a) % type) : bool := quadrupleLessEq y1234 x1234.

Instance x7_Ord{a b c d: Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d}: Ord ((a * b * c * d) % type):= {
   compare := quadrupleCompare compare compare compare compare;
   isLess := quadrupleLess;
   isLessEqual := quadrupleLessEq;
   isGreater := quadrupleGreater;
   isGreaterEqual := quadrupleGreaterEq
}.

Instance x6_SetType{a b c d: Type} `{SetType a} `{SetType b} `{SetType c} `{SetType d}: SetType ((a * b * c * d) % type):= {
   setElemCompare := quadrupleCompare setElemCompare setElemCompare setElemCompare setElemCompare
}.


Definition quintupleEqual {a b c d e : Type} `{Eq a} `{Eq b} `{Eq c} `{Eq d} `{Eq e} (p : (a*b*c*d*e) % type) (p0 : (a*b*c*d*e) % type) : bool :=
  match ( (p,p0)) with
      ( (x1, x2, x3, x4, x5), (y1, y2, y3, y4, y5)) =>
    ( ((tuple_equal_by (fun x y => x = y)
          ((fun (left : (b*((c*((d*e) % type)) % type)) % type) (right : (b*((c*((d*e) % type)) % type)) % type)=>
              (tuple_equal_by (fun x y => x = y)
                 ((fun (left : (c*((d*e) % type)) % type) (right : (c*((d*e) % type)) % type)=>
                     (tuple_equal_by (fun x y => x = y)
                        ((fun (left : (d*e) % type) (right : (d*e) % type)=>
                            (tuple_equal_by (fun x y => x = y)
                               (fun x y => x = y) left right))) left
                      right))) left right))) (x1, (x2, (x3, (x4, x5))))
          (y1, (y2, (y3, (y4, y5))))))) end.

Instance x5_Eq{a b c d e: Type} `{Eq a} `{Eq b} `{Eq c} `{Eq d} `{Eq e}: Eq ((a * b * c * d * e) % type):= {
   isEqual := quintupleEqual;
   isInequal x y := negb (quintupleEqual x y)
}.


Definition quintupleCompare {a b c d e : Type} (cmpa : a -> a -> ordering ) (cmpb : b -> b -> ordering ) (cmpc : c -> c -> ordering ) (cmpd : d -> d -> ordering ) (cmpe : e -> e -> ordering ) (p : (a*b*c*d*e) % type) (p0 : (a*b*c*d*e) % type) : ordering :=
  match ( (cmpa,cmpb,cmpc,cmpd,cmpe,p,p0)) with
      ( cmpa, cmpb, cmpc, cmpd, cmpe, (a1, b1, c1, d1, e1), (a2, b2, c2, d2, e2)) =>
    pairCompare cmpa
      (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd cmpe)))
      (a1, (b1, (c1, (d1, e1)))) (a2, (b2, (c2, (d2, e2)))) end.

Definition quintupleLess {a b c d e : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} (p : (a*b*c*d*e) % type) (p0 : (a*b*c*d*e) % type) : bool :=
  match ( (p,p0)) with
      ( (x1, x2, x3, x4, x5), (y1, y2, y3, y4, y5)) =>
    pairLess (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5)))) end.
Definition quintupleLessEq {a b c d e : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} (p : (a*b*c*d*e) % type) (p0 : (a*b*c*d*e) % type) : bool :=
  match ( (p,p0)) with
      ( (x1, x2, x3, x4, x5), (y1, y2, y3, y4, y5)) =>
    pairLessEq (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5)))) end.

Definition quintupleGreater {a b c d e : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} (x12345 : (e*d*c*b*a) % type) (y12345 : (e*d*c*b*a) % type) : bool := quintupleLess y12345 x12345.
Definition quintupleGreaterEq {a b c d e : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} (x12345 : (e*d*c*b*a) % type) (y12345 : (e*d*c*b*a) % type) : bool := quintupleLessEq y12345 x12345.

Instance x4_Ord{a b c d e: Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e}: Ord ((a * b * c * d * e) % type):= {
   compare := quintupleCompare compare compare compare compare compare;
   isLess := quintupleLess;
   isLessEqual := quintupleLessEq;
   isGreater := quintupleGreater;
   isGreaterEqual := quintupleGreaterEq
}.

Instance x3_SetType{a b c d e: Type} `{SetType a} `{SetType b} `{SetType c} `{SetType d} `{SetType e}: SetType ((a * b * c * d * e) % type):= {
   setElemCompare := quintupleCompare setElemCompare setElemCompare setElemCompare setElemCompare setElemCompare
}.


Definition sextupleEqual {a b c d e f : Type} `{Eq a} `{Eq b} `{Eq c} `{Eq d} `{Eq e} `{Eq f} (p : (a*b*c*d*e*f) % type) (p0 : (a*b*c*d*e*f) % type) : bool :=
  match ( (p,p0)) with
      ( (x1, x2, x3, x4, x5, x6), (y1, y2, y3, y4, y5, y6)) =>
    ( ((tuple_equal_by (fun x y => x = y)
          ((fun (left : (b*((c*((d*((e*f) % type)) % type)) % type)) % type) (right : (b*((c*((d*((e*f) % type)) % type)) % type)) % type)=>
              (tuple_equal_by (fun x y => x = y)
                 ((fun (left : (c*((d*((e*f) % type)) % type)) % type) (right : (c*((d*((e*f) % type)) % type)) % type)=>
                     (tuple_equal_by (fun x y => x = y)
                        ((fun (left : (d*((e*f) % type)) % type) (right : (d*((e*f) % type)) % type)=>
                            (tuple_equal_by (fun x y => x = y)
                               ((fun (left : (e*f) % type) (right : (e*f) % type)=>
                                   (tuple_equal_by (fun x y => x = y)
                                      (fun x y => x = y) left right)))
                             left right))) left right))) left right)))
          (x1, (x2, (x3, (x4, (x5, x6))))) (y1, (y2, (y3, (y4, (y5, y6))))))))
  end.

Instance x2_Eq{a b c d e f: Type} `{Eq a} `{Eq b} `{Eq c} `{Eq d} `{Eq e} `{Eq f}: Eq ((a * b * c * d * e * f) % type):= {
   isEqual := sextupleEqual;
   isInequal x y := negb (sextupleEqual x y)
}.


Definition sextupleCompare {a b c d e f : Type} (cmpa : a -> a -> ordering ) (cmpb : b -> b -> ordering ) (cmpc : c -> c -> ordering ) (cmpd : d -> d -> ordering ) (cmpe : e -> e -> ordering ) (cmpf : f -> f -> ordering ) (p : (a*b*c*d*e*f) % type) (p0 : (a*b*c*d*e*f) % type) : ordering :=
  match ( (cmpa,cmpb,cmpc,cmpd,cmpe,cmpf,p,p0)) with
      ( cmpa, cmpb, cmpc, cmpd, cmpe, cmpf, (a1, b1, c1, d1, e1, f1), (a2, b2, c2, d2, e2, f2)) =>
    pairCompare cmpa
      (pairCompare cmpb
         (pairCompare cmpc (pairCompare cmpd (pairCompare cmpe cmpf))))
      (a1, (b1, (c1, (d1, (e1, f1))))) (a2, (b2, (c2, (d2, (e2, f2))))) end.

Definition sextupleLess {a b c d e f : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} `{Ord f} (p : (a*b*c*d*e*f) % type) (p0 : (a*b*c*d*e*f) % type) : bool :=
  match ( (p,p0)) with
      ( (x1, x2, x3, x4, x5, x6), (y1, y2, y3, y4, y5, y6)) =>
    pairLess (x1, (x2, (x3, (x4, (x5, x6)))))
      (y1, (y2, (y3, (y4, (y5, y6))))) end.
Definition sextupleLessEq {a b c d e f : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} `{Ord f} (p : (a*b*c*d*e*f) % type) (p0 : (a*b*c*d*e*f) % type) : bool :=
  match ( (p,p0)) with
      ( (x1, x2, x3, x4, x5, x6), (y1, y2, y3, y4, y5, y6)) =>
    pairLessEq (x1, (x2, (x3, (x4, (x5, x6)))))
      (y1, (y2, (y3, (y4, (y5, y6))))) end.

Definition sextupleGreater {a b c d e f : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} `{Ord f} (x123456 : (f*e*d*c*b*a) % type) (y123456 : (f*e*d*c*b*a) % type) : bool := sextupleLess y123456 x123456.
Definition sextupleGreaterEq {a b c d e f : Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} `{Ord f} (x123456 : (f*e*d*c*b*a) % type) (y123456 : (f*e*d*c*b*a) % type) : bool := sextupleLessEq y123456 x123456.

Instance x1_Ord{a b c d e f: Type} `{Ord a} `{Ord b} `{Ord c} `{Ord d} `{Ord e} `{Ord f}: Ord ((a * b * c * d * e * f) % type):= {
   compare := sextupleCompare compare compare compare compare compare compare;
   isLess := sextupleLess;
   isLessEqual := sextupleLessEq;
   isGreater := sextupleGreater;
   isGreaterEqual := sextupleGreaterEq
}.

Instance x0_SetType{a b c d e f: Type} `{SetType a} `{SetType b} `{SetType c} `{SetType d} `{SetType e} `{SetType f}: SetType ((a * b * c * d * e * f) % type):= {
   setElemCompare := sextupleCompare setElemCompare setElemCompare setElemCompare setElemCompare setElemCompare setElemCompare
}.