Interpolants for proper clusters (Lemma 9.3) #
This file contains the interpolation step for proper clusters: given interpolants for all exit nodes of a cluster, we build an interpolant for the root of the cluster.
The ingredients live in the files imported here:
Pdl.InterpolationCluster (the cluster C, its quasi-tableau Q of Def 9.8, the region
formulas θ_Δ of Def 9.13 and Lemma 9.14), Pdl.QFormula (Def 9.15, Def 9.16 and
Fact 9.17), Pdl.PreInterpolant (the pre-interpolants of Def 9.18), Pdl.ClusterItp
(Def 9.20 and Lemma 10.1), Pdl.ClusterRho (Def 10.2 and Lemma 10.3) and
Pdl.ClusterSatDown (Lemmas 10.6, 10.7 and 10.8).
The three conditions on the interpolant θ_r := C.itp θ of Definition 9.20 are exactly
LoadedCluster.itp_voc(Lemma 10.1),LoadedCluster.left_unsat_neg_itp(Lemma 10.3), andLoadedCluster.right_unsat_itp(Lemma 10.8).
What this file adds is the interface: the interpolants θ used by those three results
are indexed by the fine exit nodes of the cluster, i.e. also by nodes inside a local
tableau, while clusterInterpolation_right is only given interpolants for the exits in the
coarse PathIn sense. The first half of the file bridges that gap, by pushing the
interpolants of the coarse exits upwards through the local tableaux with
LocalTableau.interpolant.
Helpers for endNodesOf #
Since endNodesOf now returns a Finset Sequent, this membership lemma replaces the
old simp only [endNodesOf, List.mem_flatten, ...] incantations. For the byLocalRule
case we use mem_endNodesOf_byLocalRule_iff from Pdl/Interpolation/FinePath.lean.
It would better belong in Pdl/Local/Tableau.lean, next to endNodesOf.
Flipping Interpolants #
When X is an interpolant for X, then ~θ is an interpolant for X.flip.
Transport an interpolant back from the flipped tableau.
Equations
- ip.unflipPath = ⟨~↑ip, ⋯⟩
Instances For
From the coarse exits to the fine exits #
A fine exit of the cluster is either a coarse node — then it is an exit in the coarse sense and we are given an interpolant for it — or a node inside a local tableau from which the cluster is never re-entered. In the latter case all end nodes of the local tableau below it are coarse exits, and we obtain an interpolant by local interpolation.
Every end node of the local tableau at a local path is an end node of the whole local tableau that is below that path.
A coarse child below a fine node really is a child of the base of that fine node.
A sharpening of FinePathIn.base_of_mem_children: a fine child that lies at a
different coarse node is a coarse node itself.
Local interpolation at fine nodes. If a fine node is not a coarse node, i.e. it
lies properly inside a local tableau, and we have interpolants for all coarse children
below it — these are the end nodes of that local tableau that are reachable from it — then
we have an interpolant for the fine node itself. This is LocalTableau.interpolant applied
to the part of the local tableau below the node.
An interpolant for the label of a fine node, whenever one exists. This is the map θ
on the fine exit nodes that Definitions 9.13 and 9.18 need.
Instances For
Every coarse child below a fine exit of the cluster is a coarse exit of the cluster.
Interpolants for the coarse exits of the cluster give interpolants for all fine exits.
The interpolants of the fine exit nodes of the cluster, given interpolants for the
coarse exits. This is the map θ of Definitions 9.13, 9.18 and 9.20.
Vocabulary preservation #
Lemma 9.2 of the paper: along the tableau the vocabulary of each of the two components
only shrinks. "By inspection of the rules": for local rules this is
localRule_does_not_increase_vocab_L and localRule_does_not_increase_vocab_R, and for
the PDL rules we check the six cases directly.
Membership in the vocabulary of a Finset of formulas.
This is Finset.mem_fvoc from Pdl/Interpolation/Local.lean.
A local rule application does not increase the vocabulary of the left component.
This is the left half of localRuleApp_does_not_increase_jvoc.
A local rule application does not increase the vocabulary of the right component.
This is the right half of localRuleApp_does_not_increase_jvoc.
Inside a local tableau the vocabulary of the left component only shrinks.
Inside a local tableau the vocabulary of the right component only shrinks.
Right rules do not change the left component #
The two "right" local rules only act on the right component and on a loaded formula on the
right, so they leave the left component of the sequent unchanged. The (M) rule does
change the left component, but it is a Tableau.pdl step and hence only applies to a basic
sequent, whose right component is then basic as well.
Where a right rule is applied, it is either a local rule or the node is basic (because
the (M) rule is only applied at basic nodes).
At a node where a right rule is applied to a non-basic right component, all children have the same left component as the node itself.
A right local rule cannot be applied when the right component of the sequent is basic: the rule only looks at the right component and at a loaded formula on the right, so it would also be applicable to the sequent with an empty left component.
The right component of the child obtained by applying the modal rule (M) to a sequent
whose loaded formula ~⌊·A⌋ξ is on the right. Note that it only depends on A, on ξ and
on the right component R of the sequent, and hence only on Λ₂ of the node.
Equations
- modRChildRightOnly A (AnyFormula.normal φ) R = (∅, {~φ} ∪ Finset.projection A R, none)
- modRChildRightOnly A (AnyFormula.loaded χ) R = (∅, Finset.projection A R, some (Sum.inr (~'χ)))
Instances For
At a fine node with a basic right component where a right rule is applied, that rule
is one of the three PdlRules acting on the right — and in particular the node is a node
in the coarse sense. The three cases are (L+), where the node is free, (L-), whose
unique child is free, and the modal rule (M), whose unique child has the projected left
component and a right component determined by Λ₂ of the node.
Left rules do not change the right component #
Dually, a left local rule leaves the right component of the sequent unchanged, provided the
loaded formula is on the right (otherwise the (¬) rule for the loaded formula on the left
would change the Olf). The left PdlRules (L+), (L-) and (M) are all only
applicable when the loaded formula is not on the right.
Where a left rule is applied, it is a local rule, unless the loaded formula is not on
the right (which for a node of a LoadedCluster cannot happen).
Part of Lemma 9.7 (c): at a node with the loaded formula on the right where a left rule is applied, all children have the same right component as the node itself.
Local invertibility of a left rule, for the left component only: if the left component of the premise holds at a world, then so does the left component of one of the conclusions.
Note that localRuleTruth does not give this, since it also speaks about the right
component, which need not hold at the world in question. That the loaded formula is on the
right is needed to exclude the rule for a loaded formula on the left.
Local invertibility at a fine node where a left rule is applied, for the left component only: if a formula follows from the left component of every child, then it follows from the left component of the node itself.
Loading on the right is inherited upwards, and rules with children are left or right #
Two ingredients for the descent of Lemma 9.7 (d) below. First, a fine node that has a
coarse child loaded on the right is itself loaded on the right — this is what lets us apply
FinePathIn.children_rightOnly_eq_of_usesLeftRule at the fine nodes of a cluster. Second,
a fine node with children applies a left or a right rule: the only local rules that are
neither are the closing rules, and those have no children.
If a child of a local rule application is loaded on the right, then so is its premise. The local rules for a loaded formula on the left never produce a loading on the right, and the one-sided rules do not change the loaded formula at all.
If some end node of a local tableau is loaded on the right, then so is its root.
The end nodes below a local path are end nodes of the local tableau at that path.
A fine node that is not a coarse node and has a coarse child loaded on the right is
itself loaded on the right. (For coarse nodes this is false: the (L+) rule loads a free
node.)
A local rule application with at least one child is a left or a right rule: only the
closing rules (¬) are neither, and they have no results.
A fine node that has children applies a left or a right rule.
Loaded-path repeats and the Dershowitz-Manna measure #
The three lemmas here are what replaces the paper's Fact lprAreCritical in the proof of
Lemma 9.7 (d) below: instead of showing that the modal rule is applied between a companion
and its repeat we show that going down along left rules strictly decreases the
Dershowitz-Manna measure of the label, while a companion carries exactly the same label as
its repeat.
A fine node whose base is a loaded-path repeat is that coarse node itself, because a
loaded-path repeat is a leaf and hence has no local tableau with internal nodes.
This would better belong next to atBigRoot in Pdl/Interpolation/FinePath.lean.
Where a left rule is applied at a node with the loaded formula on the right, the labels
of all children are strictly smaller in the Dershowitz-Manna ordering: by
FinePathIn.leftRuleStep the rule applied there is a local rule, and local rules decrease
the measure.
The two standing assumptions of the paper #
The paper fixes a uniform closed tableau and a proper cluster in it, and both assumptions
are used in Section 9. Neither of them holds for an arbitrary values of the Tableau type.
- the
Tableautype does not force any coherence between the rules applied at different nodes, whereas uniformity (U1/U2) makes the rule applied at a node with a loaded, non-basic right component depend only on that component.
This is captured in the form needed here in LoadedCluster.HasUniformSteps.
Note that this file never unfolds LoadedCluster.HasUniformSteps: it is only used
opaquely, as the hypothesis of LoadedCluster.stepOf_spec and as the conclusion of
LoadedCluster.uniformOfUniTab. So the definition of HasUniformSteps may still be
changed (for example from a List comparison to a Finset.image one) without affecting
anything here, as long as those two statements are kept.
The vocabulary fields #
Every fine node of C⁺ is ◃-reachable from the root of the cluster.
The vocL field of PaperFacts: the vocabulary of the left component only shrinks
below the root of the cluster.
The vocR field of PaperFacts: the vocabulary of the right component only shrinks
below the root of the cluster.
The remaining fields #
Lemma 9.7 (e): at a node t of C^R_Δ with Δ basic the rule applied is the modal
rule (M) for the loaded formula ~⌊·A⌋ξ of Δ. Its unique child u satisfies
Λ₁(u) = (Λ₁(t))_A, and its right component only depends on Δ.
Properness is needed to exclude the two other right PdlRules: (L+) is only applied at
a free node, while (L-) makes its unique child free, and both contradict Lemma 9.4 (a)
because by Lemma 9.4 (c) some child of t is again in the cluster.
Every element of stepOf Δ is the right component of a child of some node of C^R_Δ,
namely of the first one.
The descent for Lemma 9.7 (d) #
The paper picks a node t ∈ C_Δ that is minimal in the tree order and then follows
left-rule children downwards; by FinePathIn.children_rightOnly_eq_of_usesLeftRule this
stays inside C_Δ, and closing rules are excluded because they have no children while
Lemma 9.4 (c) (nonLpr_some_child_in_C, which needs properness) provides one.
The descent itself is FinePathIn.descent from Pdl.FinePathDescent: fine children are not
structurally smaller, so the recursion is justified by the well-foundedness of the flipped
fine child relation.
Every fine node of the cluster is loaded on the right, i.e. Lemma 9.4 (a) at the fine
level. For nodes that are coarse nodes this is all_right_loaded; for the intermediate
nodes of a local tableau it follows because a coarse child of theirs is in the cluster and
loading on the right is inherited upwards inside a local tableau.
The descent of Lemma 9.7 (d): if C_Δ is non-empty then either C^R_Δ is non-empty,
or C_Δ contains a loaded-path repeat.
Starting from any node of C_Δ we follow children: as long as no right rule is applied and
no repeat is reached, the node has a child in the cluster (Lemma 9.4 (c), which needs
properness) with the same right component (Lemma 9.7 (c)), and the descent terminates by
FinePathIn.descent — but a childless node of the cluster which is not a repeat would
contradict Lemma 9.4 (c).
This is the paper's descent. It is no longer needed for Lemma 9.7 (d) below, which is now
proved via isLrep_of_mem_nodesWithFine, but it is kept as the direct formalisation of the
argument in the paper.
If a node of C_Δ is a loaded-path repeat then its companion is again a node of C_Δ,
it carries the same label, and it is not a loaded-path repeat itself.
That the companion is in the cluster is Lemma 9.4 (c) (lpr_comp_in_C); that it carries
the same label is nodeAt_companionOf_setEq — note that with Finset sequents this is
literal equality; and it is not a repeat because it is a proper ancestor of the repeat,
while a repeat is a leaf.
Every node of C_Δ is a loaded-path repeat, provided C^R_Δ is empty.
This is the key step for Lemma 9.7 (d). The proof is by well-founded induction on the label
along the Dershowitz-Manna ordering lt_Sequent: at a node of C_Δ that is not a repeat a
left rule is applied — a right rule is excluded by the assumption — so by Lemma 9.4 (c)
there is a child in the cluster, its right component is still Δ by Lemma 9.7 (c) and its
label is strictly smaller. Applying the induction hypothesis to that child makes it a
repeat, and then its companion is again in C_Δ with the same, hence still smaller,
label, but is not a repeat — contradicting the induction hypothesis.
Lemma 9.7 (d): if C_Δ is non-empty then so is C^R_Δ.
Where the paper uses its Fact lprAreCritical — on the path from a companion to its repeat
the modal rule is applied at least once — we argue with the Dershowitz-Manna measure
instead: if C^R_Δ were empty then by isLrep_of_mem_nodesWithFine all nodes of C_Δ
would be loaded-path repeats, but the companion of such a repeat is again in C_Δ and is
not a repeat. (Since Sequent now uses Finsets, a repeat carries exactly the same label
as its companion, cf. nodeAt_companionOf_setEq.)
The leading atomic program of a basic label of Λ₂[C] is in the joint vocabulary.
That it is in the vocabulary of Γ₂ is vocabulary preservation. That it is in the
vocabulary of Γ₁ — which the paper does not mention, but which its Lemma 10.1 needs —
uses Lemma 9.7 (e): the modal rule is applied at some t ∈ C^R_Δ and its child u is
again in C, so Λ₁(u) = (Λ₁(t))_a is non-empty by Lemma 9.5 (b), which forces a box
⌈a⌉ψ in Λ₁(t).
The hypothesis hER is Lemma 9.7 (d), i.e. exists_right_of_proper.
The inner induction in the proof of Lemma 10.3, see PaperFacts.leftPropagation.
The argument is a descent along the children of t: an exit is covered by the second
hypothesis and a node of C^R_Δ by the first, while at a node of C^L_Δ all children stay
in C⁺_Δ (by FinePathIn.children_rightOnly_eq_of_usesLeftRule and
LoadedCluster.mem_fineCLplus_of_child) and the local invertibility of the left rule
applied there transfers the entailment back up. That last step is
FinePathIn.leftEntails_of_children_of_usesLeftRule; note that FinePathIn.locally_sound
is not enough here, because it speaks about the whole label while leftEntails only
assumes the left component, so we need the left-only invertibility
LocalRuleApp.left_sat_of_isLeftRule.
The descent is not along the fine child relation but, as in isLrep_of_mem_nodesWithFine,
by well-founded induction on the label along the Dershowitz-Manna ordering lt_Sequent:
left rules strictly decrease the label, and this makes the remaining case, a loaded-path
repeat in C_Δ, work out. At such a repeat no rule is applied, but by
exists_companion_mem_nodesWithFine its companion is again a node of C_Δ with exactly the
same label and is not a repeat, so the claim at the companion — which is the same claim,
since leftEntails only depends on the label — is obtained from the very same case
distinction, at the same label.
Properness of the cluster is used through LoadedCluster.exists_child_memFine_of_not_isLrep
(Lemma 9.4 (c)), which is why no separate properness hypothesis is needed.
Lemma 9.7 (f): at a non-basic Δ the children of any t ∈ C^R_Δ are the Λ₁(t);Π
for Π ∈ stepOf Δ. Here only the existence of a node of C⁺_Π with the same left
component as t is recorded, which is what the proof of Lemma 10.3 uses.
Lemma 9.7 (e), in the semantic form used in the proof of Lemma 10.3.
Note that no uniformity is needed here: by basicModalStepAt the right components of the
children of a node of C^R_Δ with Δ basic are determined by Δ alone, so the list
stepOf Δ, read off the first node of C^R_Δ, describes the children of every node of
C^R_Δ.
All facts of PaperFacts, from the two standing assumptions of the paper.
What is proved and what is still assumed #
LoadedCluster.paperFacts derives all eight fields of LoadedCluster.PaperFacts from the
two assumptions that we also have properness of the cluster (which just LoadedCluster.proper)
and uniformity of the tableau (which we have not actually shown yet).
All of them are proved here:
properis the first assumption itself;vocLandvocRarevocL_fineCLplusandvocR_fineCLplus, proved from vocabulary preservation along◃(sectionVocPreservation) together with the fact that every fine node ofC⁺is◃-reachable from the root;rightRuleChildrenisrightRuleChildren_of_uniform, proved fromstepOf_spec, i.e. from the second assumption;modalStepismodalStep_of, proved from properness alone viabasicModalStepAt, which is Lemma 9.7 (e): at a node ofC^R_ΔwithΔbasic the rule applied is the modal rule(M)for the loaded formula ofΔ;loadedProgVocisloadedProgVoc_of_proper, proved from properness and Lemma 9.7 (d);exists_right(Lemma 9.7 (d)) isexists_right_of_properandleftPropagationisleftPropagation_of_proper, both proved from properness by well-founded induction on the label along the Dershowitz-Manna orderinglt_Sequent.
Where uniformity (conditions U1/U2, formalised as LoadedCluster.HasUniformSteps with
LoadedCluster.stepOf_spec) is needed can now be read off: in exactly one of the eight
fields, namely rightRuleChildren. The reason is that C.stepOf Δ reads the right
components of the children of the first node of C^R_Δ, while the fields of the two
records quantify over all nodes of C^R_Δ:
PaperFacts.rightRuleChildren(used at non-basic type-3 nodes in the proof of Lemma 10.3) says that for everyt ∈ C^R_Δand everyΠ ∈ stepOf Δthere is a node ofC⁺_Πwith the same left component ast. Its proof takes the children oft, so it needs the right components of those children to be the liststepOf Δ— which for a non-basicΔis preciselystepOf_spec, i.e. uniformity.PaperFacts.modalStepandSatDownFacts.basicStepalso quantify overt ∈ C^R_Δ, but only for basicΔ. There the rule applied is the modal rule for the unique loaded formula ofΔ(Lemma 9.7 (e)), so the right components of the children are determined byΔalone; this is whatbasicModalStepAtshows, and it is whymodalStep_ofneeds no uniformity.- The remaining fields (
SatDownFacts.nonBasicStep,SatDownFacts.stepLT,PaperFacts.leftPropagation,exists_right, the vocabulary fields) speak aboutΔandstepOf Δonly, or about local invertibility at a single node, and are independent of uniformity.
Interpolants for proper clusters #
Lemma 9.3 for the case where the loaded formula is on the right side:
given interpolants for all exits of the cluster C, interpolate the root of C.
The interpolant is C.itp θ from Definition 9.20, where θ gives the interpolants of the
fine exit nodes, obtained from the given interpolants of the coarse exits by
LoadedCluster.fineExits_itp_spec. Its three defining properties are Lemma 10.1
(itp_voc), Lemma 10.3 (left_unsat_neg_itp) and Lemma 10.8 (right_unsat_itp).
Equations
- clusterInterpolation_right Xfree t_u C exitIPs = ⟨C.itp FinePathIn.itp, ⋯⟩
Instances For
Lemma 9.3: Given a loaded node s that is the first node of its cluster, and given
interpolants for all exits of that cluster, we get an interpolant for s.
Note how s_cr is exactly what is needed to make a LoadedCluster here.
Equations
- One or more equations did not get rendered due to their size.