remove array iterator

examples/mutable_map.c

@@ -70,8 +70,9 @@ void fsm_realloc_if_necessary(struct fixed_size_map *m);
 [[rc::requires("[alloc_initialized]")]]
 [[rc::ensures("m @ &own<{∅, replicate len Empty, len} @ fixed_size_map> ")]]
  [[rc::lemmas("fsm_invariant_init")]]
+ [[rc::tactics("all: try by apply/list_subequiv_split; solve_goal.")]]
  [[rc::tactics("all: try by rewrite length_filter_replicate_True; solve_goal.")]]
- [[rc::tactics("all: try by f_equal; solve_goal.")]]
+ [[rc::tactics("all: try by rewrite !replicate_O; solve_goal.")]]
 void fsm_init(struct fixed_size_map *m, size_t len) {
   size_t i;
   void *storage = alloc_array(sizeof(struct item), len);
@@ -81,9 +82,9 @@ void fsm_init(struct fixed_size_map *m, size_t len) {
 
   [[rc::exists("i : nat")]]
   [[rc::inv_vars("i : i @ int<size_t>")]]
-  [[rc::inv_vars("m : m @ &own<struct<struct_fixed_size_map, &own<array_iterator<" \
-                "struct_item, i, len, {replicate i Empty `at_type` item}," \
-                 "uninit<struct_item>, {replicate (len - i)%nat (uninit (struct_item))}>>, len @ int<size_t>, len @ int<size_t>>> ")]]
+  [[rc::inv_vars("m : m @ &own<struct<struct_fixed_size_map, &own<array<struct_item," \
+                "{replicate i Empty `at_type` item ++ replicate (len - i)%nat (uninit (struct_item))}>>," \
+                 "len @ int<size_t>, len @ int<size_t>>>")]]
   [[rc::constraints("{i <= len}")]]
   for(i = 0; i < len; i += 1) {
     (*m->items)[i].tag = ITEM_EMPTY;
@@ -213,12 +214,7 @@ size_t compute_min_count(size_t len) {
  [[rc::tactics("all: try by apply: fsm_copy_entries_not_add; solve_goal.")]]
  [[rc::tactics("all: try by apply: fsm_copy_entries_add; solve_goal.")]]
  [[rc::tactics("all: try by apply: fsm_copy_entries_id; solve_goal.")]]
- [[rc::tactics("all: try (apply list_subequiv_split; [solve_goal|]).")]]
- [[rc::tactics("all: try rewrite !firstn_app !take_replicate !skipn_app !drop_replicate !replicate_length !fmap_drop !drop_drop -minus_n_n.")]]
- [[rc::tactics("all: try split; f_equal.")]]
- [[rc::tactics("all: try by f_equal; lia.")]]
- [[rc::tactics("all: try have ->:(i - (i + 1) = 0)%nat by lia.")]]
- [[rc::tactics("all: try by rewrite !firstn_O.")]]
+ [[rc::tactics("all: try by apply list_subequiv_split; [solve_goal|]; normalize_and_simpl_goal; try solve_goal; f_equal; solve_goal.")]]
 void fsm_realloc_if_necessary(struct fixed_size_map *m) {
   if(compute_min_count(m->length) <= m->count) {
     return;

examples/proofs/mutable_map/generated_proof_fsm_init.v

@@ -20,7 +20,7 @@ Section proof_fsm_init.
         arg_len ◁ₗ (len @ (int (size_t))) ∗
         local_storage ◁ₗ uninit LPtr ∗
         local_i ◁ₗ (i @ (int (size_t))) ∗
-        arg_m ◁ₗ (m @ (&own (struct (struct_fixed_size_map) [@{type} &own (array_iterator (struct_item) (i) (len) (replicate i Empty `at_type` item) (uninit (struct_item)) (replicate (len - i)%nat (uninit (struct_item)))) ; len @ (int (size_t)) ; len @ (int (size_t)) ]))) ∗
+        arg_m ◁ₗ (m @ (&own (struct (struct_fixed_size_map) [@{type} &own (array (struct_item) (replicate i Empty `at_type` item ++ replicate (len - i)%nat (uninit (struct_item)))) ; len @ (int (size_t)) ; len @ (int (size_t)) ]))) ∗
         ⌜i <= len⌝
     ]> $
       ∅
@@ -33,8 +33,9 @@ Section proof_fsm_init.
       all: print_typesystem_goal "fsm_init" "#1".
     Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
     all: try by apply: fsm_invariant_init; solve_goal.
+    all: try by apply/list_subequiv_split; solve_goal.
     all: try by rewrite length_filter_replicate_True; solve_goal.
-    all: try by f_equal; solve_goal.
+    all: try by rewrite !replicate_O; solve_goal.
     all: print_sidecondition_goal "fsm_init".
   Qed.
 End proof_fsm_init.

examples/proofs/mutable_map/generated_proof_fsm_realloc_if_necessary.v

@@ -55,12 +55,7 @@ Section proof_fsm_realloc_if_necessary.
     all: try by apply: fsm_copy_entries_not_add; solve_goal.
     all: try by apply: fsm_copy_entries_add; solve_goal.
     all: try by apply: fsm_copy_entries_id; solve_goal.
-    all: try (apply list_subequiv_split; [solve_goal|]).
-    all: try rewrite !firstn_app !take_replicate !skipn_app !drop_replicate !replicate_length !fmap_drop !drop_drop -minus_n_n.
-    all: try split; f_equal.
-    all: try by f_equal; lia.
-    all: try have ->:(i - (i + 1) = 0)%nat by lia.
-    all: try by rewrite !firstn_O.
+    all: try by apply list_subequiv_split; [solve_goal|]; normalize_and_simpl_goal; try solve_goal; f_equal; solve_goal.
     all: print_sidecondition_goal "fsm_realloc_if_necessary".
   Qed.
 End proof_fsm_realloc_if_necessary.

theories/lang/base.v

@@ -117,6 +117,10 @@ Proof using Type*. move => ?. by apply: partial_alter_ext => ? <-. Qed.
 
 End theorems.
 
+Lemma replicate_O {A} (x : A) n:
+  n = 0%nat -> replicate n x = [].
+Proof. by move => ->. Qed.
+
 Global Instance set_unfold_replicate A (x y : A) n:
   SetUnfoldElemOf x (replicate n y) (x = y ∧ n ≠ 0%nat).
 Proof. constructor. apply elem_of_replicate. Qed.

theories/lithium/simpl_instances.v

@@ -286,12 +286,18 @@ Global Instance simpl_fmap_cons_impl {A B} (l : list A) l2 (f : A → B):
   SimplImplRel (=) true (f <$> l) (x :: l2) (λ T, ∀ x' l2', l = x' :: l2' → f x' = x → f <$> l2' = l2 → T).
 Proof. split; last naive_solver. intros ? ?%fmap_cons_inv. naive_solver. Qed.
 Global Instance simpl_fmap_app_and {A B} (l : list A) l1 l2 (f : A → B):
-  SimplAndRel (=) (f <$> l) (l1 ++ l2) (λ T, ∃ l1' l2', l = l1' ++ l2' ∧ f <$> l1' = l1 ∧ f <$> l2' = l2 ∧ T).
+  SimplAndRel (=) (f <$> l) (l1 ++ l2) (λ T, f <$> take (length l1) l = l1 ∧ f <$> drop (length l1) l = l2 ∧ T).
 Proof.
   split.
-  - move => [?[?[?[?[??]]]]]; subst. rewrite fmap_app. naive_solver.
-  - move => [/fmap_app_inv]. naive_solver.
+  - move => [Hl1 [Hl2 ?]]; subst. split => //.
+    rewrite -Hl1 -fmap_app fmap_length take_length_le ?take_drop //.
+    rewrite -Hl1 fmap_length take_length. lia.
+  - move => [/fmap_app_inv [? [? [? [? Hfmap]]]] ?]; subst.
+    by rewrite fmap_length take_app drop_app.
 Qed.
+Global Instance simpl_fmap_assume_inj_Unsafe {A B} (l1 l2 : list A) (f : A → B) `{!AssumeInj (=) (=) f}:
+  SimplAndUnsafe true (f <$> l1 = f <$> l2) (λ T, l1 = l2 ∧ T).
+Proof. move => T [-> ?]. naive_solver. Qed.
 
 Global Instance simpl_replicate_app_and {A} (l1 l2 : list A) x n:
   SimplAndRel (=) (replicate n x) (l1 ++ l2) (λ T, ∃ n', shelve_hint (n' ≤ n)%nat ∧ l1 = replicate n' x ∧ l2 = replicate (n - n') x ∧ T).

theories/typing/array.v

@@ -198,81 +198,4 @@ Section type.
   Global Instance type_place_array_inst l β ly1 it v (tyv : mtype) tys ly2 K:
     TypedPlace (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array ly2 tys):=
     λ T, i2p (type_place_array l β T ly1 it v tyv tys ly2 K).
-
-  (*** array iterator *)
-  Program Definition array_iterator (ly : layout) (i : nat) (len : nat) (tys1 : list type) (ty : type) (tys2 : list type) : type := {|
-    ty_own β l := ⌜i ≤ len⌝%nat ∗ ⌜length tys1 = i⌝ ∗ ⌜length tys2 = (len - i)%nat⌝ ∗ l ◁ₗ{β} array ly (<[i := ty]> (tys1 ++ tys2))
-  |}%I.
-  Next Obligation. iIntros (?????????). iDestruct 1 as (???) "Ha". do 3 iSplitR => //. by iApply ty_share. Qed.
-
-  Lemma simplify_goal_array_iterator_0 l β T ly len tys1 tys2 ty:
-    T (⌜tys1 = []⌝ ∗ ⌜length tys2 = len⌝ ∗ ⌜(0 < len)%nat → tys2 !! 0%nat = Some ty⌝ ∗ l ◁ₗ{β} array ly tys2) -∗
-      simplify_goal (l◁ₗ{β} array_iterator ly 0%nat len tys1 ty tys2) T.
-  Proof.
-    iIntros "HT". iExists _. iFrame. iIntros "[-> [<- [% [$ Ha]]]]".
-    repeat iSplit; try iPureIntro => //. lia. by rewrite -minus_n_O.
-    rewrite /= list_insert_id'; eauto.
-  Qed.
-  Global Instance simplify_goal_array_iterator_0_inst l β ly len tys1 tys2 ty:
-    SimplifyGoalPlace l β (array_iterator ly 0%nat len tys1 ty tys2)%I (Some 0%N) :=
-    λ T, i2p (simplify_goal_array_iterator_0 l β T ly len tys1 tys2 ty).
-
-  Lemma type_place_array_iterator l β T ly1 it v (tyv : mtype) (i : nat) len tys1 ty tys2 ly2 K:
-    ⌜i < len⌝%nat ∗ ⌜ly1 = ly2⌝ ∗ subsume (v ◁ᵥ tyv) (v ◁ᵥ i @ int it) (
-    typed_place K (l offset{ly2}ₗ i) β ty (λ l2 β2 ty2 typ, T l2 β2 ty2 (λ t, array_iterator ly2 i len tys1 (typ t) tys2))) -∗
-    typed_place (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array_iterator ly2 i len tys1 ty tys2) T.
-  Proof.
-    iIntros "[% [<- HP]]" (Φ) "[% [<- [% [% Hl]]]] HΦ" => /=. iIntros "Hv".
-    (* TODO: this is the same as type_place_array. Figure out if we can reuse the proof. *)
-    iDestruct ("HP" with "Hv") as "[Hv HP]".
-    iDestruct (int_val_to_int_Some with "Hv") as %?.
-    iApply wp_ptr_offset => //. by apply val_to_of_loc. lia.
-    iIntros "!#". iExists _. iSplit => //.
-    iDestruct (big_sepL_insert_acc with "Hl") as "[Hl Hc]" => //.
-      by apply list_lookup_insert; rewrite app_length; lia.
-    iApply ("HP" with "Hl"). iIntros (l' ty2 β2 typ R) "Hl' Htyp HT".
-    iApply ("HΦ" with "Hl' [-HT] HT"). iIntros (ty') "Hl'".
-    iMod ("Htyp" with "Hl'") as "[? $]". repeat  iSplitR => //.
-    setoid_rewrite list_insert_insert. by iApply ("Hc").
-  Qed.
-  Global Instance type_place_array_iterator_inst l β ly1 it v (tyv : mtype) (i : nat) len tys1 ty tys2 ly2 K:
-    TypedPlace (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array_iterator ly2 i len tys1 ty tys2) :=
-    λ T, i2p (type_place_array_iterator l β T ly1 it v tyv i len tys1 ty tys2 ly2 K).
-
-  Lemma subsume_array_iterator_next l β T i1 i2 len ly tys11 ty1 tys21 tys12 ty2 tys22 `{!CanSolve (i2 = S i1)}:
-    (∃ ty1', ⌜tys12 = tys11 ++ [ty1']⌝ ∗ ⌜length tys21 > 0⌝%nat ∗ ⌜tail tys21 = tys22⌝ ∗
-         ⌜(i2 < len)%nat → tys22 !! 0%nat = Some ty2⌝ ∗
-        subsume ((l offset{ly}ₗ i1) ◁ₗ{β} ty1) ((l offset{ly}ₗ i1) ◁ₗ{β} ty1') T) -∗
-    subsume (l ◁ₗ{β} array_iterator ly i1 len tys11 ty1 tys21) (l ◁ₗ{β} array_iterator ly i2 len tys12 ty2 tys22) T.
-  Proof.
-    unfold CanSolve in *; subst.
-    iDestruct 1 as (ty1' -> Htys21 <- Hty2) "Hsub". destruct tys21 as [|ty' tys21]; simpl in *. lia.
-    iDestruct 1 as (? <- Hlen) "Ha". rewrite insert_app_r_alt // -minus_n_n/=.
-    iDestruct (array_get_type (length tys11) with "Ha") as "[Hty1 Ha]". by rewrite lookup_app_r // -minus_n_n //.
-    iDestruct ("Hsub" with "Hty1") as "[Hty1 $]".
-    iSplit; [|iSplit]; [..|iSplit]; try iPureIntro; simpl in *. lia. by rewrite app_length /=; lia. lia.
-    iDestruct (array_put_type with "Hty1 Ha") as "Ha".
-    rewrite list_insert_insert insert_app_r_alt // insert_app_r_alt ?app_length /=; last lia.
-    rewrite  -minus_n_n/=. have -> : (S (length tys11) - (length tys11 + 1) = 0)%nat by lia.
-    destruct tys21 as [|ty'' tys21] => /=. by rewrite app_nil_r.
-    simpl in *. rewrite -app_assoc cons_middle.
-    by have [->]: Some ty'' = Some ty2 by eauto with lia.
-  Qed.
-  Global Instance subsume_array_iterator_next_inst l β i1 i2 len ly tys11 ty1 tys21 tys12 ty2 tys22 `{!CanSolve (i2 = S i1)}:
-    SubsumePlace l β (array_iterator ly i1 len tys11 ty1 tys21) (array_iterator ly i2 len tys12 ty2 tys22) :=
-    λ T, i2p (subsume_array_iterator_next l β T i1 i2 len ly tys11 ty1 tys21 tys12 ty2 tys22).
-
-  (* TODO: support not iterating until the end? *)
-  Lemma subsume_array_iterator_array l β T i len ly tys1 ty tys2 tys':
-    ⌜len ≤ i⌝%nat ∗ ⌜tys1 = tys'⌝ ∗ (⌜i = len⌝ -∗ T) -∗
-    subsume (l ◁ₗ{β} array_iterator ly i len tys1 ty tys2) (l ◁ₗ{β} array ly tys') T.
-  Proof.
-    iIntros "(%&->&HT)".
-    iDestruct 1 as (? <- Hlen) "Ha". iDestruct ("HT" with "[]") as "$". by iPureIntro; lia.
-    rewrite insert_app_r_alt // -minus_n_n/=.
-    destruct tys2; simpl in *. by rewrite app_nil_r. lia.
-  Qed.
-  Global Instance subsume_array_iterator_array_inst l β i len ly tys1 ty tys2 tys':
-    SubsumePlace l β (array_iterator ly i len tys1 ty tys2) (array ly tys') :=
-    λ T, i2p (subsume_array_iterator_array l β T i len ly tys1 ty tys2 tys').
 End type.

theories/typing/automation/normalize.v

@@ -13,10 +13,13 @@ Lemma NatZmul_add_distr_r (n1 n2 : nat) z:
 Proof. lia. Qed.
 
 Hint Rewrite @drop_0 @take_ge using can_solve_tac : refinedc_rewrite.
+Hint Rewrite @take_app_le @drop_app_ge using can_solve_tac : refinedc_rewrite.
 Hint Rewrite @insert_length @app_length @fmap_length @rotate_length @replicate_length @drop_length : refinedc_rewrite.
+Hint Rewrite <- @fmap_take @fmap_drop : refinedc_rewrite.
 Hint Rewrite @list_insert_fold : refinedc_rewrite.
 Hint Rewrite @list_insert_insert : refinedc_rewrite.
-Hint Rewrite @tail_replicate : refinedc_rewrite.
+Hint Rewrite @drop_drop : refinedc_rewrite.
+Hint Rewrite @tail_replicate @take_replicate @drop_replicate : refinedc_rewrite.
 Hint Rewrite <- @app_assoc @cons_middle : refinedc_rewrite.
 Hint Rewrite @app_nil_r @rev_involutive : refinedc_rewrite.
 Hint Rewrite @list_fmap_insert : refinedc_rewrite.