hacklex

module Sandbox

open FStar.Seq

let under (x: nat) = z:nat{z<x}

let index_for #t (x:seq t) = under (length x)

let rec select_by_key (#key_type: eqtype) 
                      (#value_type: Type) 

hacklex

module FStar.Algebra.Classes.Equatable
 
module TC = FStar.Tactics.Typeclasses

class equatable (t:Type) = {
  eq: t -> t -> bool;
  reflexivity : (x:t -> Lemma (eq x x));
  symmetry: (x:t -> y:t -> Lemma (requires eq x y) 
                               (ensures eq y x));
  transitivity: (x:t -> y:t -> z:t -> Lemma (requires eq x y /\ eq y z) 

hacklex

module Sandbox

module TC = FStar.Tactics.Typeclasses

class equatable (t:Type) = {
  eq: t -> t -> bool;
  reflexivity : (x:t -> Lemma (eq x x));
  symmetry: (x:t -> y:t -> Lemma (requires eq x y) (ensures eq y x));
  transitivity: (x:t -> y:t -> z:t -> Lemma (requires (x `eq` y /\ y `eq` z)) (ensures (x `eq` z)));
} 

hacklex

module Sandbox

module TC = FStar.Tactics.Typeclasses

class equatable (t:Type) = {
  eq: t -> t -> bool;
  reflexivity : (x:t -> Lemma (eq x x));
  symmetry: (x:t -> y:t -> Lemma (requires eq x y) (ensures eq y x));
  transitivity: (x:t -> y:t -> z:t -> Lemma (requires (x `eq` y /\ y `eq` z)) (ensures (x `eq` z)))
} 

hacklex

module Sandbox

module TC = FStar.Tactics.Typeclasses

class has_eq (t:Type) = {
  eq: t -> t -> bool;
  reflexivity : (x:t -> Lemma (eq x x));
  symmetry: (x:t -> y:t -> Lemma (requires eq x y) (ensures eq y x));
  transitivity: (x:t -> y:t -> z:t -> Lemma (requires (x `eq` y /\ y `eq` z)) (ensures (x `eq` z)))
} 

hacklex

module Sandbox

open FStar.List
open FStar.Set

type nat_from (l: set nat) = x:nat{mem x l}

type nonempty_set a = l:set a { l =!= empty }

let list_len = FStar.List.Tot.Base.length 

hacklex

module Sandbox
module CE = FStar.Algebra.CommMonoid.Equiv
module SProp = FStar.Seq.Properties
module SB = FStar.Seq.Base
module SP = FStar.Seq.Permutation

type under (x:nat) = (t:nat{t<x})

let is_left_distributive #c #eq (mul add: CE.cm c eq) = 
  forall (x y z: c). mul.mult x (add.mult y z) `eq.eq` add.mult (mul.mult x y) (mul.mult x z)

hacklex

#push-options "--ifuel 0 --fuel 0 --z3refresh --z3rlimit 20"
let poly_mul_is_associative #c (#r: commutative_ring #c) (p q w: noncompact_poly_over_ring r)
  : Lemma (requires length p>0 /\ length q>0 /\ length w > 0)
          (ensures poly_mul p (poly_mul q w) `ncpoly_eq` poly_mul (poly_mul p q) w) = 
  Classical.forall_intro (ncpoly_eq_is_reflexive_lemma #c #r);
  Classical.forall_intro_2 (ncpoly_eq_is_symmetric_lemma #c #r);
  Classical.forall_intro_3 (ncpoly_eq_is_transitive_lemma #c #r);
  let cm = poly_add_commutative_monoid r in
  let gen_qw = poly_mul_mgen q w in
  let mx_qw = matrix_seq gen_qw in  

hacklex

module MatrixIndexTransform

let ( *) (x y: int) : (t:int{(x>0 /\ y>0) ==> t>0}) = op_Multiply x y

let under (k: pos) = x:nat{x<k}
 
let flattened_index_is_under_flattened_size (m n: pos) (i: under m) (j: under n) 
  : Lemma ((((i*n)+j)) < m*n) = assert (i*n <= (m-1)*n)
   
let get_ij (m n: pos) (i:under m) (j: under n) : under (m*n) = flattened_index_is_under_flattened_size m n i j; i*n + j

hacklex

module Bug
  
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"]