Commit a0a4b119 authored by Robbert Krebbers's avatar Robbert Krebbers

Make iInduction more powerful, to e.g. support well-founded induction.

parent 6df33dac
......@@ -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 :
......
......@@ -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
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment