Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

theories/collections.v

@@ -390,7 +390,7 @@ Section simple_collection.
     split.
     - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
       setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
-    - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
+    - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |].
       intros. apply elem_of_union_r; auto.
   Qed.
 

theories/list.v

@@ -926,7 +926,7 @@ Proof. by destruct n. Qed.
 Lemma drop_length l n : length (drop n l) = length l - n.
 Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
 Lemma drop_ge l n : length l ≤ n → drop n l = [].
-Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
 Lemma drop_all l : drop (length l) l = [].
 Proof. by apply drop_ge. Qed.
 Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
@@ -2828,7 +2828,7 @@ Section fmap.
     (∀ x, f x = y) → f <$> l = replicate (length l) y.
   Proof. intros; induction l; f_equal/=; auto. Qed.
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
-  Proof. revert i. induction l; by intros [|]. Qed.
+  Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
   Lemma list_lookup_fmap_inv l i x :
     (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
   Proof.

theories/vector.v

@@ -69,12 +69,13 @@ Ltac inv_fin i :=
     revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
   end.
 
-Instance: Inj (=) (=) (@FS n).
+Instance FS_inj: Inj (=) (=) (@FS n).
 Proof. intros n i j. apply Fin.FS_inj. Qed.
-Instance: Inj (=) (=) (@fin_to_nat n).
+Instance fin_to_nat_inj : Inj (=) (=) (@fin_to_nat n).
 Proof.
   intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
 Qed.
+
 Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
 Proof. induction i; simpl; lia. Qed.
 Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (Fin.of_nat_lt H) = n.
@@ -82,6 +83,31 @@ Proof.
   revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
 Qed.
 
+Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
+    (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1))
+    (H2 : ∀ i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i :=
+  match n1 with
+  | 0 => λ P H1 H2 i, H2 i
+  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_plus_inv _ (λ i, H1 (FS i)) H2)
+  end.
+
+Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) → Type)
+    (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n1) :
+  fin_plus_inv P H1 H2 (Fin.L n2 i) = H1 i.
+Proof.
+  revert P H1 H2 i.
+  induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto.
+  intros i. apply (IH (λ i, P (FS i))).
+Qed.
+
+Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2) → Type)
+    (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n2) :
+  fin_plus_inv P H1 H2 (Fin.R n1 i) = H2 i.
+Proof.
+  revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto.
+  apply (IH (λ i, P (FS i))).
+Qed.
+
 (** * Vectors *)
 (** The type [vec n] represents lists of consisting of exactly [n] elements.
 Whereas the standard library declares exactly the same notations for vectors as