Change the definition of "is_Some" to use an existential.

theories/fin_collections.v

@@ -70,7 +70,7 @@ Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
 Proof. destruct (choose X) eqn:?; eauto using choose_Some, choose_None. Qed.
 Lemma choose_is_Some X : X ≢ ∅ ↔ is_Some (choose X).
 Proof.
-  rewrite is_Some_alt. destruct (choose X) eqn:?.
+  destruct (choose X) eqn:?.
   * rewrite elem_of_equiv_empty. split; eauto using choose_Some.
   * split. intros []; eauto using choose_None. by intros [??].
 Qed.

theories/fin_map_dom.v

@@ -33,7 +33,7 @@ Proof.
   { by apply subseteq_dom. }
   intros Hdom. destruct Hss2. intros i x Hi.
   specialize (Hdom i). rewrite !elem_of_dom in Hdom.
-  feed inversion Hdom. eauto. by erewrite (Hss1 i) in Hi by eauto.
+  destruct Hdom; eauto. erewrite (Hss1 i) in Hi by eauto. congruence.
 Qed.
 
 Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
@@ -50,9 +50,8 @@ Qed.
 
 Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
 Proof.
-  apply elem_of_equiv. intros j.
-  rewrite elem_of_union, !elem_of_dom, !is_Some_alt.
-  setoid_rewrite lookup_insert_Some.
+  apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
+  unfold is_Some. setoid_rewrite lookup_insert_Some.
   destruct (decide (i = j)); esolve_elem_of.
 Qed.
 Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
@@ -69,14 +68,12 @@ Qed.
 
 Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
 Proof.
-  apply elem_of_equiv. intros j.
-  rewrite elem_of_difference, !elem_of_dom, !is_Some_alt.
-  setoid_rewrite lookup_delete_Some. esolve_elem_of.
+  apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
+  unfold is_Some. setoid_rewrite lookup_delete_Some. esolve_elem_of.
 Qed.
 Lemma delete_partial_alter_dom {A} (m : M A) i f :
   i ∉ dom D m → delete i (partial_alter f i m) = m.
 Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
-
 Lemma delete_insert_dom {A} (m : M A) i x :
   i ∉ dom D m → delete i (<[i:=x]>m) = m.
 Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
@@ -85,7 +82,7 @@ Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ m2 ↔ dom D m1 ∩ dom D m2
 Proof.
   unfold disjoint, map_disjoint, map_intersection_forall.
   rewrite elem_of_equiv_empty. setoid_rewrite elem_of_intersection.
-  setoid_rewrite elem_of_dom. setoid_rewrite is_Some_alt. naive_solver.
+  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
 Qed.
 Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ m2 → dom D m1 ∩ dom D m2 ≡ ∅.
 Proof. apply map_disjoint_dom. Qed.
@@ -94,24 +91,22 @@ Proof. apply map_disjoint_dom. Qed.
 
 Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2.
 Proof.
-  apply elem_of_equiv. intros i.
-  rewrite elem_of_union, !elem_of_dom, !is_Some_alt.
-  setoid_rewrite lookup_union_Some_raw. destruct (m1 !! i); naive_solver.
+  apply elem_of_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
+  unfold is_Some. setoid_rewrite lookup_union_Some_raw.
+  destruct (m1 !! i); naive_solver.
 Qed.
 
 Lemma dom_intersection {A} (m1 m2 : M A) :
   dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2.
 Proof.
-  apply elem_of_equiv. intros i.
-  rewrite elem_of_intersection, !elem_of_dom, !is_Some_alt.
-  setoid_rewrite lookup_intersection_Some.
-  setoid_rewrite is_Some_alt. naive_solver.
+  apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
+  unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
 Qed.
 
 Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1 ∖ m2) ≡ dom D m1 ∖ dom D m2.
 Proof.
-  apply elem_of_equiv. intros i.
-  rewrite elem_of_difference, !elem_of_dom, !is_Some_alt.
-  setoid_rewrite lookup_difference_Some. destruct (m2 !! i); naive_solver.
+  apply elem_of_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
+  unfold is_Some. setoid_rewrite lookup_difference_Some.
+  destruct (m2 !! i); naive_solver.
 Qed.
 End fin_map_dom.

