Merge branch 'ci/ralf/mangle' into 'master'

make sure std++ does not rely on generated names

See merge request iris/stdpp!182

.gitlab-ci.yml

@@ -31,6 +31,7 @@ build-coq.dev:
   <<: *template
   variables:
     OPAM_PINS: "coq version dev"
+    MANGLE_NAMES: "1"
     CI_COQCHK: "1"
 
 build-coq.8.12.0:

tests/telescopes.v

 From stdpp Require Import tactics telescopes.
 
+Local Unset Mangle Names. (* for stable goal printing *)
+
 Section accessor.
 (* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
 Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=

theories/binders.v

@@ -62,7 +62,7 @@ Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
 Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
 Proof.
   assert (∀ bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
-  { induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
+  { intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
   induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
     first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
 Qed.

theories/countable.v

@@ -53,7 +53,7 @@ Section choice.
     intros [x Hx]. cut (∀ i p,
       i ≤ encode x → 1 + encode x = p + i → Acc choose_step p).
     { intros help. by apply (help (encode x)). }
-    induction i as [|i IH] using Pos.peano_ind; intros p ??.
+    intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??.
     { constructor. intros j. assert (p = encode x) by lia; subst.
       inversion 1 as [? Hd|?? Hd]; subst;
         rewrite decode_encode in Hd; congruence. }

theories/fin_maps.v

@@ -1053,7 +1053,7 @@ Proof.
   intros ? Hins. cut (∀ l, NoDup (l.*1) → ∀ m, map_to_list m ≡ₚ l → P m).
   { intros help m.
     apply (help (map_to_list m)); auto using NoDup_fst_map_to_list. }
-  induction l as [|[i x] l IH]; intros Hnodup m Hml.
+  intros l. induction l as [|[i x] l IH]; intros Hnodup m Hml.
   { apply map_to_list_empty_inv_alt in Hml. by subst. }
   inversion_clear Hnodup.
   apply map_to_list_insert_inv in Hml; subst m. apply Hins.
@@ -1703,7 +1703,7 @@ Proof. by apply (partial_alter_merge _). Qed.
 Lemma foldr_delete_union_with (m1 m2 : M A) is :
   foldr delete (union_with f m1 m2) is =
     union_with f (foldr delete m1 is) (foldr delete m2 is).
-Proof. induction is; simpl. done. by rewrite IHis, delete_union_with. Qed.
+Proof. induction is as [|?? IHis]; simpl. done. by rewrite IHis, delete_union_with. Qed.
 Lemma insert_union_with m1 m2 i x y z :
   f x y = Some z →
   <[i:=z]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=y]>m2).
@@ -1971,7 +1971,7 @@ Qed.
 Lemma foldr_delete_insert_ne {A} (m : M A) is j x :
   j ∉ is → foldr delete (<[j:=x]>m) is = <[j:=x]>(foldr delete m is).
 Proof.
-  induction is; simpl; [done |]. rewrite elem_of_cons. intros.
+  induction is as [|?? IHis]; simpl; [done |]. rewrite elem_of_cons. intros.
   rewrite IHis, delete_insert_ne; intuition.
 Qed.
 Lemma map_disjoint_foldr_delete_l {A} (m1 m2 : M A) is :
@@ -2065,7 +2065,7 @@ Proof. by apply (partial_alter_merge _). Qed.
 Lemma foldr_delete_intersection_with (m1 m2 : M A) is :
   foldr delete (intersection_with f m1 m2) is =
     intersection_with f (foldr delete m1 is) (foldr delete m2 is).
-Proof. induction is; simpl. done. by rewrite IHis, delete_intersection_with. Qed.
+Proof. induction is as [|?? IHis]; simpl. done. by rewrite IHis, delete_intersection_with. Qed.
 Lemma insert_intersection_with m1 m2 i x y z :
   f x y = Some z →
   <[i:=z]>(intersection_with f m1 m2) = intersection_with f (<[i:=x]>m1) (<[i:=y]>m2).

theories/fin_sets.v

@@ -155,7 +155,7 @@ Proof.
 Qed.
 Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
 Proof.
-  intros E. destruct (size_pos_elem_of X); auto with lia.
+  intros E. destruct (size_pos_elem_of X) as [x ?]; auto with lia.
   exists x. apply elem_of_equiv. split.
   - rewrite elem_of_singleton. eauto using size_singleton_inv.
   - set_solver.
@@ -283,7 +283,7 @@ Section filter.
   Global Instance set_unfold_filter X Q :
     SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q).
   Proof.
-    intros ??; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
+    intros x ?; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
   Qed.
 
   Lemma filter_empty : filter P (∅:C) ≡ ∅.

theories/finite.v

@@ -282,7 +282,7 @@ Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
 Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
   {| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
 Next Obligation.
-  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
+  intros A ?????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
   { constructor. }
   apply NoDup_app; split_and?.
   - by apply (NoDup_fmap_2 _), NoDup_enum.
@@ -316,7 +316,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
 Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
   {| enum := list_enum (enum A) n |}.
 Next Obligation.
-  intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
+  intros A ?? n. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
   revert IH. generalize (list_enum (enum A) n). intros l Hl.
   induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
   apply NoDup_app; split_and?.
@@ -329,8 +329,8 @@ Next Obligation.
   - apply IH.
 Qed.
 Next Obligation.
-  intros ???? [l Hl]. revert l Hl.
-  induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
+  intros A ?? n [l Hl]. revert l Hl.
+  induction n as [|n IH]; intros [|x l] Hl; simpl; simplify_eq.
   { apply elem_of_list_singleton. by apply (sig_eq_pi _). }
   revert IH. generalize (list_enum (enum A) n). intros k Hk.
   induction (elem_of_enum x) as [x xs|x xs]; simpl in *.

theories/hashset.v

@@ -104,7 +104,8 @@ Proof.
     intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
   - unfold elements, hashset_elements. intros [m Hm]; simpl.
     rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
-    induction Hm as [|[n l] m' [??]];
+    (* FIXME: trailing [?] works around Coq bug #12944. *)
+    induction Hm as [|[n l] m' [??] Hm ?];
       csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
     apply NoDup_app; split_and?; eauto.
     setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.

theories/mapset.v

@@ -41,15 +41,15 @@ Proof.
   - unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
     simpl. by split; intros; simplify_map_eq.
   - unfold union, elem_of, mapset_union, mapset_elem_of.
-    intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw.
+    intros [m1] [m2] x. simpl. rewrite lookup_union_Some_raw.
     destruct (m1 !! x) as [[]|]; tauto.
   - unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
-    intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
+    intros [m1] [m2] x. simpl. rewrite lookup_intersection_Some.
     assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()).
     { split; eauto. by intros [[] ?]. }
     naive_solver.
   - unfold difference, elem_of, mapset_difference, mapset_elem_of.
-    intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
+    intros [m1] [m2] x. simpl. rewrite lookup_difference_Some.
     destruct (m2 !! x) as [[]|]; intuition congruence.
 Qed.
 Global Instance mapset_leibniz : LeibnizEquiv (mapset M).

theories/relations.v

@@ -202,7 +202,7 @@ Section closure.
   Proof.
     cut (∀ m y z, bsteps R m y z → ∀ n,
       bsteps R n x y → (∀ m', n ≤ m' ∧ m' ≤ n + m → P m' y) → P (n + m) z).
-    { intros help ?. change n with (0 + n). eauto. }
+    { intros help n. change n with (0 + n). eauto. }
     induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
     intros n p1 H. rewrite <-plus_n_Sm.
     apply (IH (S n)); [by eauto using bsteps_r |].
@@ -422,7 +422,7 @@ Proof.
   cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x).
   { intros aux x. apply (aux (f x)); auto. }
   induction 1 as [y _ IH]. intros x ?. subst.
-  constructor. intros. apply (IH (f y)); auto.
+  constructor. intros y ?. apply (IH (f y)); auto.
 Qed.
 
 Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x))

theories/sorting.v

@@ -180,7 +180,8 @@ Section merge_sort_correct.
     Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
   Proof.
     intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
-      induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
+      (* FIXME: trailing [?] works around Coq bug #12944. *)
+      induction 1 as [|x2 l2 IH2 ?]; rewrite ?list_merge_cons; simpl;
       repeat case_decide;
       repeat match goal with H : ¬R _ _ |- _ => apply total_not in H end;
       constructor; eauto using HdRel_list_merge, HdRel_cons.

theories/vector.v

@@ -148,7 +148,7 @@ Qed.
 Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :
   ∃ i : fin (n + S m), x = (v +++ x ::: w) !!! i.
 Proof.
-  induction v; simpl; [by eexists 0%fin|].
+  induction v as [|??? IHv]; simpl; [by eexists 0%fin|].
   destruct IHv as [i ?]. by exists (FS i).
 Qed.
 Lemma vec_to_list_lookup_middle {A n} (v : vec A n) (l k : list A) x :
@@ -159,13 +159,13 @@ Proof.
   rewrite <-(vec_to_list_to_vec l), <-(vec_to_list_to_vec k) in H.
   rewrite <-vec_to_list_cons, <-vec_to_list_app in H.
   pose proof (vec_to_list_inj1 _ _ H); subst.
-  apply vec_to_list_inj2 in H; subst. induction l. simpl.
+  apply vec_to_list_inj2 in H; subst. induction l as [|?? IHl]. simpl.
   - eexists 0%fin. simpl. by rewrite vec_to_list_to_vec.
   - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
 Qed.
 Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) :
   drop i v = v !!! i :: drop (S i) v.
-Proof. induction i; inv_vec v; simpl; intros; [done | by rewrite IHi]. Qed.
+Proof. induction i as [|?? IHi]; inv_vec v; simpl; intros; [done | by rewrite IHi]. Qed.
 Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) :
   vec_to_list v = take i v ++ v !!! i :: drop (S i) v.
 Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed.
