diff --git a/LeanPool/PDL/Completeness/BuildTree.lean b/LeanPool/PDL/Completeness/BuildTree.lean index 16bcbf2e56..1a1bde7112 100644 --- a/LeanPool/PDL/Completeness/BuildTree.lean +++ b/LeanPool/PDL/Completeness/BuildTree.lean @@ -10,6 +10,8 @@ public import LeanPool.PDL.Completeness.TableauGame public import LeanPool.PDL.Local.Path public import LeanPool.PDL.PdlSteps +public import LeanPool.PDL.Soundness -- shake: keep + /-! # From winning strategies to model graphs, part 1: BuildTree and PreState (Section 6.3) -/ @[expose] public section diff --git a/LeanPool/PDL/Completeness/TableauGame.lean b/LeanPool/PDL/Completeness/TableauGame.lean index 242fd3dbc3..75bc5a105c 100644 --- a/LeanPool/PDL/Completeness/TableauGame.lean +++ b/LeanPool/PDL/Completeness/TableauGame.lean @@ -8,13 +8,17 @@ module public import Mathlib.Data.Finset.Powerset public import Mathlib.Data.Finset.Functor -public import LeanPool.PDL.Interpolation.Uniformity +public import LeanPool.PDL.Interpolation.UniformityCore public import LeanPool.PDL.General.Game public import LeanPool.PDL.Local.AllLocalTab public import LeanPool.PDL.Completeness.Modelgraphs public import LeanPool.PDL.StayingInFL +import Mathlib.Algebra.Order.Ring.Nat +import Mathlib.Algebra.Order.BigOperators.Group.List +import Mathlib.Data.Nat.SuccPred + /-! # The Tableau Game (Section 6.2) -/ @[expose] public section diff --git a/LeanPool/PDL/Flip.lean b/LeanPool/PDL/Flip.lean index 44ebd57475..303b38047e 100644 --- a/LeanPool/PDL/Flip.lean +++ b/LeanPool/PDL/Flip.lean @@ -6,10 +6,13 @@ Authors: PDL formalization contributors (see project card) module -public import Mathlib.Tactic.DepRewrite - +public import LeanPool.PDL.FlipCore +import all LeanPool.PDL.FlipCore -- shake: keep public import LeanPool.PDL.Soundness +meta import LeanPool.PDL.General.ImportCompatibility +import Mathlib.Util.TermReduce -- shake: keep + /-! # Flipping a tableau (for section 7) Like the paper, we only prove interpolation for clusters with a loaded formulas on the right side. @@ -22,798 +25,16 @@ The lemmas here then allow us to prove `clusterInterpolation` from `clusterInter namespace PDL -/-- Exchange the side of an optional loaded formula. -/ -def Olf.flip : Olf → Olf := Option.map Sum.swap - -@[simp] -lemma Olf.flip_inj {O1 O2 : Olf} : O1.flip = O2.flip ↔ O1 = O2 := by - rcases O1 with (_|_|_) <;> rcases O2 with (_|_|_) <;> simp_all [Olf.flip] - -@[simp] -lemma Olf.flip_flip {O : Olf} : O.flip.flip = O := by - rcases O with (_|_|_) <;> simp_all [Olf.flip] - -@[simp] -lemma Olf.flip_none : Olf.flip none = none := by simp [Olf.flip] - -/-- Exchange both sequent components and the side of its loaded formula. -/ -def Sequent.flip : Sequent → Sequent := fun ⟨L, R, O⟩ => ⟨R, L, O.flip⟩ - -@[simp] -lemma Sequent.flip_right {X : Sequent} : X.flip.right = X.left := by - rcases X with ⟨L,R,_|_|_⟩ <;> simp [Sequent.flip, Olf.flip] - -@[simp] -lemma Sequent.flip_left {X : Sequent} : X.flip.left = X.right := by - rcases X with ⟨L,R,_|_|_⟩ <;> simp [Sequent.flip, Olf.flip] - -@[simp] -lemma Sequent.flip_flip {X : Sequent} : X.flip.flip = X := by - rcases X with ⟨L,R,O⟩ - simp_all [Sequent.flip, Olf.flip] - -@[simp] -lemma Sequent.flip_isLoaded {X : Sequent} : - X.flip.isLoaded ↔ X.isLoaded := by - rcases X with ⟨L, R, O⟩ - simp only [Sequent.isLoaded, Sequent.flip, Olf.flip] - grind - -@[simp] -lemma Sequent.flip_isFree {X : Sequent} : - X.flip.isFree ↔ X.isFree := by - unfold Sequent.isFree - simp - -lemma Sequent.flip_eq_off {X Y : Sequent} : (X.flip = Y) = (X = Y.flip) := by - rcases X with ⟨L,R,O⟩ - rcases Y with ⟨L',R',O'⟩ - simp_all only [flip] - rw [@propext_iff] - constructor <;> intro h <;> cases h <;> convert rfl <;> simp - -lemma Sequent.map_flip_map_flip {Hist} : - (List.map Sequent.flip (List.map Sequent.flip Hist)) = Hist := by - induction Hist <;> simp_all - -/-- Flipping all sequents in a `Finset` twice gives back the same set. -/ -@[simp] -lemma Sequent.image_flip_image_flip {S : Finset Sequent} : - Finset.image Sequent.flip (Finset.image Sequent.flip S) = S := by - rw [Finset.image_image] - simp [Function.comp_def] - -@[simp] -lemma basic_flip {X : Sequent} : X.flip.basic ↔ X.basic := by - rcases X with ⟨L,R,O⟩ - unfold Sequent.basic Sequent.flip - simp only - simp only [Sequent.toFinset, Finset.union_assoc, Finset.mem_union, Option.mem_toFinset, - Option.mem_def, Option.map_eq_some_iff, Sum.exists, Sum.elim_inl, negUnload, Sum.elim_inr, - Formula.basic, decide_false, decide_true, Sequent.closed, not_or, not_exists, not_and] - constructor - · intro ⟨fs_basic, not_closed⟩ - constructor - · intro φ φ_in - apply fs_basic - rcases φ_in with h|h|h|h - · grind only [] - · grind only [] - · right - right - right - simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, Sum.inr.injEq, - exists_eq_right, Sum.swap_inr, reduceCtorEq, and_false, exists_false, or_false] - exact h - · right - right - left - simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, reduceCtorEq, - and_false, exists_false, Sum.swap_inr, Sum.inl.injEq, exists_eq_right, false_or] - exact h - · aesop (rule_sets := [-default]) - · intro ⟨fs_basic, not_closed⟩ - constructor - · intro φ φ_in - apply fs_basic - rcases φ_in with h|h|h|h - · grind only [] - · grind only [] - · right - right - right - simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, reduceCtorEq, - and_false, exists_false, Sum.swap_inr, Sum.inl.injEq, exists_eq_right, false_or] at h - exact h - · right - right - left - simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, Sum.inr.injEq, - exists_eq_right, Sum.swap_inr, reduceCtorEq, and_false, exists_false, or_false] at h - exact h - · aesop (rule_sets := [-default]) - -/-- Reflect a local rule by exchanging its left and right components. -/ -def LocalRule.flip {Lcond Ocond Rcond ress} (lr : LocalRule (Lcond, Rcond, Ocond) ress) : - LocalRule (Rcond, Lcond, Ocond.flip) (ress.image Sequent.flip) := by - cases lr - case oneSidedL YS orule YS_def => - apply LocalRule.oneSidedR orule - aesop - case oneSidedR YS orule YS_def => - apply LocalRule.oneSidedL orule - aesop - case LRnegL => - apply LocalRule.LRnegR - case LRnegR => - apply LocalRule.LRnegL - case loadedL YS χ lrule YS_def => - apply LocalRule.loadedR _ lrule - subst YS_def - rw [Finset.image_image] - apply Finset.image_congr - rintro ⟨L, (_|o)⟩ - <;> simp [Sequent.flip, Olf.flip] - case loadedR lrule YS_def => - apply LocalRule.loadedL _ lrule - subst YS_def - rw [Finset.image_image] - apply Finset.image_congr - rintro ⟨L, (_|o)⟩ - <;> simp [Sequent.flip, Olf.flip] - -lemma LocalRule.flip_flip {Lcond Ocond Rcond ress} (lr : LocalRule (Lcond, Rcond, Ocond) ress) : - lr.flip.flip = Olf.flip_flip ▸ Sequent.image_flip_image_flip ▸ lr := by - cases lr <;> simp_all [LocalRule.flip] <;> grind only [] - -/-- Note: is it possible and useful to rewrite this in more term and less tactic mode? -/ -def LocalRuleApp.flip : LocalRuleApp → LocalRuleApp := by - rintro ⟨L, R, O, Lcond, Rcond, Ocond, ress, rule, C, hC, preconditionProof⟩ - refine @LocalRuleApp.mk R L O.flip Rcond Lcond Ocond.flip _ rule.flip - (C.image Sequent.flip) ?_ ?_ - · subst hC - simp only [applyLocalRule] - rw [Finset.image_image, Finset.image_image] - apply Finset.image_congr - rintro ⟨Lnew, Rnew, Onew⟩ - - simp only [Function.comp_apply, Sequent.flip] - rcases O with (_|_|_) <;> rcases Onew with (_|_|_) <;> rcases Ocond with (_|_|_) - <;> simp [Olf.flip, Olf.change, SDiff.sdiff] <;> grind - · rcases preconditionProof with ⟨hL, hR, hO⟩ - refine ⟨hR, hL, ?_⟩ - rcases O with (_|_|_) <;> rcases Ocond with (_|_|_) <;> simp_all [Olf.flip, Sum.swap] - -@[simp] -lemma Sequent.flip_comp_flip : Sequent.flip ∘ Sequent.flip = id := by - ext X - rw [Function.comp_apply, Sequent.flip_flip, id_eq] - -lemma LocalRuleApp.flip_flip {lra : LocalRuleApp} : - lra.flip.flip = lra := by - rcases lra with ⟨L, R, O, C, Lcond, Rcond, Ocond, ress, rule, hC, preconditionProof⟩ - simp only [flip, Olf.flip_flip, Sequent.image_flip_image_flip, mk.injEq, and_true, true_and] - rw [LocalRule.flip_flip] - grind only [] - -lemma Sequent.flip_mem_of_mem_image_flip {B : Finset Sequent} {Y : Sequent} : - Y ∈ B.image Sequent.flip → Y.flip ∈ B := by aesop (rule_sets := [-default]) - -/-- Reflect every rule and branch of a local tableau. -/ -def LocalTableau.flip {X} : LocalTableau X → LocalTableau X.flip - | (@byLocalRule X lra X_def next) => .byLocalRule lra.flip - (by subst X_def; simp [LocalRuleApp.flip, Sequent.flip]) - (fun Y Y_in => - @Sequent.flip_flip Y ▸ (next Y.flip (Sequent.flip_mem_of_mem_image_flip Y_in)).flip) - | (@sim X Xbas) => .sim (basic_flip.mpr Xbas) - -lemma LocalTableau.flip_flip {lt : LocalTableau X} : lt.flip.flip = Sequent.flip_flip ▸ lt := by - induction lt <;> simp only [flip] - case byLocalRule X lra X_def next IH => - apply eq_of_heq - rw! (castMode := .all) [Sequent.flip_flip] -- :-) - simp only [heq_eq_eq, byLocalRule.injEq] - constructor - · exact LocalRuleApp.flip_flip - · refine Function.hfunext rfl ?_ - intro X X' X_heq_X' - apply Function.hfunext - · rw [LocalRuleApp.flip_flip] - grind only [] - · grind only [] - · grind only [] - -lemma LocalTableau.flip_inj {X} {lt : LocalTableau X} : - lt.flip.flip = (Sequent.flip_flip ▸ lt) := by - cases lt - case byLocalRule => - rw [LocalTableau.flip_flip] - · grind only [LocalTableau.flip] - -lemma endNodesOf_flip {X} {lt : LocalTableau X} {Y} : - Y ∈ endNodesOf lt.flip → Y.flip ∈ endNodesOf lt := by - intro Y_in - induction lt - case byLocalRule B next lra IH => - simp only [LocalTableau.flip, endNodesOf, Finset.sup_image, Function.id_comp, Finset.mem_sup, - Finset.mem_attach, true_and, Subtype.exists] at * - rcases Y_in with ⟨W, W_in_B, Y_in_end⟩ - refine ⟨W.flip, ?_, ?_⟩ <;> grind only [] - case sim Z Zbas => - simp_all [LocalTableau.flip] - -lemma exists_flip_of_endNodesOf {X : Sequent} {ltf : LocalTableau X.flip} {Zf} : - Zf ∈ endNodesOf ltf → ∃ Z, Zf = Z.flip ∧ Z ∈ endNodesOf ltf.flip := by - intro Z_in - cases ltf - case byLocalRule lra next X_def => - simp only [endNodesOf, Finset.sup_image, Function.id_comp, Finset.mem_sup, Finset.mem_attach, - true_and, Subtype.exists, LocalTableau.flip] at * - rcases Z_in with ⟨Yf, Yf_in_B, Zf_via_Yf⟩ - refine ⟨Zf.flip, ?_, ⟨Yf.flip, ?_, ?_⟩⟩ - · simp - · grind [LocalRuleApp.flip] - · rw! (castMode := .all) [@Sequent.flip_flip Yf] - simp only - apply endNodesOf_flip - rw [LocalTableau.flip_flip] - grind - case sim Xbas => - simp_all only [endNodesOf, Finset.mem_singleton, LocalTableau.flip] - subst_eqs - simp - -/-- Reflect a PDL rule by exchanging the sequent components. -/ -def PdlRule.flip {X Y} (r : PdlRule X Y) : PdlRule X.flip Y.flip := by - cases r - case loadL L δs α φ R in_L notBox Y_def => - apply PdlRule.loadR in_L notBox - simp_all only [Sequent.flip, Prod.mk.injEq, true_and] - rfl - case loadR R δs α φ L in_R notBox Y_def => - apply PdlRule.loadL in_R notBox - simp_all only [Sequent.flip, Prod.mk.injEq, true_and] - rfl - case freeL L R δs α φ X_def Y_def => - apply PdlRule.freeR - all_goals - subst X_def Y_def - simp_all only [Sequent.flip] - rfl - case freeR L R δs α φ X_def Y_def => - apply PdlRule.freeL - all_goals - subst X_def Y_def - simp_all only [Sequent.flip] - rfl - case modL L R a ξ X_def Y_def => - apply @PdlRule.modR Y.flip R L a X.flip ξ - all_goals - subst X_def Y_def - cases ξ <;> simp_all [Sequent.flip,Olf.flip] - case modR L R a ξ X_def Y_def => - apply @PdlRule.modL Y.flip R L a X.flip ξ - all_goals - subst X_def Y_def - cases ξ <;> simp_all [Sequent.flip,Olf.flip] - -lemma PdlRule.flip_flip {X Y} (r : PdlRule X Y) : - r.flip.flip = (Sequent.flip_flip ▸ Sequent.flip_flip ▸ r) := by - cases r <;> simp [PdlRule.flip] <;> grind only [] - -/-- Flipping sequents is injective. -/ -@[simp] -lemma Sequent.flip_eq_flip_iff {X Y : Sequent} : X.flip = Y.flip ↔ X = Y := by - constructor - · intro h - rw [← @Sequent.flip_flip X, ← @Sequent.flip_flip Y, h] - · rintro rfl - rfl - -/-- Reflect a loaded-path repeat, preserving its history position. -/ -def LoadedPathRepeat.flip {Hist X} : LoadedPathRepeat Hist X → - LoadedPathRepeat (List.map Sequent.flip Hist) X.flip -| ⟨k, hk⟩ => by - refine ⟨⟨k.1, ?_⟩, ?_⟩ - · simp_all [List.length_map] - · rcases hk with ⟨same, path_loaded⟩ - constructor - · simp only [List.get_eq_getElem, List.getElem_map, Sequent.flip_eq_flip_iff] - exact same - · simp only [List.get_eq_getElem, List.getElem_map, Sequent.flip_isLoaded] - intro m m_lt - apply path_loaded ⟨m, by grind⟩ - omega - -lemma LoadedPathRepeat.flip_flip {Hist X} (lpr : LoadedPathRepeat Hist X) : - lpr.flip.flip = Sequent.map_flip_map_flip ▸ Sequent.flip_flip ▸ lpr := by - rcases lpr with ⟨k, hk⟩ - simp only [flip, List.get_eq_getElem] - rw! [Sequent.map_flip_map_flip, Sequent.flip_flip] - rfl - -@[simp] -lemma flprep_flip {Hist} : - flprep (List.map Sequent.flip Hist) X.flip ↔ flprep Hist X := by - simp_all only [flprep, rep, ↓existsAndEq, List.mem_map, Sequent.flip_eq_flip_iff, - exists_eq_right, and_true, Sequent.isFree, Sequent.flip_isLoaded] - refine ⟨?_,?_⟩ - · rintro (frep|⟨⟨lpr⟩⟩ ) - · grind only [] - · have := lpr.flip - right - simp only [List.map_map, Sequent.flip_comp_flip, List.map_id_fun, id_eq, Sequent.flip_flip] - at this - exact ⟨this⟩ - · rintro (frep|⟨⟨lpr⟩⟩ ) - · grind only [] - · have := lpr.flip - right - exact ⟨this⟩ - -/-- Exchange the left and right sides throughout a tableau. -/ -def Tableau.flip {Hist X} : Tableau Hist X → Tableau (Hist.map Sequent.flip) X.flip -| .loc nflprep nbas lt next => .loc (by simp only [flprep_flip]; exact nflprep) - (by simp only [basic_flip]; exact nbas) - lt.flip - (fun Y Y_in => - @Sequent.flip_flip Y ▸ (next Y.flip (endNodesOf_flip Y_in)).flip) -| .pdl nflprep bas r next => .pdl (by simp only [flprep_flip]; exact nflprep) - (by simp only [basic_flip]; exact bas) - r.flip - next.flip -| .lrep lpr => .lrep lpr.flip - -lemma Hist_flip {Hist} : List.map Sequent.flip (List.map Sequent.flip Hist) = Hist := by ext; simp - -@[simp] -lemma Tableau.flip_flip {Hist X} {tab : Tableau Hist X} : - tab.flip.flip = Sequent.flip_flip ▸ Hist_flip ▸ tab := by - induction tab - case loc Hist X nflprep nbas ltX next IH => - simp only [flip] - rw! [LocalTableau.flip_flip] - rw! (castMode := .all) [Sequent.flip_flip] - simp only [] - convert Tableau.loc.congr_simp nflprep nbas ltX next next ?_ - · exact Sequent.map_flip_map_flip - · exact Sequent.map_flip_map_flip - case h Y W Y_eq_W Y_in W_in Y_heq_W => - subst Y_eq_W - simp_all only [List.map_map, Sequent.flip_comp_flip, List.map_id_fun, id_eq, heq_eq_eq, - eqRec_heq_iff] - specialize IH Y Y_in - rw! (castMode := .all) [@Sequent.flip_flip Y] - simp_all - · exact eq_of_heq (by assumption) - · apply eqRec_heq_iff.mpr - rfl - all_goals rfl - case pdl r next IH => - nth_rewrite 1 [Tableau.flip] - nth_rewrite 1 [Tableau.flip] - rw [IH]; clear IH - rw [PdlRule.flip_flip] - grind only [] - case lrep lpr => - grind only [Tableau.flip, LoadedPathRepeat.flip_flip] - -/-- Map a tableau path to the corresponding path in the reflected tableau. -/ -def PathIn.flip {Hist X} {tab : Tableau Hist X} : PathIn tab → PathIn tab.flip - | .nil => .nil - | @PathIn.loc _ _ nflprep Xnbas ltX next Y Y_in tail => - @PathIn.loc _ _ _ _ _ _ Y.flip - (by apply endNodesOf_flip; grind [LocalTableau.flip_flip]) - (by - have := tail.flip - convert this using 1 - · rfl - · rw! [@Sequent.flip_flip Y] - rfl - ) - | .pdl tail => .pdl tail.flip - -lemma PathIn_helper {HistA HistB XA XB} {tabA : Tableau HistA XA} {tabB : Tableau HistB XB} - (hHist : HistA = HistB) - (hX : XA = XB) : - tabA = hHist ▸ hX ▸ tabB → PathIn tabA = PathIn tabB := by - subst_eqs - simp_all - -lemma PathIn_type_flip_flip {Hist} {tab : Tableau Hist X} : - PathIn tab.flip.flip = PathIn tab := by - rw [Tableau.flip_flip] - grind only [] - -/-- `Eq.mpr` is a heterogeneous identity. -/ -theorem flip_aux_eq_mpr_heq {a b : Sort u} (h : a = b) (x : b) : HEq (Eq.mpr h x) x := by - cases h; rfl - -/-- Flipping a tableau twice gives back (heterogeneously) the original tableau. -/ -theorem flip_aux_Tableau_flip_flip_heq {H X} (t : Tableau H X) : HEq t.flip.flip t := by - rw [Tableau.flip_flip]; exact eqRec_heq_iff.mpr (eqRec_heq_iff.mpr HEq.rfl) - -/-- Flipping a local tableau twice gives back (heterogeneously) the original one. -/ -theorem flip_aux_LocalTableau_flip_flip_heq {X} (lt : LocalTableau X) : HEq lt.flip.flip lt := by - rw [LocalTableau.flip_flip]; exact eqRec_heq_iff.mpr HEq.rfl - -/-- Flipping a pdl rule twice gives back (heterogeneously) the original one. -/ -theorem flip_aux_PdlRule_flip_flip_heq {X Y} (r : PdlRule X Y) : HEq r.flip.flip r := by - rw [PdlRule.flip_flip]; exact eqRec_heq_iff.mpr (eqRec_heq_iff.mpr HEq.rfl) - -/-- End nodes are invariant under flipping a local tableau twice. -/ -theorem endNodesOf_flip_flip {X} (lt : LocalTableau X) : - endNodesOf lt.flip.flip = endNodesOf lt := by - rw [LocalTableau.flip_flip]; congr 1 - · exact Sequent.flip_flip - · exact eqRec_heq _ _ - -/-- `PathIn.flip` respects heterogeneous equality of paths. -/ -theorem PathIn_flip_heq {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} - {p1 : PathIn t1} {p2 : PathIn t2} - (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : - HEq p1.flip p2.flip := by - subst hH hX; obtain rfl := eq_of_heq ht; rw [eq_of_heq hp] - -/-- `Tableau.flip` respects heterogeneous equality of tableaux. -/ -theorem Tableau_flip_heq {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} - (hH : H1 = H2) (hX : X1 = X2) (h : HEq t1 t2) : HEq t1.flip t2.flip := by - subst hH hX; rw [eq_of_heq h] - -/-- Flipping a path twice gives back (after casting along `PathIn_type_flip_flip`) -the original path. -/ -theorem PathIn.flip_flip {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : - PathIn_type_flip_flip ▸ (p.flip.flip) = p := by - induction p with - | nil => - apply eq_of_heq - rw [eqRec_heq_iff] - simp only [PathIn.flip] - congr 1 <;> simp - | @pdl Hist X Y nflprep bas r next tail IH => - apply eq_of_heq - rw [eqRec_heq_iff] - simp only [PathIn.flip] - have hIH : HEq (tail.flip.flip) tail := eqRec_heq_iff.mp (heq_of_eq IH) - have hr : HEq r.flip.flip r := by - rw [PdlRule.flip_flip, eqRec_heq_iff, eqRec_heq_iff] - have hnext : HEq next.flip.flip next := by - rw! [Tableau.flip_flip]; rw [eqRec_heq_iff, eqRec_heq_iff] - congr 1 <;> first - | rfl | exact hIH | exact hr | exact hnext | exact proof_irrel_heq _ _ | simp_all - | @loc Hist X nflprep nbas lt next Y Y_in tail IH => - apply eq_of_heq - rw [eqRec_heq_iff] - simp only [PathIn.flip] - have htail : HEq (tail.flip.flip) tail := eqRec_heq_iff.mp (heq_of_eq IH) - congr 1 - case e_1 => simp - case e_2 => simp - case e_5 => rw [LocalTableau.flip_flip, eqRec_heq_iff] - case e_6 => - apply Function.hfunext rfl - intro a a' ha - obtain rfl := eq_of_heq ha - apply Function.hfunext - · rw [endNodesOf_flip_flip] - · intro b b' hb - simp only [eqRec_heq_iff] - refine HEq.trans (Tableau_flip_heq (by simp) (by simp) - (eqRec_heq_iff.mpr HEq.rfl)) ?_ - refine HEq.trans (flip_aux_Tableau_flip_flip_heq _) ?_ - rw! (castMode := .all) [Sequent.flip_flip] - apply heq_of_eq; congr 1 - case e_9 => - refine HEq.trans ?_ htail - refine HEq.trans (flip_aux_eq_mpr_heq _ _) ?_ - refine PathIn_flip_heq (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) - simp only [eqRec_heq_iff] - refine Tableau_flip_heq (by simp) (by simp) ?_ - rw! (castMode := .all) [Sequent.flip_flip] - apply heq_of_eq; congr 1 - all_goals (try exact proof_irrel_heq _ _) - all_goals (try (simp)) -/-- Undo `PathIn.flip`: flipping twice is the identity (up to the cast). -/ -def PathIn.unflip {X} {tab : Tableau .nil X} (p : PathIn tab.flip) : PathIn tab := - PathIn_type_flip_flip ▸ p.flip - -@[simp] -lemma PathIn.flip_unflip {X} {tab : Tableau .nil X} (p : PathIn tab.flip) : - p.unflip.flip = p := by - apply eq_of_heq - refine HEq.trans ?_ (eqRec_heq_iff.mp (heq_of_eq (PathIn.flip_flip p))) - refine PathIn_flip_heq (by simp) (by simp) ((flip_aux_Tableau_flip_flip_heq tab).symm) ?_ - unfold PathIn.unflip - exact cast_heq _ _ - -/-- A child of a `loc` path is again a `loc` path with the same first step. -/ -lemma edge_loc_shape {Hist X Y} {nrep nbas} {lt : LocalTableau X} - {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} - {Y_in : Y ∈ endNodesOf lt} {t : PathIn (next Y Y_in)} - {q : PathIn (Tableau.loc nrep nbas lt next)} : - (PathIn.loc Y_in t) ⋖_ q → ∃ s, q = PathIn.loc Y_in s ∧ t ⋖_ s := by - rintro (⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩ - | ⟨Hist', X', nrep', bas', Z, r, next', h, rfl⟩) - · exact ⟨t.append (h ▸ PathIn.loc Z_in .nil), rfl, - Or.inl ⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩⟩ - · exact ⟨t.append (h ▸ PathIn.pdl .nil), rfl, - Or.inr ⟨Hist', X', nrep', bas', Z, r, next', h, rfl⟩⟩ - -/-- A child of a `pdl` path is again a `pdl` path. -/ -lemma edge_pdl_shape {Hist X Y} {nrep bas} {r : PdlRule X Y} {nx : Tableau (X :: Hist) Y} - {t : PathIn nx} {q : PathIn (Tableau.pdl nrep bas r nx)} : - (PathIn.pdl t) ⋖_ q → ∃ s, q = PathIn.pdl s ∧ t ⋖_ s := by - rintro (⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩ - | ⟨Hist', X', nrep', bas', Z, r', next', h, rfl⟩) - · exact ⟨t.append (h ▸ PathIn.loc Z_in .nil), rfl, - Or.inl ⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩⟩ - · exact ⟨t.append (h ▸ PathIn.pdl .nil), rfl, - Or.inr ⟨Hist', X', nrep', bas', Z, r', next', h, rfl⟩⟩ - -/-- A path of length zero is the empty path. -/ -lemma PathIn.eq_nil_of_length_zero {Hist X} {tab : Tableau Hist X} {p : PathIn tab} : - p.length = 0 → p = .nil := by - cases p <;> simp - -/-- The `edge` relation only depends on paths up to heterogeneous equality. -/ -lemma edge_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} - {p1 q1 : PathIn t1} {p2 q2 : PathIn t2} - (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) (hq : HEq q1 q2) : - (p1 ⋖_ q1) ↔ (p2 ⋖_ q2) := by - subst hH hX - obtain rfl := eq_of_heq ht - rw [eq_of_heq hp, eq_of_heq hq] - -/-- The length of a path only depends on it up to heterogeneous equality. -/ -lemma PathIn.length_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} - {p1 : PathIn t1} {p2 : PathIn t2} - (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : - p1.length = p2.length := by - subst hH hX - obtain rfl := eq_of_heq ht - rw [eq_of_heq hp] - -/-- Flipping a path does not change its length. -/ -lemma PathIn.flip_length {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : - p.flip.length = p.length := by - induction p - case nil => simp [PathIn.flip] - case loc Hist X nflprep nbas lt next Y Y_in tail IH => - simp only [PathIn.flip, PathIn.length] - rw [← IH] - congr 1 - refine PathIn.length_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) - refine HEq.trans (eqRec_heq _ _) ?_ - exact Tableau_flip_heq (by simp) (by simp) (by congr 1 <;> simp) - case pdl IH => simp only [PathIn.flip, PathIn.length]; rw [IH] - -/-- Variant of `nil_edge_loc_nil` where the tail is only known to have length zero. -/ -lemma nil_edge_loc_of_length_zero {Hist X Y} {nrep nbas} {lt : LocalTableau X} - {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} - {Y_in : Y ∈ endNodesOf lt} {u : PathIn (next Y Y_in)} (hu : u.length = 0) : - (.nil : PathIn (Tableau.loc nrep nbas lt next)) ⋖_ (PathIn.loc Y_in u) := by - rw [PathIn.eq_nil_of_length_zero hu] - exact nil_edge_loc_nil - -/-- Variant of `nil_edge_pdl_nil` where the tail is only known to have length zero. -/ -lemma nil_edge_pdl_of_length_zero {Hist X Y} {nrep bas} {r : PdlRule X Y} - {nx : Tableau (X :: Hist) Y} {u : PathIn nx} (hu : u.length = 0) : - (.nil : PathIn (Tableau.pdl nrep bas r nx)) ⋖_ (PathIn.pdl u) := by - rw [PathIn.eq_nil_of_length_zero hu] - exact nil_edge_pdl_nil - -/-- Flipping a tableau preserves the child relation. -/ -lemma edge_flip_of_edge {Hist X} {tab : Tableau Hist X} : - ∀ (p q : PathIn tab), p ⋖_ q → p.flip ⋖_ q.flip := by - intro p - induction p with - | nil => - intro q pq - cases q with - | nil => exact absurd pq edge_is_irreflexive - | loc Y_in s => - have hs : s.length = 0 := by - have := length_succ_eq_length_of_edge pq - simp only [PathIn.length] at this - omega - simp only [PathIn.flip, Tableau.flip] - apply nil_edge_loc_of_length_zero - refine (PathIn.length_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _)).trans ?_ - · exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) - (by congr 1 <;> simp)) - · rw [PathIn.flip_length]; exact hs - | pdl s => - have hs : s.length = 0 := by - have := length_succ_eq_length_of_edge pq - simp only [PathIn.length] at this - omega - simp only [PathIn.flip, Tableau.flip] - exact nil_edge_pdl_of_length_zero (by rw [PathIn.flip_length]; exact hs) - | loc Y_in t IH => - intro q pq - obtain ⟨s, rfl, ts⟩ := edge_loc_shape pq - simp only [PathIn.flip, Tableau.flip] - rw [loc_edge_loc_iff_edge] - refine (edge_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) - (flip_aux_eq_mpr_heq _ _)).mpr (IH s ts) - exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) - (by congr 1 <;> simp)) - | pdl t IH => - intro q pq - obtain ⟨s, rfl, ts⟩ := edge_pdl_shape pq - simp only [PathIn.flip, Tableau.flip] - rw [pdl_edge_pdl_iff_edge] - exact IH s ts - -/-- Flipping a tableau does not change which nodes are children of which. -/ -lemma edge_flip {H X} {tab : Tableau H X} {p q : PathIn tab} : - (p.flip ⋖_ q.flip) ↔ p ⋖_ q := by - constructor - · intro h - refine (edge_heq_congr (H2 := H) (X2 := X) (by simp) (by simp) - (flip_aux_Tableau_flip_flip_heq tab) - (eqRec_heq_iff.mp (heq_of_eq (PathIn.flip_flip p))) - (eqRec_heq_iff.mp (heq_of_eq (PathIn.flip_flip q)))).mp (edge_flip_of_edge _ _ h) - · exact edge_flip_of_edge p q - -/-- The tableau at a path only depends on it up to heterogeneous equality. -/ -lemma tabAt_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} - {p1 : PathIn t1} {p2 : PathIn t2} - (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : - tabAt p1 = tabAt p2 := by - subst hH hX - obtain rfl := eq_of_heq ht - rw [eq_of_heq hp] - -/-- The history of a path only depends on it up to heterogeneous equality. -/ -lemma toHistory_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} - {p1 : PathIn t1} {p2 : PathIn t2} - (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : - p1.toHistory = p2.toHistory := by - subst hH hX - obtain rfl := eq_of_heq ht - rw [eq_of_heq hp] - -/-- The tableau at a flipped path is the flip of the tableau at the original path. -/ -lemma tabAt_flip {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : - tabAt p.flip - = ⟨List.map Sequent.flip (tabAt p).1, (tabAt p).2.1.flip, (tabAt p).2.2.flip⟩ := by - induction p - case nil => simp [PathIn.flip, tabAt] - case loc Hist X nflprep nbas lt next Y Y_in tail IH => - simp only [PathIn.flip, Tableau.flip] - change _ = (⟨List.map Sequent.flip (tabAt tail).1, (tabAt tail).2.1.flip, - (tabAt tail).2.2.flip⟩ : Σ H X, Tableau H X) - rw [← IH] - refine Eq.trans tabAt_loc (tabAt_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _)) - exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) - (by congr 1 <;> simp)) - case pdl IH => - simp only [PathIn.flip] - exact IH - -/-- The sequent at a flipped path is the flip of the sequent at the original path. -/ -lemma PathIn.nodeAt_flip {Hist X} {tab : Tableau Hist X} {e : PathIn tab} : - nodeAt (e.flip) = (nodeAt e).flip := by - unfold nodeAt - rw [tabAt_flip] - -/-- The history of a flipped path is the flip of the history of the original path. -/ -lemma toHistory_flip {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : - p.flip.toHistory = List.map Sequent.flip p.toHistory := by - induction p - case nil => simp [PathIn.flip, PathIn.toHistory] - case loc Hist X nflprep nbas lt next Y Y_in tail IH => - simp only [PathIn.flip, PathIn.toHistory, List.map_append, List.map_cons, List.map_nil] - rw [← IH] - congr 1 - refine toHistory_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) - exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) - (by congr 1 <;> simp)) - case pdl IH => - simp only [PathIn.flip, PathIn.toHistory, List.map_append, List.map_cons, List.map_nil] - rw [IH] - -/-- Rewinding only depends on the path up to heterogeneous equality, -and on the index only via its value. -/ -lemma PathIn.rewind_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} - {p1 : PathIn t1} {p2 : PathIn t2} {k1 : Fin (p1.toHistory.length + 1)} - {k2 : Fin (p2.toHistory.length + 1)} - (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) (hk : (k1 : ℕ) = (k2 : ℕ)) : - HEq (p1.rewind k1) (p2.rewind k2) := by - subst hH hX - obtain rfl := eq_of_heq ht - obtain rfl := eq_of_heq hp - obtain rfl : k1 = k2 := Fin.ext hk - rfl - -/-- Flipping commutes with rewinding. -/ -lemma PathIn.flip_rewind {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : - ∀ (k : Fin (p.toHistory.length + 1)) (k' : Fin (p.flip.toHistory.length + 1)), - (k : ℕ) = (k' : ℕ) → (p.rewind k).flip = p.flip.rewind k' := by - induction p - case nil => - intro k k' hk - simp [PathIn.rewind, PathIn.flip] - case loc Hist X nflprep nbas lt next Y Y_in tail IH => - have hL : ((PathIn.loc Y_in tail : - PathIn (Tableau.loc nflprep nbas lt next)).flip).toHistory.length - = tail.toHistory.length + 1 := by rw [toHistory_flip]; simp - simp only [PathIn.flip, Tableau.flip] at hL - simp only [PathIn.flip, Tableau.flip] - intro k k' hk - cases k using Fin.lastCases with - | last => - cases k' using Fin.lastCases with - | last => simp [PathIn.rewind, PathIn.flip, Tableau.flip] - | cast j' => - exfalso - have hj := j'.isLt - simp only [Fin.val_last, Fin.val_castSucc, PathIn.loc_length_eq] at hk - omega - | cast j => - cases k' using Fin.lastCases with - | last => - exfalso - have hj := j.isLt - simp only [PathIn.loc_length_eq] at hj - simp only [Fin.val_last, Fin.val_castSucc] at hk - rw [hL] at hk - omega - | cast j' => - simp only [PathIn.rewind, Fin.lastCases_castSucc, Function.comp_apply, PathIn.flip] - congr 1 - have hlen : tail.flip.toHistory.length = tail.toHistory.length := by - rw [toHistory_flip]; simp - have hm : (j : ℕ) < tail.flip.toHistory.length + 1 := by - have := j.isLt - simp only [PathIn.loc_length_eq] at this - omega - apply eq_of_heq - refine HEq.trans (flip_aux_eq_mpr_heq _ _) ?_ - rw [IH (Fin.cast (PathIn.loc_length_eq Y_in tail) j) ⟨j, hm⟩ rfl] - refine PathIn.rewind_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _).symm ?_ - · exact (HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) - (by congr 1 <;> simp))).symm - · simp only [Fin.val_castSucc] at hk - simpa only [Fin.val_cast] using hk - case pdl Hist X Z nrep bas r nx tail IH => - simp only [PathIn.flip, Tableau.flip] - intro k k' hk - cases k using Fin.lastCases with - | last => - cases k' using Fin.lastCases with - | last => simp [PathIn.rewind, PathIn.flip, Tableau.flip] - | cast j' => - exfalso - have := j'.isLt - simp only [Fin.val_last, Fin.val_castSucc, PathIn.pdl_length_eq] at hk this - rw [toHistory_flip] at this - simp at this - omega - | cast j => - cases k' using Fin.lastCases with - | last => - exfalso - have := j.isLt - simp only [Fin.val_last, Fin.val_castSucc, PathIn.pdl_length_eq] at hk this - rw [toHistory_flip] at hk - simp at hk - omega - | cast j' => - simp only [PathIn.rewind, Fin.lastCases_castSucc, Function.comp_apply, PathIn.flip] - congr 1 - refine IH _ _ ?_ - simp only [Fin.val_castSucc] at hk - simpa using hk - -/-- If a path ends in a loaded-path-repeat, then so does the flipped path, -with a repeat at the same position in the history. -/ -lemma tabAt_flip_lrep {Hist X} {tab : Tableau Hist X} (p : PathIn tab) lpr - (h : (tabAt p).2.2 = .lrep lpr) : - ∃ lpr' : LoadedPathRepeat (tabAt p.flip).1 (tabAt p.flip).2.1, - (tabAt p.flip).2.2 = .lrep lpr' ∧ (lpr'.1 : ℕ) = (lpr.1 : ℕ) := by - rw [tabAt_flip p, h] - refine ⟨lpr.flip, by simp [Tableau.flip], ?_⟩ - rcases lpr with ⟨k, hk⟩ - simp [LoadedPathRepeat.flip] +-- Retain the original auxiliary proposition after the proof moves to FlipCore. +private theorem Sequent.flip_isLoaded._proof_1_5 : + ∀ (L R : Finset Formula) (O : Olf), + (delta% Sequent.isLoaded ((R, L, Option.map Sum.swap O) : + Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula))) ↔ + (delta% Sequent.isLoaded ((L, R, O) : + Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula))) := by + intro L R O + change Sequent.isLoaded (Sequent.flip (L, R, O)) ↔ Sequent.isLoaded (L, R, O) + exact Sequent.flip_isLoaded /-- Flipping a tableau preserves the companion relation. -/ lemma companion_flip_of_companion {X} {tab : Tableau .nil X} {p q : PathIn tab} : @@ -874,3 +95,8 @@ lemma cEquiv_flip {X} {tab : Tableau .nil X} {p q : PathIn tab} : rw [cReach_flip, cReach_flip] end PDL + +run_cmd do + let source := `LeanPool.PDL.FlipCore + let target := `LeanPool.PDL.Flip + Lean.Elab.Command.liftCoreM (PDL.ImportCompatibility.retainPrivateDeclarations source target) diff --git a/LeanPool/PDL/FlipCore.lean b/LeanPool/PDL/FlipCore.lean new file mode 100644 index 0000000000..6669ee29cd --- /dev/null +++ b/LeanPool/PDL/FlipCore.lean @@ -0,0 +1,813 @@ +/- +Copyright (c) 2023 PDL formalization contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: PDL formalization contributors (see project card) +-/ + +module + +public import LeanPool.PDL.TableauPath + +import Mathlib.Data.Nat.SuccPred +import Mathlib.Tactic.Bound.Init -- shake: keep + +/-! # Flipping tableau paths and local rules -/ + +@[expose] public section + +namespace PDL + +/-- Exchange the side of an optional loaded formula. -/ +def Olf.flip : Olf → Olf := Option.map Sum.swap + +@[simp] +lemma Olf.flip_inj {O1 O2 : Olf} : O1.flip = O2.flip ↔ O1 = O2 := by + rcases O1 with (_|_|_) <;> rcases O2 with (_|_|_) <;> simp_all [Olf.flip] + +@[simp] +lemma Olf.flip_flip {O : Olf} : O.flip.flip = O := by + rcases O with (_|_|_) <;> simp_all [Olf.flip] + +@[simp] +lemma Olf.flip_none : Olf.flip none = none := by simp [Olf.flip] + +/-- Exchange both sequent components and the side of its loaded formula. -/ +def Sequent.flip : Sequent → Sequent := fun ⟨L, R, O⟩ => ⟨R, L, O.flip⟩ + +@[simp] +lemma Sequent.flip_right {X : Sequent} : X.flip.right = X.left := by + rcases X with ⟨L,R,_|_|_⟩ <;> simp [Sequent.flip, Olf.flip] + +@[simp] +lemma Sequent.flip_left {X : Sequent} : X.flip.left = X.right := by + rcases X with ⟨L,R,_|_|_⟩ <;> simp [Sequent.flip, Olf.flip] + +@[simp] +lemma Sequent.flip_flip {X : Sequent} : X.flip.flip = X := by + rcases X with ⟨L,R,O⟩ + simp_all [Sequent.flip, Olf.flip] + +@[simp] +lemma Sequent.flip_isLoaded {X : Sequent} : + X.flip.isLoaded ↔ X.isLoaded := by + rcases X with ⟨L, R, O⟩ + simp only [Sequent.isLoaded, Sequent.flip, Olf.flip] + grind -zetaDelta + +@[simp] +lemma Sequent.flip_isFree {X : Sequent} : + X.flip.isFree ↔ X.isFree := by + unfold Sequent.isFree + simp + +lemma Sequent.flip_eq_off {X Y : Sequent} : (X.flip = Y) = (X = Y.flip) := by + rcases X with ⟨L,R,O⟩ + rcases Y with ⟨L',R',O'⟩ + simp_all only [flip] + rw [@propext_iff] + constructor <;> intro h <;> cases h <;> convert rfl <;> simp + +lemma Sequent.map_flip_map_flip {Hist} : + (List.map Sequent.flip (List.map Sequent.flip Hist)) = Hist := by + induction Hist <;> simp_all + +/-- Flipping all sequents in a `Finset` twice gives back the same set. -/ +@[simp] +lemma Sequent.image_flip_image_flip {S : Finset Sequent} : + Finset.image Sequent.flip (Finset.image Sequent.flip S) = S := by + rw [Finset.image_image] + simp [Function.comp_def] + +@[simp] +lemma basic_flip {X : Sequent} : X.flip.basic ↔ X.basic := by + rcases X with ⟨L,R,O⟩ + unfold Sequent.basic Sequent.flip + simp only + simp only [Sequent.toFinset, Finset.union_assoc, Finset.mem_union, Option.mem_toFinset, + Option.mem_def, Option.map_eq_some_iff, Sum.exists, Sum.elim_inl, negUnload, Sum.elim_inr, + Formula.basic, decide_false, decide_true, Sequent.closed, not_or, not_exists, not_and] + constructor + · intro ⟨fs_basic, not_closed⟩ + constructor + · intro φ φ_in + apply fs_basic + rcases φ_in with h|h|h|h + · grind only [] + · grind only [] + · right + right + right + simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, Sum.inr.injEq, + exists_eq_right, Sum.swap_inr, reduceCtorEq, and_false, exists_false, or_false] + exact h + · right + right + left + simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, reduceCtorEq, + and_false, exists_false, Sum.swap_inr, Sum.inl.injEq, exists_eq_right, false_or] + exact h + · aesop (rule_sets := [-default]) + · intro ⟨fs_basic, not_closed⟩ + constructor + · intro φ φ_in + apply fs_basic + rcases φ_in with h|h|h|h + · grind only [] + · grind only [] + · right + right + right + simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, reduceCtorEq, + and_false, exists_false, Sum.swap_inr, Sum.inl.injEq, exists_eq_right, false_or] at h + exact h + · right + right + left + simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, Sum.inr.injEq, + exists_eq_right, Sum.swap_inr, reduceCtorEq, and_false, exists_false, or_false] at h + exact h + · aesop (rule_sets := [-default]) + +/-- Reflect a local rule by exchanging its left and right components. -/ +def LocalRule.flip {Lcond Ocond Rcond ress} (lr : LocalRule (Lcond, Rcond, Ocond) ress) : + LocalRule (Rcond, Lcond, Ocond.flip) (ress.image Sequent.flip) := by + cases lr + case oneSidedL YS orule YS_def => + apply LocalRule.oneSidedR orule + aesop + case oneSidedR YS orule YS_def => + apply LocalRule.oneSidedL orule + aesop + case LRnegL => + apply LocalRule.LRnegR + case LRnegR => + apply LocalRule.LRnegL + case loadedL YS χ lrule YS_def => + apply LocalRule.loadedR _ lrule + subst YS_def + rw [Finset.image_image] + apply Finset.image_congr + rintro ⟨L, (_|o)⟩ - <;> simp [Sequent.flip, Olf.flip] + case loadedR lrule YS_def => + apply LocalRule.loadedL _ lrule + subst YS_def + rw [Finset.image_image] + apply Finset.image_congr + rintro ⟨L, (_|o)⟩ - <;> simp [Sequent.flip, Olf.flip] + +lemma LocalRule.flip_flip {Lcond Ocond Rcond ress} (lr : LocalRule (Lcond, Rcond, Ocond) ress) : + lr.flip.flip = Olf.flip_flip ▸ Sequent.image_flip_image_flip ▸ lr := by + cases lr <;> simp_all [LocalRule.flip] <;> grind only [] + +/-- Note: is it possible and useful to rewrite this in more term and less tactic mode? -/ +def LocalRuleApp.flip : LocalRuleApp → LocalRuleApp := by + rintro ⟨L, R, O, Lcond, Rcond, Ocond, ress, rule, C, hC, preconditionProof⟩ + refine @LocalRuleApp.mk R L O.flip Rcond Lcond Ocond.flip _ rule.flip + (C.image Sequent.flip) ?_ ?_ + · subst hC + simp only [applyLocalRule] + rw [Finset.image_image, Finset.image_image] + apply Finset.image_congr + rintro ⟨Lnew, Rnew, Onew⟩ - + simp only [Function.comp_apply, Sequent.flip] + rcases O with (_|_|_) <;> rcases Onew with (_|_|_) <;> rcases Ocond with (_|_|_) + <;> simp [Olf.flip, Olf.change, SDiff.sdiff] <;> grind + · rcases preconditionProof with ⟨hL, hR, hO⟩ + refine ⟨hR, hL, ?_⟩ + rcases O with (_|_|_) <;> rcases Ocond with (_|_|_) <;> simp_all [Olf.flip, Sum.swap] + +@[simp] +lemma Sequent.flip_comp_flip : Sequent.flip ∘ Sequent.flip = id := by + ext X + rw [Function.comp_apply, Sequent.flip_flip, id_eq] + +lemma LocalRuleApp.flip_flip {lra : LocalRuleApp} : + lra.flip.flip = lra := by + rcases lra with ⟨L, R, O, C, Lcond, Rcond, Ocond, ress, rule, hC, preconditionProof⟩ + simp only [flip, Olf.flip_flip, Sequent.image_flip_image_flip, mk.injEq, and_true, true_and] + rw [LocalRule.flip_flip] + grind only [] + +lemma Sequent.flip_mem_of_mem_image_flip {B : Finset Sequent} {Y : Sequent} : + Y ∈ B.image Sequent.flip → Y.flip ∈ B := by aesop (rule_sets := [-default]) + +/-- Reflect every rule and branch of a local tableau. -/ +def LocalTableau.flip {X} : LocalTableau X → LocalTableau X.flip + | (@byLocalRule X lra X_def next) => .byLocalRule lra.flip + (by subst X_def; simp [LocalRuleApp.flip, Sequent.flip]) + (fun Y Y_in => + @Sequent.flip_flip Y ▸ (next Y.flip (Sequent.flip_mem_of_mem_image_flip Y_in)).flip) + | (@sim X Xbas) => .sim (basic_flip.mpr Xbas) + +lemma LocalTableau.flip_flip {lt : LocalTableau X} : lt.flip.flip = Sequent.flip_flip ▸ lt := by + induction lt <;> simp only [flip] + case byLocalRule X lra X_def next IH => + apply eq_of_heq + rw! (castMode := .all) [Sequent.flip_flip] -- :-) + simp only [heq_eq_eq, byLocalRule.injEq] + constructor + · exact LocalRuleApp.flip_flip + · refine Function.hfunext rfl ?_ + intro X X' X_heq_X' + apply Function.hfunext + · rw [LocalRuleApp.flip_flip] + grind only [] + · grind only [] + · grind only [] + +lemma LocalTableau.flip_inj {X} {lt : LocalTableau X} : + lt.flip.flip = (Sequent.flip_flip ▸ lt) := by + cases lt + case byLocalRule => + rw [LocalTableau.flip_flip] + · grind only [LocalTableau.flip] + +lemma endNodesOf_flip {X} {lt : LocalTableau X} {Y} : + Y ∈ endNodesOf lt.flip → Y.flip ∈ endNodesOf lt := by + intro Y_in + induction lt + case byLocalRule B next lra IH => + simp only [LocalTableau.flip, endNodesOf, Finset.sup_image, Function.id_comp, Finset.mem_sup, + Finset.mem_attach, true_and, Subtype.exists] at * + rcases Y_in with ⟨W, W_in_B, Y_in_end⟩ + refine ⟨W.flip, ?_, ?_⟩ <;> grind only [] + case sim Z Zbas => + simp_all [LocalTableau.flip] + +lemma exists_flip_of_endNodesOf {X : Sequent} {ltf : LocalTableau X.flip} {Zf} : + Zf ∈ endNodesOf ltf → ∃ Z, Zf = Z.flip ∧ Z ∈ endNodesOf ltf.flip := by + intro Z_in + cases ltf + case byLocalRule lra next X_def => + simp only [endNodesOf, Finset.sup_image, Function.id_comp, Finset.mem_sup, Finset.mem_attach, + true_and, Subtype.exists, LocalTableau.flip] at * + rcases Z_in with ⟨Yf, Yf_in_B, Zf_via_Yf⟩ + refine ⟨Zf.flip, ?_, ⟨Yf.flip, ?_, ?_⟩⟩ + · simp + · grind [LocalRuleApp.flip] + · rw! (castMode := .all) [@Sequent.flip_flip Yf] + simp only + apply endNodesOf_flip + rw [LocalTableau.flip_flip] + grind + case sim Xbas => + simp_all only [endNodesOf, Finset.mem_singleton, LocalTableau.flip] + subst_eqs + simp + +/-- Reflect a PDL rule by exchanging the sequent components. -/ +def PdlRule.flip {X Y} (r : PdlRule X Y) : PdlRule X.flip Y.flip := by + cases r + case loadL L δs α φ R in_L notBox Y_def => + apply PdlRule.loadR in_L notBox + simp_all only [Sequent.flip, Prod.mk.injEq, true_and] + rfl + case loadR R δs α φ L in_R notBox Y_def => + apply PdlRule.loadL in_R notBox + simp_all only [Sequent.flip, Prod.mk.injEq, true_and] + rfl + case freeL L R δs α φ X_def Y_def => + apply PdlRule.freeR + all_goals + subst X_def Y_def + simp_all only [Sequent.flip] + rfl + case freeR L R δs α φ X_def Y_def => + apply PdlRule.freeL + all_goals + subst X_def Y_def + simp_all only [Sequent.flip] + rfl + case modL L R a ξ X_def Y_def => + apply @PdlRule.modR Y.flip R L a X.flip ξ + all_goals + subst X_def Y_def + cases ξ <;> simp_all [Sequent.flip,Olf.flip] + case modR L R a ξ X_def Y_def => + apply @PdlRule.modL Y.flip R L a X.flip ξ + all_goals + subst X_def Y_def + cases ξ <;> simp_all [Sequent.flip,Olf.flip] + +lemma PdlRule.flip_flip {X Y} (r : PdlRule X Y) : + r.flip.flip = (Sequent.flip_flip ▸ Sequent.flip_flip ▸ r) := by + cases r <;> simp [PdlRule.flip] <;> grind only [] + +/-- Flipping sequents is injective. -/ +@[simp] +lemma Sequent.flip_eq_flip_iff {X Y : Sequent} : X.flip = Y.flip ↔ X = Y := by + constructor + · intro h + rw [← @Sequent.flip_flip X, ← @Sequent.flip_flip Y, h] + · rintro rfl + rfl + +/-- Reflect a loaded-path repeat, preserving its history position. -/ +def LoadedPathRepeat.flip {Hist X} : LoadedPathRepeat Hist X → + LoadedPathRepeat (List.map Sequent.flip Hist) X.flip +| ⟨k, hk⟩ => by + refine ⟨⟨k.1, ?_⟩, ?_⟩ + · simp_all [List.length_map] + · rcases hk with ⟨same, path_loaded⟩ + constructor + · simp only [List.get_eq_getElem, List.getElem_map, Sequent.flip_eq_flip_iff] + exact same + · simp only [List.get_eq_getElem, List.getElem_map, Sequent.flip_isLoaded] + intro m m_lt + apply path_loaded ⟨m, by grind⟩ + omega + +lemma LoadedPathRepeat.flip_flip {Hist X} (lpr : LoadedPathRepeat Hist X) : + lpr.flip.flip = Sequent.map_flip_map_flip ▸ Sequent.flip_flip ▸ lpr := by + rcases lpr with ⟨k, hk⟩ + simp only [flip, List.get_eq_getElem] + rw! [Sequent.map_flip_map_flip, Sequent.flip_flip] + rfl + +@[simp] +lemma flprep_flip {Hist} : + flprep (List.map Sequent.flip Hist) X.flip ↔ flprep Hist X := by + simp_all only [flprep, rep, ↓existsAndEq, List.mem_map, Sequent.flip_eq_flip_iff, + exists_eq_right, and_true, Sequent.isFree, Sequent.flip_isLoaded] + refine ⟨?_,?_⟩ + · rintro (frep|⟨⟨lpr⟩⟩ ) + · grind only [] + · have := lpr.flip + right + simp only [List.map_map, Sequent.flip_comp_flip, List.map_id_fun, id_eq, Sequent.flip_flip] + at this + exact ⟨this⟩ + · rintro (frep|⟨⟨lpr⟩⟩ ) + · grind only [] + · have := lpr.flip + right + exact ⟨this⟩ + +/-- Exchange the left and right sides throughout a tableau. -/ +def Tableau.flip {Hist X} : Tableau Hist X → Tableau (Hist.map Sequent.flip) X.flip +| .loc nflprep nbas lt next => .loc (by simp only [flprep_flip]; exact nflprep) + (by simp only [basic_flip]; exact nbas) + lt.flip + (fun Y Y_in => + @Sequent.flip_flip Y ▸ (next Y.flip (endNodesOf_flip Y_in)).flip) +| .pdl nflprep bas r next => .pdl (by simp only [flprep_flip]; exact nflprep) + (by simp only [basic_flip]; exact bas) + r.flip + next.flip +| .lrep lpr => .lrep lpr.flip + +lemma Hist_flip {Hist} : List.map Sequent.flip (List.map Sequent.flip Hist) = Hist := by ext; simp + +@[simp] +lemma Tableau.flip_flip {Hist X} {tab : Tableau Hist X} : + tab.flip.flip = Sequent.flip_flip ▸ Hist_flip ▸ tab := by + induction tab + case loc Hist X nflprep nbas ltX next IH => + simp only [flip] + rw! [LocalTableau.flip_flip] + rw! (castMode := .all) [Sequent.flip_flip] + simp only [] + convert Tableau.loc.congr_simp nflprep nbas ltX next next ?_ + · exact Sequent.map_flip_map_flip + · exact Sequent.map_flip_map_flip + case h Y W Y_eq_W Y_in W_in Y_heq_W => + subst Y_eq_W + simp_all only [List.map_map, Sequent.flip_comp_flip, List.map_id_fun, id_eq, heq_eq_eq, + eqRec_heq_iff] + specialize IH Y Y_in + rw! (castMode := .all) [@Sequent.flip_flip Y] + simp_all + · exact eq_of_heq (by assumption) + · apply eqRec_heq_iff.mpr + rfl + all_goals rfl + case pdl r next IH => + nth_rewrite 1 [Tableau.flip] + nth_rewrite 1 [Tableau.flip] + rw [IH]; clear IH + rw [PdlRule.flip_flip] + grind only [] + case lrep lpr => + grind only [Tableau.flip, LoadedPathRepeat.flip_flip] + +/-- Map a tableau path to the corresponding path in the reflected tableau. -/ +def PathIn.flip {Hist X} {tab : Tableau Hist X} : PathIn tab → PathIn tab.flip + | .nil => .nil + | @PathIn.loc _ _ nflprep Xnbas ltX next Y Y_in tail => + @PathIn.loc _ _ _ _ _ _ Y.flip + (by apply endNodesOf_flip; grind [LocalTableau.flip_flip]) + (by + have := tail.flip + convert this using 1 + · rfl + · rw! [@Sequent.flip_flip Y] + rfl + ) + | .pdl tail => .pdl tail.flip + +lemma PathIn_helper {HistA HistB XA XB} {tabA : Tableau HistA XA} {tabB : Tableau HistB XB} + (hHist : HistA = HistB) + (hX : XA = XB) : + tabA = hHist ▸ hX ▸ tabB → PathIn tabA = PathIn tabB := by + subst_eqs + simp_all + +lemma PathIn_type_flip_flip {Hist} {tab : Tableau Hist X} : + PathIn tab.flip.flip = PathIn tab := by + rw [Tableau.flip_flip] + grind only [] + +/-- `Eq.mpr` is a heterogeneous identity. -/ +theorem flip_aux_eq_mpr_heq {a b : Sort u} (h : a = b) (x : b) : HEq (Eq.mpr h x) x := by + cases h; rfl + +/-- Flipping a tableau twice gives back (heterogeneously) the original tableau. -/ +theorem flip_aux_Tableau_flip_flip_heq {H X} (t : Tableau H X) : HEq t.flip.flip t := by + rw [Tableau.flip_flip]; exact eqRec_heq_iff.mpr (eqRec_heq_iff.mpr HEq.rfl) + +/-- Flipping a local tableau twice gives back (heterogeneously) the original one. -/ +theorem flip_aux_LocalTableau_flip_flip_heq {X} (lt : LocalTableau X) : HEq lt.flip.flip lt := by + rw [LocalTableau.flip_flip]; exact eqRec_heq_iff.mpr HEq.rfl + +/-- Flipping a pdl rule twice gives back (heterogeneously) the original one. -/ +theorem flip_aux_PdlRule_flip_flip_heq {X Y} (r : PdlRule X Y) : HEq r.flip.flip r := by + rw [PdlRule.flip_flip]; exact eqRec_heq_iff.mpr (eqRec_heq_iff.mpr HEq.rfl) + +/-- End nodes are invariant under flipping a local tableau twice. -/ +theorem endNodesOf_flip_flip {X} (lt : LocalTableau X) : + endNodesOf lt.flip.flip = endNodesOf lt := by + rw [LocalTableau.flip_flip]; congr 1 + · exact Sequent.flip_flip + · exact eqRec_heq _ _ + +/-- `PathIn.flip` respects heterogeneous equality of paths. -/ +theorem PathIn_flip_heq {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} + {p1 : PathIn t1} {p2 : PathIn t2} + (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : + HEq p1.flip p2.flip := by + subst hH hX; obtain rfl := eq_of_heq ht; rw [eq_of_heq hp] + +/-- `Tableau.flip` respects heterogeneous equality of tableaux. -/ +theorem Tableau_flip_heq {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} + (hH : H1 = H2) (hX : X1 = X2) (h : HEq t1 t2) : HEq t1.flip t2.flip := by + subst hH hX; rw [eq_of_heq h] + +/-- Flipping a path twice gives back (after casting along `PathIn_type_flip_flip`) +the original path. -/ +theorem PathIn.flip_flip {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : + PathIn_type_flip_flip ▸ (p.flip.flip) = p := by + induction p with + | nil => + apply eq_of_heq + rw [eqRec_heq_iff] + simp only [PathIn.flip] + congr 1 <;> simp + | @pdl Hist X Y nflprep bas r next tail IH => + apply eq_of_heq + rw [eqRec_heq_iff] + simp only [PathIn.flip] + have hIH : HEq (tail.flip.flip) tail := eqRec_heq_iff.mp (heq_of_eq IH) + have hr : HEq r.flip.flip r := by + rw [PdlRule.flip_flip, eqRec_heq_iff, eqRec_heq_iff] + have hnext : HEq next.flip.flip next := by + rw! [Tableau.flip_flip]; rw [eqRec_heq_iff, eqRec_heq_iff] + congr 1 <;> first + | rfl | exact hIH | exact hr | exact hnext | exact proof_irrel_heq _ _ | simp_all + | @loc Hist X nflprep nbas lt next Y Y_in tail IH => + apply eq_of_heq + rw [eqRec_heq_iff] + simp only [PathIn.flip] + have htail : HEq (tail.flip.flip) tail := eqRec_heq_iff.mp (heq_of_eq IH) + congr 1 + case e_1 => simp + case e_2 => simp + case e_5 => rw [LocalTableau.flip_flip, eqRec_heq_iff] + case e_6 => + apply Function.hfunext rfl + intro a a' ha + obtain rfl := eq_of_heq ha + apply Function.hfunext + · rw [endNodesOf_flip_flip] + · intro b b' hb + simp only [eqRec_heq_iff] + refine HEq.trans (Tableau_flip_heq (by simp) (by simp) + (eqRec_heq_iff.mpr HEq.rfl)) ?_ + refine HEq.trans (flip_aux_Tableau_flip_flip_heq _) ?_ + rw! (castMode := .all) [Sequent.flip_flip] + apply heq_of_eq; congr 1 + case e_9 => + refine HEq.trans ?_ htail + refine HEq.trans (flip_aux_eq_mpr_heq _ _) ?_ + refine PathIn_flip_heq (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) + simp only [eqRec_heq_iff] + refine Tableau_flip_heq (by simp) (by simp) ?_ + rw! (castMode := .all) [Sequent.flip_flip] + apply heq_of_eq; congr 1 + all_goals (try exact proof_irrel_heq _ _) + all_goals (try (simp)) +/-- Undo `PathIn.flip`: flipping twice is the identity (up to the cast). -/ +def PathIn.unflip {X} {tab : Tableau .nil X} (p : PathIn tab.flip) : PathIn tab := + PathIn_type_flip_flip ▸ p.flip + +@[simp] +lemma PathIn.flip_unflip {X} {tab : Tableau .nil X} (p : PathIn tab.flip) : + p.unflip.flip = p := by + apply eq_of_heq + refine HEq.trans ?_ (eqRec_heq_iff.mp (heq_of_eq (PathIn.flip_flip p))) + refine PathIn_flip_heq (by simp) (by simp) ((flip_aux_Tableau_flip_flip_heq tab).symm) ?_ + unfold PathIn.unflip + exact cast_heq _ _ + +/-- A child of a `loc` path is again a `loc` path with the same first step. -/ +lemma edge_loc_shape {Hist X Y} {nrep nbas} {lt : LocalTableau X} + {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} + {Y_in : Y ∈ endNodesOf lt} {t : PathIn (next Y Y_in)} + {q : PathIn (Tableau.loc nrep nbas lt next)} : + (PathIn.loc Y_in t) ⋖_ q → ∃ s, q = PathIn.loc Y_in s ∧ t ⋖_ s := by + rintro (⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩ + | ⟨Hist', X', nrep', bas', Z, r, next', h, rfl⟩) + · exact ⟨t.append (h ▸ PathIn.loc Z_in .nil), rfl, + Or.inl ⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩⟩ + · exact ⟨t.append (h ▸ PathIn.pdl .nil), rfl, + Or.inr ⟨Hist', X', nrep', bas', Z, r, next', h, rfl⟩⟩ + +/-- A child of a `pdl` path is again a `pdl` path. -/ +lemma edge_pdl_shape {Hist X Y} {nrep bas} {r : PdlRule X Y} {nx : Tableau (X :: Hist) Y} + {t : PathIn nx} {q : PathIn (Tableau.pdl nrep bas r nx)} : + (PathIn.pdl t) ⋖_ q → ∃ s, q = PathIn.pdl s ∧ t ⋖_ s := by + rintro (⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩ + | ⟨Hist', X', nrep', bas', Z, r', next', h, rfl⟩) + · exact ⟨t.append (h ▸ PathIn.loc Z_in .nil), rfl, + Or.inl ⟨Hist', X', nrep', nbas', lt', next', Z, Z_in, h, rfl⟩⟩ + · exact ⟨t.append (h ▸ PathIn.pdl .nil), rfl, + Or.inr ⟨Hist', X', nrep', bas', Z, r', next', h, rfl⟩⟩ + +/-- A path of length zero is the empty path. -/ +lemma PathIn.eq_nil_of_length_zero {Hist X} {tab : Tableau Hist X} {p : PathIn tab} : + p.length = 0 → p = .nil := by + cases p <;> simp + +/-- The `edge` relation only depends on paths up to heterogeneous equality. -/ +lemma edge_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} + {p1 q1 : PathIn t1} {p2 q2 : PathIn t2} + (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) (hq : HEq q1 q2) : + (p1 ⋖_ q1) ↔ (p2 ⋖_ q2) := by + subst hH hX + obtain rfl := eq_of_heq ht + rw [eq_of_heq hp, eq_of_heq hq] + +/-- The length of a path only depends on it up to heterogeneous equality. -/ +lemma PathIn.length_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} + {p1 : PathIn t1} {p2 : PathIn t2} + (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : + p1.length = p2.length := by + subst hH hX + obtain rfl := eq_of_heq ht + rw [eq_of_heq hp] + +/-- Flipping a path does not change its length. -/ +lemma PathIn.flip_length {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : + p.flip.length = p.length := by + induction p + case nil => simp [PathIn.flip] + case loc Hist X nflprep nbas lt next Y Y_in tail IH => + simp only [PathIn.flip, PathIn.length] + rw [← IH] + congr 1 + refine PathIn.length_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) + refine HEq.trans (eqRec_heq _ _) ?_ + exact Tableau_flip_heq (by simp) (by simp) (by congr 1 <;> simp) + case pdl IH => simp only [PathIn.flip, PathIn.length]; rw [IH] + +/-- Variant of `nil_edge_loc_nil` where the tail is only known to have length zero. -/ +lemma nil_edge_loc_of_length_zero {Hist X Y} {nrep nbas} {lt : LocalTableau X} + {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} + {Y_in : Y ∈ endNodesOf lt} {u : PathIn (next Y Y_in)} (hu : u.length = 0) : + (.nil : PathIn (Tableau.loc nrep nbas lt next)) ⋖_ (PathIn.loc Y_in u) := by + rw [PathIn.eq_nil_of_length_zero hu] + exact nil_edge_loc_nil + +/-- Variant of `nil_edge_pdl_nil` where the tail is only known to have length zero. -/ +lemma nil_edge_pdl_of_length_zero {Hist X Y} {nrep bas} {r : PdlRule X Y} + {nx : Tableau (X :: Hist) Y} {u : PathIn nx} (hu : u.length = 0) : + (.nil : PathIn (Tableau.pdl nrep bas r nx)) ⋖_ (PathIn.pdl u) := by + rw [PathIn.eq_nil_of_length_zero hu] + exact nil_edge_pdl_nil + +/-- Flipping a tableau preserves the child relation. -/ +lemma edge_flip_of_edge {Hist X} {tab : Tableau Hist X} : + ∀ (p q : PathIn tab), p ⋖_ q → p.flip ⋖_ q.flip := by + intro p + induction p with + | nil => + intro q pq + cases q with + | nil => exact absurd pq edge_is_irreflexive + | loc Y_in s => + have hs : s.length = 0 := by + have := length_succ_eq_length_of_edge pq + simp only [PathIn.length] at this + omega + simp only [PathIn.flip, Tableau.flip] + apply nil_edge_loc_of_length_zero + refine (PathIn.length_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _)).trans ?_ + · exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) + (by congr 1 <;> simp)) + · rw [PathIn.flip_length]; exact hs + | pdl s => + have hs : s.length = 0 := by + have := length_succ_eq_length_of_edge pq + simp only [PathIn.length] at this + omega + simp only [PathIn.flip, Tableau.flip] + exact nil_edge_pdl_of_length_zero (by rw [PathIn.flip_length]; exact hs) + | loc Y_in t IH => + intro q pq + obtain ⟨s, rfl, ts⟩ := edge_loc_shape pq + simp only [PathIn.flip, Tableau.flip] + rw [loc_edge_loc_iff_edge] + refine (edge_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) + (flip_aux_eq_mpr_heq _ _)).mpr (IH s ts) + exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) + (by congr 1 <;> simp)) + | pdl t IH => + intro q pq + obtain ⟨s, rfl, ts⟩ := edge_pdl_shape pq + simp only [PathIn.flip, Tableau.flip] + rw [pdl_edge_pdl_iff_edge] + exact IH s ts + +/-- Flipping a tableau does not change which nodes are children of which. -/ +lemma edge_flip {H X} {tab : Tableau H X} {p q : PathIn tab} : + (p.flip ⋖_ q.flip) ↔ p ⋖_ q := by + constructor + · intro h + refine (edge_heq_congr (H2 := H) (X2 := X) (by simp) (by simp) + (flip_aux_Tableau_flip_flip_heq tab) + (eqRec_heq_iff.mp (heq_of_eq (PathIn.flip_flip p))) + (eqRec_heq_iff.mp (heq_of_eq (PathIn.flip_flip q)))).mp (edge_flip_of_edge _ _ h) + · exact edge_flip_of_edge p q + +/-- The tableau at a path only depends on it up to heterogeneous equality. -/ +lemma tabAt_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} + {p1 : PathIn t1} {p2 : PathIn t2} + (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : + tabAt p1 = tabAt p2 := by + subst hH hX + obtain rfl := eq_of_heq ht + rw [eq_of_heq hp] + +/-- The history of a path only depends on it up to heterogeneous equality. -/ +lemma toHistory_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} + {p1 : PathIn t1} {p2 : PathIn t2} + (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) : + p1.toHistory = p2.toHistory := by + subst hH hX + obtain rfl := eq_of_heq ht + rw [eq_of_heq hp] + +/-- The tableau at a flipped path is the flip of the tableau at the original path. -/ +lemma tabAt_flip {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : + tabAt p.flip + = ⟨List.map Sequent.flip (tabAt p).1, (tabAt p).2.1.flip, (tabAt p).2.2.flip⟩ := by + induction p + case nil => simp [PathIn.flip, tabAt] + case loc Hist X nflprep nbas lt next Y Y_in tail IH => + simp only [PathIn.flip, Tableau.flip] + change _ = (⟨List.map Sequent.flip (tabAt tail).1, (tabAt tail).2.1.flip, + (tabAt tail).2.2.flip⟩ : Σ H X, Tableau H X) + rw [← IH] + refine Eq.trans tabAt_loc (tabAt_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _)) + exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) + (by congr 1 <;> simp)) + case pdl IH => + simp only [PathIn.flip] + exact IH + +/-- The sequent at a flipped path is the flip of the sequent at the original path. -/ +lemma PathIn.nodeAt_flip {Hist X} {tab : Tableau Hist X} {e : PathIn tab} : + nodeAt (e.flip) = (nodeAt e).flip := by + unfold nodeAt + rw [tabAt_flip] + +/-- The history of a flipped path is the flip of the history of the original path. -/ +lemma toHistory_flip {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : + p.flip.toHistory = List.map Sequent.flip p.toHistory := by + induction p + case nil => simp [PathIn.flip, PathIn.toHistory] + case loc Hist X nflprep nbas lt next Y Y_in tail IH => + simp only [PathIn.flip, PathIn.toHistory, List.map_append, List.map_cons, List.map_nil] + rw [← IH] + congr 1 + refine toHistory_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _) + exact HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) + (by congr 1 <;> simp)) + case pdl IH => + simp only [PathIn.flip, PathIn.toHistory, List.map_append, List.map_cons, List.map_nil] + rw [IH] + +/-- Rewinding only depends on the path up to heterogeneous equality, +and on the index only via its value. -/ +lemma PathIn.rewind_heq_congr {H1 X1 H2 X2} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} + {p1 : PathIn t1} {p2 : PathIn t2} {k1 : Fin (p1.toHistory.length + 1)} + {k2 : Fin (p2.toHistory.length + 1)} + (hH : H1 = H2) (hX : X1 = X2) (ht : HEq t1 t2) (hp : HEq p1 p2) (hk : (k1 : ℕ) = (k2 : ℕ)) : + HEq (p1.rewind k1) (p2.rewind k2) := by + subst hH hX + obtain rfl := eq_of_heq ht + obtain rfl := eq_of_heq hp + obtain rfl : k1 = k2 := Fin.ext hk + rfl + +/-- Flipping commutes with rewinding. -/ +lemma PathIn.flip_rewind {Hist X} {tab : Tableau Hist X} (p : PathIn tab) : + ∀ (k : Fin (p.toHistory.length + 1)) (k' : Fin (p.flip.toHistory.length + 1)), + (k : ℕ) = (k' : ℕ) → (p.rewind k).flip = p.flip.rewind k' := by + induction p + case nil => + intro k k' hk + simp [PathIn.rewind, PathIn.flip] + case loc Hist X nflprep nbas lt next Y Y_in tail IH => + have hL : ((PathIn.loc Y_in tail : + PathIn (Tableau.loc nflprep nbas lt next)).flip).toHistory.length + = tail.toHistory.length + 1 := by rw [toHistory_flip]; simp + simp only [PathIn.flip, Tableau.flip] at hL + simp only [PathIn.flip, Tableau.flip] + intro k k' hk + cases k using Fin.lastCases with + | last => + cases k' using Fin.lastCases with + | last => simp [PathIn.rewind, PathIn.flip, Tableau.flip] + | cast j' => + exfalso + have hj := j'.isLt + simp only [Fin.val_last, Fin.val_castSucc, PathIn.loc_length_eq] at hk + omega + | cast j => + cases k' using Fin.lastCases with + | last => + exfalso + have hj := j.isLt + simp only [PathIn.loc_length_eq] at hj + simp only [Fin.val_last, Fin.val_castSucc] at hk + rw [hL] at hk + omega + | cast j' => + simp only [PathIn.rewind, Fin.lastCases_castSucc, Function.comp_apply, PathIn.flip] + congr 1 + have hlen : tail.flip.toHistory.length = tail.toHistory.length := by + rw [toHistory_flip]; simp + have hm : (j : ℕ) < tail.flip.toHistory.length + 1 := by + have := j.isLt + simp only [PathIn.loc_length_eq] at this + omega + apply eq_of_heq + refine HEq.trans (flip_aux_eq_mpr_heq _ _) ?_ + rw [IH (Fin.cast (PathIn.loc_length_eq Y_in tail) j) ⟨j, hm⟩ rfl] + refine PathIn.rewind_heq_congr (by simp) (by simp) ?_ (flip_aux_eq_mpr_heq _ _).symm ?_ + · exact (HEq.trans (eqRec_heq _ _) (Tableau_flip_heq (by simp) (by simp) + (by congr 1 <;> simp))).symm + · simp only [Fin.val_castSucc] at hk + simpa only [Fin.val_cast] using hk + case pdl Hist X Z nrep bas r nx tail IH => + simp only [PathIn.flip, Tableau.flip] + intro k k' hk + cases k using Fin.lastCases with + | last => + cases k' using Fin.lastCases with + | last => simp [PathIn.rewind, PathIn.flip, Tableau.flip] + | cast j' => + exfalso + have := j'.isLt + simp only [Fin.val_last, Fin.val_castSucc, PathIn.pdl_length_eq] at hk this + rw [toHistory_flip] at this + simp at this + omega + | cast j => + cases k' using Fin.lastCases with + | last => + exfalso + have := j.isLt + simp only [Fin.val_last, Fin.val_castSucc, PathIn.pdl_length_eq] at hk this + rw [toHistory_flip] at hk + simp at hk + omega + | cast j' => + simp only [PathIn.rewind, Fin.lastCases_castSucc, Function.comp_apply, PathIn.flip] + congr 1 + refine IH _ _ ?_ + simp only [Fin.val_castSucc] at hk + simpa using hk + +/-- If a path ends in a loaded-path-repeat, then so does the flipped path, +with a repeat at the same position in the history. -/ +lemma tabAt_flip_lrep {Hist X} {tab : Tableau Hist X} (p : PathIn tab) lpr + (h : (tabAt p).2.2 = .lrep lpr) : + ∃ lpr' : LoadedPathRepeat (tabAt p.flip).1 (tabAt p.flip).2.1, + (tabAt p.flip).2.2 = .lrep lpr' ∧ (lpr'.1 : ℕ) = (lpr.1 : ℕ) := by + rw [tabAt_flip p, h] + refine ⟨lpr.flip, by simp [Tableau.flip], ?_⟩ + rcases lpr with ⟨k, hk⟩ + simp [LoadedPathRepeat.flip] + +end PDL diff --git a/LeanPool/PDL/General/ImportCompatibility.lean b/LeanPool/PDL/General/ImportCompatibility.lean new file mode 100644 index 0000000000..a4a30d2388 --- /dev/null +++ b/LeanPool/PDL/General/ImportCompatibility.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ + +module + +public meta import Lean + +/-! # Retaining auxiliary declarations across module splits -/ + +public meta section + +open Lean + +namespace PDL.ImportCompatibility + +private def mappedExpression (source target : Name) (expression : Expr) : Expr := + expression.replace fun expression => + match expression with + | .const name levels => + if source.isPrefixOf name then some (.const (name.replacePrefix source target) levels) + else none + | _ => none + +private def mappedDeclaration (source target : Name) (info : ConstantInfo) : CoreM Declaration := do + let name := info.name.replacePrefix source target + let type := mappedExpression source target info.type + match info with + | .defnInfo value => + return .defnDecl {value with + name := name + type := type + value := mappedExpression source target value.value + all := value.all.map (fun n => n.replacePrefix source target)} + | .thmInfo value => + return .thmDecl {value with + name := name + type := type + value := mappedExpression source target value.value + all := value.all.map (fun n => n.replacePrefix source target)} + | _ => throwError "unsupported auxiliary declaration: {info.name}" + +private def privateDeclarations (moduleName : Name) : CoreM (Array ConstantInfo) := do + let env ← getEnv + unless env.header.moduleNames.contains moduleName do + throwError "module is not imported: {moduleName}" + let modulePrefix := `_private ++ moduleName + let mut result := #[] + for (name, data) in env.header.moduleNames.zip env.header.moduleData do + unless name == moduleName do continue + for declaration in data.constNames do + if modulePrefix.isPrefixOf declaration then + result := result.push (← getConstInfo declaration) + return result + +/-- Retain original auxiliary names after moving their parent declarations to another module. +The kernel checks every copied type and value; existing declarations are never replaced. -/ +def retainPrivateDeclarations (sourceModule targetModule : Name) : CoreM Unit := do + let source := `_private ++ sourceModule + let target := `_private ++ targetModule + let mut pending ← privateDeclarations sourceModule + for _ in [:pending.size] do + if pending.isEmpty then break + let mut remaining := #[] + let mut progress := false + for info in pending do + let env ← getEnv + let name := info.name.replacePrefix source target + if let some existing := env.find? name then + unless existing.type == mappedExpression source target info.type && + existing.levelParams == info.levelParams && existing.isUnsafe == info.isUnsafe && + existing.isPartial == info.isPartial do + throwError "incompatible auxiliary declaration: {name}" + progress := true + continue + let references := info.type.getUsedConstants ++ + (info.value? (allowOpaque := true)).toArray.flatMap Expr.getUsedConstants + if !(references.all fun n => !source.isPrefixOf n || + env.contains (n.replacePrefix source target)) then + remaining := remaining.push info + continue + -- Match the kernel declarations produced by Lean's auxiliary generators, without + -- compiling recursor helpers that are used only while constructing proofs. + addDecl (← mappedDeclaration source target info) + progress := true + if !progress then throwError "cyclic auxiliary declarations in {sourceModule}" + pending := remaining + unless pending.isEmpty do throwError "incomplete auxiliary declarations in {sourceModule}" + +end PDL.ImportCompatibility diff --git a/LeanPool/PDL/General/NaturalBounds.lean b/LeanPool/PDL/General/NaturalBounds.lean new file mode 100644 index 0000000000..55e9e409e6 --- /dev/null +++ b/LeanPool/PDL/General/NaturalBounds.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ + +module + +public import Mathlib.Init + +/-! # Natural-number bounds used by tableau measures -/ + +public section + +namespace PDL.NaturalBounds + +/-- A bound on the left summand gives a strict bound after adding one. -/ +theorem lt_sum_left {value left right : Nat} (bound : value ≤ left) : + value < 1 + left + right := by omega + +/-- A bound on the right summand gives a strict bound after adding one. -/ +theorem lt_sum_right {value left right : Nat} (bound : value ≤ right) : + value < 1 + left + right := by omega + +/-- Adding one turns a non-strict bound into a strict bound. -/ +theorem lt_one_add {value bound : Nat} (bounded : value ≤ bound) : + value < 1 + bound := by omega + +/-- The smallest nonzero program measure stays below a two-step extension. -/ +theorem one_lt_two_add (right : Nat) : 1 < 2 + right := by omega + +end PDL.NaturalBounds diff --git a/LeanPool/PDL/Imports.lean b/LeanPool/PDL/Imports.lean index d53ba5b668..e5b20349d8 100644 --- a/LeanPool/PDL/Imports.lean +++ b/LeanPool/PDL/Imports.lean @@ -19,9 +19,12 @@ public import LeanPool.PDL.Discon public import LeanPool.PDL.Distance public import LeanPool.PDL.FischerLadner public import LeanPool.PDL.Flip +public import LeanPool.PDL.FlipCore public import LeanPool.PDL.General.FinReach public import LeanPool.PDL.General.Game +public import LeanPool.PDL.General.ImportCompatibility public import LeanPool.PDL.General.ListFinset +public import LeanPool.PDL.General.NaturalBounds public import LeanPool.PDL.Interpolation.Cluster public import LeanPool.PDL.Interpolation.ClusterInterpolation public import LeanPool.PDL.Interpolation.ClusterItp @@ -38,6 +41,7 @@ public import LeanPool.PDL.Interpolation.QuasiTableau public import LeanPool.PDL.Interpolation.SingletonCluster public import LeanPool.PDL.Interpolation.Theorem public import LeanPool.PDL.Interpolation.Uniformity +public import LeanPool.PDL.Interpolation.UniformityCore public import LeanPool.PDL.KeepRight public import LeanPool.PDL.Local.AllLocalTab public import LeanPool.PDL.Local.Path diff --git a/LeanPool/PDL/Interpolation/Cluster.lean b/LeanPool/PDL/Interpolation/Cluster.lean index 6c5b2445c4..7a7472a42e 100644 --- a/LeanPool/PDL/Interpolation/Cluster.lean +++ b/LeanPool/PDL/Interpolation/Cluster.lean @@ -8,6 +8,11 @@ module public import LeanPool.PDL.Interpolation.FinePath public import LeanPool.PDL.Interpolation.Local +public import LeanPool.PDL.Flip +public import LeanPool.PDL.KeepRight + +import Mathlib.Algebra.Order.Ring.Nat +import LeanPool.PDL.Star /-! # Loaded Clusters (start of Section 9) diff --git a/LeanPool/PDL/Interpolation/FinePath.lean b/LeanPool/PDL/Interpolation/FinePath.lean index bee097e6fc..77d575294c 100644 --- a/LeanPool/PDL/Interpolation/FinePath.lean +++ b/LeanPool/PDL/Interpolation/FinePath.lean @@ -6,8 +6,11 @@ Authors: PDL formalization contributors (see project card) module -public import LeanPool.PDL.Flip -public import LeanPool.PDL.KeepRight +public import LeanPool.PDL.TableauPath + +import Mathlib.Data.Nat.SuccPred +import Mathlib.Algebra.Order.Ring.Nat +import Mathlib.Algebra.Order.BigOperators.Group.List /-! # Fine paths in local tableaux and in tableaux diff --git a/LeanPool/PDL/Interpolation/Uniformity.lean b/LeanPool/PDL/Interpolation/Uniformity.lean index efdb7fdf6b..840d5b403d 100644 --- a/LeanPool/PDL/Interpolation/Uniformity.lean +++ b/LeanPool/PDL/Interpolation/Uniformity.lean @@ -6,9 +6,12 @@ Authors: PDL formalization contributors (see project card) module -public import LeanPool.PDL.Local.AllLocalTab +public import LeanPool.PDL.Interpolation.UniformityCore +import all LeanPool.PDL.Interpolation.UniformityCore -- shake: keep public import LeanPool.PDL.Interpolation.ClusterSatDown +meta import LeanPool.PDL.General.ImportCompatibility + /-! # Uniformity of split tableaux (Section 8.1) This file defines when a tableau is *uniform*, by the two conditions U1 and U2 of the @@ -57,814 +60,6 @@ under different names. namespace PDL -/-! ## The components of a sequent -/ - -/-- The left component of a sequent, together with the loaded formula, again as a sequent. -This is `Λ₁` from the paper; compare `Sequent.rightOnly`, which is `Λ₂`. -/ -def Sequent.leftOnly (X : Sequent) : Sequent := ⟨X.1, ∅, X.2.2⟩ - -/-- The left component of a sequent, without any loaded formula. When the loaded formula -is on the right, i.e. in the situation of a `LoadedCluster`, this is the *unloaded* -component `Λ₁` of the node, and `Sequent.leftFree X |>.basic` says that no local rule is -applicable to it. -/ -def Sequent.leftFree (X : Sequent) : Sequent := ⟨X.1, ∅, none⟩ - -/-- The right component of a sequent, without any loaded formula. When the loaded formula -is on the left this is the *unloaded* component `Λ₂` of the node. -/ -def Sequent.rightFree (X : Sequent) : Sequent := ⟨∅, X.2.1, none⟩ - -/-- Two local rule applications use the same rule with the same principal formulas. -The fields `Lcond`, `Rcond` and `Ocond` are the principal formulas and `ress` is the list -of results of the rule, so this says that the *same rule instance* is applied at two nodes, -which may still have different sequents. -/ -def LocalRuleApp.SameRuleAs (lra₁ lra₂ : LocalRuleApp) : Prop := - lra₁.Lcond = lra₂.Lcond ∧ lra₁.Rcond = lra₂.Rcond ∧ lra₁.Ocond = lra₂.Ocond - ∧ lra₁.ress = lra₂.ress ∧ HEq lra₁.lr lra₂.lr - -/-! ## Uniformity -/ - -/-- Condition U1: at a node with a loaded component, a rule is applied to the *unloaded* -component unless the latter is basic. Since every rule is a left rule or a right rule but -not both (`FinePathIn.not_left_and_right`), we state this as: a rule on the unloaded side -is applied. - -The condition is only about nodes at which a rule is applied at all, i.e. we exclude the -leaves given by a loaded-path repeat, which is what `¬ f.base.isLrep` says. Note that this -exclusion is needed: at a loaded-path repeat the tableau stops, so no rule at all — and in -particular no rule on the unloaded component — is applied there, while the sequent of a -loaded-path repeat may well have a non-basic unloaded component. (For example, the sequent -reached again after a loop may contain a conjunction on the unloaded side; the tableau is -then forced to stop, because `Tableau.loc` and `Tableau.pdl` both require `¬ flprep`.) -Without the exclusion no tableau with such a repeat would be uniform, and `Tableau.toUniform` -would fail. -/ -def Tableau.U1 {H : History} {X : Sequent} (tab : Tableau H X) : Prop := - ∀ f : FinePathIn tab, ¬ f.base.isLrep → - (f.label.2.2.isRight → ¬ f.label.leftFree.basic → f.usesLeftRule) - ∧ (f.label.2.2.isLeft → ¬ f.label.rightFree.basic → f.usesRightRule) - -/-- Condition U2: two nodes whose loaded component is the same and not basic, and whose -unloaded components are both basic, apply the same rule to the same formula of the loaded -component. As the loaded component is not basic the rule must be a local one, so we may -state this for the local rule applications `f.lraOpt` and `g.lraOpt`. -/ -def Tableau.U2 {H : History} {X : Sequent} (tab : Tableau H X) : Prop := - ∀ (f g : FinePathIn tab) (lraf lrag : LocalRuleApp), - f.lraOpt = some lraf → g.lraOpt = some lrag → - ( (f.label.2.2.isRight → f.label.rightOnly = g.label.rightOnly → - ¬ f.label.rightOnly.basic → f.label.leftFree.basic → g.label.leftFree.basic → - lraf.isRightRule → lrag.isRightRule → lraf.SameRuleAs lrag) - ∧ (f.label.2.2.isLeft → f.label.leftOnly = g.label.leftOnly → - ¬ f.label.leftOnly.basic → f.label.rightFree.basic → g.label.rightFree.basic → - lraf.isLeftRule → lrag.isLeftRule → lraf.SameRuleAs lrag) ) - -/-- The conditions U1 and U2 together. -/ -def Tableau.UniCore {H : History} {X : Sequent} (tab : Tableau H X) : Prop := - tab.U1 ∧ tab.U2 - -/-- A sanity check that U1 and U2 are not contradictory: both conditions only constrain -nodes with a loaded component, so a tableau in which no node is loaded satisfies them. -/ -lemma Tableau.uniCore_of_all_free {H : History} {X : Sequent} {tab : Tableau H X} - (h : ∀ f : FinePathIn tab, f.label.2.2 = none) : tab.UniCore := by - refine ⟨fun f _ => ⟨?_, ?_⟩, fun f g lraf lrag _ _ => ⟨?_, ?_⟩⟩ <;> - intro hf <;> rw [h f] at hf <;> simp [Olf.isRight, Olf.isLeft] at hf - -/-- A tableau is *uniform* if it satisfies the conditions U1 and U2. - -We also demand U1 and U2 for the flipped tableau `tab.flip`, in which the left and the -right components of all sequents are swapped. This is not an extra demand: U1 and U2 are -symmetric in the two components, so `tab.UniCore` and `tab.flip.UniCore` say the same -thing. Asking for both here only spares us the purely technical work of transporting U1 -and U2 along `Tableau.flip`, which would need a `flip` operation on `FinePathIn`. -What it buys us is `Tableau.isUniform.flip` below, which is needed because the -interpolation proof flips the tableau when the loaded formula is on the left. -/ -def Tableau.isUniform {H : History} {X : Sequent} (tab : Tableau H X) : Prop := - tab.UniCore ∧ tab.flip.UniCore - -/-- Transporting `Tableau.UniCore` along an equality of tableaux. -/ -lemma Tableau.UniCore.heq_transfer {H₁ X₁ H₂ X₂} {t₁ : Tableau H₁ X₁} {t₂ : Tableau H₂ X₂} - (hH : H₁ = H₂) (hX : X₁ = X₂) (h : HEq t₁ t₂) (h₁ : t₁.UniCore) : t₂.UniCore := by - subst hH - subst hX - cases eq_of_heq h - exact h₁ - -/-- Uniformity is preserved by flipping the tableau. -/ -lemma Tableau.isUniform.flip {H : History} {X : Sequent} {tab : Tableau H X} - (h : tab.isUniform) : tab.flip.isUniform := - ⟨h.2, Tableau.UniCore.heq_transfer Hist_flip.symm Sequent.flip_flip.symm - (HEq.symm (flip_aux_Tableau_flip_flip_heq tab)) h.1⟩ - -/-! ## Uniform tableaux by construction - -To obtain uniform tableaux we follow approach (B): instead of repairing a given tableau we -describe how a uniform one is built, by fixing *which* local rule is applied at each node. -The conditions U1 and U2 only speak about the local rules applied at the nodes, and both are -conditions that can be read off a single rule application together with the sequent it is -applied to. This is what `LocalRuleApp.IsUniChoice` below says: - -* the rule is applied to the unloaded component, unless that component is basic (U1); and -* if it is applied to the loaded component (the unloaded one then being basic) then it is - *the* canonical rule for that component, given by `uniRightChoice` resp. `uniLeftChoice`. - -Since the canonical rule only depends on the loaded component `Λᵢ(s)`, any two nodes with -the same loaded component use the same rule, which is U2. A tableau all of whose rule -applications are `IsUniChoice` is called `Tableau.IsUni`, and `Tableau.IsUni.uniCore` shows -that such a tableau indeed satisfies U1 and U2. The construction is symmetric under flipping -(`Tableau.IsUni.flip`), which gives the second half of `Tableau.isUniform`. -/ - -/-! ### Flipping components, rules and rule applications -/ - -@[simp] -lemma LocalRuleApp.flip_O (lra : LocalRuleApp) : (lra.flip).O = lra.O.flip := by - rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩; rfl - -lemma LocalRuleApp.flip_X (lra : LocalRuleApp) : (lra.flip).X = lra.X.flip := by - rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ - simp [LocalRuleApp.flip, Sequent.flip] - -@[simp] -lemma LocalRuleApp.flip_isRightRule (lra : LocalRuleApp) : - (lra.flip).isRightRule = lra.isLeftRule := by - rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ - cases lr <;> simp [LocalRuleApp.flip, LocalRuleApp.isRightRule, LocalRuleApp.isLeftRule, - LocalRule.isRightRule, LocalRule.isLeftRule, LocalRule.flip] - -@[simp] -lemma LocalRuleApp.flip_isLeftRule (lra : LocalRuleApp) : - (lra.flip).isLeftRule = lra.isRightRule := by - rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ - cases lr <;> simp [LocalRuleApp.flip, LocalRuleApp.isRightRule, LocalRuleApp.isLeftRule, - LocalRule.isRightRule, LocalRule.isLeftRule, LocalRule.flip] - -@[simp] -lemma Sequent.flip_leftFree {X : Sequent} : X.flip.leftFree = X.rightFree.flip := by - rcases X with ⟨L, R, O⟩; rfl - -@[simp] -lemma Sequent.flip_rightFree {X : Sequent} : X.flip.rightFree = X.leftFree.flip := by - rcases X with ⟨L, R, O⟩; rfl - -@[simp] -lemma Sequent.flip_rightOnly {X : Sequent} : X.flip.rightOnly = X.leftOnly.flip := by - rcases X with ⟨L, R, O⟩; simp [Sequent.flip, Sequent.rightOnly, Sequent.leftOnly] - -@[simp] -lemma Sequent.flip_leftOnly {X : Sequent} : X.flip.leftOnly = X.rightOnly.flip := by - rcases X with ⟨L, R, O⟩; simp [Sequent.flip, Sequent.rightOnly, Sequent.leftOnly] - -/-- Being the same rule is preserved by flipping. -/ -lemma LocalRuleApp.SameRuleAs.flip {lra₁ lra₂ : LocalRuleApp} (h : lra₁.SameRuleAs lra₂) : - lra₁.flip.SameRuleAs lra₂.flip := by - obtain ⟨hL, hR, hO, hress, hlr⟩ := h - rcases lra₁ with ⟨L₁, R₁, O₁, Lcond₁, Rcond₁, Ocond₁, ress₁, lr₁, C₁, hC₁, pre₁⟩ - rcases lra₂ with ⟨L₂, R₂, O₂, Lcond₂, Rcond₂, Ocond₂, ress₂, lr₂, C₂, hC₂, pre₂⟩ - simp_all only - subst hL; subst hR; subst hO; subst hress - cases eq_of_heq hlr - exact ⟨rfl, rfl, rfl, rfl, HEq.rfl⟩ - -/-- Being the same rule is reflexive. -/ -lemma LocalRuleApp.SameRuleAs.refl (lra : LocalRuleApp) : lra.SameRuleAs lra := - ⟨rfl, rfl, rfl, rfl, HEq.rfl⟩ - -/-- Being the same rule is symmetric. -/ -lemma LocalRuleApp.SameRuleAs.symm {lra₁ lra₂ : LocalRuleApp} (h : lra₁.SameRuleAs lra₂) : - lra₂.SameRuleAs lra₁ := - ⟨h.1.symm, h.2.1.symm, h.2.2.1.symm, h.2.2.2.1.symm, h.2.2.2.2.symm⟩ - -/-- Being the same rule is transitive. -/ -lemma LocalRuleApp.SameRuleAs.trans {lra₁ lra₂ lra₃ : LocalRuleApp} - (h : lra₁.SameRuleAs lra₂) (h' : lra₂.SameRuleAs lra₃) : lra₁.SameRuleAs lra₃ := - ⟨h.1.trans h'.1, h.2.1.trans h'.2.1, h.2.2.1.trans h'.2.2.1, - h.2.2.2.1.trans h'.2.2.2.1, h.2.2.2.2.trans h'.2.2.2.2⟩ - -/-! ### The canonical rule for a component -/ - -/-- The canonical local rule to be applied to the right component of a sequent. -We use the first right rule in the list `LocalRuleApp.all` of all applicable rules. -Which rule exactly is picked does not matter for uniformity; all that matters is that -this is a *function* of the sequent — and that it is applied to sequents of the form -`X.rightOnly`, so that it only depends on the right component. -/ -def uniRightChoice (Y : Sequent) : Option LocalRuleApp := - (LocalRuleApp.all Y).find? (fun lra => lra.isRightRule) - -/-- The canonical local rule to be applied to the left component of a sequent. -Defined as the flip of `uniRightChoice`, which makes the whole construction symmetric. -/ -def uniLeftChoice (Y : Sequent) : Option LocalRuleApp := - (uniRightChoice Y.flip).map LocalRuleApp.flip - -lemma uniLeftChoice_flip (Y : Sequent) : - uniLeftChoice Y.flip = (uniRightChoice Y).map LocalRuleApp.flip := by - simp [uniLeftChoice] - -lemma uniRightChoice_flip (Y : Sequent) : - uniRightChoice Y.flip = (uniLeftChoice Y).map LocalRuleApp.flip := by - simp [uniLeftChoice, Option.map_map, Function.comp_def, LocalRuleApp.flip_flip] - -/-! ### Uniform rule applications -/ - -/-- The conditions on a single local rule application in a uniform tableau: the first two -fields are the local form of U1 and the last two are the local form of U2. -/ -structure LocalRuleApp.IsUniChoice (lra : LocalRuleApp) : Prop where - /-- If loaded on the right and the left component is not basic, a left rule is applied. -/ - leftFirst : lra.X.2.2.isRight → ¬ lra.X.leftFree.basic → lra.isLeftRule - /-- If loaded on the left and the right component is not basic, a right rule is applied. -/ - rightFirst : lra.X.2.2.isLeft → ¬ lra.X.rightFree.basic → lra.isRightRule - /-- A right rule applied at a node loaded on the right whose left component is basic is - the canonical rule for the right component. -/ - rightCanon : lra.isRightRule → lra.X.2.2.isRight → lra.X.leftFree.basic → - ∃ lrb, uniRightChoice lra.X.rightOnly = some lrb ∧ lra.SameRuleAs lrb - /-- A left rule applied at a node loaded on the left whose right component is basic is - the canonical rule for the left component. -/ - leftCanon : lra.isLeftRule → lra.X.2.2.isLeft → lra.X.rightFree.basic → - ∃ lrb, uniLeftChoice lra.X.leftOnly = some lrb ∧ lra.SameRuleAs lrb - -/-- The conditions on rule applications are symmetric under flipping. -/ -lemma LocalRuleApp.IsUniChoice.flip {lra : LocalRuleApp} (h : lra.IsUniChoice) : - lra.flip.IsUniChoice := by - have hXf : lra.flip.X = lra.X.flip := LocalRuleApp.flip_X lra - refine ⟨?_, ?_, ?_, ?_⟩ - · intro h1 h2 - have h1' : lra.X.2.2.isLeft := by - rw [hXf] at h1; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] - have h2' : ¬ lra.X.rightFree.basic := by - rw [hXf] at h2; simpa using h2 - simpa using h.rightFirst h1' h2' - · intro h1 h2 - have h1' : lra.X.2.2.isRight := by - rw [hXf] at h1; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] - have h2' : ¬ lra.X.leftFree.basic := by - rw [hXf] at h2; simpa using h2 - simpa using h.leftFirst h1' h2' - · intro h1 h2 h3 - have h1' : lra.isLeftRule := by simpa using h1 - have h2' : lra.X.2.2.isLeft := by - rw [hXf] at h2; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] - have h3' : lra.X.rightFree.basic := by - rw [hXf] at h3; simpa using h3 - obtain ⟨lrb, hb, hsame⟩ := h.leftCanon h1' h2' h3' - refine ⟨lrb.flip, ?_, hsame.flip⟩ - rw [hXf, Sequent.flip_rightOnly, uniRightChoice_flip, hb] - rfl - · intro h1 h2 h3 - have h1' : lra.isRightRule := by simpa using h1 - have h2' : lra.X.2.2.isRight := by - rw [hXf] at h2; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] - have h3' : lra.X.leftFree.basic := by - rw [hXf] at h3; simpa using h3 - obtain ⟨lrb, hb, hsame⟩ := h.rightCanon h1' h2' h3' - refine ⟨lrb.flip, ?_, hsame.flip⟩ - rw [hXf, Sequent.flip_leftOnly, uniLeftChoice_flip, hb] - rfl - -/-! ### Basic sequents have basic components -/ - -lemma Sequent.leftFree_basic_of_basic {X : Sequent} (h : X.basic) : X.leftFree.basic := by - rcases X with ⟨L, R, o⟩ - rcases h with ⟨hall, hcl⟩ - refine ⟨fun f hf => hall f ?_, ?_⟩ - · simp only [Sequent.leftFree, Sequent.toFinset, Finset.union_empty, Finset.union_assoc, - Finset.mem_union] at hf ⊢ - tauto - · rintro (hbot | ⟨f, hf, hnf⟩) - · exact hcl (Or.inl (by simp_all [Sequent.leftFree, Sequent.mem_def])) - · exact hcl (Or.inr ⟨f, by simp_all [Sequent.leftFree, Sequent.mem_def]⟩) - -lemma Sequent.rightFree_basic_of_basic {X : Sequent} (h : X.basic) : X.rightFree.basic := by - rcases X with ⟨L, R, o⟩ - rcases h with ⟨hall, hcl⟩ - refine ⟨fun f hf => hall f ?_, ?_⟩ - · simp only [Sequent.rightFree, Sequent.toFinset, Finset.empty_union, Finset.union_assoc, - Finset.mem_union] at hf ⊢ - tauto - · rintro (hbot | ⟨f, hf, hnf⟩) - · exact hcl (Or.inl (by simp_all [Sequent.rightFree, Sequent.mem_def])) - · exact hcl (Or.inr ⟨f, by simp_all [Sequent.rightFree, Sequent.mem_def]⟩) - -/-- All local rule applications inside a local tableau are uniform choices. -/ -def LocalTableau.IsUni : {X : Sequent} → LocalTableau X → Prop - | _, (.sim _) => True - | _, (.byLocalRule lra _ next) => - lra.IsUniChoice ∧ ∀ Y, ∀ h : Y ∈ lra.C, (next Y h).IsUni - -/-- All local rule applications inside a tableau are uniform choices. -/ -def Tableau.IsUni : {H : History} → {X : Sequent} → Tableau H X → Prop - | _, _, .loc _ _ lt next => lt.IsUni ∧ ∀ Y, ∀ h : Y ∈ endNodesOf lt, (next Y h).IsUni - | _, _, .pdl _ _ _ next => next.IsUni - | _, _, .lrep _ => True - -lemma LocalTableau.IsUni.ltAt {X} {lt : LocalTableau X} (h : lt.IsUni) (lp : LocalPathIn lt) : - (lp.ltAt).IsUni := by - induction lp - case nil => exact h - case cons X lra X_def next Y Y_in tail IH => - rw [LocalTableau.IsUni] at h - exact IH (h.2 Y Y_in) - -lemma Tableau.IsUni.lraOpt_isUniChoice {H X} {tab : Tableau H X} (h : tab.IsUni) - {f : FinePathIn tab} {lra : LocalRuleApp} (hf : f.lraOpt = some lra) : lra.IsUniChoice := by - induction f - case inLoc Hist X nrep nbas lt next lp lp_int => - rw [Tableau.IsUni] at h - have hlt := h.1.ltAt lp - simp only [FinePathIn.lraOpt] at hf - rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas - · rw [hltAt] at hf hlt - simp only [Option.some.injEq] at hf - subst hf - rw [LocalTableau.IsUni] at hlt - exact hlt.1 - · rw [hltAt] at hf; simp at hf - case pdlHere => simp [FinePathIn.lraOpt] at hf - case lrepHere => simp [FinePathIn.lraOpt] at hf - case loc Hist X nrep nbas lt next Y Y_in tail IH => - rw [Tableau.IsUni] at h - exact IH (h.2 Y Y_in) hf - case pdl IH => - rw [Tableau.IsUni] at h - exact IH h hf - -lemma FinePathIn.usesLeftRule_eq_of_lraOpt {H X} {tab : Tableau H X} {f : FinePathIn tab} - {lra : LocalRuleApp} (hf : f.lraOpt = some lra) : f.usesLeftRule = lra.isLeftRule := by - induction f - case inLoc lp lp_int => - simp only [FinePathIn.lraOpt, FinePathIn.usesLeftRule] at * - rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas <;> simp_all - case pdlHere => simp [FinePathIn.lraOpt] at hf - case lrepHere => simp [FinePathIn.lraOpt] at hf - case loc IH => simpa [FinePathIn.usesLeftRule] using IH (by simpa [FinePathIn.lraOpt] using hf) - case pdl IH => simpa [FinePathIn.usesLeftRule] using IH (by simpa [FinePathIn.lraOpt] using hf) - -lemma FinePathIn.usesRightRule_eq_of_lraOpt {H X} {tab : Tableau H X} {f : FinePathIn tab} - {lra : LocalRuleApp} (hf : f.lraOpt = some lra) : f.usesRightRule = lra.isRightRule := by - induction f - case inLoc lp lp_int => - simp only [FinePathIn.lraOpt, FinePathIn.usesRightRule] at * - rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas <;> simp_all - case pdlHere => simp [FinePathIn.lraOpt] at hf - case lrepHere => simp [FinePathIn.lraOpt] at hf - case loc IH => simpa [FinePathIn.usesRightRule] using IH (by simpa [FinePathIn.lraOpt] using hf) - case pdl IH => simpa [FinePathIn.usesRightRule] using IH (by simpa [FinePathIn.lraOpt] using hf) - -lemma FinePathIn.isLrep_or_basic_of_lraOpt_eq_none {H X} {tab : Tableau H X} {f : FinePathIn tab} - (hf : f.lraOpt = none) : f.base.isLrep ∨ f.label.basic := by - induction f - case inLoc lp lp_int => - exfalso - simp only [FinePathIn.lraOpt] at hf - rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas - · rw [hltAt] at hf; simp at hf - · exact absurd lp_int (by simp [LocalPathIn.isInternal, hltAt, LocalTableau.hasRule]) - case pdlHere Hist X Y nrep bas r next => exact Or.inr bas - case lrepHere => exact Or.inl (by simp [FinePathIn.base, PathIn.isLrep, tabAt, Tableau.isLrep]) - case loc IH => - rcases IH (by simpa [FinePathIn.lraOpt] using hf) with h | h - · exact Or.inl (by simpa [FinePathIn.base, PathIn.isLrep, tabAt] using h) - · exact Or.inr (by simpa [FinePathIn.label] using h) - case pdl IH => - rcases IH (by simpa [FinePathIn.lraOpt] using hf) with h | h - · exact Or.inl (by simpa [FinePathIn.base, PathIn.isLrep, tabAt] using h) - · exact Or.inr (by simpa [FinePathIn.label] using h) - -theorem Tableau.IsUni.uniCore {H X} {tab : Tableau H X} (h : tab.IsUni) : tab.UniCore := by - constructor - · -- U1 - intro f hnlrep - rcases hl : f.lraOpt with _ | lra - · rcases FinePathIn.isLrep_or_basic_of_lraOpt_eq_none hl with hb | hbas - · exact absurd hb hnlrep - · exact ⟨fun _ hcon => absurd (Sequent.leftFree_basic_of_basic hbas) hcon, - fun _ hcon => absurd (Sequent.rightFree_basic_of_basic hbas) hcon⟩ - · have hu := h.lraOpt_isUniChoice hl - have hX : f.label = lra.X := (f.lraOpt_spec hl).1 - constructor - · intro h1 h2 - rw [FinePathIn.usesLeftRule_eq_of_lraOpt hl] - exact hu.leftFirst (hX ▸ h1) (hX ▸ h2) - · intro h1 h2 - rw [FinePathIn.usesRightRule_eq_of_lraOpt hl] - exact hu.rightFirst (hX ▸ h1) (hX ▸ h2) - · -- U2 - intro f g lraf lrag hf hg - have huf := h.lraOpt_isUniChoice hf - have hug := h.lraOpt_isUniChoice hg - have hXf : f.label = lraf.X := (f.lraOpt_spec hf).1 - have hXg : g.label = lrag.X := (g.lraOpt_spec hg).1 - constructor - · intro hfR hfg _ hfl hgl hfRule hgRule - have hOeq : f.label.2.2 = g.label.2.2 := congrArg (fun Y => Y.2.2) hfg - have hgR : g.label.2.2.isRight := hOeq ▸ hfR - obtain ⟨lrb, hb, hsame⟩ := huf.rightCanon hfRule (hXf ▸ hfR) (hXf ▸ hfl) - obtain ⟨lrb', hb', hsame'⟩ := hug.rightCanon hgRule (hXg ▸ hgR) (hXg ▸ hgl) - have : lrb = lrb' := by - rw [← hXf, hfg] at hb - rw [← hXg] at hb' - exact Option.some.inj (hb.symm.trans hb') - exact hsame.trans (this ▸ hsame'.symm) - · intro hfL hfg _ hfr hgr hfRule hgRule - have hOeq : f.label.2.2 = g.label.2.2 := congrArg (fun Y => Y.2.2) hfg - have hgL : g.label.2.2.isLeft := hOeq ▸ hfL - obtain ⟨lrb, hb, hsame⟩ := huf.leftCanon hfRule (hXf ▸ hfL) (hXf ▸ hfr) - obtain ⟨lrb', hb', hsame'⟩ := hug.leftCanon hgRule (hXg ▸ hgL) (hXg ▸ hgr) - have : lrb = lrb' := by - rw [← hXf, hfg] at hb - rw [← hXg] at hb' - exact Option.some.inj (hb.symm.trans hb') - exact hsame.trans (this ▸ hsame'.symm) - -lemma LocalTableau.IsUni_cast {A B : Sequent} (h : A = B) (t : LocalTableau A) : - (h ▸ t).IsUni ↔ t.IsUni := by subst h; rfl - -lemma Tableau.IsUni_cast {H} {A B : Sequent} (h : A = B) (t : Tableau H A) : - (h ▸ t).IsUni ↔ t.IsUni := by subst h; rfl - -lemma LocalTableau.IsUni.flip {X} {lt : LocalTableau X} (h : lt.IsUni) : (lt.flip).IsUni := by - induction lt - case byLocalRule X lra X_def next IH => - rw [LocalTableau.IsUni] at h - rw [LocalTableau.flip, LocalTableau.IsUni] - refine ⟨h.1.flip, ?_⟩ - intro Y Y_in - rw [LocalTableau.IsUni_cast] - exact IH _ (Sequent.flip_mem_of_mem_image_flip Y_in) (h.2 _ _) - case sim bas => rw [LocalTableau.flip, LocalTableau.IsUni]; trivial - -lemma Tableau.IsUni.flip {H X} {tab : Tableau H X} (h : tab.IsUni) : (tab.flip).IsUni := by - induction tab - case loc Hist X nrep nbas lt next IH => - rw [Tableau.IsUni] at h - rw [Tableau.flip, Tableau.IsUni] - refine ⟨h.1.flip, ?_⟩ - intro Y Y_in - rw [Tableau.IsUni_cast] - exact IH _ (endNodesOf_flip Y_in) (h.2 _ _) - case pdl IH => - rw [Tableau.IsUni] at h - rw [Tableau.flip, Tableau.IsUni] - exact IH h - case lrep => trivial - -/-- A tableau all of whose local rule applications are uniform choices is uniform. -/ -theorem Tableau.IsUni.isUniform {X} {tab : Tableau .nil X} (h : tab.IsUni) : tab.isUniform := - ⟨h.uniCore, h.flip.uniCore⟩ - -/-! ## Building a uniform tableau - -We now show `Tableau.exists_isUni`: for every tableau there is one that applies the rules in -the canonical order. The construction is deterministic: `uniChoiceAt` picks, at each sequent, -the canonical rule application (first a rule for the unloaded component, and once that is -basic the canonical rule for the loaded component), and `uniLocalTab` iterates this to a -local tableau all of whose rule applications are uniform choices (`uniLocalTab_isUni`). - -Given an arbitrary tableau we then re-build it, replacing the local tableau at each `loc` -step by the canonical one. Because the end nodes of the canonical local tableau need not be -literally the same lists as the end nodes of the original one, we prove the statement in the -more flexible form `Tableau.exists_isUni_of_msEq`, allowing the sequent and the history to -change up to `Sequent.multisetEqTo`, i.e. up to permutation of the two lists in a sequent. -That the calculus does not care about such permutations is `PdlRule.exists_of_multisetEqTo` -and `lpr_of_multisetEqTo`. - -The only step that is left open is `uniLocalTab_endNode_dominated`. -/ - -/-- Put a local rule application into a different context, keeping the rule itself. -/ -def LocalRuleApp.inContext (lra : LocalRuleApp) (L R : Finset Formula) (O : Olf) - (hL : lra.Lcond ⊆ L) (hR : lra.Rcond ⊆ R) (hO : lra.Ocond ⊆ O) : - LocalRuleApp := - { L := L, R := R, O := O, - Lcond := lra.Lcond, Rcond := lra.Rcond, Ocond := lra.Ocond, - ress := lra.ress, lr := lra.lr, - C := applyLocalRule lra.lr (L, R, O), hC := rfl, - preconditionProof := ⟨hL, hR, hO⟩ } - -/-- Put a local rule application into the context of the sequent `X`, if possible. -/ -def LocalRuleApp.toContext (lra : LocalRuleApp) (X : Sequent) : LocalRuleApp := - if h : lra.Lcond ⊆ X.1 ∧ lra.Rcond ⊆ X.2.1 ∧ lra.Ocond ⊆ X.2.2 then - lra.inContext X.1 X.2.1 X.2.2 h.1 h.2.1 h.2.2 - else lra - -lemma LocalRuleApp.toContext_sameRuleAs (lra : LocalRuleApp) (X : Sequent) : - (lra.toContext X).SameRuleAs lra := by - unfold LocalRuleApp.toContext - split - · exact ⟨rfl, rfl, rfl, rfl, HEq.rfl⟩ - · exact LocalRuleApp.SameRuleAs.refl lra - -@[simp] -lemma LocalRuleApp.toContext_isLeftRule (lra : LocalRuleApp) (X : Sequent) : - (lra.toContext X).isLeftRule = lra.isLeftRule := by - unfold LocalRuleApp.toContext - split <;> rfl - -@[simp] -lemma LocalRuleApp.toContext_isRightRule (lra : LocalRuleApp) (X : Sequent) : - (lra.toContext X).isRightRule = lra.isRightRule := by - unfold LocalRuleApp.toContext - split <;> rfl - -lemma LocalRuleApp.toContext_X (lra : LocalRuleApp) (X : Sequent) - (h : lra.Lcond ⊆ X.1 ∧ lra.Rcond ⊆ X.2.1 ∧ lra.Ocond ⊆ X.2.2) : - (lra.toContext X).X = X := by - unfold LocalRuleApp.toContext - rw [dite_eq_left h] - rfl - -lemma uniRightChoice_spec {Y : Sequent} {lra : LocalRuleApp} (h : uniRightChoice Y = some lra) : - lra.X = Y ∧ lra.isRightRule := by - unfold uniRightChoice at h - exact ⟨LocalRuleApp.all_X Y lra (List.mem_of_find?_eq_some h), by - simpa using List.find?_some h⟩ - -lemma uniRightChoice_isSome {Y : Sequent} {lra : LocalRuleApp} (hX : lra.X = Y) - (hr : lra.isRightRule) : (uniRightChoice Y).isSome := by - unfold uniRightChoice - rcases h : (LocalRuleApp.all Y).find? (fun lra => lra.isRightRule) with _ | lrb - · exfalso - rw [List.find?_eq_none] at h - exact h lra (hX ▸ lra.all_spec) (by simpa using hr) - · rw [h]; rfl - -lemma uniLeftChoice_spec {Y : Sequent} {lra : LocalRuleApp} (h : uniLeftChoice Y = some lra) : - lra.X = Y ∧ lra.isLeftRule := by - unfold uniLeftChoice at h - rw [Option.map_eq_some_iff] at h - obtain ⟨lrb, hb, rfl⟩ := h - obtain ⟨hX, hr⟩ := uniRightChoice_spec hb - refine ⟨?_, by simpa using hr⟩ - rw [LocalRuleApp.flip_X, hX, Sequent.flip_flip] - -lemma uniLeftChoice_isSome {Y : Sequent} {lra : LocalRuleApp} (hX : lra.X = Y) - (hl : lra.isLeftRule) : (uniLeftChoice Y).isSome := by - unfold uniLeftChoice - have : (uniRightChoice Y.flip).isSome := by - refine uniRightChoice_isSome (lra := lra.flip) ?_ (by simpa using hl) - rw [LocalRuleApp.flip_X, hX] - simpa using this - -/-! ### Shapes of left and right rules -/ - -lemma LocalRuleApp.isLeftRule_shape {lra : LocalRuleApp} (h : lra.isLeftRule) : - lra.Rcond = ∅ ∧ (lra.Ocond = none ∨ lra.Ocond.isLeft) := by - rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ - cases lr <;> - simp_all [LocalRuleApp.isLeftRule, LocalRule.isLeftRule, Olf.isLeft] - -lemma LocalRuleApp.isRightRule_shape {lra : LocalRuleApp} (h : lra.isRightRule) : - lra.Lcond = ∅ ∧ (lra.Ocond = none ∨ lra.Ocond.isRight) := by - rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ - cases lr <;> - simp_all [LocalRuleApp.isRightRule, LocalRule.isRightRule, Olf.isRight] - -/-- Any local rule applicable to a sequent of the shape `(L, ∅, none)` is a left rule. -/ -lemma LocalRuleApp.isLeftRule_of_X_eq {lra : LocalRuleApp} {L : Finset Formula} - (h : lra.X = (L, ∅, none)) : lra.isLeftRule := by - rcases lra with ⟨L', R', O', Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ - simp only [LocalRuleApp.X] at h - obtain ⟨rfl, rfl, rfl⟩ := h - obtain ⟨preL, preR, preO⟩ := pre - cases lr - case oneSidedL => simp [LocalRuleApp.isLeftRule, LocalRule.isLeftRule] - case oneSidedR orule YS_def => - exact absurd (Finset.subset_empty.mp preR) (orule.precond_ne_nil) - case LRnegL φ => simp at preR - case LRnegR φ => simp at preR - case loadedL => simp at preO - case loadedR => simp at preO - -/-! ### Moving rules between a sequent and its components -/ - -lemma LocalRuleApp.toContext_X_of_leftOnly {lra : LocalRuleApp} {X : Sequent} - (h : lra.X = X.leftOnly) : (lra.toContext X).X = X := by - obtain ⟨preL, preR, preO⟩ := lra.preconditionProof - have hL : lra.L = X.1 := congrArg (fun Y => Y.1) h - have hR : lra.R = ∅ := congrArg (fun Y => Y.2.1) h - have hO : lra.O = X.2.2 := congrArg (fun Y => Y.2.2) h - refine lra.toContext_X X ⟨hL ▸ preL, ?_, hO ▸ preO⟩ - rw [hR] at preR - rw [Finset.subset_empty.mp preR] - exact Finset.empty_subset _ - -lemma LocalRuleApp.toContext_X_of_rightOnly {lra : LocalRuleApp} {X : Sequent} - (h : lra.X = X.rightOnly) : (lra.toContext X).X = X := by - obtain ⟨preL, preR, preO⟩ := lra.preconditionProof - have hL : lra.L = ∅ := congrArg (fun Y => Y.1) h - have hR : lra.R = X.2.1 := congrArg (fun Y => Y.2.1) h - have hO : lra.O = X.2.2 := congrArg (fun Y => Y.2.2) h - refine lra.toContext_X X ⟨?_, hR ▸ preR, hO ▸ preO⟩ - rw [hL] at preL - rw [Finset.subset_empty.mp preL] - exact Finset.empty_subset _ - -lemma LocalRuleApp.toContext_rightOnly_X {lra : LocalRuleApp} {X : Sequent} - (hX : lra.X = X) (hr : lra.isRightRule) : (lra.toContext X.rightOnly).X = X.rightOnly := by - obtain ⟨preL, preR, preO⟩ := lra.preconditionProof - subst hX - refine lra.toContext_X _ ⟨?_, preR, preO⟩ - rw [(LocalRuleApp.isRightRule_shape hr).1] - exact Finset.empty_subset _ - -/-! ### When is the canonical choice available? -/ - -lemma exists_localRuleApp_of_not_basic {Y : Sequent} (h : ¬ Y.basic) : - ∃ lra : LocalRuleApp, lra.X = Y := by - by_contra hcon - exact h (basic_iff_noLocalRuleApp.mpr hcon) - -lemma uniLeftChoice_leftOnly_isSome {X : Sequent} (h : ¬ X.leftFree.basic) : - (uniLeftChoice X.leftOnly).isSome := by - obtain ⟨lra, hlra⟩ := exists_localRuleApp_of_not_basic h - have hl : lra.isLeftRule := LocalRuleApp.isLeftRule_of_X_eq hlra - obtain ⟨preL, preR, preO⟩ := lra.preconditionProof - have hL : lra.L = X.1 := congrArg (fun Y => Y.1) hlra - have hR : lra.R = ∅ := congrArg (fun Y => Y.2.1) hlra - have hO : lra.O = none := congrArg (fun Y => Y.2.2) hlra - have hOc : lra.Ocond = none := by - rw [hO] at preO - rcases hOcond : lra.Ocond with _|(a|b) <;> simp_all - refine uniLeftChoice_isSome (lra := lra.toContext X.leftOnly) ?_ (by simpa using hl) - refine lra.toContext_X X.leftOnly ⟨hL ▸ preL, ?_, by simp [hOc, Sequent.leftOnly]⟩ - rw [(LocalRuleApp.isLeftRule_shape hl).1] - exact Finset.empty_subset _ - -lemma uniLeftChoice_leftOnly_eq_none {X : Sequent} (hb : X.leftFree.basic) - (hO : ¬ X.2.2.isLeft) : uniLeftChoice X.leftOnly = none := by - rcases hc : uniLeftChoice X.leftOnly with _ | lra - · rfl - exfalso - obtain ⟨hX, hl⟩ := uniLeftChoice_spec hc - obtain ⟨hRcond, hOcond⟩ := LocalRuleApp.isLeftRule_shape hl - obtain ⟨preL, preR, preO⟩ := lra.preconditionProof - have hLL : lra.L = X.1 := congrArg (fun Y => Y.1) hX - have hOO : lra.O = X.2.2 := congrArg (fun Y => Y.2.2) hX - have hOc : lra.Ocond = none := by - rcases hOcond with h' | h' - · exact h' - · exfalso - rw [hOO] at preO - rcases hOcond' : lra.Ocond with _|(a|b) <;> rcases hX22 : X.2.2 with _|(c|d) <;> - simp_all [Olf.isLeft] - have : ∃ lra' : LocalRuleApp, lra'.X = X.leftFree := by - refine ⟨lra.toContext X.leftFree, ?_⟩ - refine lra.toContext_X X.leftFree ⟨hLL ▸ preL, ?_, by simp [hOc, Sequent.leftFree]⟩ - rw [hRcond] - exact Finset.empty_subset _ - exact (basic_iff_noLocalRuleApp.mp hb) this - -lemma uniRightChoice_rightOnly_isSome {X : Sequent} {lra : LocalRuleApp} (hX : lra.X = X) - (hr : lra.isRightRule) : (uniRightChoice X.rightOnly).isSome := - uniRightChoice_isSome (lra := lra.toContext X.rightOnly) - (lra.toContext_rightOnly_X hX hr) (by simpa using hr) - -/-! ### The canonical rule choice -/ - -open Classical in -/-- The canonical rule application for a sequent that is free or loaded on the right: -first reduce the left component, then use the canonical rule for the right component. -/ -def uniChoiceRL (X : Sequent) : Option LocalRuleApp := - match uniLeftChoice X.leftOnly with - | some lra => some (lra.toContext X) - | none => - match uniRightChoice X.rightOnly with - | some lra => some (lra.toContext X) - | none => (LocalRuleApp.all X).head? - -lemma uniChoiceRL_X {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceRL X = some lra) : - lra.X = X := by - unfold uniChoiceRL at h - rcases hl : uniLeftChoice X.leftOnly with _ | lrl - · rcases hr : uniRightChoice X.rightOnly with _ | lrr - · rw [hl, hr] at h - simp only at h - exact LocalRuleApp.all_X X lra (List.mem_of_mem_head? h) - · rw [hl, hr] at h - simp only [Option.some.injEq] at h - subst h - exact LocalRuleApp.toContext_X_of_rightOnly (uniRightChoice_spec hr).1 - · rw [hl] at h - simp only [Option.some.injEq] at h - subst h - exact LocalRuleApp.toContext_X_of_leftOnly (uniLeftChoice_spec hl).1 - -lemma uniChoiceRL_isSome {X : Sequent} (h : ¬ X.basic) : (uniChoiceRL X).isSome := by - unfold uniChoiceRL - rcases hl : uniLeftChoice X.leftOnly with _ | lrl - · rcases hr : uniRightChoice X.rightOnly with _ | lrr - · simp only [Option.isSome] - rcases hh : (LocalRuleApp.all X).head? with _ | lra - · exfalso - rw [List.head?_eq_none_iff] at hh - exact LocalRuleApp.all_nonempty_of_nonbasic h hh - · rfl - · rfl - · rfl - -lemma uniChoiceRL_isUniChoice {X : Sequent} {lra : LocalRuleApp} (hnl : ¬ X.2.2.isLeft) - (h : uniChoiceRL X = some lra) : lra.IsUniChoice := by - have hX : lra.X = X := uniChoiceRL_X h - refine ⟨?_, ?_, ?_, ?_⟩ - · -- leftFirst - intro _ h2 - have h2' : ¬ X.leftFree.basic := by rwa [hX] at h2 - obtain ⟨lrl, hl⟩ := Option.isSome_iff_exists.mp (uniLeftChoice_leftOnly_isSome h2') - unfold uniChoiceRL at h - rw [hl] at h - simp only [Option.some.injEq] at h - subst h - simpa using (uniLeftChoice_spec hl).2 - · -- rightFirst - intro h1 - exact absurd (hX ▸ h1) hnl - · -- rightCanon - intro hr _ _ - have hnleft : uniLeftChoice X.leftOnly = none := by - rcases hl : uniLeftChoice X.leftOnly with _ | lrl - · rfl - · exfalso - unfold uniChoiceRL at h - rw [hl] at h - simp only [Option.some.injEq] at h - subst h - exact LocalRuleApp.not_left_and_right _ ⟨by simpa using (uniLeftChoice_spec hl).2, hr⟩ - rcases hrr : uniRightChoice X.rightOnly with _ | lrr - · exfalso - have : (uniRightChoice X.rightOnly).isSome := uniRightChoice_rightOnly_isSome hX hr - rw [hrr] at this - exact Bool.false_ne_true this - · refine ⟨lrr, by rw [hX, hrr], ?_⟩ - unfold uniChoiceRL at h - rw [hnleft, hrr] at h - simp only [Option.some.injEq] at h - subst h - exact LocalRuleApp.toContext_sameRuleAs lrr X - · -- leftCanon - intro _ h2 - exact absurd (hX ▸ h2) hnl - -open Classical in -/-- The canonical local rule application at a sequent: when the sequent is loaded on the -left we flip, use `uniChoiceRL` and flip back. -/ -def uniChoiceAt (X : Sequent) : Option LocalRuleApp := - if X.2.2.isLeft then (uniChoiceRL X.flip).map LocalRuleApp.flip else uniChoiceRL X - -lemma uniChoiceAt_X {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) : - lra.X = X := by - unfold uniChoiceAt at h - split at h - · rw [Option.map_eq_some_iff] at h - obtain ⟨lrb, hb, rfl⟩ := h - rw [LocalRuleApp.flip_X, uniChoiceRL_X hb, Sequent.flip_flip] - · exact uniChoiceRL_X h - -lemma uniChoiceAt_isSome {X : Sequent} (h : ¬ X.basic) : (uniChoiceAt X).isSome := by - unfold uniChoiceAt - split - · simpa using uniChoiceRL_isSome (X := X.flip) (by rwa [basic_flip]) - · exact uniChoiceRL_isSome h - -lemma uniChoiceAt_isUniChoice {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) : - lra.IsUniChoice := by - unfold uniChoiceAt at h - split at h - · rename_i hleft - rw [Option.map_eq_some_iff] at h - obtain ⟨lrb, hb, rfl⟩ := h - refine LocalRuleApp.IsUniChoice.flip (uniChoiceRL_isUniChoice ?_ hb) - clear hb - rcases X with ⟨L, R, O⟩ - rcases O with _ | (a | b) <;> simp_all [Sequent.flip, Olf.flip, Olf.isLeft] - · rename_i hleft - exact uniChoiceRL_isUniChoice hleft h - -lemma uniChoiceAt_C_lt {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) - {Y : Sequent} (hY : Y ∈ lra.C) : ltSequent Y X := by - have hdec := localRuleApp.decreases_DM lra Y hY - rwa [uniChoiceAt_X h] at hdec - -open Classical in -/-- The canonical local tableau: always apply the canonical rule `uniChoiceAt`. -/ -def uniLocalTab : (X : Sequent) → LocalTableau X - | X => - if bas : X.basic then .sim bas - else - have hX : ((uniChoiceAt X).get (uniChoiceAt_isSome bas)).X = X := - uniChoiceAt_X (Option.some_get (uniChoiceAt_isSome bas)).symm - .byLocalRule ((uniChoiceAt X).get (uniChoiceAt_isSome bas)) hX.symm - (fun Y _ => uniLocalTab Y) -termination_by X => X -decreasing_by - exact uniChoiceAt_C_lt (Option.some_get _).symm (by assumption) - -lemma uniLocalTab_isUni (X : Sequent) : (uniLocalTab X).IsUni := by - rw [uniLocalTab] - split - · rw [LocalTableau.IsUni]; trivial - · rename_i bas - rw [LocalTableau.IsUni] - refine ⟨uniChoiceAt_isUniChoice (Option.some_get (uniChoiceAt_isSome bas)).symm, ?_⟩ - intro Y hY - exact uniLocalTab_isUni Y -termination_by X -decreasing_by - exact uniChoiceAt_C_lt (Option.some_get _).symm (by assumption) - /-! ## Refutable sequents To show that the local development of a sequent does not depend on the order in which the @@ -1495,7 +690,7 @@ because that file imports this one. -/ /-- The right component of a basic sequent is basic. Same as `Sequent.basic_rightOnly` in `Pdl.ClusterInterpolation`. -/ -lemma basic_rightOnly {X : Sequent} (h : X.basic) : X.rightOnly.basic := by +private lemma basic_rightOnly_impl {X : Sequent} (h : X.basic) : X.rightOnly.basic := by rcases X with ⟨L, R, O⟩ obtain ⟨hb, hc⟩ := h constructor @@ -1517,6 +712,26 @@ lemma basic_rightOnly {X : Sequent} (h : X.basic) : X.rightOnly.basic := by Finset.notMem_empty, false_or] at hf hnf ⊢ <;> tauto +-- Keep the established auxiliary signatures independent of the imported simp cache. +section +universe u_1 + +private theorem basic_rightOnly._simp_1_2 {α : Type u_1} [inst : DecidableEq α] + {s t : Finset α} {a : α} : (a ∈ s ∪ t) = (a ∈ s ∨ a ∈ t) := + propext Finset.mem_union + +private theorem basic_rightOnly._simp_1_3 {φ : Formula} {X : Sequent} : + (φ ∈ X) = (φ ∈ X.L ∨ φ ∈ X.R) := propext Sequent.mem_def + +private theorem basic_rightOnly._simp_1_4 {α : Type u_1} (a : α) : + (a ∈ (∅ : Finset α)) = False := eq_false (Finset.notMem_empty a) + +end + +/-- A basic sequent has a basic right component, including its optional loading. -/ +lemma basic_rightOnly {X : Sequent} (h : X.basic) : X.rightOnly.basic := by + exact basic_rightOnly_impl h + /-- A right local rule cannot be applied when the right component of the sequent is basic. Same as `LocalRuleApp.not_rightOnly_basic_of_isRightRule` in `Pdl.ClusterInterpolation`. -/ lemma not_rightOnly_basic_of_isRightRule (lra : LocalRuleApp) @@ -1851,3 +1066,8 @@ theorem LoadedCluster.uniformOfUniTab {tab : Tableau .nil X} rw [Finset.image_image]; rfl end PDL + +run_cmd do + let source := `LeanPool.PDL.Interpolation.UniformityCore + let target := `LeanPool.PDL.Interpolation.Uniformity + Lean.Elab.Command.liftCoreM (PDL.ImportCompatibility.retainPrivateDeclarations source target) diff --git a/LeanPool/PDL/Interpolation/UniformityCore.lean b/LeanPool/PDL/Interpolation/UniformityCore.lean new file mode 100644 index 0000000000..900cd98aeb --- /dev/null +++ b/LeanPool/PDL/Interpolation/UniformityCore.lean @@ -0,0 +1,830 @@ +/- +Copyright (c) 2023 PDL formalization contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: PDL formalization contributors (see project card) +-/ + +module + +public import LeanPool.PDL.Local.AllLocalTab +public import LeanPool.PDL.Interpolation.FinePath +public import LeanPool.PDL.FlipCore + +import Mathlib.Tactic.Bound.Init -- shake: keep + +/-! # Canonical uniform local tableaux -/ + +@[expose] public section + +namespace PDL + +/-! ## The components of a sequent -/ + +/-- The left component of a sequent, together with the loaded formula, again as a sequent. +This is `Λ₁` from the paper; compare `Sequent.rightOnly`, which is `Λ₂`. -/ +def Sequent.leftOnly (X : Sequent) : Sequent := ⟨X.1, ∅, X.2.2⟩ + +/-- The left component of a sequent, without any loaded formula. When the loaded formula +is on the right, i.e. in the situation of a `LoadedCluster`, this is the *unloaded* +component `Λ₁` of the node, and `Sequent.leftFree X |>.basic` says that no local rule is +applicable to it. -/ +def Sequent.leftFree (X : Sequent) : Sequent := ⟨X.1, ∅, none⟩ + +/-- The right component of a sequent, without any loaded formula. When the loaded formula +is on the left this is the *unloaded* component `Λ₂` of the node. -/ +def Sequent.rightFree (X : Sequent) : Sequent := ⟨∅, X.2.1, none⟩ + +/-- Two local rule applications use the same rule with the same principal formulas. +The fields `Lcond`, `Rcond` and `Ocond` are the principal formulas and `ress` is the list +of results of the rule, so this says that the *same rule instance* is applied at two nodes, +which may still have different sequents. -/ +def LocalRuleApp.SameRuleAs (lra₁ lra₂ : LocalRuleApp) : Prop := + lra₁.Lcond = lra₂.Lcond ∧ lra₁.Rcond = lra₂.Rcond ∧ lra₁.Ocond = lra₂.Ocond + ∧ lra₁.ress = lra₂.ress ∧ HEq lra₁.lr lra₂.lr + +/-! ## Uniformity -/ + +/-- Condition U1: at a node with a loaded component, a rule is applied to the *unloaded* +component unless the latter is basic. Since every rule is a left rule or a right rule but +not both (`FinePathIn.not_left_and_right`), we state this as: a rule on the unloaded side +is applied. + +The condition is only about nodes at which a rule is applied at all, i.e. we exclude the +leaves given by a loaded-path repeat, which is what `¬ f.base.isLrep` says. Note that this +exclusion is needed: at a loaded-path repeat the tableau stops, so no rule at all — and in +particular no rule on the unloaded component — is applied there, while the sequent of a +loaded-path repeat may well have a non-basic unloaded component. (For example, the sequent +reached again after a loop may contain a conjunction on the unloaded side; the tableau is +then forced to stop, because `Tableau.loc` and `Tableau.pdl` both require `¬ flprep`.) +Without the exclusion no tableau with such a repeat would be uniform, and `Tableau.toUniform` +would fail. -/ +def Tableau.U1 {H : History} {X : Sequent} (tab : Tableau H X) : Prop := + ∀ f : FinePathIn tab, ¬ f.base.isLrep → + (f.label.2.2.isRight → ¬ f.label.leftFree.basic → f.usesLeftRule) + ∧ (f.label.2.2.isLeft → ¬ f.label.rightFree.basic → f.usesRightRule) + +/-- Condition U2: two nodes whose loaded component is the same and not basic, and whose +unloaded components are both basic, apply the same rule to the same formula of the loaded +component. As the loaded component is not basic the rule must be a local one, so we may +state this for the local rule applications `f.lraOpt` and `g.lraOpt`. -/ +def Tableau.U2 {H : History} {X : Sequent} (tab : Tableau H X) : Prop := + ∀ (f g : FinePathIn tab) (lraf lrag : LocalRuleApp), + f.lraOpt = some lraf → g.lraOpt = some lrag → + ( (f.label.2.2.isRight → f.label.rightOnly = g.label.rightOnly → + ¬ f.label.rightOnly.basic → f.label.leftFree.basic → g.label.leftFree.basic → + lraf.isRightRule → lrag.isRightRule → lraf.SameRuleAs lrag) + ∧ (f.label.2.2.isLeft → f.label.leftOnly = g.label.leftOnly → + ¬ f.label.leftOnly.basic → f.label.rightFree.basic → g.label.rightFree.basic → + lraf.isLeftRule → lrag.isLeftRule → lraf.SameRuleAs lrag) ) + +/-- The conditions U1 and U2 together. -/ +def Tableau.UniCore {H : History} {X : Sequent} (tab : Tableau H X) : Prop := + tab.U1 ∧ tab.U2 + +/-- A sanity check that U1 and U2 are not contradictory: both conditions only constrain +nodes with a loaded component, so a tableau in which no node is loaded satisfies them. -/ +lemma Tableau.uniCore_of_all_free {H : History} {X : Sequent} {tab : Tableau H X} + (h : ∀ f : FinePathIn tab, f.label.2.2 = none) : tab.UniCore := by + refine ⟨fun f _ => ⟨?_, ?_⟩, fun f g lraf lrag _ _ => ⟨?_, ?_⟩⟩ <;> + intro hf <;> rw [h f] at hf <;> simp [Olf.isRight, Olf.isLeft] at hf + +/-- A tableau is *uniform* if it satisfies the conditions U1 and U2. + +We also demand U1 and U2 for the flipped tableau `tab.flip`, in which the left and the +right components of all sequents are swapped. This is not an extra demand: U1 and U2 are +symmetric in the two components, so `tab.UniCore` and `tab.flip.UniCore` say the same +thing. Asking for both here only spares us the purely technical work of transporting U1 +and U2 along `Tableau.flip`, which would need a `flip` operation on `FinePathIn`. +What it buys us is `Tableau.isUniform.flip` below, which is needed because the +interpolation proof flips the tableau when the loaded formula is on the left. -/ +def Tableau.isUniform {H : History} {X : Sequent} (tab : Tableau H X) : Prop := + tab.UniCore ∧ tab.flip.UniCore + +/-- Transporting `Tableau.UniCore` along an equality of tableaux. -/ +lemma Tableau.UniCore.heq_transfer {H₁ X₁ H₂ X₂} {t₁ : Tableau H₁ X₁} {t₂ : Tableau H₂ X₂} + (hH : H₁ = H₂) (hX : X₁ = X₂) (h : HEq t₁ t₂) (h₁ : t₁.UniCore) : t₂.UniCore := by + subst hH + subst hX + cases eq_of_heq h + exact h₁ + +/-- Uniformity is preserved by flipping the tableau. -/ +lemma Tableau.isUniform.flip {H : History} {X : Sequent} {tab : Tableau H X} + (h : tab.isUniform) : tab.flip.isUniform := + ⟨h.2, Tableau.UniCore.heq_transfer Hist_flip.symm Sequent.flip_flip.symm + (HEq.symm (flip_aux_Tableau_flip_flip_heq tab)) h.1⟩ + +/-! ## Uniform tableaux by construction + +To obtain uniform tableaux we follow approach (B): instead of repairing a given tableau we +describe how a uniform one is built, by fixing *which* local rule is applied at each node. +The conditions U1 and U2 only speak about the local rules applied at the nodes, and both are +conditions that can be read off a single rule application together with the sequent it is +applied to. This is what `LocalRuleApp.IsUniChoice` below says: + +* the rule is applied to the unloaded component, unless that component is basic (U1); and +* if it is applied to the loaded component (the unloaded one then being basic) then it is + *the* canonical rule for that component, given by `uniRightChoice` resp. `uniLeftChoice`. + +Since the canonical rule only depends on the loaded component `Λᵢ(s)`, any two nodes with +the same loaded component use the same rule, which is U2. A tableau all of whose rule +applications are `IsUniChoice` is called `Tableau.IsUni`, and `Tableau.IsUni.uniCore` shows +that such a tableau indeed satisfies U1 and U2. The construction is symmetric under flipping +(`Tableau.IsUni.flip`), which gives the second half of `Tableau.isUniform`. -/ + +/-! ### Flipping components, rules and rule applications -/ + +@[simp] +lemma LocalRuleApp.flip_O (lra : LocalRuleApp) : (lra.flip).O = lra.O.flip := by + rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩; rfl + +lemma LocalRuleApp.flip_X (lra : LocalRuleApp) : (lra.flip).X = lra.X.flip := by + rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ + simp [LocalRuleApp.flip, Sequent.flip] + +@[simp] +lemma LocalRuleApp.flip_isRightRule (lra : LocalRuleApp) : + (lra.flip).isRightRule = lra.isLeftRule := by + rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ + cases lr <;> simp [LocalRuleApp.flip, LocalRuleApp.isRightRule, LocalRuleApp.isLeftRule, + LocalRule.isRightRule, LocalRule.isLeftRule, LocalRule.flip] + +@[simp] +lemma LocalRuleApp.flip_isLeftRule (lra : LocalRuleApp) : + (lra.flip).isLeftRule = lra.isRightRule := by + rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ + cases lr <;> simp [LocalRuleApp.flip, LocalRuleApp.isRightRule, LocalRuleApp.isLeftRule, + LocalRule.isRightRule, LocalRule.isLeftRule, LocalRule.flip] + +@[simp] +lemma Sequent.flip_leftFree {X : Sequent} : X.flip.leftFree = X.rightFree.flip := by + rcases X with ⟨L, R, O⟩; rfl + +@[simp] +lemma Sequent.flip_rightFree {X : Sequent} : X.flip.rightFree = X.leftFree.flip := by + rcases X with ⟨L, R, O⟩; rfl + +@[simp] +lemma Sequent.flip_rightOnly {X : Sequent} : X.flip.rightOnly = X.leftOnly.flip := by + rcases X with ⟨L, R, O⟩; simp [Sequent.flip, Sequent.rightOnly, Sequent.leftOnly] + +@[simp] +lemma Sequent.flip_leftOnly {X : Sequent} : X.flip.leftOnly = X.rightOnly.flip := by + rcases X with ⟨L, R, O⟩; simp [Sequent.flip, Sequent.rightOnly, Sequent.leftOnly] + +/-- Being the same rule is preserved by flipping. -/ +lemma LocalRuleApp.SameRuleAs.flip {lra₁ lra₂ : LocalRuleApp} (h : lra₁.SameRuleAs lra₂) : + lra₁.flip.SameRuleAs lra₂.flip := by + obtain ⟨hL, hR, hO, hress, hlr⟩ := h + rcases lra₁ with ⟨L₁, R₁, O₁, Lcond₁, Rcond₁, Ocond₁, ress₁, lr₁, C₁, hC₁, pre₁⟩ + rcases lra₂ with ⟨L₂, R₂, O₂, Lcond₂, Rcond₂, Ocond₂, ress₂, lr₂, C₂, hC₂, pre₂⟩ + simp_all only + subst hL; subst hR; subst hO; subst hress + cases eq_of_heq hlr + exact ⟨rfl, rfl, rfl, rfl, HEq.rfl⟩ + +/-- Being the same rule is reflexive. -/ +lemma LocalRuleApp.SameRuleAs.refl (lra : LocalRuleApp) : lra.SameRuleAs lra := + ⟨rfl, rfl, rfl, rfl, HEq.rfl⟩ + +/-- Being the same rule is symmetric. -/ +lemma LocalRuleApp.SameRuleAs.symm {lra₁ lra₂ : LocalRuleApp} (h : lra₁.SameRuleAs lra₂) : + lra₂.SameRuleAs lra₁ := + ⟨h.1.symm, h.2.1.symm, h.2.2.1.symm, h.2.2.2.1.symm, h.2.2.2.2.symm⟩ + +/-- Being the same rule is transitive. -/ +lemma LocalRuleApp.SameRuleAs.trans {lra₁ lra₂ lra₃ : LocalRuleApp} + (h : lra₁.SameRuleAs lra₂) (h' : lra₂.SameRuleAs lra₃) : lra₁.SameRuleAs lra₃ := + ⟨h.1.trans h'.1, h.2.1.trans h'.2.1, h.2.2.1.trans h'.2.2.1, + h.2.2.2.1.trans h'.2.2.2.1, h.2.2.2.2.trans h'.2.2.2.2⟩ + +/-! ### The canonical rule for a component -/ + +/-- The canonical local rule to be applied to the right component of a sequent. +We use the first right rule in the list `LocalRuleApp.all` of all applicable rules. +Which rule exactly is picked does not matter for uniformity; all that matters is that +this is a *function* of the sequent — and that it is applied to sequents of the form +`X.rightOnly`, so that it only depends on the right component. -/ +def uniRightChoice (Y : Sequent) : Option LocalRuleApp := + (LocalRuleApp.all Y).find? (fun lra => lra.isRightRule) + +/-- The canonical local rule to be applied to the left component of a sequent. +Defined as the flip of `uniRightChoice`, which makes the whole construction symmetric. -/ +def uniLeftChoice (Y : Sequent) : Option LocalRuleApp := + (uniRightChoice Y.flip).map LocalRuleApp.flip + +lemma uniLeftChoice_flip (Y : Sequent) : + uniLeftChoice Y.flip = (uniRightChoice Y).map LocalRuleApp.flip := by + simp [uniLeftChoice] + +lemma uniRightChoice_flip (Y : Sequent) : + uniRightChoice Y.flip = (uniLeftChoice Y).map LocalRuleApp.flip := by + simp [uniLeftChoice, Option.map_map, Function.comp_def, LocalRuleApp.flip_flip] + +/-! ### Uniform rule applications -/ + +/-- The conditions on a single local rule application in a uniform tableau: the first two +fields are the local form of U1 and the last two are the local form of U2. -/ +structure LocalRuleApp.IsUniChoice (lra : LocalRuleApp) : Prop where + /-- If loaded on the right and the left component is not basic, a left rule is applied. -/ + leftFirst : lra.X.2.2.isRight → ¬ lra.X.leftFree.basic → lra.isLeftRule + /-- If loaded on the left and the right component is not basic, a right rule is applied. -/ + rightFirst : lra.X.2.2.isLeft → ¬ lra.X.rightFree.basic → lra.isRightRule + /-- A right rule applied at a node loaded on the right whose left component is basic is + the canonical rule for the right component. -/ + rightCanon : lra.isRightRule → lra.X.2.2.isRight → lra.X.leftFree.basic → + ∃ lrb, uniRightChoice lra.X.rightOnly = some lrb ∧ lra.SameRuleAs lrb + /-- A left rule applied at a node loaded on the left whose right component is basic is + the canonical rule for the left component. -/ + leftCanon : lra.isLeftRule → lra.X.2.2.isLeft → lra.X.rightFree.basic → + ∃ lrb, uniLeftChoice lra.X.leftOnly = some lrb ∧ lra.SameRuleAs lrb + +/-- The conditions on rule applications are symmetric under flipping. -/ +lemma LocalRuleApp.IsUniChoice.flip {lra : LocalRuleApp} (h : lra.IsUniChoice) : + lra.flip.IsUniChoice := by + have hXf : lra.flip.X = lra.X.flip := LocalRuleApp.flip_X lra + refine ⟨?_, ?_, ?_, ?_⟩ + · intro h1 h2 + have h1' : lra.X.2.2.isLeft := by + rw [hXf] at h1; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] + have h2' : ¬ lra.X.rightFree.basic := by + rw [hXf] at h2; simpa using h2 + simpa using h.rightFirst h1' h2' + · intro h1 h2 + have h1' : lra.X.2.2.isRight := by + rw [hXf] at h1; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] + have h2' : ¬ lra.X.leftFree.basic := by + rw [hXf] at h2; simpa using h2 + simpa using h.leftFirst h1' h2' + · intro h1 h2 h3 + have h1' : lra.isLeftRule := by simpa using h1 + have h2' : lra.X.2.2.isLeft := by + rw [hXf] at h2; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] + have h3' : lra.X.rightFree.basic := by + rw [hXf] at h3; simpa using h3 + obtain ⟨lrb, hb, hsame⟩ := h.leftCanon h1' h2' h3' + refine ⟨lrb.flip, ?_, hsame.flip⟩ + rw [hXf, Sequent.flip_rightOnly, uniRightChoice_flip, hb] + rfl + · intro h1 h2 h3 + have h1' : lra.isRightRule := by simpa using h1 + have h2' : lra.X.2.2.isRight := by + rw [hXf] at h2; rcases hO : lra.O with _|(a|b) <;> simp_all [Olf.flip, Sequent.flip] + have h3' : lra.X.leftFree.basic := by + rw [hXf] at h3; simpa using h3 + obtain ⟨lrb, hb, hsame⟩ := h.rightCanon h1' h2' h3' + refine ⟨lrb.flip, ?_, hsame.flip⟩ + rw [hXf, Sequent.flip_leftOnly, uniLeftChoice_flip, hb] + rfl + +/-! ### Basic sequents have basic components -/ + +lemma Sequent.leftFree_basic_of_basic {X : Sequent} (h : X.basic) : X.leftFree.basic := by + rcases X with ⟨L, R, o⟩ + rcases h with ⟨hall, hcl⟩ + refine ⟨fun f hf => hall f ?_, ?_⟩ + · simp only [Sequent.leftFree, Sequent.toFinset, Finset.union_empty, Finset.union_assoc, + Finset.mem_union] at hf ⊢ + tauto + · rintro (hbot | ⟨f, hf, hnf⟩) + · exact hcl (Or.inl (by simp_all [Sequent.leftFree, Sequent.mem_def])) + · exact hcl (Or.inr ⟨f, by simp_all [Sequent.leftFree, Sequent.mem_def]⟩) + +lemma Sequent.rightFree_basic_of_basic {X : Sequent} (h : X.basic) : X.rightFree.basic := by + rcases X with ⟨L, R, o⟩ + rcases h with ⟨hall, hcl⟩ + refine ⟨fun f hf => hall f ?_, ?_⟩ + · simp only [Sequent.rightFree, Sequent.toFinset, Finset.empty_union, Finset.union_assoc, + Finset.mem_union] at hf ⊢ + tauto + · rintro (hbot | ⟨f, hf, hnf⟩) + · exact hcl (Or.inl (by simp_all [Sequent.rightFree, Sequent.mem_def])) + · exact hcl (Or.inr ⟨f, by simp_all [Sequent.rightFree, Sequent.mem_def]⟩) + +/-- All local rule applications inside a local tableau are uniform choices. -/ +def LocalTableau.IsUni : {X : Sequent} → LocalTableau X → Prop + | _, (.sim _) => True + | _, (.byLocalRule lra _ next) => + lra.IsUniChoice ∧ ∀ Y, ∀ h : Y ∈ lra.C, (next Y h).IsUni + +/-- All local rule applications inside a tableau are uniform choices. -/ +def Tableau.IsUni : {H : History} → {X : Sequent} → Tableau H X → Prop + | _, _, .loc _ _ lt next => lt.IsUni ∧ ∀ Y, ∀ h : Y ∈ endNodesOf lt, (next Y h).IsUni + | _, _, .pdl _ _ _ next => next.IsUni + | _, _, .lrep _ => True + +lemma LocalTableau.IsUni.ltAt {X} {lt : LocalTableau X} (h : lt.IsUni) (lp : LocalPathIn lt) : + (lp.ltAt).IsUni := by + induction lp + case nil => exact h + case cons X lra X_def next Y Y_in tail IH => + rw [LocalTableau.IsUni] at h + exact IH (h.2 Y Y_in) + +lemma Tableau.IsUni.lraOpt_isUniChoice {H X} {tab : Tableau H X} (h : tab.IsUni) + {f : FinePathIn tab} {lra : LocalRuleApp} (hf : f.lraOpt = some lra) : lra.IsUniChoice := by + induction f + case inLoc Hist X nrep nbas lt next lp lp_int => + rw [Tableau.IsUni] at h + have hlt := h.1.ltAt lp + simp only [FinePathIn.lraOpt] at hf + rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas + · rw [hltAt] at hf hlt + simp only [Option.some.injEq] at hf + subst hf + rw [LocalTableau.IsUni] at hlt + exact hlt.1 + · rw [hltAt] at hf; simp at hf + case pdlHere => simp [FinePathIn.lraOpt] at hf + case lrepHere => simp [FinePathIn.lraOpt] at hf + case loc Hist X nrep nbas lt next Y Y_in tail IH => + rw [Tableau.IsUni] at h + exact IH (h.2 Y Y_in) hf + case pdl IH => + rw [Tableau.IsUni] at h + exact IH h hf + +lemma FinePathIn.usesLeftRule_eq_of_lraOpt {H X} {tab : Tableau H X} {f : FinePathIn tab} + {lra : LocalRuleApp} (hf : f.lraOpt = some lra) : f.usesLeftRule = lra.isLeftRule := by + induction f + case inLoc lp lp_int => + simp only [FinePathIn.lraOpt, FinePathIn.usesLeftRule] at * + rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas <;> simp_all + case pdlHere => simp [FinePathIn.lraOpt] at hf + case lrepHere => simp [FinePathIn.lraOpt] at hf + case loc IH => simpa [FinePathIn.usesLeftRule] using IH (by simpa [FinePathIn.lraOpt] using hf) + case pdl IH => simpa [FinePathIn.usesLeftRule] using IH (by simpa [FinePathIn.lraOpt] using hf) + +lemma FinePathIn.usesRightRule_eq_of_lraOpt {H X} {tab : Tableau H X} {f : FinePathIn tab} + {lra : LocalRuleApp} (hf : f.lraOpt = some lra) : f.usesRightRule = lra.isRightRule := by + induction f + case inLoc lp lp_int => + simp only [FinePathIn.lraOpt, FinePathIn.usesRightRule] at * + rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas <;> simp_all + case pdlHere => simp [FinePathIn.lraOpt] at hf + case lrepHere => simp [FinePathIn.lraOpt] at hf + case loc IH => simpa [FinePathIn.usesRightRule] using IH (by simpa [FinePathIn.lraOpt] using hf) + case pdl IH => simpa [FinePathIn.usesRightRule] using IH (by simpa [FinePathIn.lraOpt] using hf) + +lemma FinePathIn.isLrep_or_basic_of_lraOpt_eq_none {H X} {tab : Tableau H X} {f : FinePathIn tab} + (hf : f.lraOpt = none) : f.base.isLrep ∨ f.label.basic := by + induction f + case inLoc lp lp_int => + exfalso + simp only [FinePathIn.lraOpt] at hf + rcases hltAt : lp.ltAt with ⟨lra', X_def, lnext⟩ | bas + · rw [hltAt] at hf; simp at hf + · exact absurd lp_int (by simp [LocalPathIn.isInternal, hltAt, LocalTableau.hasRule]) + case pdlHere Hist X Y nrep bas r next => exact Or.inr bas + case lrepHere => exact Or.inl (by simp [FinePathIn.base, PathIn.isLrep, tabAt, Tableau.isLrep]) + case loc IH => + rcases IH (by simpa [FinePathIn.lraOpt] using hf) with h | h + · exact Or.inl (by simpa [FinePathIn.base, PathIn.isLrep, tabAt] using h) + · exact Or.inr (by simpa [FinePathIn.label] using h) + case pdl IH => + rcases IH (by simpa [FinePathIn.lraOpt] using hf) with h | h + · exact Or.inl (by simpa [FinePathIn.base, PathIn.isLrep, tabAt] using h) + · exact Or.inr (by simpa [FinePathIn.label] using h) + +theorem Tableau.IsUni.uniCore {H X} {tab : Tableau H X} (h : tab.IsUni) : tab.UniCore := by + constructor + · -- U1 + intro f hnlrep + rcases hl : f.lraOpt with _ | lra + · rcases FinePathIn.isLrep_or_basic_of_lraOpt_eq_none hl with hb | hbas + · exact absurd hb hnlrep + · exact ⟨fun _ hcon => absurd (Sequent.leftFree_basic_of_basic hbas) hcon, + fun _ hcon => absurd (Sequent.rightFree_basic_of_basic hbas) hcon⟩ + · have hu := h.lraOpt_isUniChoice hl + have hX : f.label = lra.X := (f.lraOpt_spec hl).1 + constructor + · intro h1 h2 + rw [FinePathIn.usesLeftRule_eq_of_lraOpt hl] + exact hu.leftFirst (hX ▸ h1) (hX ▸ h2) + · intro h1 h2 + rw [FinePathIn.usesRightRule_eq_of_lraOpt hl] + exact hu.rightFirst (hX ▸ h1) (hX ▸ h2) + · -- U2 + intro f g lraf lrag hf hg + have huf := h.lraOpt_isUniChoice hf + have hug := h.lraOpt_isUniChoice hg + have hXf : f.label = lraf.X := (f.lraOpt_spec hf).1 + have hXg : g.label = lrag.X := (g.lraOpt_spec hg).1 + constructor + · intro hfR hfg _ hfl hgl hfRule hgRule + have hOeq : f.label.2.2 = g.label.2.2 := congrArg (fun Y => Y.2.2) hfg + have hgR : g.label.2.2.isRight := hOeq ▸ hfR + obtain ⟨lrb, hb, hsame⟩ := huf.rightCanon hfRule (hXf ▸ hfR) (hXf ▸ hfl) + obtain ⟨lrb', hb', hsame'⟩ := hug.rightCanon hgRule (hXg ▸ hgR) (hXg ▸ hgl) + have : lrb = lrb' := by + rw [← hXf, hfg] at hb + rw [← hXg] at hb' + exact Option.some.inj (hb.symm.trans hb') + exact hsame.trans (this ▸ hsame'.symm) + · intro hfL hfg _ hfr hgr hfRule hgRule + have hOeq : f.label.2.2 = g.label.2.2 := congrArg (fun Y => Y.2.2) hfg + have hgL : g.label.2.2.isLeft := hOeq ▸ hfL + obtain ⟨lrb, hb, hsame⟩ := huf.leftCanon hfRule (hXf ▸ hfL) (hXf ▸ hfr) + obtain ⟨lrb', hb', hsame'⟩ := hug.leftCanon hgRule (hXg ▸ hgL) (hXg ▸ hgr) + have : lrb = lrb' := by + rw [← hXf, hfg] at hb + rw [← hXg] at hb' + exact Option.some.inj (hb.symm.trans hb') + exact hsame.trans (this ▸ hsame'.symm) + +lemma LocalTableau.IsUni_cast {A B : Sequent} (h : A = B) (t : LocalTableau A) : + (h ▸ t).IsUni ↔ t.IsUni := by subst h; rfl + +lemma Tableau.IsUni_cast {H} {A B : Sequent} (h : A = B) (t : Tableau H A) : + (h ▸ t).IsUni ↔ t.IsUni := by subst h; rfl + +lemma LocalTableau.IsUni.flip {X} {lt : LocalTableau X} (h : lt.IsUni) : (lt.flip).IsUni := by + induction lt + case byLocalRule X lra X_def next IH => + rw [LocalTableau.IsUni] at h + rw [LocalTableau.flip, LocalTableau.IsUni] + refine ⟨h.1.flip, ?_⟩ + intro Y Y_in + rw [LocalTableau.IsUni_cast] + exact IH _ (Sequent.flip_mem_of_mem_image_flip Y_in) (h.2 _ _) + case sim bas => rw [LocalTableau.flip, LocalTableau.IsUni]; trivial + +lemma Tableau.IsUni.flip {H X} {tab : Tableau H X} (h : tab.IsUni) : (tab.flip).IsUni := by + induction tab + case loc Hist X nrep nbas lt next IH => + rw [Tableau.IsUni] at h + rw [Tableau.flip, Tableau.IsUni] + refine ⟨h.1.flip, ?_⟩ + intro Y Y_in + rw [Tableau.IsUni_cast] + exact IH _ (endNodesOf_flip Y_in) (h.2 _ _) + case pdl IH => + rw [Tableau.IsUni] at h + rw [Tableau.flip, Tableau.IsUni] + exact IH h + case lrep => trivial + +/-- A tableau all of whose local rule applications are uniform choices is uniform. -/ +theorem Tableau.IsUni.isUniform {X} {tab : Tableau .nil X} (h : tab.IsUni) : tab.isUniform := + ⟨h.uniCore, h.flip.uniCore⟩ + +/-! ## Building a uniform tableau + +We now show `Tableau.exists_isUni`: for every tableau there is one that applies the rules in +the canonical order. The construction is deterministic: `uniChoiceAt` picks, at each sequent, +the canonical rule application (first a rule for the unloaded component, and once that is +basic the canonical rule for the loaded component), and `uniLocalTab` iterates this to a +local tableau all of whose rule applications are uniform choices (`uniLocalTab_isUni`). + +Given an arbitrary tableau we then re-build it, replacing the local tableau at each `loc` +step by the canonical one. Because the end nodes of the canonical local tableau need not be +literally the same lists as the end nodes of the original one, we prove the statement in the +more flexible form `Tableau.exists_isUni_of_msEq`, allowing the sequent and the history to +change up to `Sequent.multisetEqTo`, i.e. up to permutation of the two lists in a sequent. +That the calculus does not care about such permutations is `PdlRule.exists_of_multisetEqTo` +and `lpr_of_multisetEqTo`. + +The only step that is left open is `uniLocalTab_endNode_dominated`. -/ + +/-- Put a local rule application into a different context, keeping the rule itself. -/ +def LocalRuleApp.inContext (lra : LocalRuleApp) (L R : Finset Formula) (O : Olf) + (hL : lra.Lcond ⊆ L) (hR : lra.Rcond ⊆ R) (hO : lra.Ocond ⊆ O) : + LocalRuleApp := + { L := L, R := R, O := O, + Lcond := lra.Lcond, Rcond := lra.Rcond, Ocond := lra.Ocond, + ress := lra.ress, lr := lra.lr, + C := applyLocalRule lra.lr (L, R, O), hC := rfl, + preconditionProof := ⟨hL, hR, hO⟩ } + +/-- Put a local rule application into the context of the sequent `X`, if possible. -/ +def LocalRuleApp.toContext (lra : LocalRuleApp) (X : Sequent) : LocalRuleApp := + if h : lra.Lcond ⊆ X.1 ∧ lra.Rcond ⊆ X.2.1 ∧ lra.Ocond ⊆ X.2.2 then + lra.inContext X.1 X.2.1 X.2.2 h.1 h.2.1 h.2.2 + else lra + +lemma LocalRuleApp.toContext_sameRuleAs (lra : LocalRuleApp) (X : Sequent) : + (lra.toContext X).SameRuleAs lra := by + unfold LocalRuleApp.toContext + split + · exact ⟨rfl, rfl, rfl, rfl, HEq.rfl⟩ + · exact LocalRuleApp.SameRuleAs.refl lra + +@[simp] +lemma LocalRuleApp.toContext_isLeftRule (lra : LocalRuleApp) (X : Sequent) : + (lra.toContext X).isLeftRule = lra.isLeftRule := by + unfold LocalRuleApp.toContext + split <;> rfl + +@[simp] +lemma LocalRuleApp.toContext_isRightRule (lra : LocalRuleApp) (X : Sequent) : + (lra.toContext X).isRightRule = lra.isRightRule := by + unfold LocalRuleApp.toContext + split <;> rfl + +lemma LocalRuleApp.toContext_X (lra : LocalRuleApp) (X : Sequent) + (h : lra.Lcond ⊆ X.1 ∧ lra.Rcond ⊆ X.2.1 ∧ lra.Ocond ⊆ X.2.2) : + (lra.toContext X).X = X := by + unfold LocalRuleApp.toContext + rw [dite_eq_left h] + rfl + +lemma uniRightChoice_spec {Y : Sequent} {lra : LocalRuleApp} (h : uniRightChoice Y = some lra) : + lra.X = Y ∧ lra.isRightRule := by + unfold uniRightChoice at h + exact ⟨LocalRuleApp.all_X Y lra (List.mem_of_find?_eq_some h), by + simpa using List.find?_some h⟩ + +lemma uniRightChoice_isSome {Y : Sequent} {lra : LocalRuleApp} (hX : lra.X = Y) + (hr : lra.isRightRule) : (uniRightChoice Y).isSome := by + unfold uniRightChoice + rcases h : (LocalRuleApp.all Y).find? (fun lra => lra.isRightRule) with _ | lrb + · exfalso + rw [List.find?_eq_none] at h + exact h lra (hX ▸ lra.all_spec) (by simpa using hr) + · rw [h]; rfl + +lemma uniLeftChoice_spec {Y : Sequent} {lra : LocalRuleApp} (h : uniLeftChoice Y = some lra) : + lra.X = Y ∧ lra.isLeftRule := by + unfold uniLeftChoice at h + rw [Option.map_eq_some_iff] at h + obtain ⟨lrb, hb, rfl⟩ := h + obtain ⟨hX, hr⟩ := uniRightChoice_spec hb + refine ⟨?_, by simpa using hr⟩ + rw [LocalRuleApp.flip_X, hX, Sequent.flip_flip] + +lemma uniLeftChoice_isSome {Y : Sequent} {lra : LocalRuleApp} (hX : lra.X = Y) + (hl : lra.isLeftRule) : (uniLeftChoice Y).isSome := by + unfold uniLeftChoice + have : (uniRightChoice Y.flip).isSome := by + refine uniRightChoice_isSome (lra := lra.flip) ?_ (by simpa using hl) + rw [LocalRuleApp.flip_X, hX] + simpa using this + +/-! ### Shapes of left and right rules -/ + +lemma LocalRuleApp.isLeftRule_shape {lra : LocalRuleApp} (h : lra.isLeftRule) : + lra.Rcond = ∅ ∧ (lra.Ocond = none ∨ lra.Ocond.isLeft) := by + rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ + cases lr <;> + simp_all [LocalRuleApp.isLeftRule, LocalRule.isLeftRule, Olf.isLeft] + +lemma LocalRuleApp.isRightRule_shape {lra : LocalRuleApp} (h : lra.isRightRule) : + lra.Lcond = ∅ ∧ (lra.Ocond = none ∨ lra.Ocond.isRight) := by + rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ + cases lr <;> + simp_all [LocalRuleApp.isRightRule, LocalRule.isRightRule, Olf.isRight] + +/-- Any local rule applicable to a sequent of the shape `(L, ∅, none)` is a left rule. -/ +lemma LocalRuleApp.isLeftRule_of_X_eq {lra : LocalRuleApp} {L : Finset Formula} + (h : lra.X = (L, ∅, none)) : lra.isLeftRule := by + rcases lra with ⟨L', R', O', Lcond, Rcond, Ocond, ress, lr, C, hC, pre⟩ + simp only [LocalRuleApp.X] at h + obtain ⟨rfl, rfl, rfl⟩ := h + obtain ⟨preL, preR, preO⟩ := pre + cases lr + case oneSidedL => simp [LocalRuleApp.isLeftRule, LocalRule.isLeftRule] + case oneSidedR orule YS_def => + exact absurd (Finset.subset_empty.mp preR) (orule.precond_ne_nil) + case LRnegL φ => simp at preR + case LRnegR φ => simp at preR + case loadedL => simp at preO + case loadedR => simp at preO + +/-! ### Moving rules between a sequent and its components -/ + +lemma LocalRuleApp.toContext_X_of_leftOnly {lra : LocalRuleApp} {X : Sequent} + (h : lra.X = X.leftOnly) : (lra.toContext X).X = X := by + obtain ⟨preL, preR, preO⟩ := lra.preconditionProof + have hL : lra.L = X.1 := congrArg (fun Y => Y.1) h + have hR : lra.R = ∅ := congrArg (fun Y => Y.2.1) h + have hO : lra.O = X.2.2 := congrArg (fun Y => Y.2.2) h + refine lra.toContext_X X ⟨hL ▸ preL, ?_, hO ▸ preO⟩ + rw [hR] at preR + rw [Finset.subset_empty.mp preR] + exact Finset.empty_subset _ + +lemma LocalRuleApp.toContext_X_of_rightOnly {lra : LocalRuleApp} {X : Sequent} + (h : lra.X = X.rightOnly) : (lra.toContext X).X = X := by + obtain ⟨preL, preR, preO⟩ := lra.preconditionProof + have hL : lra.L = ∅ := congrArg (fun Y => Y.1) h + have hR : lra.R = X.2.1 := congrArg (fun Y => Y.2.1) h + have hO : lra.O = X.2.2 := congrArg (fun Y => Y.2.2) h + refine lra.toContext_X X ⟨?_, hR ▸ preR, hO ▸ preO⟩ + rw [hL] at preL + rw [Finset.subset_empty.mp preL] + exact Finset.empty_subset _ + +lemma LocalRuleApp.toContext_rightOnly_X {lra : LocalRuleApp} {X : Sequent} + (hX : lra.X = X) (hr : lra.isRightRule) : (lra.toContext X.rightOnly).X = X.rightOnly := by + obtain ⟨preL, preR, preO⟩ := lra.preconditionProof + subst hX + refine lra.toContext_X _ ⟨?_, preR, preO⟩ + rw [(LocalRuleApp.isRightRule_shape hr).1] + exact Finset.empty_subset _ + +/-! ### When is the canonical choice available? -/ + +lemma exists_localRuleApp_of_not_basic {Y : Sequent} (h : ¬ Y.basic) : + ∃ lra : LocalRuleApp, lra.X = Y := by + by_contra hcon + exact h (basic_iff_noLocalRuleApp.mpr hcon) + +lemma uniLeftChoice_leftOnly_isSome {X : Sequent} (h : ¬ X.leftFree.basic) : + (uniLeftChoice X.leftOnly).isSome := by + obtain ⟨lra, hlra⟩ := exists_localRuleApp_of_not_basic h + have hl : lra.isLeftRule := LocalRuleApp.isLeftRule_of_X_eq hlra + obtain ⟨preL, preR, preO⟩ := lra.preconditionProof + have hL : lra.L = X.1 := congrArg (fun Y => Y.1) hlra + have hR : lra.R = ∅ := congrArg (fun Y => Y.2.1) hlra + have hO : lra.O = none := congrArg (fun Y => Y.2.2) hlra + have hOc : lra.Ocond = none := by + rw [hO] at preO + rcases hOcond : lra.Ocond with _|(a|b) <;> simp_all + refine uniLeftChoice_isSome (lra := lra.toContext X.leftOnly) ?_ (by simpa using hl) + refine lra.toContext_X X.leftOnly ⟨hL ▸ preL, ?_, by simp [hOc, Sequent.leftOnly]⟩ + rw [(LocalRuleApp.isLeftRule_shape hl).1] + exact Finset.empty_subset _ + +lemma uniLeftChoice_leftOnly_eq_none {X : Sequent} (hb : X.leftFree.basic) + (hO : ¬ X.2.2.isLeft) : uniLeftChoice X.leftOnly = none := by + rcases hc : uniLeftChoice X.leftOnly with _ | lra + · rfl + exfalso + obtain ⟨hX, hl⟩ := uniLeftChoice_spec hc + obtain ⟨hRcond, hOcond⟩ := LocalRuleApp.isLeftRule_shape hl + obtain ⟨preL, preR, preO⟩ := lra.preconditionProof + have hLL : lra.L = X.1 := congrArg (fun Y => Y.1) hX + have hOO : lra.O = X.2.2 := congrArg (fun Y => Y.2.2) hX + have hOc : lra.Ocond = none := by + rcases hOcond with h' | h' + · exact h' + · exfalso + rw [hOO] at preO + rcases hOcond' : lra.Ocond with _|(a|b) <;> rcases hX22 : X.2.2 with _|(c|d) <;> + simp_all [Olf.isLeft] + have : ∃ lra' : LocalRuleApp, lra'.X = X.leftFree := by + refine ⟨lra.toContext X.leftFree, ?_⟩ + refine lra.toContext_X X.leftFree ⟨hLL ▸ preL, ?_, by simp [hOc, Sequent.leftFree]⟩ + rw [hRcond] + exact Finset.empty_subset _ + exact (basic_iff_noLocalRuleApp.mp hb) this + +lemma uniRightChoice_rightOnly_isSome {X : Sequent} {lra : LocalRuleApp} (hX : lra.X = X) + (hr : lra.isRightRule) : (uniRightChoice X.rightOnly).isSome := + uniRightChoice_isSome (lra := lra.toContext X.rightOnly) + (lra.toContext_rightOnly_X hX hr) (by simpa using hr) + +/-! ### The canonical rule choice -/ + +open Classical in +/-- The canonical rule application for a sequent that is free or loaded on the right: +first reduce the left component, then use the canonical rule for the right component. -/ +def uniChoiceRL (X : Sequent) : Option LocalRuleApp := + match uniLeftChoice X.leftOnly with + | some lra => some (lra.toContext X) + | none => + match uniRightChoice X.rightOnly with + | some lra => some (lra.toContext X) + | none => (LocalRuleApp.all X).head? + +lemma uniChoiceRL_X {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceRL X = some lra) : + lra.X = X := by + unfold uniChoiceRL at h + rcases hl : uniLeftChoice X.leftOnly with _ | lrl + · rcases hr : uniRightChoice X.rightOnly with _ | lrr + · rw [hl, hr] at h + simp only at h + exact LocalRuleApp.all_X X lra (List.mem_of_mem_head? h) + · rw [hl, hr] at h + simp only [Option.some.injEq] at h + subst h + exact LocalRuleApp.toContext_X_of_rightOnly (uniRightChoice_spec hr).1 + · rw [hl] at h + simp only [Option.some.injEq] at h + subst h + exact LocalRuleApp.toContext_X_of_leftOnly (uniLeftChoice_spec hl).1 + +lemma uniChoiceRL_isSome {X : Sequent} (h : ¬ X.basic) : (uniChoiceRL X).isSome := by + unfold uniChoiceRL + rcases hl : uniLeftChoice X.leftOnly with _ | lrl + · rcases hr : uniRightChoice X.rightOnly with _ | lrr + · simp only [Option.isSome] + rcases hh : (LocalRuleApp.all X).head? with _ | lra + · exfalso + rw [List.head?_eq_none_iff] at hh + exact LocalRuleApp.all_nonempty_of_nonbasic h hh + · rfl + · rfl + · rfl + +lemma uniChoiceRL_isUniChoice {X : Sequent} {lra : LocalRuleApp} (hnl : ¬ X.2.2.isLeft) + (h : uniChoiceRL X = some lra) : lra.IsUniChoice := by + have hX : lra.X = X := uniChoiceRL_X h + refine ⟨?_, ?_, ?_, ?_⟩ + · -- leftFirst + intro _ h2 + have h2' : ¬ X.leftFree.basic := by rwa [hX] at h2 + obtain ⟨lrl, hl⟩ := Option.isSome_iff_exists.mp (uniLeftChoice_leftOnly_isSome h2') + unfold uniChoiceRL at h + rw [hl] at h + simp only [Option.some.injEq] at h + subst h + simpa using (uniLeftChoice_spec hl).2 + · -- rightFirst + intro h1 + exact absurd (hX ▸ h1) hnl + · -- rightCanon + intro hr _ _ + have hnleft : uniLeftChoice X.leftOnly = none := by + rcases hl : uniLeftChoice X.leftOnly with _ | lrl + · rfl + · exfalso + unfold uniChoiceRL at h + rw [hl] at h + simp only [Option.some.injEq] at h + subst h + exact LocalRuleApp.not_left_and_right _ ⟨by simpa using (uniLeftChoice_spec hl).2, hr⟩ + rcases hrr : uniRightChoice X.rightOnly with _ | lrr + · exfalso + have : (uniRightChoice X.rightOnly).isSome := uniRightChoice_rightOnly_isSome hX hr + rw [hrr] at this + exact Bool.false_ne_true this + · refine ⟨lrr, by rw [hX, hrr], ?_⟩ + unfold uniChoiceRL at h + rw [hnleft, hrr] at h + simp only [Option.some.injEq] at h + subst h + exact LocalRuleApp.toContext_sameRuleAs lrr X + · -- leftCanon + intro _ h2 + exact absurd (hX ▸ h2) hnl + +open Classical in +/-- The canonical local rule application at a sequent: when the sequent is loaded on the +left we flip, use `uniChoiceRL` and flip back. -/ +def uniChoiceAt (X : Sequent) : Option LocalRuleApp := + if X.2.2.isLeft then (uniChoiceRL X.flip).map LocalRuleApp.flip else uniChoiceRL X + +lemma uniChoiceAt_X {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) : + lra.X = X := by + unfold uniChoiceAt at h + split at h + · rw [Option.map_eq_some_iff] at h + obtain ⟨lrb, hb, rfl⟩ := h + rw [LocalRuleApp.flip_X, uniChoiceRL_X hb, Sequent.flip_flip] + · exact uniChoiceRL_X h + +lemma uniChoiceAt_isSome {X : Sequent} (h : ¬ X.basic) : (uniChoiceAt X).isSome := by + unfold uniChoiceAt + split + · simpa using uniChoiceRL_isSome (X := X.flip) (by rwa [basic_flip]) + · exact uniChoiceRL_isSome h + +lemma uniChoiceAt_isUniChoice {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) : + lra.IsUniChoice := by + unfold uniChoiceAt at h + split at h + · rename_i hleft + rw [Option.map_eq_some_iff] at h + obtain ⟨lrb, hb, rfl⟩ := h + refine LocalRuleApp.IsUniChoice.flip (uniChoiceRL_isUniChoice ?_ hb) + clear hb + rcases X with ⟨L, R, O⟩ + rcases O with _ | (a | b) <;> simp_all [Sequent.flip, Olf.flip, Olf.isLeft] + · rename_i hleft + exact uniChoiceRL_isUniChoice hleft h + +lemma uniChoiceAt_C_lt {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) + {Y : Sequent} (hY : Y ∈ lra.C) : ltSequent Y X := by + have hdec := localRuleApp.decreases_DM lra Y hY + rwa [uniChoiceAt_X h] at hdec + +open Classical in +/-- The canonical local tableau: always apply the canonical rule `uniChoiceAt`. -/ +def uniLocalTab : (X : Sequent) → LocalTableau X + | X => + if bas : X.basic then .sim bas + else + have hX : ((uniChoiceAt X).get (uniChoiceAt_isSome bas)).X = X := + uniChoiceAt_X (Option.some_get (uniChoiceAt_isSome bas)).symm + .byLocalRule ((uniChoiceAt X).get (uniChoiceAt_isSome bas)) hX.symm + (fun Y _ => uniLocalTab Y) +termination_by X => X +decreasing_by + exact uniChoiceAt_C_lt (Option.some_get _).symm (by assumption) + +lemma uniLocalTab_isUni (X : Sequent) : (uniLocalTab X).IsUni := by + rw [uniLocalTab] + split + · rw [LocalTableau.IsUni]; trivial + · rename_i bas + rw [LocalTableau.IsUni] + refine ⟨uniChoiceAt_isUniChoice (Option.some_get (uniChoiceAt_isSome bas)).symm, ?_⟩ + intro Y hY + exact uniLocalTab_isUni Y +termination_by X +decreasing_by + exact uniChoiceAt_C_lt (Option.some_get _).symm (by assumption) + + +end PDL diff --git a/LeanPool/PDL/Local/Rules.lean b/LeanPool/PDL/Local/Rules.lean index f8e6f8d7e6..87d9dee08c 100644 --- a/LeanPool/PDL/Local/Rules.lean +++ b/LeanPool/PDL/Local/Rules.lean @@ -49,8 +49,7 @@ theorem OneSidedLocalRule.heq_of_precond_eq : ∀ {X B X' B' : _} | exact absurd h (pair_neg_ne_singleton _ _) | exact absurd h.symm (pair_neg_ne_singleton _ _) | (cases pair_neg_inj h; rfl) - | (exfalso; simp_all; done) - | (rw [Finset.singleton_inj] at h; injections; subst_eqs; rfl) + | (rw [Finset.singleton_inj] at h; injections <;> subst_eqs <;> rfl) instance oneSidedLocalRuleSubsingleton (X B) : Subsingleton (OneSidedLocalRule X B) := ⟨fun a b => eq_of_heq (OneSidedLocalRule.heq_of_precond_eq a b rfl)⟩ diff --git a/LeanPool/PDL/Local/Tableau.lean b/LeanPool/PDL/Local/Tableau.lean index e1cb6ff25e..41d0d9193b 100644 --- a/LeanPool/PDL/Local/Tableau.lean +++ b/LeanPool/PDL/Local/Tableau.lean @@ -7,12 +7,18 @@ Authors: PDL formalization contributors (see project card) module public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.CharZero.Defs +public import Mathlib.Algebra.GroupWithZero.Nat public import Mathlib.Algebra.Order.BigOperators.Group.List public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Data.Multiset.DershowitzManna public import LeanPool.PDL.Local.Rules +import Mathlib.Tactic.Linarith.Frontend -- shake: keep +import Mathlib.Tactic.NormNum.Eq -- shake: keep +import Mathlib.Tactic.NormNum.Ineq -- shake: keep + /-! # Local Tableaux (Section 3) -/ @[expose] public section @@ -62,17 +68,21 @@ theorem testsOfProgram_sizeOf_lt α : ∀ τ ∈ testsOfProgram α, sizeOf τ < Program.test.sizeOf_spec] at * case sequence α β => rcases τ_in with τ_in | τ_in - · have := testsOfProgram_sizeOf_lt α _ τ_in; linarith - · have := testsOfProgram_sizeOf_lt β _ τ_in; linarith + · have := testsOfProgram_sizeOf_lt α _ τ_in + exact NaturalBounds.lt_sum_left (Nat.le_of_lt this) + · have := testsOfProgram_sizeOf_lt β _ τ_in + exact NaturalBounds.lt_sum_right (Nat.le_of_lt this) case union α β => rcases τ_in with τ_in | τ_in - · have := testsOfProgram_sizeOf_lt α _ τ_in; linarith - · have := testsOfProgram_sizeOf_lt β _ τ_in; linarith + · have := testsOfProgram_sizeOf_lt α _ τ_in + exact NaturalBounds.lt_sum_left (Nat.le_of_lt this) + · have := testsOfProgram_sizeOf_lt β _ τ_in + exact NaturalBounds.lt_sum_right (Nat.le_of_lt this) case star β => - have := testsOfProgram_sizeOf_lt β _ τ_in; linarith + have := testsOfProgram_sizeOf_lt β _ τ_in; exact NaturalBounds.lt_one_add (Nat.le_of_lt this) case test τ => subst_eqs - linarith + exact NaturalBounds.lt_one_add (Nat.le_refl _) open LocalTableau diff --git a/LeanPool/PDL/Local/UnfoldBox.lean b/LeanPool/PDL/Local/UnfoldBox.lean index a04a8737e5..ed632c0d9b 100644 --- a/LeanPool/PDL/Local/UnfoldBox.lean +++ b/LeanPool/PDL/Local/UnfoldBox.lean @@ -8,8 +8,8 @@ module public import Mathlib.Data.Fintype.Pi public import Mathlib.Data.List.Sublists -public import Mathlib.Tactic.Linarith +public import LeanPool.PDL.General.NaturalBounds public import LeanPool.PDL.Substitution public import LeanPool.PDL.Star @@ -253,21 +253,21 @@ theorem F_goes_down : φ ∈ F α ℓ → lengthOfFormula φ < lengthOfProgram cases φ_in case inl φ_in_Fα => have IHα := F_goes_down φ_in_Fα - linarith + exact NaturalBounds.lt_sum_left IHα.le case inr φ_in_Fβ => have IHβ := F_goes_down φ_in_Fβ - linarith + exact NaturalBounds.lt_sum_right IHβ.le case union α β => cases φ_in case inl φ_in_Fα => have IHα := F_goes_down φ_in_Fα - linarith + exact NaturalBounds.lt_sum_left IHα.le case inr φ_in_Fβ => have IHβ := F_goes_down φ_in_Fβ - linarith + exact NaturalBounds.lt_sum_right IHβ.le case star α => have IHα := F_goes_down φ_in - linarith + exact NaturalBounds.lt_one_add IHα.le case test τ => cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩) · simp_all diff --git a/LeanPool/PDL/Local/UnfoldDia.lean b/LeanPool/PDL/Local/UnfoldDia.lean index b4b8fd07ed..13740ed3e7 100644 --- a/LeanPool/PDL/Local/UnfoldDia.lean +++ b/LeanPool/PDL/Local/UnfoldDia.lean @@ -6,8 +6,8 @@ Authors: PDL formalization contributors (see project card) module -public import Mathlib.Tactic.Linarith +public import LeanPool.PDL.General.NaturalBounds public import LeanPool.PDL.Substitution public import LeanPool.PDL.Star @@ -267,24 +267,43 @@ theorem Dset_goes_down_prog (α : Program) {Fs δ} (in_D : (Fs, δ) ∈ Dset α) cases β all_goals simp_all [Dset, lengthOfProgram, Program.isAtomic, Program.isStar] - try linarith + try + aesop (rule_sets := [-default]) (config := { enableSimp := false }) + (add 50% apply [NaturalBounds.lt_sum_left, NaturalBounds.lt_sum_right, + NaturalBounds.lt_one_add, Nat.le_of_lt]) + (add safe apply [NaturalBounds.one_lt_two_add, Nat.le_refl, Nat.zero_le]) · simp_all only [ite_false, List.mem_singleton, Prod.mk.injEq, List.mem_append] rcases in_δ with bla | γ_eq_β · have IHα := Dset_goes_down_prog α Fs'_in bla cases α all_goals simp_all [Dset, lengthOfProgram, Program.isAtomic, Program.isStar] - try linarith + try + aesop (rule_sets := [-default]) (config := { enableSimp := false }) + (add 50% apply [NaturalBounds.lt_sum_left, NaturalBounds.lt_sum_right, + NaturalBounds.lt_one_add, Nat.le_of_lt]) + (add safe apply [NaturalBounds.one_lt_two_add, Nat.le_refl, Nat.zero_le]) · subst γ_eq_β - linarith + aesop (rule_sets := [-default]) (config := { enableSimp := false }) + (add 50% apply [NaturalBounds.lt_sum_left, NaturalBounds.lt_sum_right, + NaturalBounds.lt_one_add, Nat.le_of_lt]) + (add safe apply [NaturalBounds.one_lt_two_add, Nat.le_refl, Nat.zero_le]) case union α β => simp only [Program.isAtomic, Bool.false_eq_true, ↓reduceIte, Program.isStar, lengthOfProgram] simp only [Dset, List.mem_union_iff] at in_D rcases in_D with hyp | hyp · have IHα := Dset_goes_down_prog α hyp in_δ - by_cases α.isAtomic <;> by_cases α.isStar <;> simp_all <;> linarith + by_cases α.isAtomic <;> by_cases α.isStar <;> simp_all <;> + aesop (rule_sets := [-default]) (config := { enableSimp := false }) + (add 50% apply [NaturalBounds.lt_sum_left, NaturalBounds.lt_sum_right, + NaturalBounds.lt_one_add, Nat.le_of_lt]) + (add safe apply [NaturalBounds.one_lt_two_add, Nat.le_refl, Nat.zero_le]) · have IHβ := Dset_goes_down_prog β hyp in_δ - by_cases β.isAtomic <;> by_cases β.isStar <;> simp_all <;> linarith + by_cases β.isAtomic <;> by_cases β.isStar <;> simp_all <;> + aesop (rule_sets := [-default]) (config := { enableSimp := false }) + (add 50% apply [NaturalBounds.lt_sum_left, NaturalBounds.lt_sum_right, + NaturalBounds.lt_one_add, Nat.le_of_lt]) + (add safe apply [NaturalBounds.one_lt_two_add, Nat.le_refl, Nat.zero_le]) case star α => simp only [Program.isAtomic, Bool.false_eq_true, ↓reduceIte, Program.isStar, lengthOfProgram] simp only [Dset, List.empty_eq, List.cons_union, List.nil_union, List.mem_insert_iff, @@ -299,12 +318,37 @@ theorem Dset_goes_down_prog (α : Program) {Fs δ} (in_D : (Fs, δ) ∈ Dset α) subst_eqs rcases in_δ with hyp | hyp · have IHα := Dset_goes_down_prog α in_D' hyp - by_cases α.isAtomic <;> by_cases α.isStar <;> simp_all <;> linarith + by_cases α.isAtomic <;> by_cases α.isStar <;> simp_all <;> + aesop (rule_sets := [-default]) (config := { enableSimp := false }) + (add 50% apply [NaturalBounds.lt_sum_left, NaturalBounds.lt_sum_right, + NaturalBounds.lt_one_add, Nat.le_of_lt]) + (add safe apply [NaturalBounds.one_lt_two_add, Nat.le_refl, Nat.zero_le]) · subst hyp simp [lengthOfProgram] case test τ => simp_all [Dset] + +-- Keep the existing private helper names when arithmetic proof search changes its cache order. +section +universe u_1 + +private theorem Dset_goes_down_prog._simp_1_14 {α : Type u_1} {a b : α} : + (a ∈ [b]) = (a = b) := propext List.mem_singleton + +private theorem Dset_goes_down_prog._simp_1_15 {α : Type u_1} {a : α} {s t : List α} : + (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) := propext List.mem_append + +private theorem Dset_goes_down_prog._simp_1_16 {α : Type u_1} + [inst : BEq α] [inst : LawfulBEq α] {x : α} {l₁ l₂ : List α} : + (x ∈ l₁ ∪ l₂) = (x ∈ l₁ ∨ x ∈ l₂) := propext List.mem_union_iff + +private theorem Dset_goes_down_prog._simp_1_17 {α : Type u_1} + [inst : BEq α] [inst : LawfulBEq α] {b a : α} {l : List α} : + (a ∈ List.insert b l) = (a = b ∨ a ∈ l) := propext List.mem_insert_iff + +end + /-- An intermediate step to define `unfoldDiamond`. This is not used in the paper. -/ def Yset : (List Formula × List Program) → Formula → List Formula | ⟨F, δ⟩, φ => F ∪ [ ~ Formula.boxes δ φ ] diff --git a/LeanPool/PDL/TableauPath.lean b/LeanPool/PDL/TableauPath.lean index faeff95daf..66d48b2fe1 100644 --- a/LeanPool/PDL/TableauPath.lean +++ b/LeanPool/PDL/TableauPath.lean @@ -12,6 +12,10 @@ public import Mathlib.Tactic.DepRewrite public import LeanPool.PDL.Tableau +import Mathlib.Tactic.Linarith.Frontend -- shake: keep +import Mathlib.Tactic.NormNum.Eq -- shake: keep +import Mathlib.Tactic.NormNum.Ineq -- shake: keep + /-! # Navigating through tableaux with PathIn To define relations between nodes in a tableau we need to represent the whole