<commit_before>require import AllCore SmtMap List.
(*---*) import CoreMap.
require import JUtils.

(*-------------------------------------------------------------------- *)

abstract theory MonoArray.

  type elem.
  op dfl : elem.

  op size: int.

  axiom ge0_size : 0 <= size.

  type t.

  op "_.[_]"  : t -> int -> elem.

  op init : (int -> elem) -> t.

  axiom get_out (t:t) i : !(0 <= i < size) => t.[i] = dfl.

  axiom initE (f:int -> elem) i :
    (init f).[i] = if 0 <= i < size then f i else dfl.

  axiom ext_eq (t1 t2: t) :
    (forall x, 0 <= x < size => t1.[x] = t2.[x]) =>
    t1 = t2.

  lemma tP (t1 t2: t) :
    t1 = t2 <=> forall i, 0 <= i < size => t1.[i] = t2.[i].
  proof. by move=> />;apply ext_eq. qed.

  lemma init_ext (f1 f2: int -> elem):
    (forall x, 0 <= x < size => f1 x = f2 x) =>
    init f1 = init f2.
  proof. by move=> h;apply ext_eq => i hi;rewrite !initE hi h. qed.

  (* -------------------------------------------------------------------- *)
  lemma initiE (f:int -> elem) i : 0 <= i < size => (init f).[i] = f i.
  proof. by move=> hi;rewrite initE hi. qed.

  hint simplify initiE.
  (* -------------------------------------------------------------------- *)
  op "_.[_<-_]" (t:t) (i:int) (e:elem) =
    init (fun j => if j = i then e else t.[j])
  axiomatized by setE.

  lemma get_set_if (t:t) (i j :int) (a:elem) :
    t.[i <- a].[j] = if 0 <= i < size /\ j = i then a else t.[j].
  proof.
    rewrite setE initE /=; smt (get_out).
  qed.

  lemma get_setE (t:t) (x y:int) (a:elem) :
    0 <= x < size => t.[x<-a].[y] = if y = x then a else t.[y].
  proof. by move=> hx;rewrite get_set_if hx. qed.

  lemma nosmt set_eqiE (t : t) x y a :
    0 <= x < size => y = x => t.[x <- a].[y] = a.
  proof. by move=> h1 ->;rewrite get_setE. qed.

  lemma nosmt set_neqiE (t : t) x y a :
    0 <= x < size => y <> x => t.[x <- a].[y] = t.[y].
  proof. by move=> h1; rewrite get_setE // => ->. qed.

  hint simplify (set_eqiE, set_neqiE).

  lemma set_out (i : int) (e : elem) (t : t):
    ! (0 <= i < size) => t.[i <- e] = t.
  proof.
    by move=> hi; apply ext_eq => j hj; rewrite get_set_if hi.  
  qed.

  lemma set_neg (i : int) (e : elem) (t : t):
    i < 0 => t.[i<- e] = t.
  proof. move=> hi;apply set_out => /#. qed.

  lemma set_above (i : int) (e : elem) (t : t):
    size <= i => t.[i <- e] = t.
  proof. move=> hi;apply set_out => /#. qed.

  lemma set_set_if (t : t) (k k' : int) (x x' : elem):
       t.[k <- x].[k' <- x']
    =  if   k = k'
       then t.[k' <- x']
       else t.[k' <- x'].[k <- x].
  proof.
    apply ext_eq => i hi;case (k = k') => [<<- | neqk];rewrite !get_set_if /#.
  qed.

  lemma set_set_eq (t : t) (k : int) (x x' : elem):
    t.[k <- x].[k <- x'] = t.[k <- x'].
  proof. by rewrite set_set_if. qed.

  lemma set_set_eq_s (t : t) (k1 k2 : int) (x x' : elem):
    k1 = k2 => t.[k1 <- x].[k2 <- x'] = t.[k2 <- x'].
  proof. move=> ->; apply set_set_eq. qed.

  hint simplify (set_set_eq_s, set_out).

  lemma set_set_swap (t : t) (k k' : int) (x x' : elem):
    k <> k' => t.[k <- x].[k' <- x'] = t.[k' <- x'].[k <- x].
  proof. by rewrite set_set_if => ->. qed.

  lemma set_notmod (t:t) i : t.[i <- t.[i]] = t.
  proof.
    by apply ext_eq => j hj; rewrite get_set_if; case: (0 <= i < size /\ j = i).
  qed.

  (* -------------------------------------------------------------------- *)
  op of_list (l:elem list) =
    init (fun i => nth dfl l i)
  axiomatized by of_listE.

  op to_list (t:t) =
    mkseq (fun i => t.[i]) size.

  lemma to_listE (t:t) : to_list t = map (fun i => t.[i]) (iota_ 0 size).
  proof. done. qed.

  lemma size_to_list (t:t): size (to_list t) = size.
  proof. rewrite /to_listE size_mkseq /max; smt (ge0_size). qed.

  lemma get_of_list (l:elem list) i : 0 <= i < size =>
    (of_list l).[i] = nth dfl l i.
  proof. by move=> hi;rewrite of_listE initiE. qed.

  lemma get_to_list (t : t) i : nth dfl (to_list t) i = t.[i].
  proof.
    rewrite nth_mkseq_if; case:(0 <= i < size) => hi //.
    rewrite get_out //.
  qed.

  lemma of_listK (l : elem list) : size l = size =>
    to_list (of_list l) = l.
  proof.
    move=> h; apply (eq_from_nth dfl); 1:by rewrite size_to_list h.
    move=> i; rewrite size_to_list => hi.
    by rewrite get_to_list // get_of_list.
  qed.

  lemma to_listK : cancel to_list of_list.
  proof.
    move=> t; apply ext_eq => i hi.
    by rewrite get_of_list // get_to_list.
  qed.

  lemma to_list_inj : injective to_list.
  proof. by apply/(can_inj _ _ to_listK). qed.

  hint simplify (get_of_list, get_to_list)@0.
  hint simplify [reduce] to_listK@0.
  hint simplify [reduce] to_listE@1.

  lemma init_of_list f : init f = of_list (map f (iota_ 0 size)).
  proof.
    apply tP => i hi;rewrite get_of_list // (nth_map 0) 1:size_iota 1:/#.
    by rewrite nth_iota // initiE.
  qed.

  (* hint simplify init_of_list@1. *)

  (* -------------------------------------------------------------------- *)
  op create (a:elem) = init (fun (i:int) => a).

  lemma createiE (a:elem) i : 0 <= i < size => (create a).[i] = a.
  proof. by apply initiE. qed.

  lemma createL (a:elem) : create a = of_list (map (fun i => a) (iota_ 0 size)).
  proof. by rewrite /create init_of_list. qed.

  hint simplify (createiE, createL).

  (* -------------------------------------------------------------------- *)
  op map (f: elem -> elem) (t:t) : t =
     init (fun i => f t.[i])
  axiomatized by mapE.

  lemma mapiE f t i : 0 <= i < size => (map f t).[i] = f t.[i].
  proof. by rewrite mapE;apply initiE. qed.

  lemma map_of_list f ws :
    map f (of_list ws) = of_list (mapN f dfl ws size).
  proof.
    by apply tP => i hi; rewrite mapiE // !get_of_list // nth_mapN.
  qed.
<commit_msg>misc. lemmas in JArray<commit_after>require import AllCore SmtMap List.
(*---*) import CoreMap.

require import JUtils.

(*-------------------------------------------------------------------- *)

abstract theory MonoArray.

  type elem.
  op dfl : elem.

  op size: int.

  axiom ge0_size : 0 <= size.

  type t.

  op "_.[_]"  : t -> int -> elem.

  op init : (int -> elem) -> t.

  axiom get_out (t:t) i : !(0 <= i < size) => t.[i] = dfl.

  axiom initE (f:int -> elem) i :
    (init f).[i] = if 0 <= i < size then f i else dfl.

  axiom ext_eq (t1 t2: t) :
    (forall x, 0 <= x < size => t1.[x] = t2.[x]) =>
    t1 = t2.

  lemma tP (t1 t2: t) :
    t1 = t2 <=> forall i, 0 <= i < size => t1.[i] = t2.[i].
  proof. by move=> />;apply ext_eq. qed.

  lemma init_ext (f1 f2: int -> elem):
    (forall x, 0 <= x < size => f1 x = f2 x) =>
    init f1 = init f2.
  proof. by move=> h;apply ext_eq => i hi;rewrite !initE hi h. qed.

  (* -------------------------------------------------------------------- *)
  lemma initiE (f:int -> elem) i : 0 <= i < size => (init f).[i] = f i.
  proof. by move=> hi;rewrite initE hi. qed.

  hint simplify initiE.
  (* -------------------------------------------------------------------- *)
  op "_.[_<-_]" (t:t) (i:int) (e:elem) =
    init (fun j => if j = i then e else t.[j])
  axiomatized by setE.

  lemma get_set_if (t:t) (i j :int) (a:elem) :
    t.[i <- a].[j] = if 0 <= i < size /\ j = i then a else t.[j].
  proof.
    rewrite setE initE /=; smt (get_out).
  qed.

  lemma get_setE (t:t) (x y:int) (a:elem) :
    0 <= x < size => t.[x<-a].[y] = if y = x then a else t.[y].
  proof. by move=> hx;rewrite get_set_if hx. qed.

  lemma nosmt set_eqiE (t : t) x y a :
    0 <= x < size => y = x => t.[x <- a].[y] = a.
  proof. by move=> h1 ->;rewrite get_setE. qed.

  lemma nosmt set_neqiE (t : t) x y a :
    0 <= x < size => y <> x => t.[x <- a].[y] = t.[y].
  proof. by move=> h1; rewrite get_setE // => ->. qed.

  hint simplify (set_eqiE, set_neqiE).

  lemma set_out (i : int) (e : elem) (t : t):
    ! (0 <= i < size) => t.[i <- e] = t.
  proof.
    by move=> hi; apply ext_eq => j hj; rewrite get_set_if hi.  
  qed.

  lemma set_neg (i : int) (e : elem) (t : t):
    i < 0 => t.[i<- e] = t.
  proof. move=> hi;apply set_out => /#. qed.

  lemma set_above (i : int) (e : elem) (t : t):
    size <= i => t.[i <- e] = t.
  proof. move=> hi;apply set_out => /#. qed.

  lemma set_set_if (t : t) (k k' : int) (x x' : elem):
       t.[k <- x].[k' <- x']
    =  if   k = k'
       then t.[k' <- x']
       else t.[k' <- x'].[k <- x].
  proof.
    apply ext_eq => i hi;case (k = k') => [<<- | neqk];rewrite !get_set_if /#.
  qed.

  lemma set_set_eq (t : t) (k : int) (x x' : elem):
    t.[k <- x].[k <- x'] = t.[k <- x'].
  proof. by rewrite set_set_if. qed.

  lemma set_set_eq_s (t : t) (k1 k2 : int) (x x' : elem):
    k1 = k2 => t.[k1 <- x].[k2 <- x'] = t.[k2 <- x'].
  proof. move=> ->; apply set_set_eq. qed.

  hint simplify (set_set_eq_s, set_out).

  lemma set_set_swap (t : t) (k k' : int) (x x' : elem):
    k <> k' => t.[k <- x].[k' <- x'] = t.[k' <- x'].[k <- x].
  proof. by rewrite set_set_if => ->. qed.

  lemma set_notmod (t:t) i : t.[i <- t.[i]] = t.
  proof.
    by apply ext_eq => j hj; rewrite get_set_if; case: (0 <= i < size /\ j = i).
  qed.

  (* -------------------------------------------------------------------- *)
  op of_list (l:elem list) =
    init (fun i => nth dfl l i)
  axiomatized by of_listE.

  op to_list (t:t) =
    mkseq (fun i => t.[i]) size.

  lemma to_listE (t:t) : to_list t = map (fun i => t.[i]) (iota_ 0 size).
  proof. done. qed.

  lemma size_to_list (t:t): size (to_list t) = size.
  proof. rewrite /to_listE size_mkseq /max; smt (ge0_size). qed.

  lemma get_of_list (l:elem list) i : 0 <= i < size =>
    (of_list l).[i] = nth dfl l i.
  proof. by move=> hi;rewrite of_listE initiE. qed.

  lemma get_to_list (t : t) i : nth dfl (to_list t) i = t.[i].
  proof.
    rewrite nth_mkseq_if; case:(0 <= i < size) => hi //.
    rewrite get_out //.
  qed.

  lemma of_listK (l : elem list) : size l = size =>
    to_list (of_list l) = l.
  proof.
    move=> h; apply (eq_from_nth dfl); 1:by rewrite size_to_list h.
    move=> i; rewrite size_to_list => hi.
    by rewrite get_to_list // get_of_list.
  qed.

  lemma to_listK : cancel to_list of_list.
  proof.
    move=> t; apply ext_eq => i hi.
    by rewrite get_of_list // get_to_list.
  qed.

  lemma to_list_inj : injective to_list.
  proof. by apply/(can_inj _ _ to_listK). qed.

  hint simplify (get_of_list, get_to_list)@0.
  hint simplify [reduce] to_listK@0.
  hint simplify [reduce] to_listE@1.

  lemma init_of_list f : init f = of_list (map f (iota_ 0 size)).
  proof.
    apply tP => i hi;rewrite get_of_list // (nth_map 0) 1:size_iota 1:/#.
    by rewrite nth_iota // initiE.
  qed.

  lemma of_listW (p : elem -> bool) (xs : elem list) :
        all p xs
     => size <= size xs
     => forall (i : int), 0 <= i < size => p (of_list xs).[i].
  proof.
  move=> pxs ge128_sz_xs i rg_i; rewrite get_of_list //.
  by move/allP: pxs; apply; rewrite mem_nth /#.
  qed.

  (* hint simplify init_of_list@1. *)

  (* -------------------------------------------------------------------- *)
  op create (a:elem) = init (fun (i:int) => a).

  lemma createiE (a:elem) i : 0 <= i < size => (create a).[i] = a.
  proof. by apply initiE. qed.

  lemma createL (a:elem) : create a = of_list (map (fun i => a) (iota_ 0 size)).
  proof. by rewrite /create init_of_list. qed.

  hint simplify (createiE, createL).

  (* -------------------------------------------------------------------- *)
  op map (f: elem -> elem) (t:t) : t =
     init (fun i => f t.[i])
  axiomatized by mapE.

  lemma mapiE f t i : 0 <= i < size => (map f t).[i] = f t.[i].
  proof. by rewrite mapE;apply initiE. qed.

  lemma map_of_list f ws :
    map f (of_list ws) = of_list (mapN f dfl ws size).
  proof.
    by apply tP => i hi; rewrite mapiE // !get_of_list // nth_mapN.
  qed.

{'fraction_non_alphanumeric': 0.24566498676005807, 'fraction_numerical': 0.010250277611685317, 'mean_word_length': 1.749002113172106, 'pattern_counts': {'":': 0, '<': 134, '<?xml version=': 0, '>': 152, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7342016', 'n_tokens_mistral': 5075, 'n_tokens_neox': 4703, 'n_words': 1533}