feat(ModelTheory/Complexity): define literals

[metinersin]

Defines FirstOrder.Language.BoundedFormula.IsLiteral and FirstOrder.Language.BoundedFormula.simpleNot - an auxiliary operation that takes the negation of a formula and does some simplification.

---

• depends on: [Merged by Bors] - feat(ModelTheory/Equivalence): Implication of formulas modulo a theory #16800

[github-actions]

PR summary 96ffb83c8b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsAtomic.isLiteral
+ IsAtomic.simpleNot_eq_not
+ IsAtomic.simpleNot_not
+ IsLiteral
+ IsLiteral.simpleNot
+ inf
+ inf_sup_left_iff
+ inf_sup_right_iff
+ not_all_iff_ex_not
+ not_ex_iff_all_not
+ not_inf_iff_sup_not
+ not_sup_iff_inf_not
+ realize_falsum
+ realize_simpleNot
+ simpleNot
+ simpleNot_iff_not
+ sup
+ sup_inf_left_iff
+ sup_inf_right_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[awainverse]

Rather than defining simpleNotAux as having values in {ψ : L.BoundedFormula α n // ψ ⇔[∅] ∼φ},
I feel like it might be simpler to just define simpleNot directly, and then prove simpleNot_semanticallyEquivalent_not by induction. (This is how I defined toPrenex.)

At least - I think it might be easier to use, once simpleNot becomes a recursive definition, instead of the first part of a recursive definition, but clearly this way is compatible with your subsequent work, so it may be subjective.

[metinersin]

Rather than defining simpleNotAux as having values in {ψ : L.BoundedFormula α n // ψ ⇔[∅] ∼φ}, I feel like it might be simpler to just define simpleNot directly, and then prove simpleNot_semanticallyEquivalent_not by induction. (This is how I defined toPrenex.)

At least - I think it might be easier to use, once simpleNot becomes a recursive definition, instead of the first part of a recursive definition, but clearly this way is compatible with your subsequent work, so it may be subjective.

I agree. Defining simpleNot directly is more beautiful. I did it this way because the match pattern inside it was a little more complicated originally, and the split tactic did not work against it. I will update the code.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(ModelTheory/Equivalence): Implication of formulas modulo a theory #16800
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

What's the point of this change?

[metinersin]

I defined separate sup and inf functions with a match_pattern tag to be able to use sup φ ψ and inf φ ψ inside match in the definition of simpleNot. Do you know how to make the expressions φ ⊔ ψ and φ ⊓ ψ matchable?