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

Improve documentation for `use_tac_specialize_intuitionistic_helper`.

parent 929c1043
......@@ -952,9 +952,10 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
let pats := spec_pat.parse pat in iSpecializePat_go H pats.
(** The tactics [iSpecialize trm as #] and [iSpecializeCore trm as true] allow
one to use the entire spatial context for proving the premises [Q1 .. Qn] of
[H : Q1 -* .. -∗ Qn -∗ R], as well as the remaining goal. This is possible if
all of the following properties hold:
one to use the entire spatial context /twice/: the first time for proving the
premises [Q1 .. Qn] of [H : Q1 -* .. -∗ Qn -∗ R], and the second time for
proving the remaining goal. This is possible if all of the following properties
hold:
1. The conclusion [R] of the hypothesis [H] is persistent.
2. The specialization pattern [[> ..]] for wrapping a modality is not used for
any of the premises [Q1 .. Qn].
......@@ -974,12 +975,13 @@ and friends, the behavior on violations of these conditions is as follows:
hypotheses for proving the premises [Q1 .. Qn]. That is, it will fall back to
not using [tac_specialize_intuitionistic_helper].
The function [use_tac_specialize_intuitionistic_helper Δ pat] below checks if
the specialization pattern [pat] consumes any spatial hypotheses, and does not
contain the pattern [[> ..]] (cf. condition 2). If the specialization pattern
[pat] does not consume any spatial hypotheses, there is no benefit in using
[tac_specialize_intuitionistic_helper], and we thus do not need to require
condition 1 and 3 to hold. *)
The function [use_tac_specialize_intuitionistic_helper Δ pat] below returns
[true] iff the specialization pattern [pat] consumes any spatial hypotheses,
and does not contain the pattern [[> ..]] (cf. condition 2). If the function
returns [false], then the conclusion can be moved in the intuitionistic context
even if conditions 1 and 3 do not hold. Therefore, in that case, we prefer
putting the conclusion to the intuitionistic context directly and not using
[tac_specialize_intuitionistic_helper], which requires conditions 1 and 3. *)
Fixpoint use_tac_specialize_intuitionistic_helper {M}
(Δ : envs M) (pats : list spec_pat) : bool :=
match pats with
......@@ -991,7 +993,7 @@ Fixpoint use_tac_specialize_intuitionistic_helper {M}
match envs_lookup_delete false H Δ with
| Some (false, _, Δ) => true
| Some (true, _, Δ) => use_tac_specialize_intuitionistic_helper Δ pats
| None => false
| None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
end
| SGoal (SpecGoal GModal _ _ _ _) :: _ => false
| SGoal (SpecGoal GIntuitionistic _ _ _ _) :: pats =>
......@@ -1002,7 +1004,7 @@ Fixpoint use_tac_specialize_intuitionistic_helper {M}
| Some (Δ1,Δ2) => if env_spatial_is_nil Δ1
then use_tac_specialize_intuitionistic_helper Δ2 pats
else true
| None => false
| None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
end
end.
......
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