Commit 1bff65be authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/into_ih_Forall' into 'master'

Extend `iInduction` with support for induction schemes containing `Forall`.

Closes #430

See merge request iris/iris!731
parents d45e839a e3a16b57
Pipeline #62353 passed with stage
in 16 minutes and 38 seconds
......@@ -19,6 +19,8 @@ lemma.
to occur when the conclusion contains variables that are not in scope of the
evar, thus blocking the default behavior of instantiating the premise with
the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
* `iInduction` now supports induction schemes that involve `Forall` and
`Forall2` (for example, for trees with finite branching).
## Iris 3.6.0 (2022-01-22)
......
......@@ -458,15 +458,51 @@ Proof.
Qed.
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
into_ih : φ of_envs Δ Q.
into_ih : φ of_envs Δ Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
Proof. by rewrite envs_entails_eq /IntoIH. Qed.
Proof. by rewrite envs_entails_eq /IntoIH bi.intuitionistically_elim. 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.
(** The instances [into_ih_Forall] and [into_ih_Forall2] are used to support
induction principles for mutual inductive types such as finitely branching trees:
Inductive ntree := Tree : list ntree → ntree.
Lemma ntree_ind (P : ntree → Prop) :
(∀ l, Forall P l → P (Tree l)) → ∀ t, P t.
Note 1: We need an [IntoIH] instance for any predicate transformer (like
[Forall]) that is used in induction principles. However, since nested induction
with lists is most common, we currently only support [Forall] and [Forall2].
Note 2: We could also write the instance [into_ih_Forall] using the big operator
for conjunction, or using the forall quantifier. We use the big operator
because that corresponds most closely to [Forall], and we use the version with
separating conjunction because we do not have a binary version of the big
operator for conjunctions, and want to treat [Forall] and [Forall2]
consistently. *)
Global Instance into_ih_Forall {A} (φ : A Prop) l Δ Φ :
( x, IntoIH (φ x) Δ (Φ x))
IntoIH (Forall φ l) Δ ([ list] x l, Φ x) | 2.
Proof.
rewrite /IntoIH=> HΔ. induction 1 as [|x l ? IH]; simpl.
{ apply (affine _). }
rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
apply intuitionistically_intro', HΔ; auto.
Qed.
Global Instance into_ih_Forall2 {A B} (φ : A B Prop) l1 l2 Δ Φ :
( x1 x2, IntoIH (φ x1 x2) Δ (Φ x1 x2))
IntoIH (Forall2 φ l1 l2) Δ ([ list] x1;x2 l1;l2, Φ x1 x2) | 2.
Proof.
rewrite /IntoIH=> HΔ. induction 1 as [|x1 x2 l1 l2 ? IH]; simpl.
{ apply (affine _). }
rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
apply intuitionistically_intro', HΔ; auto.
Qed.
Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
IntoIH φ Δ P
......@@ -476,8 +512,9 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
Proof.
rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
rewrite (env_spatial_is_nil_intuitionistically Δ) //.
rewrite -(idemp bi_and ( (of_envs Δ))%I) {1}HP // HPQ.
rewrite {1}intuitionistically_into_persistently_1 intuitionistically_elim impl_elim_r //.
rewrite -(idemp bi_and ( (of_envs Δ))%I).
rewrite -{1}intuitionistically_idemp {1}intuitionistically_into_persistently_1.
by rewrite {1}HP // intuitionistically_elim HPQ impl_elim_r.
Qed.
Lemma tac_assert Δ j P Q :
......
......@@ -2312,9 +2312,13 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
let rec fix_ihs rev_tac :=
lazymatch goal with
| H : context [envs_entails _ _] |- _ =>
eapply (tac_revert_ih _ _ _ H _);
[pm_reflexivity
|| fail "iInduction: spatial context not empty, this should not happen"
notypeclasses refine (tac_revert_ih _ _ _ H _ _ _);
[iSolveTC ||
let φ := match goal with |- IntoIH ?φ _ _ => φ end in
fail "iInduction: cannot import IH" φ
"into proof mode context (IntoIH instance missing)"
|pm_reflexivity ||
fail "iInduction: spatial context not empty, this should not happen"
|clear H];
fix_ihs ltac:(fun j =>
let IH' := eval vm_compute in
......
......@@ -790,3 +790,24 @@ Tactic failure: iIntuitionistic: "H" not fresh.
: string
The command has indeed failed with message:
Tactic failure: iSpatial: "H" not fresh.
"test_iInduction_Forall"
: string
1 goal
PROP : bi
P : ntree → PROP
l : list ntree
============================
"H" : ∀ l0 : list ntree, (∀ x : ntree, ⌜x ∈ l0⌝ → P x) -∗ P (Tree l0)
"IH" : [∗ list] x ∈ l, □ P x
--------------------------------------□
P (Tree l)
"test_iInduction_Forall_fail"
: string
The command has indeed failed with message:
Tactic failure: iInduction: cannot import IH
(my_Forall
(λ t : ntree,
"H" : ∀ l : list ntree, ([∗ list] x ∈ l, P x) -∗ P (Tree l)
--------------------------------------□
P t) l) into proof mode context (IntoIH instance missing).
......@@ -1712,3 +1712,63 @@ Proof.
Abort.
End tactic_tests.
Section mutual_induction.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Implicit Types φ : nat PROP.
Implicit Types Ψ : nat nat PROP.
Unset Elimination Schemes.
Inductive ntree := Tree : list ntree ntree.
(** The common induction principle for finitely branching trees. By default,
Coq generates a too weak induction principle, so we have to prove it by hand. *)
Lemma ntree_ind (φ : ntree Prop) :
( l, Forall φ l φ (Tree l))
t, φ t.
Proof.
intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
induction l as [|t l IH]; constructor; auto.
Qed.
(** Now let's test that we can derive the internal induction principle for
finitely branching trees in separation logic. There are many variants of the
induction principle, but we pick the variant with an induction hypothesis of
the form [∀ x, ⌜ x ∈ l ⌝ → ...]. This is most interesting, since the proof
mode generates a version with [[∗ list]]. *)
Check "test_iInduction_Forall".
Lemma test_iInduction_Forall (P : ntree PROP) :
( l, ( x, x l P x) - P (Tree l)) -
t, P t.
Proof.
iIntros "#H" (t). iInduction t as [] "IH".
Show. (* make sure that the induction hypothesis is exactly what we want *)
iApply "H". iIntros (x ?). by iApply (big_sepL_elem_of with "IH").
Qed.
(** Now let us define a custom version of [Forall], called [my_Forall], and
use that in the variant [ntree_ind_alt] of the induction principle. The proof
mode does not support [my_Forall], so we test if [iInduction] generates a
proper error message. *)
Inductive my_Forall {A} (φ : A Prop) : list A Prop :=
| my_Forall_nil : my_Forall φ []
| my_Forall_cons x l : φ x my_Forall φ l my_Forall φ (x :: l).
Lemma ntree_ind_alt (φ : ntree Prop) :
( l, my_Forall φ l φ (Tree l))
t, φ t.
Proof.
intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
induction l as [|t l IH]; constructor; auto.
Qed.
Check "test_iInduction_Forall_fail".
Lemma test_iInduction_Forall_fail (P : ntree PROP) :
( l, ([ list] x l, P x) - P (Tree l)) -
t, P t.
Proof.
iIntros "#H" (t).
Fail iInduction t as [] "IH" using ntree_ind_alt.
Abort.
End mutual_induction.
Supports Markdown
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