Merge branch 'add-proofmode-tests' into 'master'

Add tests for iRename, iTypeOf, and iInduction with multiple IHs

Closes #334

See merge request !768

iris/proofmode/ltac_tactics.v

@@ -2301,9 +2301,9 @@ result in the following actions:
   hypotheses containing the induction variable [x]
 - Revert the pure hypotheses [x1..xn]
 
-- Actuall perform induction
+- Actually perform induction
 
-- Introduce thee pure hypotheses [x1..xn]
+- Introduce the pure hypotheses [x1..xn]
 - Introduce the spatial hypotheses and intuitionistic hypotheses involving [x]
 - Introduce the proofmode hypotheses [Hs]
 *)

tests/proofmode.ref

@@ -147,6 +147,20 @@ Tactic failure: iSpecialize: Q not persistent.
      : string
 The command has indeed failed with message:
 Tactic failure: iSpecialize: (|==> P)%I not persistent.
+"test_iInduction_multiple_IHs"
+     : string
+1 goal
+  
+  PROP : bi
+  l, t1 : tree
+  Φ : tree → PROP
+  ============================
+  "Hleaf" : Φ leaf
+  "Hnode" : ∀ l0 r : tree, Φ l0 -∗ Φ r -∗ Φ (node l0 r)
+  "IH" : Φ l
+  "IH1" : Φ t1
+  --------------------------------------□
+  Φ (node l t1)
 The command has indeed failed with message:
 Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
 P.
@@ -210,6 +224,16 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
      : string
 The command has indeed failed with message:
 Tactic failure: iEval: %: unsupported selection pattern.
+"test_iRename"
+     : string
+1 goal
+  
+  PROP : bi
+  P : PROP
+  ============================
+  "X" : P
+  --------------------------------------□
+  P
 "test_iFrame_later_1"
      : string
 1 goal

tests/proofmode.v

@@ -678,6 +678,18 @@ Proof.
     by iApply "IH".
 Qed.
 
+Inductive tree := leaf | node (l r: tree).
+
+Check "test_iInduction_multiple_IHs".
+Lemma test_iInduction_multiple_IHs (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.
@@ -890,6 +902,28 @@ Check "test_iSimpl_in4".
 Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
 Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
 
+Check "test_iRename".
+Lemma test_iRename P : □P -∗ P.
+Proof. iIntros "#H". iRename "H" into "X". Show. iExact "X". Qed.
+
+(** [iTypeOf] is an internal tactic for the proofmode *)
+Lemma test_iTypeOf Q R φ : □ Q ∗ R ∗ ⌜φ⌝ -∗ True.
+Proof.
+  iIntros "(#HQ & H)".
+  lazymatch iTypeOf "HQ" with
+  | Some (true, Q) => idtac
+  | ?x => fail "incorrect iTypeOf HQ" x
+  end.
+  lazymatch iTypeOf "H" with
+  | Some (false, (R ∗ ⌜φ⌝)%I) => idtac
+  | ?x => fail "incorrect iTypeOf H" x
+  end.
+  lazymatch iTypeOf "missing" with
+  | None => idtac
+  | ?x => fail "incorrect iTypeOf missing" x
+  end.
+Abort.
+
 Lemma test_iPureIntro_absorbing (φ : Prop) :
   φ → ⊢@{PROP} <absorb> ⌜φ⌝.
 Proof. intros ?. iPureIntro. done. Qed.