Some tests for legacy syntax and error messages.

tests/proofmode.ref

@@ -445,6 +445,20 @@ Tactic failure: iCombine: cannot find 'gives' clause for hypotheses
   "IHr" : Φ r
   --------------------------------------□
   Φ (node l r)
+"test_iInduction_multiple_IHs_legacy"
+     : string
+1 goal
+  
+  PROP : bi
+  l, r : tree
+  Φ : tree → PROP
+  ============================
+  "Hleaf" : Φ leaf
+  "Hnode" : ∀ l0 r0 : tree, Φ l0 -∗ Φ r0 -∗ Φ (node l0 r0)
+  "IH" : Φ l
+  "IH1" : Φ r
+  --------------------------------------□
+  Φ (node l r)
 The command has indeed failed with message:
 Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
 P.
@@ -1164,6 +1178,16 @@ The command has indeed failed with message:
 Tactic failure: sel_pat.parse: the term m
 is expected to be a selection pattern (usually a string),
 but has unexpected type nat.
+"iInduction_non_fresh_IH"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntro: "IH" not fresh.
+The command has indeed failed with message:
+Tactic failure: iIntro: "IH" not fresh.
+"iInduction_non_fresh_Coq_IH"
+     : string
+The command has indeed failed with message:
+IH is already used.
 "test_iIntros_let_entails_fail"
      : string
 The command has indeed failed with message:

tests/proofmode.v

@@ -1025,6 +1025,44 @@ Proof.
     iApply ("Hnode" with "IHl IHr").
 Qed.
 
+(* Copies of the above tests for the legacy syntax of naming IHs *)
+Lemma test_iInduction_wf_legacy (x : nat) P Q :
+  □ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝.
+Proof.
+  iIntros "#HP HQ".
+  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
+  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
+Qed.
+
+Lemma test_iInduction_using_legacy (m : gmap nat nat) (Φ : nat → nat → PROP) y :
+  ([∗ map] x ↦ i ∈ m, Φ y x) -∗ ([∗ map] x ↦ i ∈ m, emp ∗ Φ y x).
+Proof.
+  iIntros "Hm". iInduction m as [|i x m ?] "IH" using map_ind forall (y).
+  - by rewrite !big_sepM_empty.
+  - rewrite !big_sepM_insert //. iDestruct "Hm" as "[$ ?]".
+    by iApply "IH".
+Qed.
+
+Lemma test_iInduction_big_sepL_impl' {A} (Φ Ψ : nat → A → PROP) (l1 l2 : list A) :
+  length l1 = length l2 →
+  ([∗ list] k↦x ∈ l1, Φ k x) -∗
+  □ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
+  [∗ list] k↦x ∈ l2, Ψ k x.
+Proof.
+  iIntros (Hlen) "Hl #Himpl".
+  iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen).
+Abort.
+
+Check "test_iInduction_multiple_IHs_legacy".
+Lemma test_iInduction_multiple_IHs_legacy (t: tree) (Φ : tree → PROP) :
+  □ Φ leaf -∗ □ (∀ l r, Φ l -∗ Φ r -∗ Φ (node l r)) -∗ Φ t.
+Proof.
+  iIntros "#Hleaf #Hnode". iInduction t as [|l ? r] "IH".
+  - iExact "Hleaf".
+  - Show. (* should have "IH" and "IH1", since [node] has two trees *)
+    iApply ("Hnode" with "IH IH1").
+Qed.
+
 Lemma test_iIntros_start_proof :
   ⊢@{PROP} True.
 Proof.
@@ -2057,6 +2095,26 @@ Proof.
   Fail iInduction n as [|n IH] forall m.
 Abort.
 
+Check "iInduction_non_fresh_IH".
+Lemma iInduction_non_fresh_IH Q (P : nat → PROP) n :
+  □ Q -∗ P n.
+Proof.
+  iIntros "IH".
+  Fail iInduction n as [|n IH].
+  Fail iInduction n as [|n] "IH".
+Abort.
+
+Check "iInduction_non_fresh_Coq_IH".
+Lemma iInduction_non_fresh_Coq_IH φ (P : nat → PROP) n :
+  □ ⌜ φ ⌝ -∗ P n.
+Proof.
+  iIntros (IH).
+  (* Names for IHs should also be fresh in Coq context *)
+  Fail iInduction n as [|n IH].
+  (* But for the legacy syntax this is no problem. *)
+  iInduction n as [|n] "IH".
+Abort.
+
 Check "test_iIntros_let_entails_fail".
 Lemma test_iIntros_let_entails_fail P :
   let Q := (P ∗ P)%I in