theories/fin_maps.v

@@ -427,7 +427,7 @@ Proof. split; auto using elem_of_map_of_list_1, elem_of_map_of_list_2. Qed.
 Lemma not_elem_of_map_of_list_1 {A} (l : list (K * A)) i :
   i ∉ fst <$> l → map_of_list l !! i = None.
 Proof.
-  rewrite elem_of_list_fmap, eq_None_not_Some, is_Some_alt.
+  rewrite elem_of_list_fmap, eq_None_not_Some.
   intros Hi [x ?]. destruct Hi. exists (i,x). simpl.
   auto using elem_of_map_of_list_2.
 Qed.
@@ -749,7 +749,7 @@ Proof. eauto using map_disjoint_weaken. Qed.
 Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x:
   m1 ⊥ m2 → m1 !! i = Some x → m2 !! i = None.
 Proof.
-  intros Hdisjoint ?. rewrite eq_None_not_Some, is_Some_alt.
+  intros Hdisjoint ?. rewrite eq_None_not_Some.
   intros [x2 ?]. by apply (Hdisjoint i x x2).
 Qed.
 Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
@@ -1110,10 +1110,8 @@ Qed.
 Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x :
   (m1 ∩ m2) !! i = Some x ↔ m1 !! i = Some x ∧ is_Some (m2 !! i).
 Proof.
-  unfold intersection, map_intersection,
-    intersection_with, map_intersection_with.
-  rewrite (lookup_merge _).
-  rewrite is_Some_alt.
+  unfold intersection, map_intersection, intersection_with,
+    map_intersection_with. rewrite (lookup_merge _).
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
 

theories/list.v

@@ -373,45 +373,43 @@ Proof. by destruct i. Qed.
 Lemma lookup_tail l i : tail l !! i = l !! S i.
 Proof. by destruct l. Qed.
 
-Lemma lookup_lt_length l i : is_Some (l !! i) ↔ i < length l.
-Proof.
-  revert i. induction l.
-  * split; by inversion 1.
-  * intros [|?]; simpl.
-    + split; eauto with arith.
-    + by rewrite <-NPeano.Nat.succ_lt_mono.
-Qed.
-Lemma lookup_lt_length_1 l i : is_Some (l !! i) → i < length l.
-Proof. apply lookup_lt_length. Qed.
-Lemma lookup_lt_length_alt l i x : l !! i = Some x → i < length l.
-Proof. intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
-Lemma lookup_lt_length_2 l i : i < length l → is_Some (l !! i).
-Proof. apply lookup_lt_length. Qed.
-
-Lemma lookup_ge_length l i : l !! i = None ↔ length l ≤ i.
-Proof. rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
-Lemma lookup_ge_length_1 l i : l !! i = None → length l ≤ i.
-Proof. by rewrite lookup_ge_length. Qed.
-Lemma lookup_ge_length_2 l i : length l ≤ i → l !! i = None.
-Proof. by rewrite lookup_ge_length. Qed.
-
-Lemma list_eq_length_eq l1 l2 :
+Lemma lookup_lt_Some l i x : l !! i = Some x → i < length l.
+Proof.
+  revert i. induction l; intros [|?] ?;
+    simpl in *; simplify_equality; simpl; auto with arith.
+Qed.
+Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) → i < length l.
+Proof. intros [??]; eauto using lookup_lt_Some. Qed.
+Lemma lookup_lt_is_Some_2 l i : i < length l → is_Some (l !! i).
+Proof.
+  revert i. induction l; intros [|?] ?;
+    simpl in *; simplify_equality; simpl; eauto with lia.
+Qed.
+Lemma lookup_lt_is_Some l i : is_Some (l !! i) ↔ i < length l.
+Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.
+
+Lemma lookup_ge_None l i : l !! i = None ↔ length l ≤ i.
+Proof. rewrite eq_None_not_Some, lookup_lt_is_Some. lia. Qed.
+Lemma lookup_ge_None_1 l i : l !! i = None → length l ≤ i.
+Proof. by rewrite lookup_ge_None. Qed.
+Lemma lookup_ge_None_2 l i : length l ≤ i → l !! i = None.
+Proof. by rewrite lookup_ge_None. Qed.
+
+Lemma list_eq_length l1 l2 :
   length l2 = length l1 →
   (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2.
 Proof.
-  intros Hlength Hlookup. apply list_eq. intros i.
-  destruct (l2 !! i) as [x|] eqn:E.
-  * feed inversion (lookup_lt_length_2 l1 i) as [y]; [|eauto with f_equal].
-    pose proof (lookup_lt_length_alt l2 i x E). lia.
-  * rewrite lookup_ge_length in E |- *. lia.
+  intros Hl ?. apply list_eq. intros i. destruct (l2 !! i) as [x|] eqn:Hx.
+  * destruct (lookup_lt_is_Some_2 l1 i) as [y ?]; subst.
+    + rewrite <-Hl. eauto using lookup_lt_Some.
+    + naive_solver.
+  * by rewrite lookup_ge_None, <-Hl, <-lookup_ge_None.
 Qed.
 
-Lemma lookup_app_l l1 l2 i :
-  i < length l1 → (l1 ++ l2) !! i = l1 !! i.
+Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i.
 Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
-Lemma lookup_app_l_Some l1 l2 i x :
-  l1 !! i = Some x → (l1 ++ l2) !! i = Some x.
-Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.
+Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x → (l1 ++ l2) !! i = Some x.
+Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
 Lemma lookup_app_r l1 l2 i : (l1 ++ l2) !! (length l1 + i) = l2 !! i.
 Proof.
   revert i. induction l1; intros [|i]; simpl in *; simplify_equality; auto.
@@ -451,7 +449,7 @@ Qed.
 Lemma list_lookup_insert l i x : i < length l → <[i:=x]>l !! i = Some x.
 Proof.
   intros Hi. unfold insert, list_insert. rewrite list_lookup_alter.
-  by feed inversion (lookup_lt_length_2 l i).
+  by destruct (lookup_lt_is_Some_2 l i); simplify_option_equality.
 Qed.
 Lemma list_lookup_insert_ne l i j x : i ≠ j → <[i:=x]>l !! j = l !! j.
 Proof. apply list_lookup_alter_ne. Qed.
@@ -1597,7 +1595,7 @@ Section contains_dec.
   Lemma list_remove_list_contains l1 l2 :
     l1 `contains` l2 ↔ is_Some (list_remove_list l1 l2).
   Proof.
-    rewrite is_Some_alt. split.
+    split.
     * revert l2. induction l1 as [|x l1 IH]; simpl.
       { intros l2 _. by exists l2. }
       intros l2. rewrite contains_cons_l. intros (k&Hk&?).
@@ -1646,10 +1644,7 @@ Section same_length.
 
   Lemma same_length_lookup l k i :
     l `same_length` k → is_Some (l !! i) → is_Some (k !! i).
-  Proof.
-    rewrite same_length_length. setoid_rewrite lookup_lt_length.
-    intros E. by rewrite E.
-  Qed.
+  Proof. rewrite same_length_length. rewrite !lookup_lt_is_Some. lia. Qed.
 
   Lemma same_length_take l k n :
     l `same_length` k → take n l `same_length` take n k.

theories/mapset.v

@@ -27,10 +27,9 @@ Instance mapset_elems: Elements K (mapset M) := λ X,
 
 Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
 Proof.
-  split.
-  * intros. by subst.
-  * destruct X1 as [m1], X2 as [m2]. simpl. intros E.
-    f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
+  split; [by intros; subst |].
+  destruct X1 as [m1], X2 as [m2]. simpl. intros E.
+  f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
 Qed.
 
 Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)}
@@ -56,7 +55,7 @@ Proof.
   * unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
     intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
     setoid_replace (is_Some (m2 !! x)) with (m2 !! x = Some ()); [done |].
-    rewrite is_Some_alt. split; eauto. by intros [[] ?].
+    split; eauto. by intros [[] ?].
   * unfold difference, elem_of, mapset_difference, mapset_elem_of.
     intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
     destruct (m2 !! x) as [[]|]; intuition congruence.
