Theorem: projection_set_length_leq (Bml/Tableau.lean)

State before:
⊢ ∀ (X : Finset Formula), lengthOfSet (projection X) ≤ lengthOfSet X
Tactic:
intro X
State after:
X : Finset Formula
⊢ lengthOfSet (projection X) ≤ lengthOfSet X

State before:
X : Finset Formula
⊢ lengthOfSet (projection X) ≤ lengthOfSet X
Tactic:
induction X using Finset.induction_on
State after:
case empty

⊢ lengthOfSet (projection ∅) ≤ lengthOfSet ∅

case insert
a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : lengthOfSet (projection s✝) ≤ lengthOfSet s✝
⊢ lengthOfSet (projection (insert a✝² s✝)) ≤ lengthOfSet (insert a✝² s✝)

State before:
case empty

⊢ lengthOfSet (projection ∅) ≤ lengthOfSet ∅
Tactic:
simp [projection]
State after:
no goals

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ lengthOfSet (projection (insert f S)) ≤ lengthOfSet (insert f S)
Tactic:
unfold lengthOfSet
State after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    let X := insert f S;
    X.sum lengthOfFormula

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    let X := insert f S;
    X.sum lengthOfFormula
Tactic:
rw [Finset.sum_insert f_not_in_S]
State after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x
Tactic:
have insert_comm_proj : ∀ X f, projection (insert f X) = projection {f} ∪ projection X :=
  by
  intro X f
  unfold projection
  simp
State after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
Tactic:
intro X f
State after:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ projection (insert f X) = projection {f} ∪ projection X

State before:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ projection (insert f X) = projection {f} ∪ projection X
Tactic:
unfold projection
State after:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ (let X := insert f X;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := {f};
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset

State before:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ (let X := insert f X;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := {f};
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset
Tactic:
simp
State after:
no goals

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x
Tactic:
calc
  (projection (insert f S)).sum lengthOfFormula
    = (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
State after:
no goals

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection (insert f S)).sum lengthOfFormula = (projection {f} ∪ projection S).sum lengthOfFormula
Tactic:
rw [insert_comm_proj S f]
State after:
no goals

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection {f} ∪ projection S).sum lengthOfFormula ≤
    (projection {f}).sum lengthOfFormula + (projection S).sum lengthOfFormula
Tactic:
apply sum_union_le
State after:
no goals

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection {f}).sum lengthOfFormula + (projection S).sum lengthOfFormula ≤
    lengthOfFormula f + (projection S).sum lengthOfFormula
Tactic:
simp only [add_le_add_iff_right, projection_length_leq]
State after:
no goals

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ lengthOfFormula f + (projection S).sum lengthOfFormula ≤ lengthOfFormula f + S.sum lengthOfFormula
Tactic:
simp
State after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection S).sum lengthOfFormula ≤ S.sum lengthOfFormula

State before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection S).sum lengthOfFormula ≤ S.sum lengthOfFormula
Tactic:
apply IH
State after:
no goals