Summary.v 5.18 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
(* pretty printing for coqdoc *)
(** printing ->> $ \Rightarrow$ #⇒#*)
(** printing <<->> $ \Leftrightarrow $ #&hArr;#*)
(** printing |[]| $\square$ #&#x25A1;#*)
(** printing (|[]| $(\square$ #&#x25A1;#*)
(** printing -! $\neg$ #&not;#*)
(** printing (-! $(\neg$ #&not;#*)
(** printing -+! $\neg\neg$  #&not;&not;#*)
(** printing (-+! $(\neg\neg$ #&not;&not;#*)
(** printing & $\wedge$ #&and;#*)
(** printing ||| $\lor$ #&or;# *)
(** printing tt $\top$ #&#8868;# *)
(** printing ff $\bot$ #&#8869;# *)



(**
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
31 32
      deduction system for the intuitionistic modal logic, [weakening], [not_intro]
      and [not_elim] (compare the part about negations). It is widely used throughout
33 34 35 36 37
      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.
38
     Additionally, they also include important double negation theorems
Miriam Polzer's avatar
Miriam Polzer committed
39 40
		   from Oliva & Ferreira ([[DNEG]]) and congruence for implication,
				   conjunction and disjunction respectively.  Using these
41
				   databases, we could shorten proofs involving only simple
Miriam Polzer's avatar
Miriam Polzer committed
42
				   equivalences about double negations.
43 44 45 46 47 48 49 50 51 52 53 54


   - [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
Miriam Polzer's avatar
Miriam Polzer committed
55 56 57
- [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.
58 59

** Apply Simple Rewrites
Miriam Polzer's avatar
Miriam Polzer committed
60 61
- [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, 
62
    e.g. [permute_context perm_takeit_6] will flip the context's first two elements.
Miriam Polzer's avatar
Miriam Polzer committed
63 64
- [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 
65
    by building implications
Miriam Polzer's avatar
Miriam Polzer committed
66
- [create_imp n] - creates n implications in the goal by using [eapply KIbox_impE]. 
67 68
    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].
Miriam Polzer's avatar
Miriam Polzer committed
69
- [solve_simpl_box B] - can be applied if we want to prove [KIbox Z G |[]| A], [|[]| B] 
70 71 72
    is contained in [G] and we know that [KIbox Z [B] A] holds.

** Proof by Contradiction
Miriam Polzer's avatar
Miriam Polzer committed
73 74
- [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.
75

76
** KIbox Implication and Equivalence
Miriam Polzer's avatar
Miriam Polzer committed
77 78 79
- [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 
80
    the form [X ->> Y].
Miriam Polzer's avatar
Miriam Polzer committed
81 82 83 84
- [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]. 
85
    We can use both directions.
86 87 88 89

* 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
Miriam Polzer's avatar
Miriam Polzer committed
90
-[[RUI]] Tadeusz Litak's formalization of W. Ruitenburg JSL 1984 paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus"
91 92
-[[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.
litak's avatar
litak committed
93
-[[DNM]] our manuscript "Negative Translations and Normal Modality"
94

95
*)