@@ -113,7 +112,7 @@ Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
 Instance mapset_dom_spec: FinMapDom K M (mapset M).
 Proof.
   split; try apply _. intros. unfold dom, mapset_dom.
-  rewrite is_Some_alt, elem_of_mapset_dom_with. naive_solver.
+  rewrite elem_of_mapset_dom_with. unfold is_Some. naive_solver.
 Qed.
 End mapset.
 

theories/natmap.v

@@ -17,11 +17,10 @@ Proof. by destruct l. Qed.
 Lemma natmap_wf_lookup {A} (l : natmap_raw A) :
   natmap_wf l → l ≠ [] → ∃ i x, mjoin (l !! i) = Some x.
 Proof.
-  intros Hwf Hl. induction l as [|[x|] l IH]; simpl.
-  * done.
+  intros Hwf Hl. induction l as [|[x|] l IH]; simpl; [done| |].
   * exists 0. simpl. eauto.
   * destruct IH as (i&x&?); eauto using natmap_wf_inv.
-    { intro. subst. inversion Hwf. }
+    { intro. subst. by destruct Hwf. }
     by exists (S i) x.
 Qed.
 
@@ -221,8 +220,7 @@ Proof.
     + by specialize (E 0).
     + destruct (natmap_wf_lookup (None :: l1)) as [i [??]]; auto with congruence.
     + by specialize (E 0).
-    + f_equal. apply IH; eauto using natmap_wf_inv.
-      intros i. apply (E (S i)).
+    + f_equal. apply IH; eauto using natmap_wf_inv. intros i. apply (E (S i)).
   * done.
   * intros ?? [??] ?. apply natmap_lookup_alter_raw.
   * intros ?? [??] ??. apply natmap_lookup_alter_raw_ne.

theories/option.v

@@ -26,70 +26,48 @@ Definition from_option {A} (a : A) (x : option A) : A :=
 
 (** An alternative, but equivalent, definition of equality on the option
 data type. This theorem is useful to prove that two options are the same. *)
-Lemma option_eq {A} (x y : option A) :
-  x = y ↔ ∀ a, x = Some a ↔ y = Some a.
-Proof.
-  split; [by intros; by subst |]. intros E. destruct x, y.
-  + by apply E.
-  + symmetry. by apply E.
-  + by apply E.
-  + done.
-Qed.
+Lemma option_eq {A} (x y : option A) : x = y ↔ ∀ a, x = Some a ↔ y = Some a.
+Proof. split; [by intros; by subst |]. destruct x, y; naive_solver. Qed.
 
-Inductive is_Some {A} : option A → Prop :=
-  mk_is_Some x : is_Some (Some x).
+Definition is_Some {A} (x : option A) := ∃ y, x = Some y.
+Lemma mk_is_Some {A} (x : option A) y : x = Some y → is_Some x.
+Proof. intros; red; subst; eauto. Qed.
+Hint Resolve mk_is_Some.
+Lemma is_Some_None {A} : ¬is_Some (@None A).
+Proof. by destruct 1. Qed.
+Hint Resolve is_Some_None.
 
 Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
 Proof.
