Sat.Fmla.reify_one
theorem Sat.Fmla.reify_one :
∀ {v : Sat.Valuation} {c : Sat.Clause} {a : Prop}, Sat.Clause.reify v c a → Sat.Fmla.reify v (Sat.Fmla.one c) a
The theorem `Sat.Fmla.reify_one` states that for any valuation `v`, clause `c`, and proposition `a`, if `a` is the reification of `c` under `v`, then `a` is also the reification of a single clause formula where `c` is the only clause, again under `v`. Here, a "reification" represents the process of turning an abstract concept into something concrete or turning a list of literals into a proposition. In other words, if a proposition `a` can be obtained by assigning truth values to the literals in clause `c` according to valuation `v`, then the same proposition `a` can also be obtained by treating the clause `c` as a single clause formula and applying the same valuation `v`.
More concisely: For any valuation `v`, if proposition `a` is the reification of clause `c`, then there exists a single-clause formula `b` such that `a` is the reification of `b` under `v` and `c` is the only clause in `b`.
|
Sat.Clause.reify_and
theorem Sat.Clause.reify_and :
∀ {v : Sat.Valuation} {l : Sat.Literal} {a : Prop} {c : Sat.Clause} {b : Prop},
Sat.Literal.reify v l a → Sat.Clause.reify v c b → Sat.Clause.reify v (Sat.Clause.cons l c) (a ∧ b)
The theorem `Sat.Clause.reify_and` states that for any given valuation `v`, literal `l`, proposition `a`, clause `c`, and proposition `b`, if the reification of the literal `l` under valuation `v` is equal to the proposition `a` and the reification of clause `c` under valuation `v` is equal to the proposition `b`, then the reification of the clause obtained by appending `l` to `c` under the same valuation `v` is equal to the conjunction of propositions `a` and `b`. This theorem demonstrates the behavior of negation in the context of propositional logic, specifically how it turns disjunctions (OR operations) into conjunctions (AND operations).
More concisely: For any valuation `v`, if literal `l` reifies to proposition `a` under `v` and clause `c` reifies to proposition `b` under `v`, then the reification of the clause obtained by appending `l` to `c` under `v` is equal to the conjunction of propositions `a` and `b`.
|
Sat.Fmla.reify_or
theorem Sat.Fmla.reify_or :
∀ {v : Sat.Valuation} {f₁ : Sat.Fmla} {a : Prop} {f₂ : Sat.Fmla} {b : Prop},
Sat.Fmla.reify v f₁ a → Sat.Fmla.reify v f₂ b → Sat.Fmla.reify v (f₁.and f₂) (a ∨ b)
This theorem states that for any valuation `v`, two formulas `f₁` and `f₂`, and two propositions `a` and `b`, if the valuation reifies `f₁` into `a` and `f₂` into `b`, then the valuation also reifies the conjunction (the 'and' operation) of `f₁` and `f₂` into the disjunction (the 'or' operation) of `a` and `b`. In other words, the negation operation turns 'and' into 'or' when reifying formulas, i.e., `¬⟦f₁ ∧ f₂⟧_v ≡ ¬⟦f₁⟧_v ∨ ¬⟦f₂⟧_v`.
More concisely: For any valuation `v`, the negation of the conjunction of formulas `f₁` and `f₂` under `v` is logically equivalent to the disjunction of the negations of `f₁` and `f₂` under `v`.
|
Sat.Clause.reify_zero
theorem Sat.Clause.reify_zero : ∀ {v : Sat.Valuation}, Sat.Clause.reify v Sat.Clause.nil True
This theorem states that the reification of an empty clause under any given valuation is `True`. In other words, the negation of the reification of an empty clause, represented as `¬⟦⊥⟧_v`, is always equivalent to `True` under any valuation `v`, where a valuation is a mapping that assigns truth values to all propositional variables.
More concisely: The reification of an empty clause is always true under all valuations. (In Lean: `∀ v, ¬⟦⊥⟧_v = true`)
|
Sat.Fmla.refute
theorem Sat.Fmla.refute :
∀ {p : Prop} {ps : List Prop} (f : Sat.Fmla),
f.proof [] → (∀ (v : Sat.Valuation), v.implies (Sat.Fmla.reify v f p) ps 0) → p
The theorem `Sat.Fmla.refute` states that for any propositional variable `p`, list of propositions `ps`, and formula `f` (which is a list of clauses), if `f` is unsatisfiable and every valuation `v` that is consistent with `ps` implies that the negation of the interpretation of `f` under `v` implies `p`, then `p` is true. Equivalently, this can be seen as stating that there exists a valuation `v` that is consistent with `ps`, and for each such valuation, the interpretation of `f` under `v` is false because `f` is unsatisfiable.
More concisely: If a list of clauses `f` is unsatisfiable and for every consistent valuation `v` with respect to `ps`, the interpretation of `f` under `v` implies the negation of `p`, then `p` is true.
|
Sat.Valuation.by_cases
theorem Sat.Valuation.by_cases :
∀ {v : Sat.Valuation} {l : Sat.Literal}, (v.neg l.negate → False) → (v.neg l → False) → False
The theorem `Sat.Valuation.by_cases` represents the core unit-propagation step in propositional logic. Given a valuation `v` and a literal `l`, it states that if assuming the negation of the negation of `l` (i.e., `l` itself) falsifies our model, and similarly, assuming the negation of `l` also falsifies our model, then we derive a contradiction (`False`). This situation typically arises when we have a clause in the global context such that all literals in the clause are falsified except for the negation of `l`. If we suppose that the negation of `l` is also falsified, then the entire clause is falsified, leading to a contradiction.
More concisely: If a valuation falsifies both a literal and its negation, then we have a contradiction.
|
Sat.Clause.reify_one
theorem Sat.Clause.reify_one :
∀ {v : Sat.Valuation} {l : Sat.Literal} {a : Prop},
Sat.Literal.reify v l a → Sat.Clause.reify v (Sat.Clause.cons l Sat.Clause.nil) a
This theorem, `Sat.Clause.reify_one`, states that for any valuation `v`, literal `l` and a proposition `a`, if `a` is the reification of the literal `l` under the valuation `v` (denoted as `Sat.Literal.reify v l a`), then `a` is also the reification of a clause consisting of only `l` under the same valuation `v` (denoted as `Sat.Clause.reify v (Sat.Clause.cons l Sat.Clause.nil) a`). In simpler terms, the proposition `a` that represents the truth value of a literal `l` under a given valuation `v` also represents the truth value of a clause that contains only `l` under the same valuation.
More concisely: For any valuation `v`, if a literal `l` maps to proposition `a` (Sat.Literal.reify v l a), then the clause consisting of only `l` maps to `a` under `v` (Sat.Clause.reify v (Sat.Clause.cons l Sat.Clause.nil) a).
|
Sat.Literal.reify_neg
theorem Sat.Literal.reify_neg :
∀ {v : Sat.Valuation} {a : Prop} {n : ℕ}, (v n ↔ a) → Sat.Literal.reify v (Sat.Literal.neg n) a
The theorem `Sat.Literal.reify_neg` states that for any valuation `v`, propositional variable `a`, and natural number `n`, if `v n` is equivalent to `a`, then the reification of a negative literal in the context of this valuation `v` and `n` equals to `a`. In other words, it asserts that the valuation of the negation of a negated propositional variable is equivalent to the valuation of the propositional variable itself, under the given valuation `v`. It is essentially an instantiation of the principle of double negation in propositional logic within the framework of valuations and literals in Lean.
More concisely: For any valuation `v`, propositional variable `a`, and natural number `n`, if `v n` is equal to `a`, then the reification of the negation of `a` is equal to `a`.
|
Sat.Literal.reify_pos
theorem Sat.Literal.reify_pos :
∀ {v : Sat.Valuation} {a : Prop} {n : ℕ}, (v n ↔ a) → Sat.Literal.reify v (Sat.Literal.pos n) ¬a
The theorem `Sat.Literal.reify_pos` states that for any valuation `v` of type `Sat.Valuation`, any proposition `a`, and any natural number `n`, if the valuation `v` of `n` is equivalent to the proposition `a` (`v n ↔ a`), then the reification of a positive literal represented by `n` in the valuation `v` is the negation of `a` (`¬a`). Here, reification is the process of turning an abstract concept into something concrete or tangible. In this context, it means representing a propositional variable as a specific proposition.
More concisely: For any valuation `v`, proposition `a`, and natural number `n`, if `v(n) ≤f/>= a` then `∥v.reify (Sat.Pos.mk n) = ¬a`. (Here, `∥_∥` represents the reification function and `Sat.Pos.mk n` represents the positive literal represented by the natural number `n`.)
|
Sat.Fmla.proof_of_subsumes
theorem Sat.Fmla.proof_of_subsumes : ∀ {f : Sat.Fmla} {c : Sat.Clause}, f.subsumes (Sat.Fmla.one c) → f.proof c := by
sorry
The theorem `Sat.Fmla.proof_of_subsumes` states that if a formula `f` subsumes a clause `c` (in other words, if `c` is an element of `f`), then `f` has a proof for `c`. Here, a formula is a list of clauses, where each clause is seen as a disjunction of literals (like `a ∨ b ∨ ¬c`), and the entire formula is seen as a conjunction of these clauses (like `(a ∨ b) ∧ c ∧ (¬c ∨ ¬d)`). The term "subsumes" essentially means that the clause is part of the formula.
More concisely: If a formula `f` contains a clause `c` as a subcomponent, then `c` has a proof in the context of `f`.
|
Sat.Valuation.mk_implies
theorem Sat.Valuation.mk_implies :
∀ {p : Prop} {as ps : List Prop} (as₁ : List Prop),
as = as₁.reverseAux ps → (Sat.Valuation.mk as).implies p ps as₁.length → p
"The theorem `Sat.Valuation.mk_implies` states the fundamental relationship between the `mk` and `implies` operations in the `Sat.Valuation` type. Specifically, for any proposition `p` and any lists of propositions `as`, `ps`, and `as₁`, if `as` equals the result of reversing `as₁` and appending `ps`, then the result of applying `implies` to the valuation created from `as` with `p`, `ps`, and the length of `as₁`, is equivalent to `p` itself."
More concisely: If `as` is the reversed appending of `as₁` and `ps`, then `mk (as : list Prop) p ps (length as₁).val = p`.
|