Non-computational setoids

FStar.Algebra.Setoid.fst

module FStar.Algebra.Setoid

module TC = FStar.Tactics.Typeclasses
module F = FStar.FunctionalExtensionality


open FStar.Tactics

class equivalence_relation a = {
  eq : a -> a -> bool;
  reflexivity : (x:a -> Lemma (eq x x));
  symmetry: (x:a -> y:a -> Lemma (x `eq` y <==> y `eq` x));
  transitivity: (x:a -> y:a -> z:a -> Lemma (((eq x y) /\ (eq y z)) ==> eq x z));  
} 

type setoid t {| equivalence_relation t |} = 
  (f:F.restricted_g_t t (fun _ -> bool){ 
    (exists z. f z == true /\ (forall p. f p == eq p z))
  })
 
// ec stands for equivalence class.
let ec #a {| e:equivalence_relation a |} (x:a) : setoid a = 
  reflexivity x;
  Classical.forall_intro_2 e.symmetry;
  Classical.forall_intro_3 e.transitivity;
  F.on_g a (fun t -> eq x t)

let get_x #t {| equivalence_relation t |} (sx: setoid t) : GTot(z:t{sx z == true}) = 
  IndefiniteDescription.indefinite_description_ghost t (fun p -> sx p == true)

let main_lemma #t {| z: equivalence_relation t |} (x y: t)
  : Lemma (requires eq x y)
          (ensures ec x == ec y) =
  Classical.forall_intro_2 z.symmetry;
  Classical.forall_intro_3 z.transitivity;
  assert (forall p. ec x p == ec y p);
  assert (F.feq_g (ec x) (ec y))

class has_mul t = {
  [@@@TC.no_method] has_mul_has_eq : equivalence_relation t;
  mul: t -> t -> t;  
  mul_congruence: (x:t) -> (y:t) -> (z:t) -> (w:t) 
    -> Lemma (requires eq x z /\ eq y w) (ensures eq (mul x y) (mul z w))  
}

class has_mul_eq t = {
  ( * ) : t -> t -> t;
  mul_eq_congruence: (x:t) -> (y:t) -> (z:t) -> (w:t) 
    -> Lemma (requires (x == z) /\ (y == w)) 
            (ensures  (x * y) == (z * w))    
}

instance has_mul_has_eq t (hm: has_mul t) : equivalence_relation t = hm.has_mul_has_eq

class mul_semigroup t = {
  [@@@TC.no_method] mul_semigroup_has_mul : has_mul t;
  mul_associativity: (x:t) -> (y:t) -> (z:t) -> Lemma (eq (mul x (mul y z)) (mul (mul x y) z))
}

instance mul_semigroup_has_mul t (ms: mul_semigroup t) : has_mul t = ms.mul_semigroup_has_mul

class mul_monoid t = {
  [@@@TC.no_method] mul_monoid_sg : mul_semigroup t;
  mul_neutral : t;
  mul_identity : (x:t) -> Lemma ((mul x mul_neutral `eq` x) /\ (mul mul_neutral x `eq` x))
}

class mul_semigroup_eq t = {
  [@@@TC.no_method] mul_semigroup_eq_has_mul_eq : has_mul_eq t;
  mul_eq_associativity: (x:t) -> (y:t) -> (z:t) -> Lemma ((x * (y * z)) == ((x * y) * z))
}

instance mul_semigroup_eq_has_mul_eq t (ms: mul_semigroup_eq t) : has_mul_eq t = ms.mul_semigroup_eq_has_mul_eq

class mul_monoid_eq t = {
  [@@@TC.no_method] mul_monoid_eq_mul_semigroup_eq : mul_semigroup_eq t;
  mul_eq_neutral : t;
  mul_eq_identity : (x:t) -> Lemma (x * mul_eq_neutral == x /\ mul_eq_neutral * x == x)
}

instance has_mul_setoid t {| hm: has_mul t |} 
  : has_mul_eq (setoid t) = 
{
  ( * ) = (fun (x y: setoid t) -> let ex = get_x x in
                               let ey = get_x y in 
                               let r = F.on_g t (fun p -> eq p (hm.mul ex ey)) in
                               reflexivity (hm.mul ex ey);
                               r);
  mul_eq_congruence = fun (x y z w: setoid t) -> ()
}

instance mul_semigroup_setoid t ( mm: mul_semigroup t ) : mul_semigroup_eq (setoid t) = 
  let ( * ) (p q: setoid t) = p * q in
  Classical.forall_intro_3 mm.mul_associativity;
  Classical.forall_intro   mm.mul_semigroup_has_mul.has_mul_has_eq.reflexivity;
  Classical.forall_intro_2 mm.mul_semigroup_has_mul.has_mul_has_eq.symmetry;
  Classical.forall_intro_3 mm.mul_semigroup_has_mul.has_mul_has_eq.transitivity;
  {  
    mul_semigroup_eq_has_mul_eq = has_mul_setoid t;
    mul_eq_associativity = (fun (x y z: setoid t) -> 
      let eq = mm.mul_semigroup_has_mul.has_mul_has_eq.eq in
      let sx = get_x x in
      let sy = get_x y in
      let sz = get_x z in
      let yz = F.on_g t (fun p -> eq p (mul sy sz)) in
      let xy = F.on_g t (fun p -> eq p (mul sx sy)) in
      assert (get_x yz `eq` mul sy sz);    
      assert (F.feq_g (y*z) yz);
      assert (F.feq_g (x*y) xy);    
      // assert (yz == y*z);
      assert (F.feq_g (x*(y*z)) (F.on_g t (fun p -> eq p (mul (get_x x) (get_x yz)))));
      // assert ((x*(y*z)) == F.on_g t (fun p -> eq p (mul (get_x x) (get_x yz))));
      let x_yz = x * (y*z) in
      let xy_z = (x * y)*z in
      // assert (get_x x_yz `eq` mul sx (get_x yz)); 
      // assert (get_x xy_z `eq` mul (get_x xy) sz); 
      mm.mul_semigroup_has_mul.mul_congruence sx (get_x yz) sx (mul sy sz); 
      mm.mul_semigroup_has_mul.mul_congruence (get_x xy) sz (mul sx sy) sz;
      assert (F.feq_g x_yz xy_z)
    )
  }

let test_lemma #t {| sg: mul_semigroup t |} (p q r s: t)
  : Lemma (ensures (ec p * ec q * ec r * ec s == (ec p * ec q) * (ec r * ec s))) =  
  let hm : mul_semigroup_eq (setoid t) = TC.solve in
  hm.mul_eq_associativity (ec p) (ec q) (ec r);  
  Classical.forall_intro_3 hm.mul_eq_associativity