Huge verification freeze on this, see the last definition @ line 315

Sandbox.fst

module Sandbox

type binary_op (a:Type) = a -> a -> a
type unary_op (a:Type) = a -> a
type predicate (a:Type) = a -> bool
type binary_relation (a: Type) = a -> a -> bool
 
[@@"opaque_to_smt"]
let is_reflexive  (#a:Type) (r: binary_relation a) = forall (x:a).     x `r` x
[@@"opaque_to_smt"]
let is_symmetric  (#a:Type) (r: binary_relation a) = forall (x y:a).   x `r` y == y `r` x
[@@"opaque_to_smt"]
let is_transitive (#a:Type) (r: binary_relation a) = forall (x y z:a). x `r` y /\ y `r` z ==> x `r` z 

type equivalence_relation (a: Type) = r:binary_relation a{is_reflexive r /\ is_symmetric r /\ is_transitive r}

[@@"opaque_to_smt"]
let congruence_condition (#a: Type) (op: binary_op a) (eq: equivalence_relation a) = 
  forall (x y z:a). eq x y ==> (op x z `eq` op y z) && (op z x `eq` op z y)

[@@"opaque_to_smt"]
let unary_congruence_condition (#a: Type) (op: unary_op a) (eq: equivalence_relation a) = 
  forall (x y: a). eq x y ==> (op x `eq` op y) && (op y `eq` op x)

type op_with_congruence (#a:Type) (eq: equivalence_relation a) = op:binary_op a{congruence_condition op eq}

type unary_op_with_congruence #a (eq: equivalence_relation a) = op: unary_op a{unary_congruence_condition op eq}

[@@"opaque_to_smt"]
let is_associative (#a:Type) (#eq: equivalence_relation a) (op: op_with_congruence eq) 
  = forall (x y z:a). ((x `op` y) `op` z) `eq` (x `op` (y `op` z))
  
[@@"opaque_to_smt"]
let is_commutative (#a:Type) (#eq: equivalence_relation a) (op: op_with_congruence eq) 
  = forall (x y:a). ((x `op` y) `eq` (y `op` x)) /\ ((y `op` x) `eq` (x `op` y))
 
[@@"opaque_to_smt"]
let is_left_id_of  (#a:Type) (u:a) (#eq: equivalence_relation a) (op: op_with_congruence eq) = forall (x:a). (u `op` x) `eq` x // left identity

[@@"opaque_to_smt"]
let is_right_id_of (#a:Type) (u:a) (#eq: equivalence_relation a) (op: op_with_congruence eq) = forall (x:a). (x `op` u) `eq` x // right identity

[@@"opaque_to_smt"]
let is_neutral_of  (#a:Type) (u:a) (#eq: equivalence_relation a) (op: op_with_congruence eq) = is_left_id_of u op /\ is_right_id_of u op // neutral element

type neutral_element_of (#a: Type) (#eq: equivalence_relation a) (op: op_with_congruence eq) = (x:a{is_neutral_of x op})

[@@"opaque_to_smt"]
let is_absorber_of (#a:Type) 
                   (z:a) 
                   (#eq: equivalence_relation a) 
                   (op: op_with_congruence eq) 
  = forall (x:a). ((x `op` z) `eq` z) && ((z `op` x) `eq` z)

unfold type absorber_of (#a:Type) (#eq: equivalence_relation a) (op: op_with_congruence eq)
  = z:a{is_absorber_of z op}
  
unfold type non_absorber_of (#a:Type) (#eq: equivalence_relation a) (op: op_with_congruence eq)
  = z:a{~(is_absorber_of z op)}

[@@"opaque_to_smt"]
let is_unit (#a: Type) (x: a) (#eq: equivalence_relation a) (op:op_with_congruence eq) 
  = exists (y:a). (is_neutral_of (x `op` y) op /\ is_neutral_of (y `op` x) op)
 
type units_of (#a: Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq) = x:a{is_unit x mul}

[@@"opaque_to_smt"]
let yields_units (#a: Type) (f: a->a) (#eq: equivalence_relation a) (op: op_with_congruence eq) 
 = forall (x:a). is_unit (f x) op 

type unary_op_on_units_of (#a:Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq) =
  unary_op_with_congruence #(units_of mul) (    
     reveal_opaque (`%is_reflexive) (is_reflexive #a); 
     reveal_opaque (`%is_reflexive) (is_reflexive #(units_of mul)); 
     reveal_opaque (`%is_symmetric) (is_symmetric #a);   
     reveal_opaque (`%is_symmetric) (is_symmetric #(units_of mul));   
     reveal_opaque (`%is_transitive) (is_transitive #a);
     reveal_opaque (`%is_transitive) (is_transitive #(units_of mul));
     eq)

let yields_inverses_for_units (#a:Type) (#eq: equivalence_relation a) 
                              (#op: op_with_congruence eq) 
                              (inv: unary_op_on_units_of op) = 
  forall (x: units_of op). is_neutral_of (op (inv x) x) op /\ 
                      is_neutral_of (op x (inv x)) op 
                
let all_are_units (#a:Type) (#eq: equivalence_relation a) 
                  (op: op_with_congruence eq{is_associative op}) = forall (x:a). is_unit x op

[@@"opaque_to_smt"]
let is_inverse_operation_for (#a: Type) (#eq: equivalence_relation a) 
                             (inv: unary_op_with_congruence eq) 
                             (op: op_with_congruence eq)
  = (forall (x:a). is_neutral_of (op x (inv x)) op /\ is_neutral_of (op (inv x) x) op)


noeq type magma (a: Type) =  
{
  eq: equivalence_relation a;
  op: op_with_congruence eq;
  inv: unary_op_on_units_of op;
  neutral: a
}

let magma_inv_respects_eq (#a:Type) (m: magma a) : Lemma (  
  reveal_opaque (`%is_reflexive) (is_reflexive #a); 
  reveal_opaque (`%is_reflexive) (is_reflexive #(units_of m.op)); 
  reveal_opaque (`%is_symmetric) (is_symmetric #a);   
  reveal_opaque (`%is_symmetric) (is_symmetric #(units_of m.op));   
  reveal_opaque (`%is_transitive) (is_transitive #a);
  reveal_opaque (`%is_transitive) (is_transitive #(units_of m.op)); 
  unary_congruence_condition #(units_of m.op) m.inv m.eq) = ()

type semigroup (a:Type)             = g: magma a{is_associative g.op /\ yields_inverses_for_units g.inv}
type commutative_magma (a:Type)     = g: magma a{is_commutative g.op}
type commutative_semigroup (a:Type) = g: semigroup a{is_commutative g.op}
type monoid (a:Type)                = g: semigroup a{is_neutral_of g.neutral g.op}
type commutative_monoid (a:Type)    = g: monoid a{is_commutative g.op}
type group (a:Type)                 = g: (m:monoid a{all_are_units m.op}){is_inverse_operation_for #a ( 
  reveal_opaque (`%unary_congruence_condition) (unary_congruence_condition #a); 
  reveal_opaque (`%unary_congruence_condition) (unary_congruence_condition #(units_of g.op));
//  reveal_opaque (`%is_inverse_operation_for) (is_inverse_operation_for #a #g.eq);  
g.inv) g.op}
type commutative_group (a:Type)     = g: group a{is_commutative g.op}

[@@"opaque_to_smt"]
let is_left_distributive (#a:Type) (#eq: equivalence_relation a) 
                         (op_mul: op_with_congruence eq) 
                         (op_add: op_with_congruence eq) =
  forall (x y z:a). (x `op_mul` (y `op_add` z)) `eq` ((x `op_mul` y) `op_add` (x `op_mul` z))
  
[@@"opaque_to_smt"]
let is_right_distributive (#a:Type) (#eq: equivalence_relation a) 
                          (op_mul: op_with_congruence eq) 
                          (op_add: op_with_congruence eq) =
  forall (x y z:a). ((x `op_add` y) `op_mul` z) `eq` ((x `op_mul` z) `op_add` (y `op_mul` z))
  
[@@"opaque_to_smt"]
let is_fully_distributive (#a:Type) (#eq: equivalence_relation a) 
                          (op_mul: op_with_congruence eq) 
                          (op_add: op_with_congruence eq) =
  forall (x y z:a). ((x `op_mul` (y `op_add` z)) `eq` ((x `op_mul` y) `op_add` (x `op_mul` z))) /\ 
               (((x `op_add` y) `op_mul` z) `eq` ((x `op_mul` z) `op_add` (y `op_mul` z)))

let unary_distributivity_condition (#a: Type) (#eq: equivalence_relation a) 
                                   (f: a->a) (op: op_with_congruence eq) (x y: a)
 = f (x `op` y) `eq` (f x `op` f y)
 
[@@"opaque_to_smt"]
let unary_distributes_over (#a: Type) (f: a->a) (#eq: equivalence_relation a) (op: op_with_congruence eq) = 
  forall (x y: a). unary_distributivity_condition f op x y

 
[@@"opaque_to_smt"]
let unary_over_nonzeros_distributes_over (#a: Type) 
                                         (#eq: equivalence_relation a) 
                                         (f: a->a) (op: op_with_congruence eq) = 
  forall (x y: non_absorber_of op). unary_distributivity_condition f op x y

let is_unit_normal (#a:Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq) (unit_part_func: a -> a) (x:a) = is_neutral_of (unit_part_func x) mul

type unit_normal_of (#a: Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq) (unit_part_func: a -> a) 
  = x:a { is_unit_normal mul unit_part_func x }

let nat_function_defined_on_non_absorbers (#a:Type) (#eq: equivalence_relation a) (op: op_with_congruence eq) 
  = f: (a -> (option nat)) { forall (x:a). (f x)=None ==> is_absorber_of x op }

noeq type ring (a: Type) = {
  addition: commutative_group a;
  multiplication: (z:monoid a{z.eq == addition.eq});
  eq: (t:equivalence_relation a { 
         congruence_condition addition.op t /\ 
         congruence_condition multiplication.op t /\ 
         t==addition.eq /\ t==multiplication.eq /\
         is_fully_distributive multiplication.op addition.op /\
         is_absorber_of addition.neutral multiplication.op
       });
  unit_part_of: a -> units_of multiplication.op;
  normal_part_of: a -> unit_normal_of multiplication.op unit_part_of;
  euclidean_norm: nat_function_defined_on_non_absorbers multiplication.op 
} 

[@@"opaque_to_smt"]
let has_no_absorber_divisors (#a:Type) (#eq: equivalence_relation a) (op: op_with_congruence eq)  
  = forall (x y: a). is_absorber_of (op x y) op <==> (is_absorber_of x op) \/ (is_absorber_of y op)
  
type domain (a: Type) = r:ring a { 
  has_no_absorber_divisors r.multiplication.op /\ 
  ~(r.eq r.addition.neutral r.multiplication.neutral) 
}

[@@"opaque_to_smt"]
let is_idempotent (#a:Type) (#eq: equivalence_relation a) (r: unary_op_with_congruence eq) 
  = forall (x:a). (r x) `eq` (r (r x))
  
[@@"opaque_to_smt"]
let is_neutral_invariant (#a: Type) (#eq: equivalence_relation a) 
                         (op: op_with_congruence eq) (f: a -> a) = 
  forall (x:a). (is_neutral_of x op ==> eq x (f x) /\ eq (f x) x)
  
let is_unit_part_function (#a: Type) (#eq: equivalence_relation a) (#op: op_with_congruence eq) 
                          (f: a -> units_of op) = 
  unary_congruence_condition f eq /\
  is_idempotent #a #eq f /\
  is_neutral_invariant op f /\
  yields_units f op  /\
  unary_over_nonzeros_distributes_over f op

[@@"opaque_to_smt"]
let yields_unit_normals (#a:Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq) (unit_part_func: a -> a) (f: a -> a) =
  forall (x:a). is_unit_normal mul unit_part_func (f x)
  
[@@"opaque_to_smt"]
let unit_and_normal_decomposition_property (#a:Type) (#eq: equivalence_relation a) 
                                           (mul: op_with_congruence eq)
                                           (up: a->a) (np: a->a) 
  = forall (x:a). (eq x (up x `mul` np x)) /\ (eq (up x `mul` np x) x)
  
[@@"opaque_to_smt"]
let is_normal_part_function (#a:Type) (#eq: equivalence_relation a) 
                            (#mul: op_with_congruence eq) 
                            (unit_part_func: a -> a) 
                            (f: a -> unit_normal_of mul unit_part_func) = 
  is_neutral_invariant mul f /\
  unary_congruence_condition f eq /\
  is_idempotent #a #eq f /\ 
  yields_unit_normals mul unit_part_func f /\
  unary_distributes_over f mul /\
  unit_and_normal_decomposition_property mul unit_part_func f
 
type integral_domain (a: Type) = r:domain a 
{ 
  is_commutative r.multiplication.op /\
  is_unit_part_function r.unit_part_of /\
  is_normal_part_function r.unit_part_of r.normal_part_of    
}

let ring_multiplicative_group_condition (#a:Type) (r: ring a) 
  = forall (x:a). (is_unit x r.multiplication.op <==> ~(is_absorber_of x r.multiplication.op))

type field (a:Type) = r:domain a {
  is_commutative r.multiplication.op /\
  ring_multiplicative_group_condition r
}

unfold let mul_of (#a:Type) (r: ring a) = r.multiplication.op

let is_zero_of #a (r: ring a) p = is_absorber_of p (mul_of r)

let is_valid_denominator_of (#a:Type) (d: integral_domain a) (x: a) = 
  is_unit_normal d.multiplication.op d.unit_part_of x /\ ~(is_zero_of d x)

type valid_denominator_of (#a:Type) (d: integral_domain a) = (t: a{is_valid_denominator_of d t})

type fraction (#a:Type) (d: integral_domain a) = 
 | Fraction : (num: a) -> (den: valid_denominator_of d) -> fraction d

unfold private let fractions_are_equal 
  (#a: Type) (#d: integral_domain a) 
  (x: fraction d) (y: fraction d) = 
   ((x.num `mul_of d` y.den) `d.eq` (x.den `mul_of d` y.num)) 

let fraction_eq (#a:Type) (#d: integral_domain a) : equivalence_relation (fraction d) = 
  admit();
  fractions_are_equal

assume val fraction_add (#a:Type) (#d: integral_domain a) 
  : (f: op_with_congruence (fraction_eq #a #d) { is_associative f /\ is_commutative f })

assume val fraction_mul (#a:Type) (#d: integral_domain a) 
  : (f:op_with_congruence (fraction_eq #a #d){is_commutative f /\ is_associative f})

private let fraction_distributivity_lemma (#p: Type) (#dom: integral_domain p) 
  : Lemma (is_fully_distributive #(fraction dom) fraction_mul (fraction_add #p #dom)) = admit()
  
assume val fraction_one (#a:Type) (d: integral_domain a) 
  : (u: neutral_element_of #(fraction d) fraction_mul { 
        (u.num `d.eq` d.multiplication.neutral) 
      /\ (u.den `d.eq` d.multiplication.neutral)
      /\ is_unit u fraction_mul })

assume val fraction_additive_group (#a:Type) (d: integral_domain a) 
  : (g:commutative_group (fraction d){g.eq == fraction_eq #a #d /\ g.op == fraction_add})

let fraction_absorber (#a:Type) (d: integral_domain a) : absorber_of #(fraction d) fraction_mul = 
  admit();
  (fraction_additive_group d).neutral

assume val fraction_one_is_not_equal_to_fraction_zero (#a: Type) (#d: integral_domain a) 
  : Lemma (~(fraction_eq (fraction_one d) (fraction_absorber d)) /\ 
           ~(fraction_eq (fraction_absorber d) (fraction_one d))) 
           
assume val fraction_nonabsorbers_are_regular (#p:Type) (#d: integral_domain p)
  : Lemma (has_no_absorber_divisors #(fraction d) fraction_mul)
  
assume val fraction_unit_cant_be_absorber (#a:Type) (#d: integral_domain a) (x: units_of fraction_mul) 
  : Lemma (~(is_absorber_of #(fraction d) x #(fraction_eq #a #d) fraction_mul)) 

assume val fraction_nonabsorber_is_unit (#a:Type) (#d: integral_domain a) (x: non_absorber_of #(fraction d) fraction_mul) 
  : Lemma (ensures is_unit x fraction_mul)
  

assume val fraction_multiplicative_almost_group (#a:Type) (#d: integral_domain a) 
  : (m:commutative_monoid (fraction d){m.eq == fraction_eq #a #d /\ m.op == fraction_mul #a #d})

assume val fraction_unit_part_f (#a: Type) (d: integral_domain a) : (fraction d) -> units_of (fraction_mul #a #d)
 
assume val fraction_normal_part_f (#a:Type) (d: integral_domain a) : (fraction d) -> unit_normal_of (fraction_mul #a #d) (fraction_unit_part_f d)
   
assume val fraction_norm_f (#a:Type) (d: integral_domain a) 
  : nat_function_defined_on_non_absorbers (fraction_mul #a #d)
  
#push-options "--ifuel 0 --fuel 0 --z3rlimit 1"
#restart-solver
let fraction_field (#a:Type) (d: integral_domain a) : ring (fraction d) = 

  fraction_distributivity_lemma #a #d;
  fraction_one_is_not_equal_to_fraction_zero #a #d;
  fraction_nonabsorbers_are_regular #a #d;
  FStar.Classical.forall_intro (fraction_unit_cant_be_absorber #a #d);  
  FStar.Classical.forall_intro (fraction_nonabsorber_is_unit #a #d);
  let addition = fraction_additive_group d in
  let multiplication = fraction_multiplicative_almost_group #a #d in
  let eq = fraction_eq #a #d in
  let zero = fraction_absorber d in
  assert (zero == addition.neutral);
  assert (is_fully_distributive multiplication.op addition.op);
  assert (is_absorber_of addition.neutral multiplication.op);  
  { 
    addition = addition;
    multiplication = multiplication;
    eq = eq;
    unit_part_of = fraction_unit_part_f d;
    normal_part_of = fraction_normal_part_f d;
    euclidean_norm = fraction_norm_f d
  }
#pop-options