(* pretty printing for coqdoc *)
(** printing ->> $ \Rightarrow$ #⇒#*)
(** printing <<->> $ \Leftrightarrow $ #⇔#*)
(** printing |[]| $\square$ #□#*)
(** printing (|[]| $(\square$ #□#*)
(** printing -! $\neg$ #¬#*)
(** printing (-! $(\neg$ #¬#*)
(** printing -+! $\neg\neg$ #¬¬#*)
(** printing (-+! $(\neg\neg$ #¬¬#*)
(** printing & $\wedge$ #∧#*)
(** printing ||| $\lor$ #∨# *)
(** printing tt $\top$ #⊤# *)
(** printing ff $\bot$ #⊥# *)
(**
This file does not contain any coq code. It is an overview of the dnegmod project. We provide a sorted table of contents, only relevant for HTML readers. Additionally we give a summary of the introduced tactics and auto libraries and list our references.
* Contents
- [IntModalSetup] - definition of formulas with box and substitutions
- [KIbox_NaturalDeduction] - natural deduction for intuitionistic normal modal logic with box
- [KIbox_Rules] - rules and tautologies for syntactic proofs
- [DNTrans] - translations between intuitionistic and classical setup
* Hint Databases
The formalization contains a couple of hint databases, which are briefly explained here.
- [KIboxDB]: This database includes the constructors of the natural
deduction system for the intuitionistic modal logic, [weakening], [not_intro]
and [not_elim] (compare the part about negations). It is widely used throughout
this work mostly with a limiting number of steps (often 3, sometimes 4).
- [eq_impDB, eq_andDB, eq_orDB]: These three all contain the fact that
equality is symmetric, transitive and monotonic by double negation.
Additionally, they also include important double negation theorems
from Oliva & Ferreira ([[DNEG]]) and congruence for implication,
conjunction and disjunction respectively. Using these
databases, we could shorten proofs involving only simple
equivalences about double negations.
- [eq_triangle]: Also includes that equality is symmetric, transitive and
monotonic by double negation and additionally the equivalence of the three
negative translations (kur, ggr, kol). It is often used to prove that
corollaries are also valid for the other translations.
* Tactics
This section provides an overview of the tactics defined throughout the project.
** Solve Trivial Goals
- [contained A] - solves goals of the form [KIbox Z G A] where [A] is contained in the context [G].
- [perm_contained] - applies permutation and containment rules to solve simple goals.
- [stronger_assumption] - looks for an assumption with the same formula but weaker context.
** Apply Simple Rewrites
- [introduce_KIbox] - applies the introduction rules of KIbox (apart from or introduction) exhaustively.
- [permute_context H] - permutes the goals context using the given permutation lemma,
e.g. [permute_context perm_takeit_6] will flip the context's first two elements.
- [push_left, push_left_in H] - exhaustively push implication antecedents into the context.
- [push_right, push_right_in H] - exhaustively push the context into the formula to be proven
by building implications
- [create_imp n] - creates n implications in the goal by using [eapply KIbox_impE].
For example if we have a goal of the form [KIbox Z G A], [create_imp 1]
will lead to the goals [KIbox Z G ?1 -> A] and [KIbox Z G ?1].
- [solve_simpl_box B] - can be applied if we want to prove [KIbox Z G |[]| A], [|[]| B]
is contained in [G] and we know that [KIbox Z [B] A] holds.
** Proof by Contradiction
- [context_contradiction A] - proves goal if the context contains [A] and [-! A].
- [elim_false A] - prove bottom by contradiction via [A] and [-! A]. [-! A] should be in the context before applying this tactic. [A] is left to prove afterwards.
** KIbox Implication and Equivalence
- [apply_imp H] - uses implication [H] on the goal.
- [apply_imp_ass] - is similar to [apply_imp], but searches in the current assumptions for an implication.
- [context_mp_closed X Y] - applies modus ponens in the context using an implication of
the form [X ->> Y].
- [eq_dest H] - destructs an equivalence in H.
- [eq_split] - proves an equivalence by splitting into both directions.
- [eq_rewrite1 H, eq_rewrite2 H] - rewrites the goal using equivalence [H], two directions are possible.
- [eq_trans1 H, eq_trans2 H] - transitively rewrites an equivalence goal with equivalence [H].
We can use both directions.
* References
-[[DNEG]] Ferreira, Gilda, and Paulo Oliva. "On various negative translations." arXiv preprint arXiv:1101.5442 (2011).
-[[IPC]] Hara, Masaki "Intuitionistic Propositional Calculus" https://github.com/qnighy/IPC-Coq
-[[RUI]] Tadeusz Litak's formalization of W. Ruitenburg JSL 1984 paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus"
-[[CMP]] Litak, Tadeusz. "Constructive modalities with provability smack." Leo Esakia on Duality in Modal and Intuitionistic Logics. Springer Netherlands, 2014. 187-216.
-[[CML]] Bellin, Gianluigi, Valeria De Paiva, and Eike Ritter. "Extended Curry-Howard correspondence for a basic constructive modal logic." In Proceedings of Methods for Modalities. 2001.
-[[DNM]] our manuscript "Negative Translations and Normal Modality"
*)