small steps towards improving subsume_list

examples/mutable_map.c

@@ -140,6 +140,7 @@ size_t fsm_probe(struct fixed_size_map *m, size_t key) {
 [[rc::ensures("{count - 1 <= count2}", "{length items <= length items2}")]]
  [[rc::lemmas("fsm_invariant_insert")]]
  [[rc::tactics("all: try by erewrite length_filter_insert => //; solve_goal.")]]
+ [[rc::tactics("all: try by eexists _; solve_goal.")]]
 void *fsm_insert(struct fixed_size_map *m, size_t key, void *value) {
     fsm_realloc_if_necessary(m);
     size_t slot_idx = fsm_probe(m, key);
@@ -165,6 +166,7 @@ void *fsm_insert(struct fixed_size_map *m, size_t key, void *value) {
 [[rc::ensures("own m : {alter (λ _, place p) key mp, items2, count} @ fixed_size_map")]]
  [[rc::lemmas("fsm_invariant_alter")]]
  [[rc::tactics("all: try by erewrite length_filter_insert => //; solve_goal.")]]
+ [[rc::tactics("all: try by eexists _; solve_goal.")]]
  [[rc::tactics("all: try by apply inhabitant.")]]
 void *fsm_get(struct fixed_size_map *m, size_t key) {
     size_t slot_idx = fsm_probe(m, key);
@@ -184,6 +186,7 @@ void *fsm_get(struct fixed_size_map *m, size_t key) {
 [[rc::ensures("own m : {delete key mp, items2, count} @ fixed_size_map")]]
  [[rc::lemmas("fsm_invariant_delete")]]
  [[rc::tactics("all: try by erewrite length_filter_insert => //; solve_goal.")]]
+ [[rc::tactics("all: try by eexists _; solve_goal.")]]
 void *fsm_remove(struct fixed_size_map *m, size_t key) {
     void* removed;
     size_t slot_idx = fsm_probe(m, key);

examples/proofs/mutable_map/generated_proof_fsm_get.v

@@ -25,6 +25,7 @@ Section proof_fsm_get.
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: try by apply: fsm_invariant_alter; solve_goal.
     all: try by erewrite length_filter_insert => //; solve_goal.
+    all: try by eexists _; solve_goal.
     all: try by apply inhabitant.
     all: print_sidecondition_goal "fsm_get".
   Qed.

examples/proofs/mutable_map/generated_proof_fsm_insert.v

@@ -26,6 +26,7 @@ Section proof_fsm_insert.
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: try by apply: fsm_invariant_insert; solve_goal.
     all: try by erewrite length_filter_insert => //; solve_goal.
+    all: try by eexists _; solve_goal.
     all: print_sidecondition_goal "fsm_insert".
   Qed.
 End proof_fsm_insert.

examples/proofs/mutable_map/generated_proof_fsm_remove.v

@@ -25,6 +25,7 @@ Section proof_fsm_remove.
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: try by apply: fsm_invariant_delete; solve_goal.
     all: try by erewrite length_filter_insert => //; solve_goal.
+    all: try by eexists _; solve_goal.
     all: print_sidecondition_goal "fsm_remove".
   Qed.
 End proof_fsm_remove.

examples/proofs/mutable_map/mutable_map_extra.v

@@ -231,7 +231,7 @@ Section defs.
   Qed.
 
   Global Instance simpl_lookup_fsm_map_and mp key items n ir o `{!FastDone (fsm_invariant mp items)} `{!FastDone (probe_ref key items = Some (n, ir))}:
-      SimplAndRel (=) (mp !! key) o (λ T, item_ref_to_ty ir = o ∧ T).
+      SimplBothRel (=) (mp !! key) o (item_ref_to_ty ir = o).
   Proof. unfold FastDone in *. by rewrite (fsm_invariant_lookup _ items _ n ir (item_ref_to_ty ir)). Qed.
 
   Global Instance simpl_fsm_invariant_and mp1 mp2 items `{!IsProtected mp1} `{!FastDone (fsm_invariant mp2 items)}:

examples/proofs/paper_example_2_1/generated_proof_thread_safe_alloc.v

@@ -13,8 +13,8 @@ Section proof_thread_safe_alloc.
   Lemma type_thread_safe_alloc (global_data global_lock global_alloc global_sl_lock global_sl_unlock : loc) :
     global_locs !! "data" = Some global_data →
     global_locs !! "lock" = Some global_lock →
-    global_initialized_types !! "data" = Some (GT lock_id (λ 'lid, (tylocked (lid) ("data") (mem_t)) : type)) →
-    global_initialized_types !! "lock" = Some (GT lock_id (λ 'lid, (spinlock (lid)) : type)) →
+    global_initialized_types !! "data" = Some (GT lock_id (λ 'lid, (tylocked (lid) ("data") (mem_t)) : type)%I) →
+    global_initialized_types !! "lock" = Some (GT lock_id (λ 'lid, (spinlock (lid)) : type)%I) →
     global_alloc ◁ᵥ global_alloc @ function_ptr type_of_alloc -∗
     global_sl_lock ◁ᵥ global_sl_lock @ function_ptr type_of_sl_lock -∗
     global_sl_unlock ◁ᵥ global_sl_unlock @ function_ptr type_of_sl_unlock -∗

frontend/coq_pp.ml

@@ -1175,7 +1175,7 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
       match List.find_opt (fun (name, _) -> name = f) ast.global_vars with
       | Some(_, Some(global_type)) ->
          let (param_names, param_types) = List.split global_type.ga_parameters in
-          pp "global_initialized_types !! \"%s\" = Some (GT %a (λ '%a, %a : type)) →@;"
+          pp "global_initialized_types !! \"%s\" = Some (GT %a (λ '%a, %a : type)%%I) →@;"
             f pp_prod param_types (pp_as_tuple pp_str) param_names (pp_type_expr_guard None Guard_none) global_type.ga_type
       | _                 -> ()
     in

theories/lithium/classes.v

@@ -128,13 +128,14 @@ Definition subsume {Σ} (P1 P2 T : iProp Σ) : iProp Σ :=
   P1 -∗ P2 ∗ T.
 Class Subsume {Σ} (P1 P2 : iProp Σ) : Type :=
   subsume_proof T : iProp_to_Prop (subsume P1 P2 T).
-Definition subsume_list {Σ} A (l1 l2 : list A) (f : nat → A → iProp Σ) (T : iProp Σ) : iProp Σ :=
-  ⌜length l1 = length l2⌝ -∗ ([∗ list] i↦x∈l1, f i x) -∗ ([∗ list] i↦x∈l2, f i x) ∗ T.
-Class SubsumeList {Σ} A (l1 l2 : list A) (f : nat → A → iProp Σ) :  Type :=
-  subsume_list_proof T : iProp_to_Prop (subsume_list A l1 l2 f T).
+Definition subsume_list {Σ} A (ig : list nat) (l1 l2 : list A) (f : nat → A → iProp Σ) (T : iProp Σ) : iProp Σ :=
+  ([∗ list] i↦x∈l1, if bool_decide (i ∈ ig) then True%I else f i x) -∗
+       ⌜length l1 = length l2⌝ ∗ ([∗ list] i↦x∈l2, if bool_decide (i ∈ ig) then True%I else f i x) ∗ T.
+Class SubsumeList {Σ} A (ig : list nat) (l1 l2 : list A) (f : nat → A → iProp Σ) :  Type :=
+  subsume_list_proof T : iProp_to_Prop (subsume_list A ig l1 l2 f T).
 
 Hint Mode Subsume + + ! : typeclass_instances.
-Hint Mode SubsumeList + + + + ! : typeclass_instances.
+Hint Mode SubsumeList + + + + + ! : typeclass_instances.
 
 (** ** Instances *)
 Lemma subsume_id {Σ} (P : iProp Σ) T:
@@ -164,27 +165,35 @@ Global Instance subsume_simplify_inst {Σ} (P1 P2 : iProp Σ) o1 o2 `{!SimplifyH
   Subsume P1 P2 | 1000 :=
   λ T, i2p (subsume_simplify P1 P2 T o1 o2).
 
-Lemma subsume_list_eq {Σ} A (l1 l2 : list A) (f : nat → A → iProp Σ) (T : iProp Σ) :
-  ⌜l1 = l2⌝ ∗ T -∗ subsume_list A l1 l2 f T.
-Proof. by iIntros "[-> $] _ $". Qed.
-Global Instance subsume_list_eq_inst {Σ} A l1 l2 f:
-  SubsumeList A l1 l2 f | 1000 :=
-  λ T : iProp Σ, i2p (subsume_list_eq A l1 l2 f T).
-
-Lemma subsume_list_trivial_eq {Σ} A (l : list A) (f : nat → A → iProp Σ) (T : iProp Σ) :
-  T -∗ subsume_list A l l f T.
-Proof. iIntros "$ _ $". Qed.
-Global Instance subsume_list_trivial_eq_inst {Σ} A l f:
-  SubsumeList A l l f | 5 :=
-  λ T : iProp Σ, i2p (subsume_list_trivial_eq A l f T).
-
-Lemma subsume_list_cons {Σ} A (x1 x2 : A) (l1 l2 : list A) (f : nat → A → iProp Σ) (T : iProp Σ) :
-  subsume (f 0%nat x1) (f 0%nat x2) (subsume_list A l1 l2 (λ i, f (S i)) T) -∗
-          subsume_list A (x1 :: l1) (x2 :: l2) f T.
+Lemma subsume_list_eq {Σ} A ig (l1 l2 : list A) (f : nat → A → iProp Σ) (T : iProp Σ) :
+  ⌜l1 = l2⌝ ∗ T -∗ subsume_list A ig l1 l2 f T.
+Proof. by iIntros "[-> $] $". Qed.
+Global Instance subsume_list_eq_inst {Σ} A ig l1 l2 f:
+  SubsumeList A ig l1 l2 f | 1000 :=
+  λ T : iProp Σ, i2p (subsume_list_eq A ig l1 l2 f T).
+
+Lemma subsume_list_trivial_eq {Σ} A ig (l : list A) (f : nat → A → iProp Σ) (T : iProp Σ) :
+  T -∗ subsume_list A ig l l f T.
+Proof. by iIntros "$ $". Qed.
+Global Instance subsume_list_trivial_eq_inst {Σ} A ig l f:
+  SubsumeList A ig l l f | 5 :=
+  λ T : iProp Σ, i2p (subsume_list_trivial_eq A ig l f T).
+
+Lemma subsume_list_cons_l {Σ} A ig (x1 : A) (l1 l2 : list A) (f : nat → A → iProp Σ) (T : iProp Σ) :
+  (⌜0 ∉ ig⌝ ∗ ∃ x2 l2', ⌜l2 = x2 :: l2'⌝ ∗
+      subsume (f 0%nat x1) (f 0%nat x2) (subsume_list A (pred <$> ig) l1 l2' (λ i, f (S i)) T)) -∗
+   subsume_list A ig (x1 :: l1) l2 f T.
 Proof.
-  iIntros "Hs Hlen". iDestruct "Hlen" as %Hlen. inversion Hlen. rewrite !big_sepL_cons.
-  iIntros "[H0 H]". iDestruct ("Hs" with "H0") as "[$ Hs]". by iApply "Hs".
+  iIntros "[% Hs]". iDestruct "Hs" as (???) "Hs". subst.
+  rewrite /subsume_list !big_sepL_cons /=.
+  case_bool_decide => //. iIntros "[H0 H]".
+  iDestruct ("Hs" with "H0") as "[$ Hs]".
+  iDestruct ("Hs" with "[H]") as (->) "[H $]"; [|iSplit => //].
+  all: iApply (big_sepL_impl with "H"); iIntros "!#" (???) "?".
+  all: case_bool_decide as Hx1 => //; case_bool_decide as Hx2 => //; contradict Hx2.
+  - set_unfold. eexists _. split; [|done]. done.
+  - by move: Hx1 => /(elem_of_list_fmap_2 _ _ _)[[|?]//=[->?]].
 Qed.
-Global Instance subsume_list_cons_inst {Σ} A x1 x2 l1 l2 f:
-  SubsumeList A (x1 :: l1) (x2 :: l2) f | 40 :=
-  λ T : iProp Σ, i2p (subsume_list_cons A x1 x2 l1 l2 f T).
+Global Instance subsume_list_cons_inst {Σ} A ig x1 l1 l2 f:
+  SubsumeList A ig (x1 :: l1) l2 f | 40 :=
+  λ T : iProp Σ, i2p (subsume_list_cons_l A ig x1 l1 l2 f T).

theories/lithium/interpreter.v

@@ -385,7 +385,14 @@ Ltac unfold_instantiated_evars :=
 Ltac solve_protected_eq :=
   (* intros because it is less aggressive than move => * *)
   intros; repeat rewrite protected_eq;
-  try ( liUnfoldAllEvars; match goal with |- ?a = ?b => unify a b with typeclass_instances end );
+  try (
+      liUnfoldAllEvars;
+      lazymatch goal with |- ?a = ?b => unify a b with typeclass_instances end;
+      (* For some weird reason we need to do this twice that the has_evar check works *)
+      lazymatch goal with |- ?a = ?b => unify a b with typeclass_instances end;
+      lazymatch goal with
+      | |- ?g => assert_fails (has_evar g)
+      end);
   exact: eq_refl.
 
 Ltac liEnforceInvariantAndUnfoldInstantiatedEvars :=
@@ -396,7 +403,7 @@ Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
 Ltac convert_to_i2p P cont :=
   lazymatch P with
   | subsume ?P1 ?P2 ?T => cont uconstr:(((_ : Subsume _ _) _).(i2p_proof))
-  | subsume_list ?A ?l1 ?l2 ?f ?T => cont uconstr:(((_ : SubsumeList _ _ _ _) _).(i2p_proof))
+  | subsume_list ?A ?ig ?l1 ?l2 ?f ?T => cont uconstr:(((_ : SubsumeList _ _ _ _ _) _).(i2p_proof))
   | _ => let converted := convert_to_i2p_tac P in cont converted
   end.
 Ltac extensible_judgment_hook := idtac.

theories/typing/array.v

@@ -190,16 +190,9 @@ Section array.
     λ T, i2p (subsume_array_replicate_uninit l β T n ly1 ly2).
 
   Lemma subsume_array ly1 ly2 tys1 tys2 l β T:
-    ⌜ly1 = ly2⌝ ∗ ⌜length tys1 = length tys2⌝ ∗
-    subsume_list type tys1 tys2 (λ i ty, (l offset{ly1}ₗ i) ◁ₗ{β} ty) T -∗
+    ⌜ly1 = ly2⌝ ∗ subsume_list type [] tys1 tys2 (λ i ty, (l offset{ly1}ₗ i) ◁ₗ{β} ty) T -∗
       subsume (l ◁ₗ{β} array ly1 tys1) (l ◁ₗ{β} array ly2 tys2) T.
-  Proof.
-    iIntros "[-> [Hlen H]] ($&Hb&H1)". iDestruct "Hlen" as %Hlen.
-    iDestruct ("H" $! Hlen) as "H2".
-    iAssert (([^bi_sep list] i↦x ∈ tys2, (l offset{ly2}ₗ i) ◁ₗ{β} x) ∗ T)%I
-      with "[H1 H2]" as "[$ $]"; first by iApply "H2".
-    by rewrite Hlen.
-  Qed.
+  Proof. iIntros "[-> H] ($&Hb&H1)". by iDestruct ("H" with "H1") as (->) "[$ $]". Qed.
   Global Instance subsume_array_inst ly1 ly2 tys1 tys2 l β:
     SubsumePlace l β (array ly1 tys1) (array ly2 tys2) | 100 :=
     λ T, i2p (subsume_array ly1 ly2 tys1 tys2 l β T).
@@ -214,7 +207,7 @@ Section array.
     iDestruct ("Hsub" with "H1") as "[H1 HT]".
     iDestruct (array_put_type i with "H1 Ha") as "Ha".
     iApply (subsume_array with "[HT] Ha"). iFrame "HT".
-    rewrite !list_insert_insert. repeat iSplit => //. by iIntros "_ $".
+    rewrite !list_insert_insert. repeat iSplit => //. by iIntros "$".
   Qed.
   Global Instance subsume_array_insert_inst ly (i : nat) ty tys1 tys2 l β:
     SubsumePlace l β (array ly (<[i := ty]>tys1)) (array ly tys2) | 10:=
@@ -243,5 +236,7 @@ Section array.
     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).
 End array.
+
 Notation "array< ty , tys >" := (array ty tys)
   (only printing, format "'array<' ty ,  tys '>'") : printing_sugar.
+Typeclasses Opaque array.

theories/typing/own.v

@@ -547,8 +547,8 @@ Section optionable.
     λ T, i2p (subsume_optional_place_val_null ty l β T b ty').
 
   Lemma subsume_optionalO_place_val_null A (ty : A → type) l β T b ty' `{!∀ x, Movable (ty x)} `{!∀ x, Optionable (ty x) null ot1 ot2}:
-    (∃ x, ⌜b = Some x⌝ ∗ subsume (l ◁ₗ{β} ty') (l ◁ᵥ ty x) T) -∗ subsume (l ◁ₗ{β} ty') (l ◁ᵥ b @ optionalO ty null) T.
-  Proof. iDestruct 1 as (x ->) "Hsub". iIntros "Hl". by iApply "Hsub". Qed.
+    (⌜is_Some b⌝ ∗ ∀ x, ⌜b = Some x⌝ -∗ subsume (l ◁ₗ{β} ty') (l ◁ᵥ ty x) T) -∗ subsume (l ◁ₗ{β} ty') (l ◁ᵥ b @ optionalO ty null) T.
+  Proof. iDestruct 1 as ([x ->]) "Hsub". iIntros "Hl". by iApply "Hsub". Qed.
   Global Instance subsume_optionalO_place_val_null_inst A (ty : A → type) l β b ty' `{!∀ x, Movable (ty x)} `{!∀ x, Optionable (ty x) null ot1 ot2}:
     Subsume (l ◁ₗ{β} ty') (l ◁ᵥ b @ optionalO ty null)%I | 20 :=
     λ T, i2p (subsume_optionalO_place_val_null A ty l β T b ty').

tutorial/proofs/t04_alloc/generated_proof_alloc.v

@@ -12,7 +12,7 @@ Section proof_alloc.
   (* Typing proof for [alloc]. *)
   Lemma type_alloc (global_allocator_state global_sl_lock global_sl_unlock : loc) :
     global_locs !! "allocator_state" = Some global_allocator_state →
-    global_initialized_types !! "allocator_state" = Some (GT () (λ '(), (alloc_state) : type)) →
+    global_initialized_types !! "allocator_state" = Some (GT () (λ '(), (alloc_state) : type)%I) →
     global_sl_lock ◁ᵥ global_sl_lock @ function_ptr type_of_sl_lock -∗
     global_sl_unlock ◁ᵥ global_sl_unlock @ function_ptr type_of_sl_unlock -∗
     typed_function (impl_alloc global_allocator_state global_sl_lock global_sl_unlock) type_of_alloc.

tutorial/proofs/t04_alloc/generated_proof_free.v

@@ -12,7 +12,7 @@ Section proof_free.
   (* Typing proof for [free]. *)
   Lemma type_free (global_allocator_state global_sl_lock global_sl_unlock : loc) :
     global_locs !! "allocator_state" = Some global_allocator_state →
-    global_initialized_types !! "allocator_state" = Some (GT () (λ '(), (alloc_state) : type)) →
+    global_initialized_types !! "allocator_state" = Some (GT () (λ '(), (alloc_state) : type)%I) →
     global_sl_lock ◁ᵥ global_sl_lock @ function_ptr type_of_sl_lock -∗
     global_sl_unlock ◁ᵥ global_sl_unlock @ function_ptr type_of_sl_unlock -∗
     typed_function (impl_free global_allocator_state global_sl_lock global_sl_unlock) type_of_free.

tutorial/proofs/t04_alloc/generated_proof_init_alloc.v

@@ -12,7 +12,7 @@ Section proof_init_alloc.
   (* Typing proof for [init_alloc]. *)
   Lemma type_init_alloc (global_allocator_state global_sl_init : loc) :
     global_locs !! "allocator_state" = Some global_allocator_state →
-    global_initialized_types !! "allocator_state" = Some (GT () (λ '(), (alloc_state) : type)) →
+    global_initialized_types !! "allocator_state" = Some (GT () (λ '(), (alloc_state) : type)%I) →
     global_sl_init ◁ᵥ global_sl_init @ function_ptr type_of_sl_init -∗
     typed_function (impl_init_alloc global_allocator_state global_sl_init) type_of_init_alloc.
   Proof.

tutorial/proofs/t05_main/generated_proof_main.v

@@ -14,7 +14,7 @@ Section proof_main.
   Lemma type_main (global_allocator_data global_initialized global_free global_init_alloc global_latch_release global_test : loc) :
     global_locs !! "allocator_data" = Some global_allocator_data →
     global_locs !! "initialized" = Some global_initialized →
-    global_initialized_types !! "initialized" = Some (GT () (λ '(), (latch (alloc_initialized)) : type)) →
+    global_initialized_types !! "initialized" = Some (GT () (λ '(), (latch (alloc_initialized)) : type)%I) →
     global_free ◁ᵥ global_free @ function_ptr type_of_free -∗
     global_init_alloc ◁ᵥ global_init_alloc @ function_ptr type_of_init_alloc -∗
     global_latch_release ◁ᵥ global_latch_release @ function_ptr type_of_latch_release -∗

tutorial/proofs/t05_main/generated_proof_main2.v

@@ -13,7 +13,7 @@ Section proof_main2.
   (* Typing proof for [main2]. *)
   Lemma type_main2 (global_initialized global_latch_wait global_test : loc) :
     global_locs !! "initialized" = Some global_initialized →
-    global_initialized_types !! "initialized" = Some (GT () (λ '(), (latch (alloc_initialized)) : type)) →
+    global_initialized_types !! "initialized" = Some (GT () (λ '(), (latch (alloc_initialized)) : type)%I) →
     global_latch_wait ◁ᵥ global_latch_wait @ function_ptr type_of_latch_wait -∗
     global_test ◁ᵥ global_test @ function_ptr type_of_test -∗
     typed_function (impl_main2 global_initialized global_latch_wait global_test) type_of_main2.