-  intros [?] p2. by refine
-    match p2 in is_Some o return
-      match o with Some y => (mk_is_Some y =) | _ => λ _, False end p2
-    with mk_is_Some y => _ end.
+  set (P (y : option A) := match y with Some _ => True | _ => False end).
+  set (f x := match x return P x → is_Some x with
+    Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
+  set (g x (H : is_Some x) :=
+    match H return P x with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
+  assert (∀ x H, f x (g x H) = H) as f_g by (by intros ? [??]; subst).
+  intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct x, p1.
 Qed.
-
-Lemma mk_is_Some_alt `(x : option A) a : x = Some a → is_Some x.
-Proof. intros. by subst. Qed.
-Hint Resolve mk_is_Some_alt.
-Lemma is_Some_None {A} : ¬is_Some (@None A).
-Proof. by inversion 1. Qed.
-Hint Resolve is_Some_None.
-
-Lemma is_Some_alt `(x : option A) : is_Some x ↔ ∃ y, x = Some y.
-Proof. split. inversion 1; eauto. intros [??]. by subst. Qed.
-
-Ltac inv_is_Some := repeat
-  match goal with H : is_Some _ |- _ => inversion H; clear H; subst end.
-
-Definition is_Some_proj `{x : option A} : is_Some x → A :=
+Instance is_Some_dec {A} (x : option A) : Decision (is_Some x) :=
   match x with
-  | Some a => λ _, a
-  | None => False_rect _ ∘ is_Some_None
+  | Some x => left (ex_intro _ x eq_refl)
+  | None => right is_Some_None
   end.
-Definition Some_dec `(x : option A) : { a | x = Some a } + { x = None } :=
+
+Definition is_Some_proj {A} {x : option A} : is_Some x → A :=
+  match x with Some a => λ _, a | None => False_rect _ ∘ is_Some_None end.
+Definition Some_dec {A} (x : option A) : { a | x = Some a } + { x = None } :=
   match x return { a | x = Some a } + { x = None } with
   | Some a => inleft (a ↾ eq_refl _)
   | None => inright eq_refl
   end.
-Instance is_Some_dec `(x : option A) : Decision (is_Some x) :=
-  match x with
-  | Some x => left (mk_is_Some x)
-  | None => right is_Some_None
-  end.
-Instance None_dec `(x : option A) : Decision (x = None) :=
-  match x with
-  | Some x => right (Some_ne_None x)
-  | None => left eq_refl
-  end.
+Instance None_dec {A} (x : option A) : Decision (x = None) :=
+  match x with Some x => right (Some_ne_None x) | None => left eq_refl end.
 
-Lemma eq_None_not_Some `(x : option A) : x = None ↔ ¬is_Some x.
-Proof. split. by destruct 2. destruct x. by intros []. done. Qed.
+Lemma eq_None_not_Some {A} (x : option A) : x = None ↔ ¬is_Some x.
+Proof. destruct x; unfold is_Some; naive_solver. Qed.
 Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x.
 Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
 
-Lemma mk_eq_Some {A} (x : option A) a :
-  is_Some x → (∀ b, x = Some b → b = a) → x = Some a.
-Proof. destruct 1. intros. f_equal. auto. Qed.
-
 (** Equality on [option] is decidable. *)
 Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)}
     (x y : option A) : Decision (x = y) :=
@@ -122,20 +100,18 @@ Definition mapM `{!MBind M} `{!MRet M} {A B}
   | x :: l => y ← f x; k ← go l; mret (y :: k)
   end.
 
-Lemma fmap_is_Some {A B} (f : A → B) (x : option A) :
-  is_Some (f <$> x) ↔ is_Some x.
-Proof. split; inversion 1. by destruct x. done. Qed.
-Lemma fmap_Some {A B} (f : A → B) (x : option A) y :
+Lemma fmap_is_Some {A B} (f : A → B) x : is_Some (f <$> x) ↔ is_Some x.
+Proof. unfold is_Some; destruct x; naive_solver. Qed.
+Lemma fmap_Some {A B} (f : A → B) x y :
   f <$> x = Some y ↔ ∃ x', x = Some x' ∧ y = f x'.
-Proof. unfold fmap, option_fmap. destruct x; naive_solver. Qed.
-Lemma fmap_None {A B} (f : A → B) (x : option A) :
-  f <$> x = None ↔ x = None.
-Proof. unfold fmap, option_fmap. by destruct x. Qed.
+Proof. destruct x; naive_solver. Qed.
+Lemma fmap_None {A B} (f : A → B) x : f <$> x = None ↔ x = None.
+Proof. by destruct x. Qed.
 
 Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
 Proof. by destruct x. Qed.
 Lemma option_bind_assoc {A B C} (f : A → option B)
-    (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f).
+  (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f).
 Proof. by destruct x; simpl. Qed.
 Lemma option_bind_ext {A B} (f g : A → option B) x y :
   (∀ a, f a = g a) → x = y → x ≫= f = y ≫= g.