change handling of array indices

examples/proofs/mutable_map/mutable_map_extra.v

@@ -188,7 +188,9 @@ Section defs.
       assert (probe_ref key (<[n:=ir']> items) = Some (n, ir')) as ->. 2: destruct ir'; naive_solver.
       naive_simpl. revert select (_ ∈ _). rewrite rotate_take_insert;[case_decide|..]; naive_solver lia.
     - rewrite lookup_partial_alter_ne // Hinv1. f_equiv => i. split; naive_simpl.
-      1,3: case_bool_decide; naive_solver. 2: case_bool_decide; [naive_solver|].
+      1: { rewrite list_lookup_insert_Some. naive_solver. }
+      2: { revert select ( <[ _ := _ ]> _ !! _ = Some _). rewrite list_lookup_insert_Some. naive_solver. }
+      2: revert select ( <[ _ := _ ]> _ !! _ = Some _); rewrite list_lookup_insert_Some => -[?|[??]]; [ naive_solver |].
       all: revert select (_ ∈ _); revert select (∀ y, y ∈ _ → _); rewrite rotate_take_insert ?insert_length; [|lia];
         case_decide;[|naive_solver lia].
       + move => ? /(list_elem_of_insert1 _ _ _ _)[?|?]; subst; destruct ir'; naive_solver.

theories/lithium/simpl_instances.v

@@ -399,18 +399,17 @@ Proof.
   - move => Hf /(list_lookup_fmap_inv _ _ _ _)?. naive_solver.
   - move => HT y ? Hl; subst. apply HT. by rewrite list_lookup_fmap Hl.
 Qed.
-
-Global Instance simpl_lookup_insert {A} (l : list A) i j x x':
-  SimplBothRel (=) (<[i := x']> l !! j) (Some x) ((if bool_decide(i = j) then x = x' else l !! j = Some x) ∧ (j < length l)%nat).
+Global Instance simpl_lookup_insert_eq {A} (l : list A) i j x x' `{!CanSolve (i = j)}:
+  SimplBothRel (=) (<[i := x']> l !! j) (Some x) (x = x' ∧ (j < length l)%nat).
 Proof.
-  split.
-  - move => /list_lookup_insert_Some [|].
-    + move => [-> [-> ?]]. by rewrite bool_decide_true.
-    + move => [? H]. rewrite bool_decide_false; last done.
-      split; first done. by apply lookup_lt_Some in H.
-  - destruct (decide (i = j)) as [->|Hne].
-    + rewrite bool_decide_true; last done. move => [-> H]. by rewrite list_lookup_insert.
-    + rewrite bool_decide_false; last done. rewrite list_lookup_insert_ne; by naive_solver.
+  unfold SimplBothRel, CanSolve in *; subst.
+  rewrite list_lookup_insert_Some. naive_solver.
+Qed.
+Global Instance simpl_lookup_insert_neq {A} (l : list A) i j x x' `{!CanSolve (i ≠ j)}:
+  SimplBothRel (=) (<[i := x']> l !! j) (Some x) (l !! j = Some x).
+Proof.
+  unfold SimplBothRel, CanSolve in *; subst.
+  rewrite list_lookup_insert_Some. naive_solver.
 Qed.
 
 Global Instance simpl_learn_insert_some_len_impl {A} l i (x : A) :

theories/typing/array.v

@@ -179,18 +179,19 @@ Section type.
 
 
   Lemma type_place_array l β T ly1 it v (tyv : mtype) tys ly2 K:
-    (∃ i', ⌜ly1 = ly2⌝ ∗ subsume (v ◁ᵥ tyv) (v ◁ᵥ i' @ int it) (∃ i : nat, ⌜i' = i⌝ ∗ ⌜i < length tys⌝%nat ∗
-     ∀ ty, ⌜tys !! i = Some ty⌝ -∗
-    typed_place K (l offset{ly2}ₗ i) β ty (λ l2 β2 ty2 typ, T l2 β2 ty2 (λ t, array ly2 (<[i := typ t]>tys))))) -∗
+    (∃ i, ⌜ly1 = ly2⌝ ∗ subsume (v ◁ᵥ tyv) (v ◁ᵥ i @ int it) (⌜0 ≤ i⌝ ∗ ⌜i < length tys⌝ ∗
+     ∀ ty, ⌜tys !! Z.to_nat i = Some ty⌝ -∗
+    typed_place K (l offset{ly2}ₗ i) β ty (λ l2 β2 ty2 typ, T l2 β2 ty2 (λ t, array ly2 (<[Z.to_nat i := typ t]>tys))))) -∗
     typed_place (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array ly2 tys) T.
   Proof.
-    iDestruct 1 as (i' ->) "HP". iIntros (Φ) "[% Hl] HΦ" => /=. iIntros "Hv".
+    iDestruct 1 as (i ->) "HP". iIntros (Φ) "[% Hl] HΦ" => /=. iIntros "Hv".
     iDestruct ("HP" with "Hv") as "[Hv HP]".
-    iDestruct "HP" as (i -> [ty ?]%lookup_lt_is_Some_2) "HP".
+    iDestruct "HP" as (? Hlen) "HP".
+    have [|ty ?]:= lookup_lt_is_Some_2 tys (Z.to_nat i). lia.
     iDestruct (int_val_to_int_Some with "Hv") as %?.
-    iApply wp_ptr_offset => //. by apply val_to_of_loc. lia.
+    iApply wp_ptr_offset => //. by apply val_to_of_loc.
     iIntros "!#". iExists _. iSplit => //.
-    iDestruct (big_sepL_insert_acc with "Hl") as "[Hl Hc]" => //.
+    iDestruct (big_sepL_insert_acc with "Hl") as "[Hl Hc]" => //. rewrite Z2Nat.id//.
     iApply ("HP" $! ty 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 "[? $]". iSplitR => //. by iApply "Hc".

theories/typing/automation/normalize.v

@@ -22,7 +22,7 @@ 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.
+Hint Rewrite <- @list_fmap_insert : refinedc_rewrite.
 Hint Rewrite <- minus_n_O plus_n_O minus_n_n : refinedc_rewrite.
 Hint Rewrite Nat2Z.id : refinedc_rewrite.
 Hint Rewrite Z2Nat.inj_mul Z2Nat.inj_sub Z2Nat.id using can_solve_tac : refinedc_rewrite.

theories/typing/programs.v

@@ -464,6 +464,21 @@ Section typing.
     SimplifyGoalPlace l (match β with | Own => Own | Shr => Shr end) ty (Some 0%N) :=
     λ T, i2p (simplify_bad_own_state_goal l β ty T).
 
+  (* TODO: generalize this to more simplifications? *)
+  Lemma simplify_hyp_place_Z_to_nat ly l β ty n T:
+    ⌜0 ≤ n⌝ ∗ ((l offset{ly}ₗ n) ◁ₗ{β} ty -∗ T) -∗ simplify_hyp ((l offset{ly}ₗ Z.to_nat n) ◁ₗ{β} ty) T.
+  Proof. iIntros "[% HT]". rewrite Z2Nat.id //. Qed.
+  Global Instance simplify_hyp_place_Z_to_nat_inst ly l β ty n:
+    SimplifyHypPlace (l offset{ly}ₗ Z.to_nat n) β ty (Some 0%N) :=
+    λ T, i2p (simplify_hyp_place_Z_to_nat ly l β ty n T).
+
+  Lemma simplify_goal_place_Z_to_nat ly l β ty n T:
+    ⌜0 ≤ n⌝ ∗ T ((l offset{ly}ₗ n) ◁ₗ{β} ty) -∗ simplify_goal ((l offset{ly}ₗ Z.to_nat n) ◁ₗ{β} ty) T.
+  Proof. iIntros "[% HT]". rewrite Z2Nat.id //. iExists _. iFrame. iIntros "$". Qed.
+  Global Instance simplify_goal_place_Z_to_nat_inst ly l β ty n:
+    SimplifyGoalPlace (l offset{ly}ₗ Z.to_nat n) β ty (Some 0%N) :=
+    λ T, i2p (simplify_goal_place_Z_to_nat ly l β ty n T).
+
   Global Instance simple_subsume_place_id ty : SimpleSubsumePlace ty ty True | 1.
   Proof. iIntros (??) "_ $". Qed.
   Global Instance simple_subsume_place_r_id ty x : SimpleSubsumePlaceR ty ty x x True | 1.