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

Tweaks.

parent b203a304
Pipeline #61884 passed with stage
in 7 minutes and 45 seconds
......@@ -480,10 +480,11 @@ Note 1: We need an [IntoIH] instance for any predicate transformer (like
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 operating
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. *)
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.
......
......@@ -2315,7 +2315,8 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
notypeclasses refine (tac_revert_ih _ _ _ H _ _ _);
[iSolveTC ||
let φ := match goal with |- IntoIH ?φ _ _ => φ end in
fail "iInduction: cannot import IH" φ "into proof mode context"
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];
......
......@@ -810,4 +810,4 @@ Tactic failure: iInduction: cannot import IH
(λ t : ntree,
"H" : ∀ l : list ntree, ([∗ list] x ∈ l, P x) -∗ P (Tree l)
--------------------------------------□
P t) l) into proof mode context.
P t) l) into proof mode context (IntoIH instance missing).
......@@ -1747,8 +1747,8 @@ Section mutual_induction.
iApply "H". iIntros (x ?). by iApply (big_sepL_elem_of with "IH").
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
(** 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 :=
......
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