From a0a4b1199b90c144ae61d122a5d676bfc8ca2853 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Oct 2017 10:14:43 +0900
Subject: [PATCH] Make iInduction more powerful, to e.g. support well-founded
 induction.

---
 theories/proofmode/coq_tactics.v | 19 +++++++++++++++----
 theories/proofmode/tactics.v     |  8 ++++----
 theories/tests/proofmode.v       |  8 ++++++++
 3 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 775d56558..f52984b25 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -647,14 +647,25 @@ Proof.
   by rewrite HQ /uPred_always_if wand_elim_r.
 Qed.
 
-Lemma tac_revert_ih Δ P Q :
+Class IntoIH (φ : Prop) (Δ : envs M) (Q : uPred M) :=
+  into_ih : φ → Δ ⊢ Q.
+Global Instance into_ih_entails Δ Q : IntoIH (of_envs Δ ⊢ Q) Δ Q.
+Proof. by rewrite /IntoIH. Qed.
+Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
+  (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
+Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
+Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
+  IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌝ → Q) | 1.
+Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
+
+Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
+  IntoIH φ Δ P →
   env_spatial_is_nil Δ = true →
-  (of_envs Δ ⊢ P) →
   (of_envs Δ ⊢ □ P → Q) →
   (of_envs Δ ⊢ Q).
 Proof.
-  intros ? HP HPQ.
-  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
+  rewrite /IntoIH. intros HP ? HPQ.
+  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP // HPQ impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index c9379be10..7d01214b8 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1360,10 +1360,10 @@ result in the following actions:
 Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(IH) :=
   let rec fix_ihs :=
     lazymatch goal with
-    | H : coq_tactics.of_envs _ ⊢ _ |- _ =>
-       eapply tac_revert_ih;
-         [reflexivity || fail "iInduction: spatial context not empty, this should not happen"
-         |apply H|];
+    | H : context [coq_tactics.of_envs _ ⊢ _] |- _ =>
+       eapply (tac_revert_ih _ _ _ H _);
+         [reflexivity
+          || fail "iInduction: spatial context not empty, this should not happen"|];
        clear H; fix_ihs;
        let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
     | _ => idtac
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index e09f3f234..28e615223 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -190,6 +190,14 @@ Proof.
   by iExists (S n).
 Qed.
 
+Lemma test_iInduction_wf (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 omega.
+Qed.
+
 Lemma test_iIntros_start_proof :
   (True : uPred M)%I.
 Proof.
-- 
GitLab