diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 69a56f1..81e416f 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -11,7 +11,7 @@ jobs: name: Build runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: fetch-depth: ${{ env.GIT_HISTORY_DEPTH }} @@ -25,11 +25,29 @@ jobs: - name: make run: make + bml: + name: Build Bml + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: ${{ env.GIT_HISTORY_DEPTH }} + + - name: install elan + run: | + set -o pipefail + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y + ~/.elan/bin/lean --version + echo "$HOME/.elan/bin" >> $GITHUB_PATH + + - name: make bml + run: make bml + stats: name: Stats runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: install ripgrep run: sudo apt install -y ripgrep @@ -41,3 +59,11 @@ jobs: - name: count sorries run: | rg --count-matches sorry Pdl | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}' + + - name: Bml count lines in src + run: | + shopt -s globstar + wc -l Bml/**/*.lean + - name: Bml count sorries + run: | + rg --count-matches sorry Bml | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}' diff --git a/Bml.lean b/Bml.lean new file mode 100644 index 0000000..eaa2ca4 --- /dev/null +++ b/Bml.lean @@ -0,0 +1,12 @@ +import «Bml».Syntax +import «Bml».Semantics +import «Bml».Setsimp +import «Bml».Modelgraphs +import «Bml».Tableau +import «Bml».Examples +import «Bml».Vocabulary +import «Bml».Soundness +import «Bml».Tableauexamples +import «Bml».Completeness +import «Bml».Partitions +import «Bml».Interpolation diff --git a/Bml/Completeness.lean b/Bml/Completeness.lean new file mode 100644 index 0000000..5cbda99 --- /dev/null +++ b/Bml/Completeness.lean @@ -0,0 +1,255 @@ +-- COMPLETENESS + +import Bml.Syntax +import Bml.Tableau +import Bml.Soundness + +-- TODO: import Bml.modelgraphs + +open HasSat + +-- Each local rule preserves truth "upwards" +theorem localRuleTruth {W : Type} {M : KripkeModel W} {w : W} {X : Finset Formula} + {B : Finset (Finset Formula)} : LocalRule X B → (∃ Y ∈ B, (M, w)⊨Y) → (M, w)⊨X := + by + intro r + cases r + case bot => simp + case Not => simp + case neg f notnotf_in_a => + intro hyp + rcases hyp with ⟨b, b_in_B, w_sat_b⟩ + intro phi phi_in_a + have b_is_af : b = insert f (X \ {~~f}) := by simp at *; subst b_in_B; tauto + have phi_in_b_or_is_f : phi ∈ b ∨ phi = ~~f := + by + rw [b_is_af] + simp + tauto + cases' phi_in_b_or_is_f with phi_in_b phi_is_notnotf + · apply w_sat_b + exact phi_in_b + · rw [phi_is_notnotf] + unfold Evaluate at * + simp + -- this removes double negation + apply w_sat_b + rw [b_is_af] + simp at * + case Con f g fandg_in_a => + intro hyp + rcases hyp with ⟨b, b_in_B, w_sat_b⟩ + intro phi phi_in_a + simp at b_in_B + have b_is_fga : b = insert f (insert g (X \ {f⋀g})) := by subst b_in_B; ext1; simp + have phi_in_b_or_is_fandg : phi ∈ b ∨ phi = f⋀g := + by + rw [b_is_fga] + simp + tauto + cases' phi_in_b_or_is_fandg with phi_in_b phi_is_fandg + · apply w_sat_b + exact phi_in_b + · rw [phi_is_fandg] + unfold Evaluate at * + constructor + · apply w_sat_b; rw [b_is_fga]; simp + · apply w_sat_b; rw [b_is_fga]; simp + case nCo f g not_fandg_in_a => + intro hyp + rcases hyp with ⟨b, b_in_B, w_sat_b⟩ + intro phi phi_in_a + simp at * + have phi_in_b_or_is_notfandg : phi ∈ b ∨ phi = ~(f⋀g) := by + cases b_in_B + case inl b_in_B => rw [b_in_B]; simp; tauto + case inr b_in_B => rw [b_in_B]; simp; tauto + cases b_in_B + case inl b_in_B => -- b contains ~f + cases' phi_in_b_or_is_notfandg with phi_in_b phi_def + · exact w_sat_b phi phi_in_b + · rw [phi_def] + unfold Evaluate + rw [b_in_B] at w_sat_b + specialize w_sat_b (~f) + aesop + case inr b_in_B => -- b contains ~g + cases' phi_in_b_or_is_notfandg with phi_in_b phi_def + · exact w_sat_b phi phi_in_b + · rw [phi_def] + unfold Evaluate + rw [b_in_B] at w_sat_b + specialize w_sat_b (~g) + aesop + +-- Each local rule is "complete", i.e. preserves satisfiability "upwards" +theorem localRuleCompleteness {X : Finset Formula} {B : Finset (Finset Formula)} : + LocalRule X B → (∃ Y ∈ B, Satisfiable Y) → Satisfiable X := + by + intro lr + intro sat_B + rcases sat_B with ⟨Y, Y_in_B, sat_Y⟩ + unfold Satisfiable at * + rcases sat_Y with ⟨W, M, w, w_sat_Y⟩ + use W, M, w + apply localRuleTruth lr + tauto + +-- Lemma 11 (but rephrased to be about local tableau!?) +theorem inconsUpwards {X} {ltX : LocalTableau X} : + (∀ en ∈ endNodesOf ⟨X, ltX⟩, Inconsistent en) → Inconsistent X := + by + intro lhs + unfold Inconsistent at * + let leafTableaus : ∀ en ∈ endNodesOf ⟨X, ltX⟩, ClosedTableau en := fun Y YinEnds => + (lhs Y YinEnds).some + constructor + exact ClosedTableau.loc ltX leafTableaus + +-- Converse of Lemma 11 +theorem consToEndNodes {X} {ltX : LocalTableau X} : + Consistent X → ∃ en ∈ endNodesOf ⟨X, ltX⟩, Consistent en := + by + intro consX + unfold Consistent at * + have claim := Not.imp consX (@inconsUpwards X ltX) + simp at claim + tauto + +def projOfConsSimpIsCons : + ∀ {X ϕ}, Consistent X → Simple X → ~(□ϕ) ∈ X → Consistent (projection X ∪ {~ϕ}) := + by + intro X ϕ consX simpX notBoxPhi_in_X + unfold Consistent at * + unfold Inconsistent at * + contrapose consX + simp at * + cases' consX with ctProj + constructor + apply ClosedTableau.atm notBoxPhi_in_X simpX + simp + exact ctProj + +theorem locTabEndSatThenSat {X Y} (ltX : LocalTableau X) (Y_endOf_X : Y ∈ endNodesOf ⟨X, ltX⟩) : + Satisfiable Y → Satisfiable X := by + intro satY + induction ltX + case byLocalRule X B lr next IH => + apply localRuleCompleteness lr + cases lr + case bot W bot_in_W => + simp at * + case Not ϕ h => + simp at * + case neg ϕ notNotPhi_inX => + simp at * + specialize IH (insert ϕ (X.erase (~~ϕ))) + simp at IH + apply IH + rcases Y_endOf_X with ⟨W, W_def, Y_endOf_W⟩ + subst W_def + exact Y_endOf_W + case Con ϕ ψ _ => + simp at * + specialize IH (insert ϕ (insert ψ (X.erase (ϕ⋀ψ)))) + simp at IH + apply IH + rcases Y_endOf_X with ⟨W, W_def, Y_endOf_W⟩ + subst W_def + exact Y_endOf_W + case nCo ϕ ψ _ => + rw [nCoEndNodes, Finset.mem_union] at Y_endOf_X + cases Y_endOf_X + case inl Y_endOf_X => + specialize IH (X \ {~(ϕ⋀ψ)} ∪ {~ϕ}) + use X \ {~(ϕ⋀ψ)} ∪ {~ϕ} + constructor + · simp + · apply IH + convert Y_endOf_X; + case inr Y_endOf_X => + specialize IH (X \ {~(ϕ⋀ψ)} ∪ {~ψ}) + use X \ {~(ϕ⋀ψ)} ∪ {~ψ} + constructor + · simp + · apply IH + convert Y_endOf_X; + case sim X simpX => aesop + +theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Satisfiable X := + by + intro n + induction n using Nat.strong_induction_on + case h n IH => + intro X lX_is_n consX + refine' if simpX : Simple X then _ else _ + -- CASE 1: X is simple + rw [Lemma1_simple_sat_iff_all_projections_sat simpX] + constructor + · -- show that X is not closed + by_contra h + unfold Consistent at consX + unfold Inconsistent at consX + simp at consX + cases' consX with myfalse + apply myfalse + unfold Closed at h + refine' if botInX : ⊥ ∈ X then _ else _ + · apply ClosedTableau.loc; rotate_left; apply LocalTableau.byLocalRule + exact LocalRule.bot botInX + intro Y YinEmpty; exfalso; cases YinEmpty + rw [botNoEndNodes]; intro Y YinEmpty; exfalso; cases YinEmpty + · have f1 : ∃ (f : Formula) (_ : f ∈ X), ~f ∈ X := by tauto + have : Nonempty (ClosedTableau X) := + by + rcases f1 with ⟨f, f_in_X, notf_in_X⟩ + fconstructor + apply ClosedTableau.loc; rotate_left; apply LocalTableau.byLocalRule + apply LocalRule.Not ⟨f_in_X, notf_in_X⟩ + intro Y YinEmpty; exfalso; cases YinEmpty + rw [notNoEndNodes]; intro Y YinEmpty; exfalso; cases YinEmpty + exact Classical.choice this + · -- show that all projections are sat + intro R notBoxR_in_X + apply IH (lengthOfSet (projection X ∪ {~R})) + · -- projection decreases lengthOfSet + subst lX_is_n + exact atmRuleDecreasesLength notBoxR_in_X + · rfl + · exact projOfConsSimpIsCons consX simpX notBoxR_in_X + -- CASE 2: X is not simple + rename' simpX => notSimpX + rcases notSimpleThenLocalRule notSimpX with ⟨B, lrExists⟩ + have lr := Classical.choice lrExists + have rest : ∀ Y : Finset Formula, Y ∈ B → LocalTableau Y := + by + intro Y _ + set N := HasLength.lengthOf Y + exact Classical.choice (existsLocalTableauFor N Y (by rfl)) + rcases@consToEndNodes X (LocalTableau.byLocalRule lr rest) consX with ⟨E, E_endOf_X, consE⟩ + have satE : Satisfiable E := by + apply IH (lengthOfSet E) + · -- end Node of local rule is LT + subst lX_is_n + apply endNodesOfLocalRuleLT E_endOf_X + · rfl + · exact consE + exact locTabEndSatThenSat (LocalTableau.byLocalRule lr rest) E_endOf_X satE + +-- Theorem 4, page 37 +theorem completeness : ∀ X, Consistent X ↔ Satisfiable X := + by + intro X + constructor + · intro X_is_consistent + let n := lengthOfSet X + apply almostCompleteness n X (by rfl) X_is_consistent + -- use Theorem 2: + exact correctness X + +theorem singletonCompleteness : ∀ φ, Consistent {φ} ↔ Satisfiable φ := + by + intro f + have := completeness {f} + simp only [singletonSat_iff_sat] at * + tauto diff --git a/Bml/Examples.lean b/Bml/Examples.lean new file mode 100644 index 0000000..ebcb960 --- /dev/null +++ b/Bml/Examples.lean @@ -0,0 +1,50 @@ +-- EXAMPLES +import Bml.Syntax +import Bml.Semantics + +open HasSat + +theorem mytaut1 (p : Char) : Tautology ((·p)↣·p) := + by + unfold Tautology Evaluate + intro W M w + simp + +open Classical + +theorem mytaut2 (p : Char) : Tautology ((~~·p)↣·p) := + by + unfold Tautology Evaluate + intro W M w + classical + simp + +def myModel : KripkeModel ℕ where + val _ _ := True + Rel _ v := HEq v 1 + +theorem mysat (p : Char) : Satisfiable (·p) := + by + unfold Satisfiable + exists ℕ + exists myModel + exists 1 + +-- Some validities of basic modal logic + +theorem boxTop : Tautology (□⊤) := by + unfold Tautology Evaluate + tauto + +theorem A3 (X Y : Formula) : Tautology (□(X⋀Y) ↣ □X⋀□Y) := + by + unfold Tautology Evaluate + intro W M w + by_contra hyp + simp at hyp + unfold Evaluate at hyp + cases' hyp with hl hr + contrapose! hr + constructor + · intro v1 ass; exact (hl v1 ass).1 + · intro v2 ass; exact (hl v2 ass).2 diff --git a/Bml/Interpolation.lean b/Bml/Interpolation.lean new file mode 100644 index 0000000..0d74920 --- /dev/null +++ b/Bml/Interpolation.lean @@ -0,0 +1,36 @@ +-- INTERPOLATION + +import Bml.Syntax +import Bml.Completeness +import Bml.Partitions + +open HasVocabulary + +def Interpolant (φ : Formula) (ψ : Formula) (θ : Formula) := + Tautology (φ↣θ) ∧ Tautology (θ↣ψ) ∧ voc θ ⊆ voc φ ∩ voc ψ + +theorem interpolation {ϕ ψ} : Tautology (ϕ↣ψ) → ∃ θ, Interpolant ϕ ψ θ := + by + intro hyp + let X1 : Finset Formula := {ϕ} + let X2 : Finset Formula := {~ψ} + have ctX : ClosedTableau (X1 ∪ X2) := + by + rw [tautImp_iff_comboNotUnsat] at hyp + rw [← completeness] at hyp + -- using completeness! + unfold Consistent at hyp + simp at hyp + unfold Inconsistent at hyp + change ClosedTableau {ϕ, ~ψ} + exact Classical.choice hyp + have partInt := tabToInt ctX + -- using tableau interpolation! + rcases partInt with ⟨θ, pI_prop⟩ + unfold PartInterpolant at pI_prop + use θ + constructor + · rw [tautImp_iff_comboNotUnsat]; tauto + constructor + · rw [tautImp_iff_comboNotUnsat]; simp at *; tauto + · cases pI_prop; simp at *; tauto diff --git a/Bml/Modelgraphs.lean b/Bml/Modelgraphs.lean new file mode 100644 index 0000000..3deafd7 --- /dev/null +++ b/Bml/Modelgraphs.lean @@ -0,0 +1,102 @@ +-- MODELGRAPHS +import Bml.Syntax +import Bml.Semantics + +open Formula + +-- Definition 18, page 31 +def Saturated : Finset Formula → Prop + | X => + ∀ P Q : Formula, (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X) + +-- TODO: closure for program combinators! +-- Definition 19, page 31 +-- TODO: change [] to [A] later +@[simp] +def ModelGraph (Worlds : Finset (Finset Formula)) := + let W := Subtype fun x => x ∈ Worlds + let i := ∀ X : W, Saturated X.val ∧ ⊥ ∉ X.val ∧ ∀ P, P ∈ X.val → ~P ∉ X.val + let ii := fun M : KripkeModel W => ∀ (X : W) (pp), (·pp) ∈ X.val ↔ M.val X pp + let iii :=-- Note: Borzechowski only has → in ii. We follow BRV, Def 4.18 and 4.84. + fun M : KripkeModel W => ∀ (X Y : W) (P), M.Rel X Y → □P ∈ X.val → P ∈ Y.val + let iv := fun M : KripkeModel W => ∀ (X : W) (P), ~(□P) ∈ X.val → ∃ Y, M.Rel X Y ∧ ~P ∈ Y.val + Subtype fun M : KripkeModel W => i ∧ ii M ∧ iii M ∧ iv M + +-- Lemma 9, page 32 +theorem truthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) : + ∀ X : Worlds, ∀ P, P ∈ X.val → Evaluate (MG.val, X) P := + by + intro X P + cases' MG with M M_prop + rcases M_prop with ⟨i, ii, iii, iv⟩ + -- induction loading!! + let plus P (X : Worlds) := P ∈ X.val → Evaluate (M, X) P + let minus P (X : Worlds) := ~P ∈ X.val → ¬Evaluate (M, X) P + let oh P (X : Worlds) := □P ∈ X.val → ∀ Y, M.Rel X Y → P ∈ Y.val + have claim : ∀ P X, plus P X ∧ minus P X ∧ oh P X := + by + intro P + induction P; all_goals intro X + case bottom => + specialize i X + rcases i with ⟨_, bot_not_in_X, _⟩ + repeat' constructor + · intro P_in_X; apply absurd P_in_X bot_not_in_X + · tauto + · intro boxBot_in_X Y X_rel_Y; exact iii X Y ⊥ X_rel_Y boxBot_in_X + case atom_prop pp => + repeat' constructor + · intro P_in_X; unfold Evaluate; rw [ii X pp] at P_in_X ; exact P_in_X + · intro notP_in_X; unfold Evaluate; rw [← ii X pp] + rcases i X with ⟨_, _, P_in_then_notP_not_in⟩ + specialize P_in_then_notP_not_in (·pp); tauto + · intro boxPp_in_X Y X_rel_Y; exact iii X Y (·pp) X_rel_Y boxPp_in_X + case neg P IH => + rcases IH X with ⟨plus_IH, minus_IH, _⟩ + repeat' constructor + · intro notP_in_X; unfold Evaluate + exact minus_IH notP_in_X + · intro notnotP_in_X + rcases i X with ⟨X_saturated, _, _⟩ + cases' X_saturated P ⊥ with doubleNeg + -- ⊥ is unused! + unfold Evaluate; + simp + exact plus_IH (doubleNeg notnotP_in_X) + · intro notPp_in_X Y X_rel_Y; exact iii X Y (~P) X_rel_Y notPp_in_X + case And P Q IH_P IH_Q => + rcases IH_P X with ⟨plus_IH_P, minus_IH_P, _⟩ + rcases IH_Q X with ⟨plus_IH_Q, minus_IH_Q, _⟩ + rcases i X with ⟨X_saturated, _, _⟩ + unfold Saturated at X_saturated + rcases X_saturated P Q with ⟨_, andSplit, notAndSplit⟩ + repeat' constructor + · intro PandQ_in_X + specialize andSplit PandQ_in_X; cases' andSplit with P_in_X Q_in_X + unfold Evaluate + constructor + · exact plus_IH_P P_in_X + · exact plus_IH_Q Q_in_X + · intro notPandQ_in_X + unfold Evaluate; rw [not_and_or] + specialize notAndSplit notPandQ_in_X + cases' notAndSplit with notP_in_X notQ_in_X + · left; exact minus_IH_P notP_in_X + · right; exact minus_IH_Q notQ_in_X + · intro PandQ_in_X Y X_rel_Y; exact iii X Y (P⋀Q) X_rel_Y PandQ_in_X + case box P IH => + repeat' constructor + · intro boxP_in_X; unfold Evaluate + intro Y X_rel_Y + rcases IH Y with ⟨plus_IH_Y, _, _⟩ + apply plus_IH_Y + rcases IH X with ⟨_, _, oh_IH_X⟩ + exact oh_IH_X boxP_in_X Y X_rel_Y + · intro notBoxP_in_X; unfold Evaluate + push_neg + rcases iv X P notBoxP_in_X with ⟨Y, X_rel_Y, notP_in_Y⟩ + use Y; constructor; exact X_rel_Y + rcases IH Y with ⟨_, minus_IH_Y, _⟩ + exact minus_IH_Y notP_in_Y + · intro boxBoxP_in_X Y X_rel_Y; exact iii X Y (□P) X_rel_Y boxBoxP_in_X + apply (claim P X).left diff --git a/Bml/Partitions.lean b/Bml/Partitions.lean new file mode 100644 index 0000000..7cf7325 --- /dev/null +++ b/Bml/Partitions.lean @@ -0,0 +1,852 @@ +-- PARTITIONS + +import Bml.Syntax +import Bml.Tableau +import Bml.Semantics +import Bml.Soundness +import Bml.Vocabulary + +open HasVocabulary HasSat + +def Partition := + Finset Formula × Finset Formula + +-- Definition 24 +def PartInterpolant (X1 X2 : Finset Formula) (θ : Formula) := + voc θ ⊆ voc X1 ∩ voc X2 ∧ ¬Satisfiable (X1 ∪ {~θ}) ∧ ¬Satisfiable (X2 ∪ {θ}) + +-- Lemma 14 +theorem botInter {X1 X2} : ⊥ ∈ X1 ∪ X2 → ∃ θ, PartInterpolant X1 X2 θ := + by + intro bot_in_X + refine' if side : ⊥ ∈ X1 then _ else _ + · -- case ⊥ ∈ X1 + use ⊥ + constructor + · unfold voc; simp; tauto + constructor + all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩; specialize sat ⊥; simp at * + apply sat + exact side + · -- case ⊥ ∈ X2 + have : ⊥ ∈ X2 := by simp at *; tauto + use ~⊥ + constructor + · unfold voc; simp; tauto + constructor + all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ + · specialize sat (~~⊥); simp at * + · specialize sat ⊥; simp at *; tauto + +theorem notInter {X1 X2 ϕ} : ϕ ∈ X1 ∪ X2 ∧ ~ϕ ∈ X1 ∪ X2 → ∃ θ, PartInterpolant X1 X2 θ := + by + intro in_both; cases' in_both with pIn nIn + by_cases pSide : ϕ ∈ X1; all_goals by_cases nSide : ~ϕ ∈ X1 + -- four cases + · use⊥ + -- both in X1 + constructor + · unfold voc; simp; tauto + constructor + all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ + · have h1 := sat ϕ; have h2 := sat (~ϕ); simp at *; tauto + · specialize sat ⊥; aesop + · use ϕ + -- ϕ ∈ X1 and ~ϕ ∈ X2 + constructor + · unfold voc; intro a aIn; simp + constructor + · use ϕ + tauto + · have h : ~ϕ ∈ X2 := by rw [Finset.mem_union] at nIn; tauto + have := vocElem_subs_vocSet h + simp at * + tauto + constructor + all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ + · simp at *; tauto + · have h1 := sat (~ϕ); simp at *; tauto + · use ~ϕ + -- ~ϕ ∈ X1 and ϕ ∈ X2 + constructor + · unfold voc; intro a aIn; simp + constructor + · use (~ϕ) + tauto + · have h : ϕ ∈ X2 := by rw [Finset.mem_union] at pIn; tauto + have := vocElem_subs_vocSet h + simp at * + tauto + constructor + all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ + · have h1 := sat (~ϕ); simp at *; tauto + · simp at *; tauto + · use~⊥ + -- both in X2 + constructor + · unfold voc; simp; tauto + constructor + all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ + · specialize sat (~~⊥); simp at * + · have h1 := sat ϕ; have h2 := sat (~ϕ); simp at *; tauto + +theorem notnotInterpolantX1 {X1 X2 ϕ θ} : + ~~ϕ ∈ X1 → PartInterpolant (X1 \ {~~ϕ} ∪ {ϕ}) (X2 \ {~~ϕ}) θ → PartInterpolant X1 X2 θ := + by + intro notnotphi_in_X1 theta_is_chInt + rcases theta_is_chInt with ⟨vocSub, noSatX1, noSatX2⟩ + unfold PartInterpolant + constructor + · rw [vocPreserved X1 (~~ϕ) ϕ notnotphi_in_X1 (by unfold voc; simp)] + have : voc (X2 \ {~~ϕ}) ⊆ voc X2 := vocErase + rw [Finset.subset_inter_iff] at vocSub + rw [Finset.subset_inter_iff] + tauto + constructor + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + · have : Satisfiable (X1 \ {~~ϕ} ∪ {ϕ} ∪ {~θ}) := + by + unfold Satisfiable + use W, M, w + intro ψ psi_in_newX_u_notTheta + simp at psi_in_newX_u_notTheta + cases psi_in_newX_u_notTheta + case inl psi_is_phi => + specialize sat (~~ϕ) + subst psi_is_phi + simp at sat + apply sat + right + exact notnotphi_in_X1 + case inr c => + cases c + case inl psi_in_newX_u_notTheta => + rw [psi_in_newX_u_notTheta]; apply of_not_not + rw [← psi_in_newX_u_notTheta] + have := sat (~~ϕ); simp at *; aesop + · apply sat; simp at *; tauto + tauto + · have : Satisfiable (X2 \ {~~ϕ} ∪ {θ}) := + by + unfold Satisfiable at * + use W, M, w + intro ψ psi_in_newX2cupTheta + apply sat; simp at *; tauto + tauto + +theorem notnotInterpolantX2 {X1 X2 ϕ θ} : + ~~ϕ ∈ X2 → PartInterpolant (X1 \ {~~ϕ}) (X2 \ {~~ϕ} ∪ {ϕ}) θ → PartInterpolant X1 X2 θ := + by + intro notnotphi_in_X2 theta_is_chInt + rcases theta_is_chInt with ⟨vocSub, noSatX1, noSatX2⟩ + unfold PartInterpolant + constructor + · rw [vocPreserved X2 (~~ϕ) ϕ notnotphi_in_X2 (by simp)] + have : voc (X1 \ {~~ϕ}) ⊆ voc X1 := vocErase + rw [Finset.subset_inter_iff] + rw [Finset.subset_inter_iff] at vocSub + tauto + constructor + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + · apply noSatX1 + unfold Satisfiable + use W, M, w + intro ψ psi_in_newX_u_notTheta + simp at psi_in_newX_u_notTheta + cases' psi_in_newX_u_notTheta with psi_in_newX_u_notTheta psi_in_newX_u_notTheta + · apply sat; rw [psi_in_newX_u_notTheta]; simp at * + cases psi_in_newX_u_notTheta + · apply sat; simp at *; tauto + · apply noSatX2 + unfold Satisfiable at * + use W, M, w + intro ψ psi_in_newX2cupTheta + simp at psi_in_newX2cupTheta + cases psi_in_newX2cupTheta + case inl psi_is_phi => + specialize sat (~~ϕ) + subst psi_is_phi + simp at sat + apply sat + right + exact notnotphi_in_X2 + case inr psi_in_newX2cupTheta => + apply sat; simp; tauto + +theorem conInterpolantX1 {X1 X2 ϕ ψ θ} : + ϕ⋀ψ ∈ X1 → PartInterpolant (X1 \ {ϕ⋀ψ} ∪ {ϕ, ψ}) (X2 \ {ϕ⋀ψ}) θ → PartInterpolant X1 X2 θ := + by + intro con_in_X1 theta_is_chInt + rcases theta_is_chInt with ⟨vocSub, noSatX1, noSatX2⟩ + unfold PartInterpolant + constructor + · rw [vocPreservedTwo (ϕ⋀ψ) ϕ ψ con_in_X1 (by simp)] + have : voc (X2 \ {ϕ⋀ψ}) ⊆ voc X2 := vocErase + rw [Finset.subset_inter_iff] + rw [Finset.subset_inter_iff] at vocSub + tauto + constructor + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + · apply noSatX1 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_in pi_in + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; exact con_in_X1); unfold Evaluate at sat ; tauto + cases' pi_in with pi_in pi_in + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; exact con_in_X1); unfold Evaluate at sat ; tauto + cases' pi_in with pi_in pi_in + · subst pi_in + exact sat (~θ) (by simp) + · exact sat π (by simp; tauto) + · apply noSatX2 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_in pi_in + · rw [pi_in]; apply sat θ; simp + · apply sat; simp at *; tauto + +theorem conInterpolantX2 {X1 X2 ϕ ψ θ} : + ϕ⋀ψ ∈ X2 → PartInterpolant (X1 \ {ϕ⋀ψ}) (X2 \ {ϕ⋀ψ} ∪ {ϕ, ψ}) θ → PartInterpolant X1 X2 θ := + by + intro con_in_X2 theta_is_chInt + rcases theta_is_chInt with ⟨vocSub, noSatX1, noSatX2⟩ + unfold PartInterpolant + constructor + · rw [vocPreservedTwo (ϕ⋀ψ) ϕ ψ con_in_X2 (by simp)] + have : voc (X1 \ {ϕ⋀ψ}) ⊆ voc X1 := vocErase + rw [Finset.subset_inter_iff] + rw [Finset.subset_inter_iff] at vocSub + tauto + constructor + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + · apply noSatX1 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_in pi_in + · rw [pi_in]; apply sat (~θ); simp + · apply sat; simp at *; tauto + · apply noSatX2 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_in pi_in + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; right; exact con_in_X2); unfold Evaluate at sat ; tauto + cases' pi_in with pi_in pi_in + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; right; exact con_in_X2); unfold Evaluate at sat ; + tauto + cases' pi_in with pi_in pi_in + · rw [pi_in]; apply sat θ; simp + · exact sat π (by simp; tauto) + +theorem nCoInterpolantX1 {X1 X2 ϕ ψ θa θb} : + ~(ϕ⋀ψ) ∈ X1 → + PartInterpolant (X1 \ {~(ϕ⋀ψ)} ∪ {~ϕ}) (X2 \ {~(ϕ⋀ψ)}) θa → + PartInterpolant (X1 \ {~(ϕ⋀ψ)} ∪ {~ψ}) (X2 \ {~(ϕ⋀ψ)}) θb → + PartInterpolant X1 X2 (~(~θa⋀~θb)) := + by + intro nCo_in_X1 tA_is_chInt tB_is_chInt + rcases tA_is_chInt with ⟨a_vocSub, a_noSatX1, a_noSatX2⟩ + rcases tB_is_chInt with ⟨b_vocSub, b_noSatX1, b_noSatX2⟩ + unfold PartInterpolant + constructor + · simp + rw [Finset.subset_inter_iff] + constructor; all_goals rw [Finset.union_subset_iff] ; constructor <;> intro a aIn + · have sub : voc (~ϕ) ⊆ voc (~(ϕ⋀ψ)) := by simp; apply Finset.subset_union_left + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ϕ) nCo_in_X1 sub + rw [Finset.subset_iff] at claim + specialize @claim a + rw [Finset.subset_iff] at a_vocSub + specialize a_vocSub aIn + aesop + · have sub : voc (~ψ) ⊆ voc (~(ϕ⋀ψ)) := by simp; apply Finset.subset_union_right + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ψ) nCo_in_X1 sub + rw [Finset.subset_iff] at claim + specialize @claim a + rw [Finset.subset_iff] at b_vocSub + specialize b_vocSub aIn + aesop + · rw [Finset.subset_iff] at a_vocSub + specialize a_vocSub aIn + have : voc (X2 \ {~(ϕ⋀ψ)}) ⊆ voc X2 := vocErase + unfold voc at * + simp at * + tauto + · rw [Finset.subset_iff] at b_vocSub + specialize b_vocSub aIn + have : voc (X2 \ {~(ϕ⋀ψ)}) ⊆ voc X2 := vocErase + unfold voc at * + simp at * + tauto + constructor + all_goals by_contra hyp; unfold Satisfiable at hyp; rcases hyp with ⟨W, M, w, sat⟩ + · have : ¬ Evaluate (M, w) ϕ ∨ ¬ Evaluate (M,w) ψ := by + specialize sat (~(ϕ⋀ψ)) (by simp; assumption) + simp at sat + tauto + cases this + · apply a_noSatX1 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_is_notPhi pi_in + · subst pi_is_notPhi; simp; assumption + · cases' pi_in with pi_is_notThetA pi_in_X1 + · subst pi_is_notThetA; + specialize sat (~~(~θa⋀~θb)) (by simp) + aesop + · apply sat π; simp; right; exact pi_in_X1.right + · apply b_noSatX1 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_is_notPhi pi_in + · subst pi_is_notPhi; simp; assumption + · cases' pi_in with pi_is_notThetB pi_in_X1 + · subst pi_is_notThetB; + specialize sat (~~(~θa⋀~θb)) (by simp) + aesop + · simp at pi_in_X1 + apply sat π; simp; right; exact pi_in_X1.right + · have : Evaluate (M, w) θa ∨ Evaluate (M,w) θb := by + specialize sat (~(~θa⋀~θb)) (by simp) + simp at sat + tauto + cases this + · apply a_noSatX2 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_is_thetA pi_in_X2 + · subst pi_is_thetA; assumption + · apply sat π; simp; right; exact pi_in_X2.right + · apply b_noSatX2 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_is_thetB pi_in_X2 + · subst pi_is_thetB; assumption + · apply sat π; simp; right; exact pi_in_X2.right + +theorem nCoInterpolantX2 {X1 X2 ϕ ψ θa θb} : + ~(ϕ⋀ψ) ∈ X2 → + PartInterpolant (X1 \ {~(ϕ⋀ψ)}) (X2 \ {~(ϕ⋀ψ)} ∪ {~ϕ}) θa → + PartInterpolant (X1 \ {~(ϕ⋀ψ)}) (X2 \ {~(ϕ⋀ψ)} ∪ {~ψ}) θb → PartInterpolant X1 X2 (θa⋀θb) := + by + intro nCo_in_X2 tA_is_chInt tB_is_chInt + rcases tA_is_chInt with ⟨a_vocSub, a_noSatX1, a_noSatX2⟩ + rcases tB_is_chInt with ⟨b_vocSub, b_noSatX1, b_noSatX2⟩ + unfold PartInterpolant + constructor + · simp + rw [Finset.subset_inter_iff] + constructor; all_goals rw [Finset.union_subset_iff] ; constructor <;> intro a aIn + · rw [Finset.subset_iff] at a_vocSub + specialize a_vocSub aIn + have claim : voc (X1 \ {~(ϕ⋀ψ)}) ⊆ voc X1 := vocErase + unfold voc at claim + simp at * + tauto + · rw [Finset.subset_iff] at b_vocSub + specialize b_vocSub aIn + have claim : voc (X1 \ {~(ϕ⋀ψ)}) ⊆ voc X1 := vocErase + unfold voc at claim + simp at * + tauto + · have sub : voc (~ϕ) ⊆ voc (~(ϕ⋀ψ)) := by simp; apply Finset.subset_union_left + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ϕ) nCo_in_X2 sub + rw [Finset.subset_iff] at claim + rw [Finset.subset_iff] at a_vocSub + specialize a_vocSub aIn + aesop + · have sub : voc (~ψ) ⊆ voc (~(ϕ⋀ψ)) := by simp; apply Finset.subset_union_right + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ψ) nCo_in_X2 sub + rw [Finset.subset_iff] at claim + rw [Finset.subset_iff] at b_vocSub + specialize b_vocSub aIn + aesop + constructor + all_goals by_contra hyp; unfold Satisfiable at hyp; rcases hyp with ⟨W, M, w, sat⟩ + · apply a_noSatX1 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_in pi_in + · rw [pi_in] + by_contra; apply b_noSatX1 + unfold Satisfiable + use W, M, w + intro χ chi_in + simp at chi_in + cases chi_in + case inl chi_is_not_thetab => + subst chi_is_not_thetab; specialize sat (~(θa⋀θb)); simp at *; tauto + · apply sat; simp; tauto + · apply sat; simp; tauto + · apply a_noSatX2 + unfold Satisfiable + use W, M, w + intro π pi_in + simp at pi_in + cases' pi_in with pi_in pi_in + · subst pi_in + by_contra; apply b_noSatX2 + unfold Satisfiable + use W, M, w + intro χ chi_in + simp at chi_in + cases' chi_in with chi_in chi_in + case inl notnot_phi => simp at notnot_phi; specialize sat (~(ϕ⋀ψ)); aesop + cases' chi_in with chi_in chi_in + · specialize sat (θa⋀θb); simp at sat ; rw [chi_in]; exact sat.right + · apply sat; simp; tauto + cases' pi_in with pi_in pi_in + · rw [pi_in]; specialize sat (θa⋀θb); simp at sat ; unfold Evaluate at *; tauto + · apply sat; simp; tauto + +theorem localTabToInt : + ∀ n X, + n = lengthOfSet X → + ∀ {X1 X2}, + X = X1 ∪ X2 → + (∃ ltX : LocalTableau X, + ∀ Y1 Y2, Y1 ∪ Y2 ∈ endNodesOf ⟨X, ltX⟩ → ∃ θ, PartInterpolant Y1 Y2 θ) → + ∃ θ, PartInterpolant X1 X2 θ := + by + intro N + induction N using Nat.strong_induction_on + case h n IH => + intro X lenX_is_n X1 X2 defX pt + rcases pt with ⟨pt, nextInter⟩ + cases pt + case sim foo => + apply nextInter + subst defX + simp + case byLocalRule B next lr => + cases lr + -- The bot and not cases use Lemma 14 + case bot bot_in_X => rw [defX] at bot_in_X ; exact botInter bot_in_X + case Not ϕ in_both => rw [defX] at in_both ; exact notInter in_both + case neg ϕ + notnotphi_in => + have notnotphi_in_union : ~~ϕ ∈ X1 ∪ X2 := by rw [defX] at notnotphi_in ; assumption + simp at * + cases' notnotphi_in_union with notnotphi_in_X1 notnotphi_in_X2 + · -- case ~~ϕ ∈ X1 + subst defX + let newX1 := X1 \ {~~ϕ} ∪ {ϕ} + let newX2 := X2 \ {~~ϕ} + -- to deal with possible overlap + have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {~~ϕ} ∪ {ϕ}} := + by + rw [Finset.mem_singleton] + change X1 \ {~~ϕ} ∪ {ϕ} ∪ X2 \ {~~ϕ} = (X1 ∪ X2) \ {~~ϕ} ∪ {ϕ} + ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto + set m := lengthOfSet (newX1 ∪ newX2) + have m_lt_n : m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.neg notnotphi_in) (newX1 ∪ newX2) yclaim + have nextNextInter : + ∀ Y1 Y2 : Finset Formula, + Y1 ∪ Y2 ∈ endNodesOf ⟨newX1 ∪ newX2, next (newX1 ∪ newX2) yclaim⟩ → + Exists (PartInterpolant Y1 Y2) := + by intro Y1 Y2; apply nextInter Y1 Y2 (newX1 ∪ newX2); aesop + have childInt : Exists (PartInterpolant newX1 newX2) := + IH m m_lt_n (newX1 ∪ newX2) (refl _) (refl _) (next (newX1 ∪ newX2) yclaim) nextNextInter + cases' childInt with θ theta_is_chInt + use θ + exact notnotInterpolantX1 notnotphi_in_X1 theta_is_chInt + · -- case ~~ϕ ∈ X2 + ---- based on copy-paste from previous case, changes marked with "!" --- + subst defX + let newX1 := X1 \ {~~ϕ} + -- to deal with possible overlap -- ! + let newX2 := X2 \ {~~ϕ} ∪ {ϕ} + -- ! + have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {~~ϕ} ∪ {ϕ}} := + by + rw [Finset.mem_singleton] + change X1 \ {~~ϕ} ∪ (X2 \ {~~ϕ} ∪ {ϕ}) = (X1 ∪ X2) \ {~~ϕ} ∪ {ϕ} + -- ! + ext1 a; + constructor <;> · intro hyp; simp at hyp ; simp; tauto + set m := lengthOfSet (newX1 ∪ newX2) + have m_lt_n : m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.neg notnotphi_in) (newX1 ∪ newX2) yclaim + have nextNextInter : + ∀ Y1 Y2 : Finset Formula, + Y1 ∪ Y2 ∈ endNodesOf ⟨newX1 ∪ newX2, next (newX1 ∪ newX2) yclaim⟩ → + Exists (PartInterpolant Y1 Y2) := + by intro Y1 Y2; apply nextInter Y1 Y2 (newX1 ∪ newX2); aesop + have childInt : Exists (PartInterpolant newX1 newX2) := + IH m m_lt_n (newX1 ∪ newX2) (refl _) (refl _) (next (newX1 ∪ newX2) yclaim) nextNextInter + cases' childInt with θ theta_is_chInt + use θ + exact notnotInterpolantX2 notnotphi_in_X2 theta_is_chInt + case Con ϕ ψ + con_in_X => + have con_in_union : ϕ⋀ψ ∈ X1 ∨ ϕ⋀ψ ∈ X2 := by subst defX; simp at con_in_X; assumption + cases con_in_union + case inl con_in_X1 => -- case ϕ⋀ψ ∈ X1 + subst defX + let newX1 := X1 \ {ϕ⋀ψ} ∪ {ϕ, ψ} + let newX2 := X2 \ {ϕ⋀ψ} + have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ}} := + by + rw [Finset.mem_singleton] + change X1 \ {ϕ⋀ψ} ∪ {ϕ, ψ} ∪ X2 \ {ϕ⋀ψ} = (X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ} + ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto + set m := lengthOfSet (newX1 ∪ newX2) + have m_lt_n : m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.Con con_in_X) (newX1 ∪ newX2) yclaim + have nextNextInter : + ∀ Y1 Y2 : Finset Formula, + Y1 ∪ Y2 ∈ endNodesOf ⟨newX1 ∪ newX2, next (newX1 ∪ newX2) yclaim⟩ → + Exists (PartInterpolant Y1 Y2) := + by + intro Y1 Y2 Y_in; apply nextInter; unfold endNodesOf + simp only [true_and, endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, Subtype.exists] + exact ⟨newX1 ∪ newX2, yclaim, Y_in⟩ + have childInt : Exists (PartInterpolant newX1 newX2) := + by + apply IH m m_lt_n (newX1 ∪ newX2) (refl _) (refl _) + fconstructor + apply next (newX1 ∪ newX2) yclaim; exact nextNextInter + cases' childInt with θ theta_is_chInt + use θ + exact conInterpolantX1 con_in_X1 theta_is_chInt + case inr con_in_X2 => -- case ϕ⋀ψ ∈ X2 + subst defX + let newX1 := X1 \ {ϕ⋀ψ} + let newX2 := X2 \ {ϕ⋀ψ} ∪ {ϕ, ψ} + have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ}} := + by + rw [Finset.mem_singleton] + change X1 \ {ϕ⋀ψ} ∪ (X2 \ {ϕ⋀ψ} ∪ {ϕ, ψ}) = (X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ} + ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto + set m := lengthOfSet (newX1 ∪ newX2) + have m_lt_n : m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.Con con_in_X) (newX1 ∪ newX2) yclaim + have nextNextInter : + ∀ Y1 Y2 : Finset Formula, + Y1 ∪ Y2 ∈ endNodesOf ⟨newX1 ∪ newX2, next (newX1 ∪ newX2) yclaim⟩ → + Exists (PartInterpolant Y1 Y2) := + by + intro Y1 Y2 Y_in; apply nextInter; unfold endNodesOf + simp only [true_and, endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, Subtype.exists] + exact ⟨newX1 ∪ newX2, yclaim, Y_in⟩ + have childInt : Exists (PartInterpolant newX1 newX2) := + by + apply IH m m_lt_n (newX1 ∪ newX2) (refl _) (refl _) + fconstructor + apply next (newX1 ∪ newX2) yclaim; exact nextNextInter + cases' childInt with θ theta_is_chInt + use θ + exact conInterpolantX2 con_in_X2 theta_is_chInt + case nCo ϕ ψ + nCo_in_X => + have nCo_in_union : ~(ϕ⋀ψ) ∈ X1 ∨ ~(ϕ⋀ψ) ∈ X2 := by subst defX; simp at nCo_in_X; assumption + cases nCo_in_union + case inl nCo_in_X1 => -- case ~(ϕ⋀ψ) ∈ X1 + subst defX + -- splitting rule! + -- first get an interpolant for the ~ϕ branch: + let a_newX1 := X1 \ {~(ϕ⋀ψ)} ∪ {~ϕ} + let a_newX2 := X2 \ {~(ϕ⋀ψ)} + have a_yclaim : + a_newX1 ∪ a_newX2 ∈ + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : + Finset (Finset Formula)) := + by simp; left; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto + set a_m := lengthOfSet (a_newX1 ∪ a_newX2) + have a_m_lt_n : a_m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.nCo nCo_in_X) (a_newX1 ∪ a_newX2) a_yclaim + have a_childInt : Exists (PartInterpolant a_newX1 a_newX2) := + by + apply IH a_m a_m_lt_n (a_newX1 ∪ a_newX2) (refl _) (refl _) + fconstructor + apply next (a_newX1 ∪ a_newX2) a_yclaim + -- remains to show nextNextInter + intro Y1 Y2 Y_in; + apply nextInter; unfold endNodesOf + simp only [true_and, endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, + Subtype.exists] + exact ⟨a_newX1 ∪ a_newX2, a_yclaim, Y_in⟩ + cases' a_childInt with θa a_theta_is_chInt + -- now get an interpolant for the ~ψ branch: + let b_newX1 := X1 \ {~(ϕ⋀ψ)} ∪ {~ψ} + let b_newX2 := X2 \ {~(ϕ⋀ψ)} + have b_yclaim : + b_newX1 ∪ b_newX2 ∈ + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : + Finset (Finset Formula)) := + by simp; right; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto + set b_m := lengthOfSet (b_newX1 ∪ b_newX2) + have b_m_lt_n : b_m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.nCo nCo_in_X) (b_newX1 ∪ b_newX2) b_yclaim + have b_childInt : Exists (PartInterpolant b_newX1 b_newX2) := + by + apply IH b_m b_m_lt_n (b_newX1 ∪ b_newX2) (refl _) (refl _) + fconstructor + apply next (b_newX1 ∪ b_newX2) b_yclaim + -- remains to show nextNextInter + intro Y1 Y2 Y_in; + apply nextInter; unfold endNodesOf + simp only [true_and, endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, + Subtype.exists] + exact ⟨b_newX1 ∪ b_newX2, b_yclaim, Y_in⟩ + cases' b_childInt with θb b_theta_is_chInt + -- finally, combine the two interpolants using disjunction: + use~(~θa⋀~θb) + exact nCoInterpolantX1 nCo_in_X1 a_theta_is_chInt b_theta_is_chInt + case inr nCo_in_X2 => -- case ~(ϕ⋀ψ) ∈ X2 + subst defX + -- splitting rule! + -- first get an interpolant for the ~ϕ branch: + let a_newX1 := X1 \ {~(ϕ⋀ψ)} + let a_newX2 := X2 \ {~(ϕ⋀ψ)} ∪ {~ϕ} + have a_yclaim : + a_newX1 ∪ a_newX2 ∈ + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : + Finset (Finset Formula)) := + by simp; left; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto + set a_m := lengthOfSet (a_newX1 ∪ a_newX2) + have a_m_lt_n : a_m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.nCo nCo_in_X) (a_newX1 ∪ a_newX2) a_yclaim + have a_childInt : Exists (PartInterpolant a_newX1 a_newX2) := + by + apply IH a_m a_m_lt_n (a_newX1 ∪ a_newX2) (refl _) (refl _) + fconstructor + apply next (a_newX1 ∪ a_newX2) a_yclaim + -- remains to show nextNextInter + intro Y1 Y2 Y_in; + apply nextInter; unfold endNodesOf + simp only [true_and, endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, Subtype.exists] + exact ⟨a_newX1 ∪ a_newX2, a_yclaim, Y_in⟩ + cases' a_childInt with θa a_theta_is_chInt + -- now get an interpolant for the ~ψ branch: + let b_newX1 := X1 \ {~(ϕ⋀ψ)} + let b_newX2 := X2 \ {~(ϕ⋀ψ)} ∪ {~ψ} + have b_yclaim : + b_newX1 ∪ b_newX2 ∈ + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : + Finset (Finset Formula)) := + by simp; right; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto + set b_m := lengthOfSet (b_newX1 ∪ b_newX2) + have b_m_lt_n : b_m < n := by + rw [lenX_is_n] + exact localRulesDecreaseLength (LocalRule.nCo nCo_in_X) (b_newX1 ∪ b_newX2) b_yclaim + have b_childInt : Exists (PartInterpolant b_newX1 b_newX2) := + by + apply IH b_m b_m_lt_n (b_newX1 ∪ b_newX2) (refl _) (refl _) + fconstructor + apply next (b_newX1 ∪ b_newX2) b_yclaim + -- remains to show nextNextInter + intro Y1 Y2 Y_in; + apply nextInter; unfold endNodesOf + simp only [true_and, endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, Subtype.exists] + exact ⟨b_newX1 ∪ b_newX2, b_yclaim, Y_in⟩ + cases' b_childInt with θb b_theta_is_chInt + -- finally, combine the two interpolants using conjunction: + use θa⋀θb + exact nCoInterpolantX2 nCo_in_X2 a_theta_is_chInt b_theta_is_chInt + +theorem vocProj (X) : voc (projection X) ⊆ voc X := + by + simp + intro ϕ phi_in_proj + rw [proj] at phi_in_proj + intro a aInVocPhi + simp + tauto + +theorem projUnion {X Y} : projection (X ∪ Y) = projection X ∪ projection Y := + by + ext1 + rw [proj] + simp + rw [proj] + rw [proj] + +open HasLength + +-- tableau interpolation -- IDEA: similar to almostCompleteness +-- part of this is part of Lemma 15 +theorem almostTabToInt {X} (ctX : ClosedTableau X) : + ∀ X1 X2, X = X1 ∪ X2 → ∃ θ, PartInterpolant X1 X2 θ := + by + induction ctX + case loc X ltX next IH => + intro X1 X2 defX + have nextLtAndInter : + ∃ ltX : LocalTableau X, + ∀ Y1 Y2, Y1 ∪ Y2 ∈ endNodesOf ⟨X, ltX⟩ → ∃ θ, PartInterpolant Y1 Y2 θ := + by + use ltX + intro Y1 Y2 y_is_endOfX + specialize next (Y1 ∪ Y2) y_is_endOfX + exact IH (Y1 ∪ Y2) y_is_endOfX Y1 Y2 (refl _) + exact localTabToInt _ X (refl _) defX nextLtAndInter + case atm X ϕ notBoxPhi_in_X simpleX ctProjNotPhi + IH => + intro X1 X2 defX + subst defX + simp at * + cases notBoxPhi_in_X + · -- case ~□ϕ ∈ X1 + let newX1 := projection X1 ∪ {~ϕ} + let newX2 := projection X2 + have yclaim : newX1 ∪ newX2 = projection (X1 ∪ X2) ∪ {~ϕ} := by rw [projUnion]; ext1; simp + rw [← yclaim] at ctProjNotPhi + have nextInt : ∃ θ, PartInterpolant newX1 newX2 θ := IH newX1 newX2 (by rw [yclaim]; simp) + rcases nextInt with ⟨θ, vocSub, unsat1, unsat2⟩ + use~(□~θ) + repeat' constructor + -- it remains to show the three properties of the interpolant + · change voc θ ⊆ voc X1 ∩ voc X2 + have inc1 : voc newX1 ⊆ voc X1 := by + intro a aIn; simp at * + cases' aIn with a_in_vocPhi other + · use~(□ϕ); tauto + · rcases other with ⟨ψ, psi_in_projX1, _⟩ + use□ψ; change □ψ ∈ X1 ∧ a ∈ voc (□ψ); rw [← proj]; tauto + have inc2 : voc newX2 ⊆ voc X2 := by + intro a aIn; simp at * + rcases aIn with ⟨ψ, psi_in_projX2⟩ + · use□ψ; change □ψ ∈ X2 ∧ a ∈ voc (□ψ); rw [← proj]; tauto + rw [Finset.subset_inter_iff] at vocSub + rcases vocSub with ⟨vocTh_in_X1, vocTh_in_X2⟩ + rw [Finset.subset_inter_iff] + tauto + all_goals unfold Satisfiable at * + case left notBoxPhi_in_X => + by_contra hyp + rcases hyp with ⟨W, M, w, sat⟩ + apply unsat1 + use W, M + --- we use ~□ϕ to get a different world: + let othersat := sat (~(□ϕ)) (by simp; apply notBoxPhi_in_X) + unfold Evaluate at othersat + simp at othersat + rcases othersat with ⟨v, rel_w_v, v_not_phi⟩ + use v + intro ψ psi_in_newX1 + simp at psi_in_newX1 + cases psi_in_newX1 + case inl psi_in_newX1 => + subst psi_in_newX1; specialize sat (~~(□~θ)); simp at *; + exact v_not_phi + case inr psi_in_newX1 => + cases' psi_in_newX1 with psi_in_newX1 psi_in + · rw [psi_in_newX1] + specialize sat (~(~(□(~θ)))) + simp at sat + simp + exact sat v rel_w_v + · rw [proj] at psi_in + specialize sat (□ψ) (by simp; exact psi_in) + simp at sat + exact sat v rel_w_v + · by_contra hyp + rcases hyp with ⟨W, M, w, sat⟩ + apply unsat2 + use W, M + --- we use ~□~θ to get a different world: + let othersat := sat (~(□~θ)) (by simp) + unfold Evaluate at othersat + simp at othersat + rcases othersat with ⟨v, rel_w_v, v_not_phi⟩ + use v + intro ψ psi_in_newX2 + simp at psi_in_newX2 + cases' psi_in_newX2 with psi_is_theta psi_in_projX2 + · subst psi_is_theta; assumption + · rw [proj] at psi_in_projX2 ; specialize sat (□ψ); apply sat; simp; assumption; assumption + · -- case ~□ϕ ∈ X2 + let newX1 := projection X1 + let newX2 := projection X2 ∪ {~ϕ} + ---- what follows is *based* on copying the previous case ---- + have yclaim : newX1 ∪ newX2 = projection (X1 ∪ X2) ∪ {~ϕ} := by rw [projUnion]; ext1; simp + rw [← yclaim] at ctProjNotPhi + have nextInt : ∃ θ, PartInterpolant newX1 newX2 θ := IH newX1 newX2 (by rw [yclaim]; simp) + rcases nextInt with ⟨θ, vocSub, unsat1, unsat2⟩ + use□θ + -- !! + repeat' constructor + -- it remains to show the three properties of the interpolant + · change voc θ ⊆ voc X1 ∩ voc X2 + have inc1 : voc newX2 ⊆ voc X2 := by + intro a aIn; simp at * + cases' aIn with a_in_vocPhi other + · use~(□ϕ); tauto + · rcases other with ⟨ψ, psi_in_projX2, _⟩ + use□ψ; change □ψ ∈ X2 ∧ a ∈ voc (□ψ); rw [← proj]; tauto + have inc2 : voc newX1 ⊆ voc X1 := by + intro a aIn; simp at * + rcases aIn with ⟨ψ, psi_in_projX1⟩ + · use□ψ; change □ψ ∈ X1 ∧ a ∈ voc (□ψ); rw [← proj]; tauto + rw [Finset.subset_inter_iff] at vocSub + rcases vocSub with ⟨vocTh_in_X1, vocTh_in_X2⟩ + rw [Finset.subset_inter_iff] + tauto + all_goals unfold Satisfiable at * + · by_contra hyp + rcases hyp with ⟨W, M, w, sat⟩ + apply unsat1 + use W, M + --- we use ~□θ to get a different world: + let othersat := sat (~(□θ)) (by simp) + unfold Evaluate at othersat + simp at othersat + rcases othersat with ⟨v, rel_w_v, v_not_phi⟩ + use v + intro ψ psi_in_newX1 + simp at psi_in_newX1 + cases' psi_in_newX1 with psi_in_newX1 psi_in_newX1 + · subst psi_in_newX1; specialize sat (~(□θ)); simp at sat; tauto + · rw [proj] at psi_in_newX1 ; specialize sat (□ψ); apply sat; simp; assumption; assumption + · by_contra hyp + rcases hyp with ⟨W, M, w, sat⟩ + apply unsat2 + use W, M + --- we use ~□ϕ to get a different world: + let othersat := sat (~(□ϕ)) (by simp; assumption) + unfold Evaluate at othersat + simp at othersat + rcases othersat with ⟨v, rel_w_v, v_not_phi⟩ + use v + intro ψ psi_in_newX2 + simp at psi_in_newX2 + cases' psi_in_newX2 with psi_is_notPhi psi_in_newX2 + · subst psi_is_notPhi; simp; assumption + cases' psi_in_newX2 + case inl psi_is_theta => + subst psi_is_theta + specialize sat (□ψ) (by simp) + simp at sat + exact sat v rel_w_v + case inr psi_in_newX2 => + rw [proj] at psi_in_newX2 ; specialize sat (□ψ); simp at sat + apply sat; right; assumption; assumption + +theorem tabToInt {X1 X2} : ClosedTableau (X1 ∪ X2) → ∃ θ, PartInterpolant X1 X2 θ + | ctX => almostTabToInt ctX X1 X2 (refl _) diff --git a/Bml/Semantics.lean b/Bml/Semantics.lean new file mode 100644 index 0000000..346db2e --- /dev/null +++ b/Bml/Semantics.lean @@ -0,0 +1,91 @@ +-- SEMANTICS +import Mathlib.Data.Finset.Basic + +import Mathlib.Order.CompleteLattice +import Mathlib.Order.FixedPoints +import Mathlib.Data.Set.Lattice + +import Bml.Syntax + +-- Definition 2, page 6 +structure KripkeModel (W : Type) : Type where + val : W → Char → Prop + Rel : W → W → Prop + +-- Definition 3, page 6 +@[simp] +def Evaluate {W : Type} : KripkeModel W × W → Formula → Prop + | (_, _), ⊥ => False + | (M, w), ·p => M.val w p + | (M, w), ~φ => ¬Evaluate (M, w) φ + | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ + | (M, w), □φ => ∀ v : W, M.Rel w v → Evaluate (M, v) φ + +def Tautology (φ : Formula) := + ∀ (W) (M : KripkeModel W) (w), Evaluate (M, w) φ + +def Contradiction (φ : Formula) := + ∀ (W) (M : KripkeModel W) (w), ¬Evaluate (M, w) φ + +-- Definition 5, page 9 +class HasSat (α : Type) where + Satisfiable : α → Prop + +open HasSat +@[simp] +instance formHasSat : HasSat Formula := + HasSat.mk fun ϕ => ∃ (W : _) (M : KripkeModel W) (w : _), Evaluate (M, w) ϕ +@[simp] +instance setHasSat : HasSat (Finset Formula) := + HasSat.mk fun X => ∃ (W : _) (M : KripkeModel W) (w : _), ∀ φ ∈ X, Evaluate (M, w) φ + +theorem notsatisfnotThenTaut : ∀ φ, ¬Satisfiable (~φ) → Tautology φ := + by + intro phi + unfold Satisfiable + unfold Tautology + simp + +@[simp] +theorem singletonSat_iff_sat : ∀ φ, Satisfiable ({φ} : Finset Formula) ↔ Satisfiable φ := + by + intro phi + simp + +theorem tautImp_iff_comboNotUnsat {ϕ ψ} : + Tautology (ϕ↣ψ) ↔ ¬Satisfiable ({ϕ, ~ψ} : Finset Formula) := + by + unfold Tautology + simp + +def SemImpliesSets (X : Finset Formula) (Y : Finset Formula) := + ∀ (W : Type) (M : KripkeModel W) (w), (∀ φ ∈ X, Evaluate (M, w) φ) → ∀ ψ ∈ Y, Evaluate (M, w) ψ + +-- Definition 5, page 9 +class VDash (α β : Type) where + SemImplies : α → β → Prop + +open VDash + +@[simp] +instance modelCanSemImplyForm {W : Type} : VDash (KripkeModel W × W) Formula := ⟨@Evaluate W⟩ +@[simp] +instance modelCanSemImplySet {W : Type} : VDash (KripkeModel W × W) (Finset Formula) := ⟨fun Mw X => ∀ f ∈ X, @Evaluate W Mw f⟩ +instance setCanSemImplySet : VDash (Finset Formula) (Finset Formula):= ⟨SemImpliesSets⟩ +instance setCanSemImplyForm : VDash (Finset Formula) Formula := ⟨fun X ψ => SemImpliesSets X {ψ}⟩ +instance formCanSemImplySet : VDash Formula (Finset Formula) := ⟨fun φ X => SemImpliesSets {φ} X⟩ +instance formCanSemImplyForm : VDash (Formula) (Formula):= ⟨fun φ ψ => SemImpliesSets {φ} {ψ}⟩ + +infixl:40 "⊨" => SemImplies + +infixl:40 "⊭" => fun a b => ¬a⊨b + +theorem forms_to_sets {φ ψ : Formula} : φ⊨ψ → ({φ} : Finset Formula)⊨({ψ} : Finset Formula) := + by + intro impTaut + intro W M w lhs ψ1 psi1_in_setpsi + specialize impTaut W M w + simp at * + subst psi1_in_setpsi + apply impTaut + exact lhs diff --git a/Bml/Setsimp.lean b/Bml/Setsimp.lean new file mode 100644 index 0000000..2285b81 --- /dev/null +++ b/Bml/Setsimp.lean @@ -0,0 +1,64 @@ +-- SETSIMP +import Mathlib.Algebra.BigOperators.Basic +import Mathlib.Data.Finset.Basic + +import Bml.Syntax + +@[simp] +theorem union_singleton_is_insert {X : Finset Formula} {ϕ : Formula} : X ∪ {ϕ} = insert ϕ X := + by + have fo := Finset.insert_eq ϕ X + aesop + +@[simp] +theorem sdiff_singleton_is_erase {X : Finset Formula} {ϕ : Formula} : X \ {ϕ} = X.erase ϕ := + by + induction X using Finset.induction_on + simp + ext1 + aesop + +@[simp] +theorem lengthAdd {X : Finset Formula} {ϕ} : + ϕ ∉ X → lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ := + by + intro notin + unfold lengthOfSet + rw [Finset.sum_insert notin] + apply Nat.add_comm + +@[simp] +theorem lengthOf_insert_leq_plus {X : Finset Formula} {ϕ : Formula} : + lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ := + by + cases' em (ϕ ∈ X) with in_x not_in_x + · rw [Finset.insert_eq_of_mem in_x]; simp + · rw [lengthAdd not_in_x] + +@[simp] +theorem lengthRemove (X : Finset Formula) : + ∀ ϕ ∈ X, lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X := + by + intro ϕ in_X + have claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ := + by + apply lengthAdd + simp + have anotherClaim : insert ϕ (X \ {ϕ}) = X := by + ext1 + simp only [Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton] + constructor + aesop + tauto + rw [anotherClaim] at claim + aesop + +@[simp] +theorem sum_union_le {T} [DecidableEq T] : + ∀ {X Y : Finset T} {F : T → ℕ}, (X ∪ Y).sum F ≤ X.sum F + Y.sum F := + by + intro X Y F + · + calc + (X ∪ Y).sum F ≤ (X ∪ Y).sum F + (X ∩ Y).sum F := by simp + _ = X.sum F + Y.sum F := Finset.sum_union_inter diff --git a/Bml/Soundness.lean b/Bml/Soundness.lean new file mode 100644 index 0000000..6feef48 --- /dev/null +++ b/Bml/Soundness.lean @@ -0,0 +1,465 @@ +-- SOUNDNESS + +import Bml.Syntax +import Bml.Tableau + +open Classical + +-- attribute [local instance 10] prop_decidable -- delete me? + +open HasSat + +-- Combine a collection of pointed models with one new world using the given valuation. +-- TODO: rewrite to term mode? +def combinedModel {β : Type} (collection : β → Σ W : Type, KripkeModel W × W) + (newVal : Char → Prop) : + KripkeModel (Sum Unit (Σ k : β, (collection k).fst)) × Sum Unit (Σ k : β, (collection k).fst) := + by + constructor + constructor + · -- making the valuation function: + intro world + cases world + case inl newWorld => -- the one new world + cases newWorld + exact newVal -- use new given valuation here!! + case inr oldWorld => -- world in one of the given models: + cases' oldWorld with R w + exact (collection R).snd.fst.val w + · -- defining relations: + intro worldOne worldTwo + cases worldOne <;> cases worldTwo -- four cases about two new or old worlds + case inl.inl => exact False -- no reflexive loop at the new world. + case inl.inr newWorld oldWorld => + exact HEq oldWorld.snd (collection oldWorld.fst).snd.snd -- conect new world to given points. + case inr.inl => exact False -- no connection from models to new world + case inr.inr oldWorldOne oldWorldTwo => + -- connect two old worlds iff they are from the same model and were connected there already: + cases' oldWorldOne with kOne wOne + cases' oldWorldTwo with kTwo wTwo + have help : kOne = kTwo → Prop := by + intro same + have sameCol : collection kOne = collection kTwo := by rw [← same] + rw [← sameCol] at wTwo + exact (collection kOne).snd.fst.Rel wOne wTwo + exact dite (kOne = kTwo) (fun same => help same) fun _ => False + · -- point at the new world: + left + exact () + +-- The combined model preserves all truths at the old worlds. +theorem combMo_preserves_truth_at_oldWOrld {β : Type} + (collection : β → Σ W : Type, KripkeModel W × W) (newVal : Char → Prop) : + ∀ (f : Formula) (R : β) (oldWorld : (collection R).fst), + Evaluate ((combinedModel collection newVal).fst, Sum.inr ⟨R, oldWorld⟩) f ↔ + Evaluate ((collection R).snd.fst, oldWorld) f := + by + intro f + induction f <;> intro R oldWorld + case bottom => aesop + case atom_prop c => + unfold combinedModel + simp + case neg f f_IH => + unfold Evaluate + rw [f_IH R oldWorld] + case And f g f_IH g_IH => + unfold Evaluate + rw [f_IH R oldWorld] + rw [g_IH R oldWorld] + case box f f_IH => + unfold Evaluate + constructor + · intro true_in_combo + intro otherWorld rel_in_old_model + specialize f_IH R otherWorld + rw [← f_IH] + specialize true_in_combo (Sum.inr ⟨R, otherWorld⟩) + apply true_in_combo + unfold combinedModel + simp + exact rel_in_old_model + · intro true_in_old + simp + constructor + · intro newWorld + unfold combinedModel + tauto + -- the new world is never reachable, trivial case + · intro otherR otherWorld + intro rel_in_new_model + specialize f_IH otherR otherWorld + unfold combinedModel at rel_in_new_model + have sameR : R = otherR := by + by_contra + aesop + subst sameR + rw [f_IH] + apply true_in_old + -- remains to show that related in old model + simp at * + exact rel_in_new_model + +-- The combined model for X satisfies X. +theorem combMo_sat_X {X : Finset Formula} {β : Set Formula} + {beta_def : β = {R : Formula | ~R.box ∈ X}} (simple_X : Simple X) (not_closed_X : ¬Closed X) + (collection : β → Σ W : Type, KripkeModel W × W) + (all_pro_sat : + ∀ R : β, + ∀ f ∈ projection X ∪ {~R}, Evaluate ((collection R).snd.fst, (collection R).snd.snd) f) : + ∀ f ∈ X, + Evaluate + ((combinedModel collection fun c => Formula.atom_prop c ∈ X).fst, + (combinedModel collection fun c => Formula.atom_prop c ∈ X).snd) + f := + by + intro f f_in_X + cases f + -- no induction because X is simple + case bottom => + unfold Closed at not_closed_X + tauto + case atom_prop => + unfold combinedModel + unfold Evaluate + simp + exact f_in_X + case + neg f => + -- subcases :-/ + cases f + case atom_prop => + unfold combinedModel + unfold Evaluate + unfold Closed at not_closed_X + rw [not_or] at not_closed_X + simp at * + tauto + case box f => + -- set coMo := , + simp only [Evaluate, not_forall] + -- need reachable world with ~f, use the β-witness + let h : f ∈ β := by rw [beta_def]; use f_in_X + let oldWorld : Sum Unit (Σ k : β, (collection k).fst) := + Sum.inr ⟨⟨f, h⟩, (collection ⟨f, h⟩).snd.snd⟩ + use oldWorld + constructor + · -- show that f is false at old world + have coMoLemma := + combMo_preserves_truth_at_oldWOrld collection (fun c : Char => (·c) ∈ X) f ⟨f, h⟩ + (collection ⟨f, h⟩).snd.snd + rw [coMoLemma] + specialize all_pro_sat ⟨f, h⟩ (~f) + unfold Evaluate at all_pro_sat + simp at * + exact all_pro_sat + ·-- show that worlds are related in combined model (def above, case 2) + unfold combinedModel; + simp + case bottom => tauto + case neg f => + unfold Simple SimpleForm at simple_X + simp at simple_X + specialize simple_X (~~f) f_in_X + simp at simple_X + case And f g => + unfold Simple SimpleForm at simple_X + simp at simple_X + specialize simple_X (~(f⋀g)) f_in_X + simp at simple_X + case And fa fb => + unfold Simple at simple_X + simp at simple_X + specialize simple_X (fa⋀fb) f_in_X + simp at simple_X + case box f => + unfold Evaluate + intro otherWorld is_rel + cases otherWorld + · cases is_rel + case inr otherWorld => -- otherWorld cannot be the (unreachable) new world + have coMoLemma := + combMo_preserves_truth_at_oldWOrld collection (fun c => (·c) ∈ X) f otherWorld.fst + otherWorld.snd + simp at coMoLemma + rw [coMoLemma] + specialize all_pro_sat otherWorld.fst f + simp at all_pro_sat + rw [or_imp] at all_pro_sat + cases' all_pro_sat with _ all_pro_sat_right + rw [← proj] at f_in_X + specialize all_pro_sat_right f_in_X + have sameWorld : otherWorld.snd = (collection otherWorld.fst).snd.snd := by + rw [heq_iff_eq.mp (HEq.symm is_rel)] + rw [sameWorld] + simp + exact all_pro_sat_right + +-- Lemma 1 (page 16) +-- A simple set of formulas X is satisfiable if and only if +-- it is not closed and for all ¬[A]R ∈ X also XA; ¬R is satisfiable. +theorem Lemma1_simple_sat_iff_all_projections_sat {X : Finset Formula} : + Simple X → (Satisfiable X ↔ ¬Closed X ∧ ∀ R, ~(□R) ∈ X → Satisfiable (projection X ∪ {~R})) := + by + intro X_is_simple + constructor + · -- left to right + intro sat_X + unfold Satisfiable at * + rcases sat_X with ⟨W, M, w, w_sat_X⟩ + constructor + · -- show that X is not closed: + by_contra hyp + unfold Closed at hyp + cases' hyp with bot_in_X f_and_notf_in_X + · exact w_sat_X ⊥ bot_in_X + · rcases f_and_notf_in_X with ⟨f, f_in_X, notf_in_X⟩ + let w_sat_f := w_sat_X f f_in_X + let w_sat_notf := w_sat_X (~f) notf_in_X + exact absurd w_sat_f w_sat_notf + · -- show that for each ~[]R ∈ X the projection with ~R is satisfiable: + intro R notboxr_in_X + let w_sat_notboxr := w_sat_X (~(□R)) notboxr_in_X + unfold Evaluate at w_sat_notboxr + simp at w_sat_notboxr + rcases w_sat_notboxr with ⟨v, w_rel_v, v_sat_notr⟩ + use W, M, v + intro g + simp at * + rw [or_imp] + constructor + · intro g_is_notR + rw [g_is_notR] + exact v_sat_notr + · intro boxg_in_X + rw [proj] at boxg_in_X + specialize w_sat_X (□g) boxg_in_X + unfold Evaluate at w_sat_X + exact w_sat_X v w_rel_v + · -- right to left + intro rhs + cases' rhs with not_closed_X all_pro_sat + unfold Satisfiable at * + -- Let's build a new Kripke model! + let β := {R : Formula | ~(□R) ∈ X} + -- beware, using Axioms of Choice here! + choose typeFor this_pro_sat using all_pro_sat + choose modelFor this_pro_sat using this_pro_sat + choose worldFor this_pro_sat using this_pro_sat + -- define the collection: + let collection : β → Σ W : Type, KripkeModel W × W := + by + intro k + cases' k with R notboxr_in_X + simp at notboxr_in_X + use typeFor R notboxr_in_X, modelFor R notboxr_in_X, worldFor R notboxr_in_X + let newVal c := Formula.atom_prop c ∈ X + let BigM := combinedModel collection newVal + use Sum Unit (Σ k : β, (collection k).fst) + use BigM.fst, BigM.snd + -- apply Lemma, missing last argument "all_pro_sat" + -- we need to use that X_is_simple (to restrict cases what phi can be) + -- and that X is not closed (to ensure that it is locally consistent) + apply combMo_sat_X X_is_simple not_closed_X collection + -- it remains to show that the new big model satisfies X + intro R f f_inpro_or_notr + cases' R with R notrbox_in_X + simp only [Finset.mem_union, Finset.mem_insert, Finset.mem_singleton, Subtype.coe_mk] at * + specialize this_pro_sat R notrbox_in_X + cases' f_inpro_or_notr with f_inpro f_is_notboxR + · -- if f is in the projection + specialize this_pro_sat f + rw [or_imp] at this_pro_sat + cases' this_pro_sat with this_pro_sat_l this_pro_sat_r + exact this_pro_sat_l f_inpro + · -- case where f is ~[]R + cases f_is_notboxR + case refl => + specialize this_pro_sat (~R) + rw [or_imp] at this_pro_sat + cases' this_pro_sat with this_pro_sat_l this_pro_sat_r + tauto + simp + +-- to check β +-- Each rule is sound and preserves satisfiability "downwards" +theorem localRuleSoundness {α : Finset Formula} {B : Finset (Finset Formula)} : + LocalRule α B → Satisfiable α → ∃ β ∈ B, Satisfiable β := + by + intro r + intro a_sat + unfold Satisfiable at a_sat + rcases a_sat with ⟨W, M, w, w_sat_a⟩ + cases r + case bot bot_in_a => + by_contra + let w_sat_bot := w_sat_a ⊥ bot_in_a + unfold Evaluate at w_sat_bot + exact w_sat_bot + case Not f hyp => + by_contra + have w_sat_f : Evaluate (M, w) f := by + apply w_sat_a + exact hyp.left + have w_sat_not_f : Evaluate (M, w) (~f) := + by + apply w_sat_a (~f) + exact hyp.right + simp at * + exact absurd w_sat_f w_sat_not_f + case neg f + hyp => + have w_sat_f : Evaluate (M, w) f := + by + specialize w_sat_a (~~f) hyp + aesop + use α \ {~~f} ∪ {f} + simp + use W, M, w + constructor + · exact w_sat_f + · intro _ _ + apply w_sat_a + case Con f g hyp => + use α \ {f⋀g} ∪ {f, g} + constructor + simp + unfold Satisfiable + use W, M, w + simp only [and_imp, forall_eq_or_imp, sdiff_singleton_is_erase, Ne.def, Finset.union_insert, + Finset.mem_insert, Finset.mem_erase] + constructor + · -- f + specialize w_sat_a (f⋀g) hyp + simp at * + exact w_sat_a.left + · intro h hhyp + simp at hhyp + cases hhyp + case inl h_is_g => -- h = g + specialize w_sat_a (f⋀g) hyp + simp at * + rw [h_is_g] + exact w_sat_a.right + case inr h_in_a => -- h in a + exact w_sat_a h h_in_a.right + case nCo f g notfandg_in_a => + unfold Satisfiable + let w_sat_phi := w_sat_a (~(f⋀g)) notfandg_in_a + simp [Evaluate] at w_sat_phi + rw [imp_iff_not_or] at w_sat_phi + cases' w_sat_phi with not_w_f not_w_g + · use α \ {~(f⋀g)} ∪ {~f} + simp + use W, M, w + tauto + · use α \ {~(f⋀g)} ∪ {~g} + constructor + · simp at * + · use W, M, w + intro psi + simp + intro psi_def + cases psi_def + case inl psi_def => + rw [psi_def] + unfold Evaluate + exact not_w_g + case inr psi_def => + cases' psi_def with psi_in_a psi_def_right + exact w_sat_a psi psi_def_right + +-- The critical roule is sound and preserves satisfiability "downwards". +-- TODO: is this the same as (one of the directions of) Lemma 1 ?? +theorem atmSoundness {α : Finset Formula} {f} (not_box_f_in_a : ~(□f) ∈ α) : + Simple α → Satisfiable α → Satisfiable (projection α ∪ {~f}) := + by + intro _s -- sus?! + intro aSat + unfold Satisfiable at aSat + rcases aSat with ⟨W, M, w, w_sat_a⟩ + constructor + simp + -- get the other reachable world: + let w_sat_not_box_f := w_sat_a (~f.box) not_box_f_in_a + unfold Evaluate at w_sat_not_box_f + simp at w_sat_not_box_f + rcases w_sat_not_box_f with ⟨v, w_rel_v, v_not_sat_f⟩ + -- show that the projection is satisfiable: + use M, v + constructor + · exact v_not_sat_f + intro phi phi_in_proj + rw [proj] at phi_in_proj + · specialize w_sat_a phi.box _ + exact phi_in_proj + unfold Evaluate at w_sat_a + exact w_sat_a v w_rel_v + +theorem localTableauAndEndNodesUnsatThenNotSat {Z} (ltZ : LocalTableau Z) : + (∀ Y, Y ∈ endNodesOf ⟨Z, ltZ⟩ → ¬Satisfiable Y) → ¬Satisfiable Z := + by + intro endsOfXnotSat + induction ltZ + case byLocalRule X YS lr next IH => + by_contra satX + rcases localRuleSoundness lr satX with ⟨Y, Y_in_YS, satY⟩ + specialize IH Y Y_in_YS + set ltY := next Y Y_in_YS + have endNodesInclusion : + ∀ W, W ∈ endNodesOf ⟨Y, ltY⟩ → W ∈ endNodesOf ⟨X, LocalTableau.byLocalRule lr next⟩ := + by + rw [endNodesOf] + intro W W_endOF_Y + simp only [endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, + Subtype.exists] + use Y, Y_in_YS + have endsOfYnotSat : ∀ Y_1 : Finset Formula, Y_1 ∈ endNodesOf ⟨Y, ltY⟩ → ¬Satisfiable Y_1 := + by + intro W W_is_endOf_Y + apply endsOfXnotSat W (endNodesInclusion W W_is_endOf_Y) + aesop + case sim X X_is_simple => + apply endsOfXnotSat + unfold endNodesOf + simp + +theorem tableauThenNotSat : ∀ X, ClosedTableau X → ¬Satisfiable X := + by + intro X t + induction t + case loc Y ltY _ IH => + apply localTableauAndEndNodesUnsatThenNotSat ltY + intro Z ZisEndOfY + exact IH Z ZisEndOfY + case atm φ notBoxPhiInY Y_is_simple ltProYnPhi notSatProj => + rw [Lemma1_simple_sat_iff_all_projections_sat Y_is_simple] + simp + aesop + +-- Theorem 2, page 30 +theorem correctness : ∀ X, Satisfiable X → Consistent X := + by + intro X + contrapose + unfold Consistent + unfold Inconsistent + simp only [not_nonempty_iff, not_isEmpty_iff, not_exists, not_forall, exists_prop, Nonempty.forall] + intro hyp + apply tableauThenNotSat X hyp + +theorem soundTableau : ∀ φ, Provable φ → ¬Satisfiable ({~φ} : Finset Formula) := + by + intro phi + intro prov + cases' prov with _ tabl + apply tableauThenNotSat + assumption + +theorem soundness : ∀ φ, Provable φ → Tautology φ := + by + intro φ prov + apply notsatisfnotThenTaut + rw [← singletonSat_iff_sat] + apply soundTableau + exact prov diff --git a/Bml/Syntax.lean b/Bml/Syntax.lean new file mode 100644 index 0000000..156e57e --- /dev/null +++ b/Bml/Syntax.lean @@ -0,0 +1,96 @@ +-- SYNTAX +import Mathlib.Algebra.BigOperators.Basic +import Mathlib.Data.Finset.Basic + +-- Definition 1, page 4 +inductive Formula : Type + | bottom : Formula + | atom_prop : Char → Formula + | neg : Formula → Formula + | And : Formula → Formula → Formula + | box : Formula → Formula + deriving DecidableEq + +-- Predefined atomic propositions for convenience +def p := Formula.atom_prop 'p' +def q := Formula.atom_prop 'q' +def r := Formula.atom_prop 'r' + +notation "·" -- Notation and abbreviations +c => Formula.atom_prop c + +prefix:88 "~" => Formula.neg + +prefix:77 "□" => Formula.box + +infixr:66 "⋀" => Formula.And + +@[simp] +def impl (φ ψ : Formula) := ~(φ ⋀ ~ψ) + +infixr:55 "↣" => impl + +infixl:77 "⟷" => fun ϕ ψ => (ϕ↣ψ)⋀(ψ↣ϕ) + +@[simp] +instance : Bot Formula := + ⟨Formula.bottom⟩ + +instance : Top Formula := + ⟨Formula.neg Formula.bottom⟩ + +-- showing formulas as strings that are valid Lean code +def formToString : Formula → ℕ → Lean.Format + | ⊥, _ => "⊥" + | ·c, _ => "·" ++ repr c + | ~ϕ, n => "~" ++ formToString ϕ n + | ϕ⋀ψ, n => "(" ++ formToString ϕ n ++ " ⋀ " ++ formToString ψ n ++ ")" + | □ϕ, n => "(□ " ++ formToString ϕ n ++ ")" + +instance : Repr Formula := + ⟨formToString⟩ + +-- COMPLEXITY +-- this should later be the measure from Lemma 2, page 20 +@[simp] +def lengthOfFormula : Formula → ℕ + | ⊥ => 1 + | ·_ => 1 + | ~φ => 1 + lengthOfFormula φ + | φ⋀ψ => 1 + lengthOfFormula φ + lengthOfFormula ψ + | □φ => 1 + lengthOfFormula φ + +@[simp] +def lengthOfSet : Finset Formula → ℕ + | X => X.sum lengthOfFormula + +class HasLength (α : Type) where + lengthOf : α → ℕ + +open HasLength +@[simp] +instance formulaHasLength : HasLength Formula := ⟨lengthOfFormula⟩ +@[simp] +instance setFormulaHasLength : HasLength (Finset Formula) := ⟨lengthOfSet⟩ + +@[simp] +def complexityOfFormula : Formula → ℕ + | ⊥ => 1 + | ·_ => 1 + | ~φ => 1 + complexityOfFormula φ + | φ⋀ψ => 1 + max (complexityOfFormula φ) (complexityOfFormula ψ) + | □φ => 1 + complexityOfFormula φ + +def complexityOfSet : Finset Formula → ℕ + | X => X.sum complexityOfFormula + +class HasComplexity (α : Type) where + complexityOf : α → ℕ + +open HasComplexity + +instance formulaHasComplexity : HasComplexity Formula := + HasComplexity.mk complexityOfFormula + +instance setFormulaHasComplexity : HasComplexity (Finset Formula) := + HasComplexity.mk complexityOfSet diff --git a/Bml/Tableau.lean b/Bml/Tableau.lean new file mode 100644 index 0000000..00e1af0 --- /dev/null +++ b/Bml/Tableau.lean @@ -0,0 +1,367 @@ +-- TABLEAU + +import Mathlib.Algebra.BigOperators.Order +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Finset.PImage +import Mathlib.Order.WellFoundedSet +import Mathlib.Tactic.Ring + +import Bml.Syntax +import Bml.Semantics +import Bml.Setsimp + +open Formula + +open HasLength + +-- Definition 9, page 15 +-- A set X is closed iff 0 ∈ X or X contains a formula and its negation. +def Closed : Finset Formula → Prop := fun X => ⊥ ∈ X ∨ ∃ f ∈ X, ~f ∈ X + +-- A set X is simple iff all P ∈ X are (negated) atoms or [A]_ or ¬[A]_. +@[simp] +def SimpleForm : Formula → Bool + | ⊥ => True + | ~⊥ => True + | ·_ => True + | ~·_ => True + | □_ => True + | ~(□_) => True + | _ => False + +def Simple : Finset Formula → Bool + | X => ∀ P ∈ X, SimpleForm P + +-- Let X_A := { R | [A]R ∈ X }. +@[simp] +def formProjection : Formula → Option Formula + | □f => some f + | _ => none + +def projection : Finset Formula → Finset Formula + | X => X.biUnion fun x => (formProjection x).toFinset + +-- TODO @[simp] +theorem proj {g : Formula} {X : Finset Formula} : g ∈ projection X ↔ □g ∈ X := + by + rw [projection] + simp + constructor + · intro lhs + rcases lhs with ⟨boxg, boxg_in_X, projboxg_is_g⟩ + cases boxg + repeat' aesop + · intro rhs + use □g + +theorem projSet {X : Finset Formula} : ↑(projection X) = {ϕ | □ϕ ∈ X} := + by + ext1 + simp + exact proj + +theorem projection_length_leq : ∀ f, (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f := + by + intro f + cases f + · unfold projection; simp + · unfold projection; simp + · unfold projection; simp + · unfold projection; simp + case box f => + have subsubClaim : projection {□f} = {f} := by ext1; rw [proj]; simp + rw [subsubClaim] + simp + +theorem projection_set_length_leq : ∀ X, lengthOfSet (projection X) ≤ lengthOfSet X := + by + intro X + induction X using Finset.induction_on + · simp + case insert f S f_not_in_S IH => + unfold lengthOfSet + rw [Finset.sum_insert f_not_in_S] + simp + have insert_comm_proj : ∀ X f, projection (insert f X) = projection {f} ∪ projection X := + by + intro X f + unfold projection + ext1 g + simp + · + calc + (projection (insert f S)).sum lengthOfFormula = + (projection (insert f S)).sum lengthOfFormula := + refl _ + _ = (projection {f} ∪ projection S).sum lengthOfFormula := by rw [insert_comm_proj S f] + _ ≤ (projection {f}).sum lengthOfFormula + (projection S).sum lengthOfFormula := by + apply sum_union_le + _ ≤ lengthOfFormula f + (projection S).sum lengthOfFormula := by + simp only [add_le_add_iff_right, projection_length_leq] + _ ≤ lengthOfFormula f + S.sum lengthOfFormula := by simp; apply IH + +-- local rules: given this set, we get these sets as child nodes +inductive LocalRule : Finset Formula → Finset (Finset Formula) → Type + -- closing rules: + | bot {X} (h : ⊥ ∈ X) : LocalRule X ∅ + | Not {X ϕ} (h : ϕ ∈ X ∧ ~ϕ ∈ X) : LocalRule X ∅ + -- one-child rules: + | neg {X ϕ} (h : ~~ϕ ∈ X) : LocalRule X {X \ {~~ϕ} ∪ {ϕ}} + | Con {X ϕ ψ} (h : ϕ⋀ψ ∈ X) : LocalRule X {X \ {ϕ⋀ψ} ∪ {ϕ, ψ}} + -- splitting rule: + | nCo {X ϕ ψ} (h : ~(ϕ⋀ψ) ∈ X) : LocalRule X {X \ {~(ϕ⋀ψ)} ∪ {~ϕ}, X \ {~(ϕ⋀ψ)} ∪ {~ψ}} + +-- If X is not simple, then a local rule can be applied. +-- (page 13) +theorem notSimpleThenLocalRule {X} : ¬Simple X → ∃ B, Nonempty (LocalRule X B) := + by + intro notSimple + unfold Simple at notSimple + simp at notSimple + rcases notSimple with ⟨ϕ, ϕ_in_X, ϕ_not_simple⟩ + cases ϕ + case bottom => tauto + case atom_prop => tauto + case neg ψ => + cases ψ + case bottom => tauto + case atom_prop => tauto + case neg ψ => + use{X \ {~~ψ} ∪ {ψ}} + use LocalRule.neg ϕ_in_X + case And ψ1 ψ2 => + use{X \ {~(ψ1⋀ψ2)} ∪ {~ψ1}, X \ {~(ψ1⋀ψ2)} ∪ {~ψ2}} + use LocalRule.nCo ϕ_in_X + case box => tauto + case And ψ1 ψ2 => + use{X \ {ψ1⋀ψ2} ∪ {ψ1, ψ2}} + use LocalRule.Con ϕ_in_X + case box => tauto + +theorem localRulesDecreaseLength {X : Finset Formula} {B : Finset (Finset Formula)} + (r : LocalRule X B) : ∀ Y ∈ B, lengthOfSet Y < lengthOfSet X := + by + cases r + all_goals intro β inB; simp at * + case neg ϕ notnot_in_X => + subst inB + · + calc + lengthOfSet (insert ϕ (X.erase (~~ϕ))) ≤ lengthOfSet (X.erase (~~ϕ)) + lengthOf ϕ := by + apply lengthOf_insert_leq_plus + _ < lengthOfSet (X.erase (~~ϕ)) + lengthOf ϕ + 2 := by simp + _ = lengthOfSet (X.erase (~~ϕ)) + lengthOf (~~ϕ) := by simp; ring + _ = lengthOfSet X := lengthRemove X (~~ϕ) notnot_in_X + case Con ϕ ψ in_X => + subst inB + · + calc + lengthOf (insert ϕ (insert ψ (X.erase (ϕ⋀ψ)))) ≤ + lengthOf (insert ψ (X.erase (ϕ⋀ψ))) + lengthOf ϕ := + by apply lengthOf_insert_leq_plus + _ ≤ lengthOf (X.erase (ϕ⋀ψ)) + lengthOf ψ + lengthOf ϕ := by simp; apply lengthOf_insert_leq_plus + _ = lengthOf (X.erase (ϕ⋀ψ)) + lengthOf ϕ + lengthOf ψ := by ring + _ < lengthOf (X.erase (ϕ⋀ψ)) + lengthOf ϕ + lengthOf ψ + 1 := by simp + _ = lengthOf (X.erase (ϕ⋀ψ)) + lengthOf (ϕ⋀ψ) := by simp; ring + _ = lengthOfSet X := lengthRemove X (ϕ⋀ψ) in_X + case nCo ϕ ψ in_X => + cases inB + -- splitting rule! + case inl inB => -- f + subst inB + calc lengthOfSet (insert (~ϕ) (X.erase (~(ϕ⋀ψ)))) + ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~ϕ) := lengthOf_insert_leq_plus + _ < lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + (1 + lengthOf ϕ) := by simp + _ ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + (1 + lengthOf ϕ) + lengthOf ψ := by simp + _ = lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~(ϕ⋀ψ)) := by simp; ring + _ = lengthOfSet X := lengthRemove X (~(ϕ⋀ψ)) in_X + case inr inB => -- g + subst inB + calc lengthOfSet (insert (~ψ) (X.erase (~(ϕ⋀ψ)))) + ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~ψ) := lengthOf_insert_leq_plus + _ < lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + (1 + lengthOf ψ) := by simp + _ ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + lengthOf ϕ + (1 + lengthOf ψ) := by simp + _ = lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~(ϕ⋀ψ)) := by simp; ring + _ = lengthOfSet X := lengthRemove X (~(ϕ⋀ψ)) in_X + +theorem atmRuleDecreasesLength {X : Finset Formula} {ϕ} : + ~(□ϕ) ∈ X → lengthOfSet (projection X ∪ {~ϕ}) < lengthOfSet X := + by + intro notBoxPhi_in_X + simp + have otherClaim : projection X = projection (X.erase (~(□ϕ))) := + by + ext1 phi + rw [proj]; rw [proj] + simp + · + calc + lengthOfSet (insert (~ϕ) (projection X)) ≤ lengthOfSet (projection X) + lengthOf (~ϕ) := + lengthOf_insert_leq_plus + _ = lengthOfSet (projection X) + 1 + lengthOf ϕ := by simp; ring + _ < lengthOfSet (projection X) + 1 + 1 + lengthOf ϕ := by simp + _ = lengthOfSet (projection X) + lengthOf (~(□ϕ)) := by simp; ring + _ = lengthOfSet (projection (X.erase (~(□ϕ)))) + lengthOf (~(□ϕ)) := by rw [otherClaim] + _ ≤ lengthOfSet (X.erase (~(□ϕ))) + lengthOf (~(□ϕ)) := by simp; apply projection_set_length_leq + _ = lengthOfSet X := lengthRemove X (~(□ϕ)) notBoxPhi_in_X + +-- Definition 8, page 14 +-- mixed with Definition 11 (with all PDL stuff missing for now) +-- a local tableau for X, must be maximal +inductive LocalTableau : Finset Formula → Type + | byLocalRule {X B} (_ : LocalRule X B) (next : ∀ Y ∈ B, LocalTableau Y) : LocalTableau X + | sim {X} : Simple X → LocalTableau X + +open LocalTableau + +-- needed for endNodesOf +instance localTableauHasSizeof : SizeOf (Σ X, LocalTableau X) := + ⟨fun ⟨X, _⟩ => lengthOfSet X⟩ + +-- open end nodes of a given localTableau +@[simp] +def endNodesOf : (Σ X, LocalTableau X) → Finset (Finset Formula) + | ⟨X, @byLocalRule _ B lr next⟩ => + B.attach.biUnion fun ⟨Y, h⟩ => + have : lengthOfSet Y < lengthOfSet X := localRulesDecreaseLength lr Y h + endNodesOf ⟨Y, next Y h⟩ + | ⟨X, sim _⟩ => {X} + +@[simp] +theorem botNoEndNodes {X h n} : + endNodesOf ⟨X, LocalTableau.byLocalRule (@LocalRule.bot X h) n⟩ = ∅ := by unfold endNodesOf; simp + +@[simp] +theorem notNoEndNodes {X h ϕ n} : + endNodesOf ⟨X, LocalTableau.byLocalRule (@LocalRule.Not X h ϕ) n⟩ = ∅ := by unfold endNodesOf; simp + +theorem negEndNodes {X ϕ h n} : + endNodesOf ⟨X, LocalTableau.byLocalRule (@LocalRule.neg X ϕ h) n⟩ = + endNodesOf ⟨X \ {~~ϕ} ∪ {ϕ}, n (X \ {~~ϕ} ∪ {ϕ}) (by simp)⟩ := + by + ext1 + simp only [endNodesOf, Finset.mem_singleton, Finset.mem_biUnion, Finset.mem_attach, + exists_true_left, Subtype.exists] + constructor + · intro lhs; rcases lhs with ⟨b, bDef, bIn⟩; subst bDef; simp at *; exact bIn + · intro rhs; use X \ {~~ϕ} ∪ {ϕ}; constructor; simp at *; exact rhs; rfl + +theorem conEndNodes {X ϕ ψ h n} : + endNodesOf ⟨X, LocalTableau.byLocalRule (@LocalRule.Con X ϕ ψ h) n⟩ = + endNodesOf ⟨X \ {ϕ⋀ψ} ∪ {ϕ, ψ}, n (X \ {ϕ⋀ψ} ∪ {ϕ, ψ}) (by simp)⟩ := + by + ext1 + simp only [endNodesOf, Finset.mem_singleton, Finset.mem_biUnion, Finset.mem_attach, + exists_true_left, Subtype.exists] + constructor + · intro lhs; rcases lhs with ⟨b, bDef, bIn⟩; subst bDef; simp at *; exact bIn + · intro rhs; use X \ {ϕ⋀ψ} ∪ {ϕ, ψ}; constructor; simp at *; exact rhs; rfl + +theorem nCoEndNodes {X ϕ ψ h n} : + endNodesOf ⟨X, LocalTableau.byLocalRule (@LocalRule.nCo X ϕ ψ h) n⟩ = + endNodesOf ⟨X \ {~(ϕ⋀ψ)} ∪ {~ϕ}, n (X \ {~(ϕ⋀ψ)} ∪ {~ϕ}) (by simp)⟩ ∪ + endNodesOf ⟨X \ {~(ϕ⋀ψ)} ∪ {~ψ}, n (X \ {~(ϕ⋀ψ)} ∪ {~ψ}) (by simp)⟩ := + by + ext1 + simp only [endNodesOf, Finset.mem_singleton, Finset.mem_biUnion, Finset.mem_attach, + exists_true_left, Subtype.exists] + constructor + · intro lhs; rcases lhs with ⟨b, bDef, bIn⟩ + simp only [Finset.mem_insert, Finset.mem_singleton] at bDef ; cases' bDef with bD1 bD2 + · subst bD1; simp; left; simp at *; exact bIn + · subst bD2; simp; right; simp at *; exact bIn + · intro rhs; rw [Finset.mem_union] at rhs ; cases rhs + · use X \ {~(ϕ⋀ψ)} ∪ {~ϕ}; aesop + · use X \ {~(ϕ⋀ψ)} ∪ {~ψ}; aesop + +-- Definition 16, page 29 +inductive ClosedTableau : Finset Formula → Type + | loc {X} (lt : LocalTableau X) : (∀ Y ∈ endNodesOf ⟨X, lt⟩, ClosedTableau Y) → ClosedTableau X + | atm {X ϕ} : ~(□ϕ) ∈ X → Simple X → ClosedTableau (projection X ∪ {~ϕ}) → ClosedTableau X + +inductive Provable : Formula → Prop + | byTableau {φ : Formula} : ClosedTableau {~φ} → Provable φ + +-- Definition 17, page 30 +def Inconsistent : Finset Formula → Prop + | X => Nonempty (ClosedTableau X) + +def Consistent : Finset Formula → Prop + | X => ¬Inconsistent X + +def existsLocalTableauFor : ∀ N α, N = lengthOf α → Nonempty (LocalTableau α) := + by + intro N + induction N using Nat.strong_induction_on + case h n IH => + intro α nDef + have canApplyRule := em ¬∃ B, Nonempty (LocalRule α B) + cases canApplyRule + case inl canApplyRule => + constructor + apply LocalTableau.sim + by_contra hyp + have := notSimpleThenLocalRule hyp + tauto + case inr canApplyRule => + simp at canApplyRule + cases' canApplyRule with B r_exists + cases' r_exists with r + cases r + case bot h => + have t := LocalTableau.byLocalRule (LocalRule.bot h) ?_; use t + intro Y; intro Y_in_empty; tauto + case Not h => + have t := LocalTableau.byLocalRule (LocalRule.Not h) ?_; use t + intro Y; intro Y_in_empty; tauto + case neg f h => + have t := LocalTableau.byLocalRule (LocalRule.neg h) ?_; use t + intro Y Y_def + have rDec := localRulesDecreaseLength (LocalRule.neg h) Y Y_def + subst nDef + specialize IH (lengthOf Y) rDec Y (refl _) + apply Classical.choice IH + case Con f g h => + have t := LocalTableau.byLocalRule (LocalRule.Con h) ?_; use t + intro Y Y_def + have rDec := localRulesDecreaseLength (LocalRule.Con h) Y Y_def + subst nDef + specialize IH (lengthOf Y) rDec Y (refl _) + apply Classical.choice IH + case nCo f g h => + have t := LocalTableau.byLocalRule (LocalRule.nCo h) ?_; use t + intro Y Y_def + have rDec := localRulesDecreaseLength (LocalRule.nCo h) Y Y_def + subst nDef + specialize IH (lengthOf Y) rDec Y (refl _) + apply Classical.choice IH + +theorem endNodesOfLEQ {X Z ltX} : Z ∈ endNodesOf ⟨X, ltX⟩ → lengthOf Z ≤ lengthOf X := + by + induction ltX + case byLocalRule Y B lr next IH => + intro Z_endOf_Y + unfold endNodesOf at Z_endOf_Y + simp at Z_endOf_Y + rcases Z_endOf_Y with ⟨W, W_in_B, Z_endOf_W⟩ + apply le_of_lt + · + calc + lengthOf Z ≤ lengthOf W := IH W W_in_B Z_endOf_W + _ < lengthOf Y := localRulesDecreaseLength lr W W_in_B + case sim a b => + intro Z_endOf_Y + unfold endNodesOf at Z_endOf_Y + aesop + +theorem endNodesOfLocalRuleLT {X Z B next lr} : + Z ∈ endNodesOf ⟨X, @LocalTableau.byLocalRule _ B lr next⟩ → lengthOf Z < lengthOf X := + by + intro ZisEndNode + rw [endNodesOf] at ZisEndNode + simp at ZisEndNode + rcases ZisEndNode with ⟨a, a_in_WS, Z_endOf_a⟩ + change Z ∈ endNodesOf ⟨a, next a a_in_WS⟩ at Z_endOf_a + · calc + lengthOf Z ≤ lengthOf a := endNodesOfLEQ Z_endOf_a + _ < lengthOfSet X := localRulesDecreaseLength lr a a_in_WS diff --git a/Bml/Tableauexamples.lean b/Bml/Tableauexamples.lean new file mode 100644 index 0000000..2434b4e --- /dev/null +++ b/Bml/Tableauexamples.lean @@ -0,0 +1,144 @@ +-- TABLEAU-EXAMPLES + +import Mathlib.Data.Finset.Basic + +import Bml.Syntax +import Bml.Tableau + +theorem noBot : Provable (~⊥) := by + apply Provable.byTableau + apply ClosedTableau.loc + swap + · apply LocalTableau.byLocalRule (LocalRule.neg (Finset.mem_singleton.mpr (refl (~~⊥)))) + intro β inB + rw [Finset.sdiff_self] at inB + rw [Finset.empty_union] at inB + rw [Finset.mem_singleton] at inB + rw [inB] + apply LocalTableau.byLocalRule (LocalRule.bot (Finset.mem_singleton.mpr (refl ⊥))) + intro Y YinEmpty + aesop + · -- show that endNodesOf is empty + intro Y + intro YisEndNode + unfold endNodesOf at * + simp at * + exfalso + rcases YisEndNode with ⟨a, h, hyp⟩ + subst h + simp at * + +def emptyTableau : ∀ β : Finset Formula, β ∈ (∅ : Finset (Finset Formula)) → LocalTableau β := + by + intro beta b_in_empty + exact absurd b_in_empty (Finset.not_mem_empty beta) + +-- an example: +theorem noContradiction : Provable (~(p⋀~p)) := + by + apply Provable.byTableau + apply ClosedTableau.loc + swap + · apply LocalTableau.byLocalRule (@LocalRule.neg _ (p⋀~p) _) + -- neg: + intro β β_prop + simp at β_prop + subst β_prop + -- con: + apply LocalTableau.byLocalRule (@LocalRule.Con _ p (~p) _) + intro β2 β2_prop + simp at β2_prop + subst β2_prop + -- closed: + apply LocalTableau.byLocalRule (@LocalRule.Not _ p _) emptyTableau + all_goals aesop + · -- show that endNodesOf is empty + intro Y + intro YisEndNode + simp at * + exfalso + rcases YisEndNode with ⟨a, h, hyp⟩ + subst h + simp at * + rcases hyp with ⟨Y, Ydef, YinEndNodes⟩ + subst Ydef + aesop + +-- preparing example 2 +def subTabForEx2 : ClosedTableau {r, ~(□p), □(p⋀q)} := + by + apply @ClosedTableau.atm {r, ~(□p), □(p⋀q)} p (by simp) (by simp at *) + apply ClosedTableau.loc + rotate_left + -- con: + apply LocalTableau.byLocalRule (@LocalRule.Con {p⋀q, ~p} p q (by simp)) + intro child childDef + rw [Finset.mem_singleton] at childDef + -- not: + apply LocalTableau.byLocalRule (@LocalRule.Not _ p _) emptyTableau + · subst childDef; exact by decide + · -- show that endNodesOf is empty + intro Y + intro YisEndNode + simp at * + +-- Example 2 +example : ClosedTableau {r⋀~(□p), r↣□(p⋀q)} := + by + apply ClosedTableau.loc + rotate_left + · -- con + apply LocalTableau.byLocalRule + apply LocalRule.Con + simp only [impl, Finset.mem_insert, Finset.mem_singleton, or_false_iff] + constructor + intro branch branch_def + rw [Finset.mem_singleton] at branch_def + rw [Finset.union_insert] at branch_def + -- nCo + apply LocalTableau.byLocalRule + apply @LocalRule.nCo _ r (~(□(p⋀q))) + · rw [branch_def]; simp + intro b b_in + simp only [Finset.mem_insert, Finset.mem_singleton] at b_in + refine' if h1 : b = branch \ {~(r⋀~(□(p⋀q)))} ∪ {~r} then _ else _ + · -- right branch + -- not: + apply LocalTableau.byLocalRule (@LocalRule.Not _ r _) emptyTableau + aesop + · --left branch + have h2 : b = branch \ {~(r⋀~(□(p⋀q)))} ∪ {~~(□(p⋀q))} := by tauto + -- neg: + apply LocalTableau.byLocalRule (@LocalRule.neg _ (□(p⋀q)) _) + rotate_left; · rw [h2]; simp + intro child childDef + -- ending local tableau with a simple node: + apply LocalTableau.sim + rw [Finset.mem_singleton] at childDef + rw [childDef] + unfold Simple; simp at * + intro f f_notDef1 f_in_branch + cases b_in + · tauto + case inr b_in => + rw [b_in] at f_in_branch + simp at f_in_branch + cases f_in_branch + · tauto + case inr f_in_branch => + rw [branch_def] at f_in_branch + cases' f_in_branch with l r + aesop + · -- tableau for the simple end nodes: + rw [conEndNodes] + rw [nCoEndNodes] + intro Y Yin + simp at * + · -- notnotbranch + have Yis : Y = {r, ~(□p), □(p⋀q)} := by + subst Yin + ext1 + constructor <;> · intro hyp; aesop + subst Yis + exact subTabForEx2 + diff --git a/Bml/Vocabulary.lean b/Bml/Vocabulary.lean new file mode 100644 index 0000000..19bbbdc --- /dev/null +++ b/Bml/Vocabulary.lean @@ -0,0 +1,115 @@ +-- VOCABULARY + +import Mathlib.Tactic.NormNum + +import Bml.Syntax +import Bml.Setsimp + +@[simp] +def vocabOfFormula : Formula → Finset Char + | ⊥ => Set.toFinset { } + | ·c => {c} + | ~φ => vocabOfFormula φ + | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ + | □φ => vocabOfFormula φ + +@[simp] +def vocabOfSetFormula : Finset Formula → Finset Char + | X => Finset.biUnion X vocabOfFormula + +class HasVocabulary (α : Type) where + voc : α → Finset Char + +open HasVocabulary + +@[simp] +instance formulaHasVocabulary : HasVocabulary Formula := + HasVocabulary.mk vocabOfFormula + +@[simp] +instance setFormulaHasVocabulary : HasVocabulary (Finset Formula) := + HasVocabulary.mk vocabOfSetFormula + +@[simp] +theorem vocOfNeg {ϕ} : vocabOfFormula (~ϕ) = vocabOfFormula ϕ := by constructor + +theorem vocElem_subs_vocSet {ϕ X} : ϕ ∈ X → vocabOfFormula ϕ ⊆ vocabOfSetFormula X := + by + induction X using Finset.induction_on + -- case ∅: + case empty => + intro phi_in_X; + cases phi_in_X + case insert ψ S _ IH => + intro psi_in_insert + simp at * + intro a aIn + aesop + +theorem vocMonotone {X Y : Finset Formula} (hyp : X ⊆ Y) : voc X ⊆ voc Y := + by + unfold voc + simp at * + intro a aIn + unfold Finset.biUnion at * + intro p pIn + aesop + +theorem vocErase {X : Finset Formula} {ϕ : Formula} : voc (X \ {ϕ}) ⊆ voc X := + by + apply vocMonotone + rw [sdiff_singleton_is_erase] + intro a aIn + exact Finset.mem_of_mem_erase aIn + +theorem vocUnion {X Y : Finset Formula} : voc (X ∪ Y) = voc X ∪ voc Y := + by + simp + ext1 + aesop + +theorem vocPreserved (X : Finset Formula) (ψ ϕ) : + ψ ∈ X → voc ϕ = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ}) := + by + intro psi_in_X eq_voc + simp at * + ext1 + constructor + all_goals intro a_in + all_goals norm_num at * + · rcases a_in with ⟨θ, _, a_in_vocTheta⟩ + by_cases h : θ = ψ + · aesop + · aesop + · aesop + +theorem vocPreservedTwo {X : Finset Formula} (ψ ϕ1 ϕ2) : + ψ ∈ X → voc ({ϕ1, ϕ2} : Finset Formula) = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ1, ϕ2}) := + by + intro psi_in_X eq_voc + rw [vocUnion] + simp at * + ext1 + constructor + all_goals intro a_in; norm_num at * + · rcases a_in with ⟨θ, theta_in_X, a_in_vocTheta⟩ + by_cases h : θ = ψ + · right; subst h; unfold vocabOfSetFormula vocabOfFormula at *; simp at *; + rw [← eq_voc] at a_in_vocTheta ; simp at a_in_vocTheta ; tauto + · constructor + · use θ + cases a_in + · aesop + · use ψ; constructor + · aesop + · rw [← eq_voc]; simp; aesop + +theorem vocPreservedSub {X : Finset Formula} (ψ ϕ) : + ψ ∈ X → voc ϕ ⊆ voc ψ → voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X := + by + intro psi_in_X sub_voc + simp at * + intro a a_in; norm_num at * + cases a_in + · use ψ; rw [Finset.subset_iff] at sub_voc ; tauto + · aesop diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..261eeb9 --- /dev/null +++ b/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/Makefile b/Makefile index f906693..83a9cd1 100644 --- a/Makefile +++ b/Makefile @@ -2,6 +2,9 @@ default: .first-run-done lake build +bml: .first-run-done + lake build Bml + # https://leanprover-community.github.io/install/project.html#creating-a-lean-project .first-run-done: lake exe cache get diff --git a/lakefile.lean b/lakefile.lean index 433646d..ca0fda6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -10,3 +10,6 @@ require mathlib from git @[default_target] lean_lib «Pdl» where -- add any library configuration options here + +lean_lib «Bml» where + -- add any library configuration options here