F* Self-contained setoid test

Sandbox.fst

module Sandbox
 
// no complications or wasted verification time is permitted below this line.
#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"

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}

module F = FStar.FunctionalExtensionality

let setoid_f t = F.restricted_t t (fun _ -> bool)

noeq type setoid_t #t (eq: equivalence_relation t) = {
  reflexivity: (x:t) -> Lemma (eq x x);
  symmetry: (x:t) -> (y:t) -> Lemma (eq x y = eq y x);
  transitivity: (x:t) -> (y:t) -> (z:t) -> Lemma ((eq x y && eq y z) ==> eq x z)  
}

let equal #t (s1 s2: setoid_f t) = F.feq s1 s2

let equal_smt #t (s1 s2: setoid_f t) : Lemma (requires equal s1 s2)
                                             (ensures s1 == s2)
                                             [SMTPat (equal s1 s2)] = ()

let s #t #eq (s_t: setoid_t eq) (x:t) : setoid_f t
  = F.on_domain t (fun z -> eq x z)

let setoid_lemma #t #eq (st: setoid_t eq) (x y:t)
  : Lemma (requires eq x y) (ensures s st x == s st y) =
  F.extensionality t (fun _ -> bool) (s st x) (s st y);
  let xs = F.on_domain t (fun z -> eq x z) in
  let ys = F.on_domain t (fun z -> eq y z) in
  reveal_opaque (`%is_reflexive) (is_reflexive #t);
  reveal_opaque (`%is_symmetric) (is_symmetric #t);
  reveal_opaque (`%is_transitive) (is_transitive #t)

let setoid_lemma_backwards #t #eq (st: setoid_t eq) (x y:t)
  : Lemma (requires equal (s st x) (s st y)) (ensures eq x y) = 
  reveal_opaque (`%is_reflexive) (is_reflexive #t);
  assert (forall z. s st x z == s st y z);
  assert (forall z. s st x z == eq x z);
  assert (forall z. s st y z == eq y z) // first 2 asserts only show 
                                   // the human thought process.

[@@"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}

noeq type integral_domain t = 
{
  eq : equivalence_relation t;
  add: op_with_congruence eq;
  mul: op_with_congruence eq;
  add_associativity: (x:t)->(y:t)->(z:t) -> Lemma (add x (add y z) `eq` add (add x y) z);
  mul_associativity: (x:t)->(y:t)->(z:t) -> Lemma (mul x (mul y z) `eq` mul (mul x y) z);
  add_commutativity: (x:t)->(y:t) -> Lemma (eq (add x y) (add y x));
  mul_commutativity: (x:t)->(y:t) -> Lemma (eq (mul x y) (mul y x));
  left_distributivity: (x:t)->(y:t)->(z:t) -> Lemma (mul x (add y z) `eq` add (mul x y) (mul x z));
  right_distributivity: (x:t)->(y:t)->(z:t) -> Lemma (mul (add x y) z `eq` add (mul x z) (mul y z));
  zero: t;
  zero_addition: (x:t) -> Lemma (eq (add x zero) x);
  one: (o:t{not (eq o zero)});
  one_multiplication: (x:t) -> Lemma (eq (mul x one) x);
  neg: unary_op_with_congruence eq;
  neg_law: (x:t) -> Lemma (add x (neg x) `eq` zero);
  domain_law: (x:t)->(y:t) -> Lemma (mul x y `eq` zero <==> (eq x zero || eq y zero))
}

let nonzero_of #t (d: integral_domain t) = (x:t{not (d.eq x d.zero)})

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

let fraction_eq #t (#d: integral_domain t) (f1 f2: fraction d) = 
  d.eq (d.mul f1.num f2.den) (f1.den `d.mul` f2.num)
  
let fraction_eq_reflexivity (#t:Type) (#d:integral_domain t) 
                                   (x: fraction d)
  : Lemma (fraction_eq x x) = d.mul_commutativity x.num x.den


let fraction_eq_symmetry (#t:Type) (#d:integral_domain t) 
                                (x y: fraction d)
  : Lemma (fraction_eq x y == fraction_eq y x)
  = reveal_opaque (`%is_symmetric) (is_symmetric #t);
  reveal_opaque (`%is_transitive) (is_transitive #t);
  let ( * ) (x y: t) = d.mul x y in
  let ( = ) = d.eq in  
  let ab (x y: fraction d) : Lemma (requires fraction_eq x y) (ensures fraction_eq y x) = 
    d.mul_commutativity x.den y.num;
    d.mul_commutativity x.num y.den in 
  Classical.move_requires_2 ab x y;
  Classical.move_requires_2 ab y x

assume val fraction_eq_transitivity (#t:Type) (#d:integral_domain t) (x y z: fraction d)
  : Lemma ((fraction_eq x y && fraction_eq y z) ==> fraction_eq x z)
  
let fraction_equiv #t (d: integral_domain t) : equivalence_relation (fraction d) = 
  reveal_opaque (`%is_symmetric) (is_symmetric #(fraction d));
  reveal_opaque (`%is_reflexive) (is_reflexive #(fraction d));
  reveal_opaque (`%is_transitive) (is_transitive #(fraction d));
  Classical.forall_intro (fraction_eq_reflexivity #t #d);
  Classical.forall_intro_2 (fraction_eq_symmetry #t #d);
  Classical.forall_intro_3 (fraction_eq_transitivity #t #d);
  fraction_eq
  
let fraction_setoid #t (d: integral_domain t) : setoid_t (fraction_equiv d) = {
  reflexivity = fraction_eq_reflexivity;
  symmetry = fraction_eq_symmetry;
  transitivity = fraction_eq_transitivity
}

let ( / ) #t (#d: integral_domain t) (x:t) (y: nonzero_of d) = s (fraction_setoid d) (Fraction x y)

let test #t (#d: integral_domain t) (a:t) (b: nonzero_of d) (p:t) (q:nonzero_of d{fraction_eq (Fraction a b) (Fraction p q)}) =
  let ab = a/b in
  let pq = p/q in
  setoid_lemma (fraction_setoid d) (Fraction a b) (Fraction p q);
  assert (ab == pq);
  ()
  
let test2 #t (#d: integral_domain t) (a:t) (b: nonzero_of d) (p:t) (q:nonzero_of d{equal (a/b) (p/q) }) =
  let ab = a/b in
  let pq = p/q in
  reveal_opaque (`%is_reflexive) (is_reflexive #(fraction d));
  assert (a/b == p/q);
  setoid_lemma_backwards (fraction_setoid d) (Fraction a b) (Fraction p q);
  assert (fraction_eq (Fraction a b) (Fraction p q));
  ()