@@ -236,7 +236,7 @@ Lemma vlookup_map `(f : A → B) {n} (v : vec A n) i :
 Proof. by induction v; inv_fin i; eauto. Qed.
 Lemma vec_to_list_map `(f : A → B) {n} (v : vec A n) :
   vec_to_list (vmap f v) = f <$> vec_to_list v.
-Proof. induction v; simpl. done. by rewrite IHv. Qed.
+Proof. induction v as [|??? IHv]; simpl. done. by rewrite IHv. Qed.
 
 (** The function [vzip_with f v w] combines the vectors [v] and [w] element
 wise using the function [f]. *)
@@ -254,7 +254,7 @@ Lemma vec_to_list_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n
   vec_to_list (vzip_with f v1 v2) =
     zip_with f (vec_to_list v1) (vec_to_list v2).
 Proof.
-  revert v2. induction v1; intros v2; inv_vec v2; intros; simpl; [done|].
+  revert v2. induction v1 as [|??? IHv1]; intros v2; inv_vec v2; intros; simpl; [done|].
   by rewrite IHv1.
 Qed.
 
@@ -268,14 +268,14 @@ Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n → vec A n :=
 
 Lemma vec_to_list_insert {A n} i x (v : vec A n) :
   vec_to_list (vinsert i x v) = insert (fin_to_nat i) x (vec_to_list v).
-Proof. induction v; inv_fin i. done. simpl. intros. by rewrite IHv. Qed.
+Proof. induction v as [|??? IHv]; inv_fin i. done. simpl. intros. by rewrite IHv. Qed.
 
 Lemma vlookup_insert {A n} i x (v : vec A n) : vinsert i x v !!! i = x.
 Proof. by induction i; inv_vec v. Qed.
 Lemma vlookup_insert_ne {A n} i j x (v : vec A n) :
   i ≠ j → vinsert i x v !!! j = v !!! j.
 Proof.
-  induction i; inv_fin j; inv_vec v; simpl; try done.
+  induction i as [|?? IHi]; inv_fin j; inv_vec v; simpl; try done.
   intros. apply IHi. congruence.
 Qed.
 Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v.