Commit a9354385 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add `iInduction` tests.

parent 6ab9c4e7
...@@ -781,3 +781,11 @@ Tactic failure: iPure: (φ n) not pure. ...@@ -781,3 +781,11 @@ Tactic failure: iPure: (φ n) not pure.
: string : string
The command has indeed failed with message: The command has indeed failed with message:
Tactic failure: iIntuitionistic: Q not persistent. Tactic failure: iIntuitionistic: Q not persistent.
The command has indeed failed with message:
Tactic failure: iInduction: cannot import IH
(my_Forall
(λ t : tree,
"H" : ∀ l : list tree, ([∗ list] x ∈ l, P x) -∗ P (Tree l)
--------------------------------------□
P t
) l) into proof mode context.
...@@ -1618,3 +1618,62 @@ Proof. ...@@ -1618,3 +1618,62 @@ Proof.
Qed. Qed.
End tactic_tests. 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 tree := Tree : list tree tree.
(** 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 tree_ind (φ : tree 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 the big op [[∗ list]] in
the induction hypothesis. This is also most interesting, since the proof mode
generates an induction hypothesis of the form [∀ x, ⌜ x ∈ l ⌝ → ...]. *)
Lemma test_iInduction_Forall (P : tree PROP) :
( l, ([ list] x l, P x) - P (Tree l)) -
t, P t.
Proof.
iIntros "#H" (t). iInduction t as [] "IH".
iApply "H". iApply big_sepL_intro.
iIntros "!#" (k t' ?%elem_of_list_lookup_2).
by iApply ("IH" with "[%]").
Qed.
(** Now let's define a custom version of [Forall], called [my_Forall], and
use that in the variant [tree_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 tree_ind_alt (φ : tree 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.
Lemma test_iInduction_Forall_fail (P : tree PROP) :
( l, ([ list] x l, P x) - P (Tree l)) -
t, P t.
Proof.
iIntros "#H" (t).
Fail iInduction t as [] "IH" using tree_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