FStar Opaques Example

OpaqueExample.fst

module OpaqueExample

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

let equivalence_is_symmetric (#a:Type) (eq: equivalence_relation a) (x y:a)
  : Lemma (x `eq` y = y `eq` x) = reveal_opaque (`%is_symmetric) (is_symmetric #a)
 
let trans_lemma (#a:Type) (eq: equivalence_relation a) (x y z:a)
  : Lemma (requires (eq x y \/ eq y x) /\ (eq y z \/ eq z y))  
          (ensures (x `eq` z) && (z `eq` x))   
  = reveal_opaque (`%is_transitive) (is_transitive eq);
    reveal_opaque (`%is_symmetric) (is_symmetric eq)

let trans_lemma_4 (#a:Type) (eq: equivalence_relation a) (x y z w:a)
  : Lemma (requires (eq x y \/ eq y x) /\ (eq y z \/ eq z y) /\ (eq z w \/ eq w z))
          (ensures x `eq` w && w `eq` x) = 
  reveal_opaque (`%is_transitive) (is_transitive eq);
  reveal_opaque (`%is_symmetric) (is_symmetric eq)

let trans_lemma_5 (#a:Type) (eq: equivalence_relation a) (x y z w v: a)                            
  : Lemma (requires (eq x y \/ eq y x) /\ (eq y z \/ eq z y) /\ (eq z w \/ eq w z) /\ (eq w v \/ eq v w))
          (ensures eq x v && eq v x) = 
  reveal_opaque (`%is_transitive) (is_transitive eq);
  reveal_opaque (`%is_symmetric) (is_symmetric eq)                                                        

let refl_lemma #a (eq:equivalence_relation a) (x:a) 
  : Lemma (eq x x) = reveal_opaque (`%is_reflexive) (is_reflexive #a) 

let symm_lemma (#a:Type) (eq:equivalence_relation a) (x y:a) 
  : Lemma (eq x y == eq y x) = reveal_opaque (`%is_symmetric) (is_symmetric eq) 

/// Reflexivity, symmetry and transitivity properties are made opaque. That means,
/// FStar does not automatically apply lemmas on equivalence being symmetric, reflexive and transitive.
/// So, I at least write the preconditions in such a way that I would care about `eq` operand order 
/// as little as possible
let congruence_lemma_3 (#a: Type) (#eq: equivalence_relation a) (op: op_with_congruence eq) (e1 e2 z: a)
  : Lemma 
  (requires e1 `eq` e2 \/ e2 `eq` e1) 
  (ensures 
    (e1 `op` z) `eq` (e2 `op` z) /\    
    (e2 `op` z) `eq` (e1 `op` z) /\    
    (z `op` e1) `eq` (z `op` e2) /\
    (z `op` e2) `eq` (z `op` e1)) = reveal_opaque (`%congruence_condition) (congruence_condition op);
                                    reveal_opaque (`%is_symmetric) (is_symmetric eq) 

let congruence_lemma_4 (#a:Type) 
                       (#eq: equivalence_relation a) 
                       (op: op_with_congruence eq)
                       (x y p q: a) 
  : Lemma (requires ((x `eq` p) \/ (p `eq` x)) /\ ((y `eq` q) \/ (q `eq` y)))
          (ensures (((x `op` y) `eq` (p `op` q)) /\ ((y `op` x) `eq` (q `op` p)))) =          
  reveal_opaque (`%congruence_condition) (congruence_condition op);
  reveal_opaque (`%is_transitive) (is_transitive eq);
  congruence_lemma_3 op x p y;
  congruence_lemma_3 op y q p