Commit 3d92ffa5 authored by Miriam Polzer's avatar Miriam Polzer

spellchecked everyhting

parent 040720ba
......@@ -151,7 +151,7 @@ Corollary ggr_dneg_eq_con : forall Z G f, KIbox Z G (ggr f) <-> KIbox Z G (-+! g
Qed.
(** * Definition of Restrictions on Formulas *)
(** Here comes a first try at restricting formulas. Our goal is to prove that for certain axioms the double negation translations are adequate. As shown in the ALCOP slides, this does not hold for all axioms. It later turned out that the following definitions were more restrictive than necessary (TODO Ulrich, is that correct?) and we introduced a concept called "envelopes", see further down. *)
(** Now we introduce restrictions on formulas. Our goal is to prove that for certain axioms the double negation translations behave as expected. As shown in [[DNM]], this does not hold for all axioms. We will later show that they hold for formulas fulfilling some of the following properties. *)
Fixpoint box_free (f : form) : Prop :=
match f with
......@@ -203,32 +203,15 @@ Fixpoint dis_free_under_box (f : form) : Prop :=
| _ => True
end.
Definition sub_vars_dneg (A : form) := sub (fun n => -+! var n) A.
Lemma sub_vars_dneg_eq:
forall G Z f, box_free f -> disjunction_free f ->
KIbox Z G ((sub_vars_dneg f) <<->> -+! (sub_vars_dneg f)).
Proof.
induction f; unfold sub_vars_dneg; intros; simpl; try inversion H; try inversion H0.
- apply eq_split; split. apply imp_dneg.
apply imp_contrapos. apply imp_dneg.
- eauto with eq_impDB.
- eauto with eq_andDB.
- apply tt_dneg.
- apply ff_dneg.
Qed.
(** * Towards Theorem 5 *)
(** This sections defines KClbox, which is simply an extension of KIbox by the axiom
([-+! p ->> p]), and introduces the notion of adequateness. A translation for a logic
definied by given axiom is adequate if the translation of a formula holds
intuitionstically iff the original formula holds classically. We show that
defined by given axiom is adequate if the translation of a formula holds
intuitionistically iff the original formula holds classically. We show that
adequateness is equivalent for the translations in the triangle and that
a system extended by an axiom is adequate iff the translation of the axioms holds
intuitionstically.
intuitionistically.
After that, we introduce the notion of envelopes to capture the properties,
axioms are required to have, in order to ensure adequateness of the resulting system.
......@@ -482,6 +465,8 @@ Qed.
Note the small difference between ¬¬- and Kuroda-envelopes.
*)
Definition sub_vars_dneg (A : form) := sub (fun n => -+! var n) A.
Definition pre_envelope (A : form) :=
forall Z, KIbox Z [] (-+! (sub_vars_dneg A) ->> (kol A)).
......@@ -509,13 +494,22 @@ Qed.
(** ** Lemma 4 from the corrected ALCOP slides *)
(** Here are concrete examples of envelopes.
ggr_sub_vars_dneg is an old result, which we tried to use before we introduced the
concept of envelopes. We reused it in order to show that certain
formulas are envelopes.
(** Following are concrete examples of envelopes. We first tried to prove adequateness without envelopes, but it turned out our restrictions were stronger than necessary. Still they are relevant for practical purpose and we will now show that our results apply to them as well.
*)
Lemma sub_vars_dneg_eq:
forall G Z f, box_free f -> disjunction_free f ->
KIbox Z G ((sub_vars_dneg f) <<->> -+! (sub_vars_dneg f)).
Proof.
induction f; unfold sub_vars_dneg; intros; simpl; try inversion H; try inversion H0.
- apply eq_split; split. apply imp_dneg.
apply imp_contrapos. apply imp_dneg.
- eauto with eq_impDB.
- eauto with eq_andDB.
- apply tt_dneg.
- apply ff_dneg.
Qed.
Lemma ggr_sub_vars_dneg:
forall Z f, (box_free f \/ (shallow f /\ dis_free_under_box f)) ->
KIbox Z [] ((ggr f) <<->> -+! (sub_vars_dneg f)).
......@@ -615,7 +609,7 @@ Qed.
(** ** Theorem 5 from ALCOP slides *)
(** Axioms of the form ([B ->> C], where B is a post-envelope and C a pre-envelope,
(** Axioms of the form [(B ->> C)], where B is a post-envelope and C a pre-envelope,
form a adequate system. Kuroda- and ¬¬-envelopes also guarantee adequateness.
*)
......
......@@ -15,7 +15,7 @@
(**
This file contains the definition of formulas with box and a section for substitutions.
Its content is partly taken from Tadeusz Litak's formalisation of W. Ruitenburg JSL 1984 paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" [[RUI]].
Its content is partly taken from Tadeusz Litak's formalization of W. Ruitenburg JSL 1984 paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" [[RUI]].
Note that there is an additional summary file. It explains all tactics and hint databases and contains the references pointed to by [[REF]].
*)
......@@ -35,7 +35,7 @@ Inductive form :=
(* These notations have to sit strictly between level 80 (precendence of /\)
(* These notations have to sit strictly between level 80 (precedence of /\)
and level 70 (precedence of =). *)
(*Infix "|--" := hil (at level 80, no associativity).*)
Infix "&" := and (at level 75, right associativity).
......
......@@ -21,11 +21,11 @@ Require Export Coq.Program.Equality.
(** This file contains a natural deduction system for intuitionistic normal modal logics IK [] with axioms.
We first define this system and then prove that it is in fact an intuitionistic normal modal logic. In the last section we validite 'standard' structural rules, e.g. contraction. *)
We first define this system and then prove that it is in fact an intuitionistic normal modal logic. In the last section we validate 'standard' structural rules, e.g. contraction. *)
(** * Definition *)
(** Definition of [KIbox] corresponds to page 5 in [[CML]].
It is a natural deduction system for intuitionistic normal modal logics based on the modal logic K. We use only one modal operator, box. Adding diamond is possible, but not straightforward since box and diamond are not dual in KI (/IK).TODO: explain more of KIbox here?
It is a natural deduction system for intuitionistic normal modal logics based on the modal logic K. We use only one modal operator, box. Adding diamond is possible, but not straightforward since box and diamond are not dual in KI (/IK).
We usually denote axioms with [Z], the context with [G] and formulas with upper case letters starting from [A] or [f] and subscripts. [KIbox Z G f] means that in a logic with axiom [Z], [f] holds under the assumptions of list [G].*)
......@@ -61,11 +61,11 @@ Ltac introduce_KIbox := repeat (match goal with
| [|- KIbox _ (ff :: _) _] => apply KIbox_ffE
end).
(** %\noindent% [contained] solves context containment goals using datatype automatization. *)
(** %\noindent% [contained] solves context containment goals using datatype automatizing. *)
Ltac contained C:= solve [eapply KIbox_axiomIn with (f := C); auto with datatypes].
(** %\noindent% This tacitc permutes the context using the given permutation lemma e.g. [permute_context perm_takeit_6] will switch the first two elements. *)
(** %\noindent% This tactic permutes the context using the given permutation lemma e.g. [permute_context perm_takeit_6] will switch the first two elements. *)
Ltac permute_context H := eapply KIbox_perm; [idtac | apply H].
......@@ -82,7 +82,7 @@ Ltac perm_contained :=
Hint Extern 3 => perm_contained.
Hint Extern 3 => perm.
(** * KIbox is Intuitionistic Mormal Modal Logic *)
(** * KIbox is Intuitionistic Normal Modal Logic *)
(** %\noindent% Closure under substitution *)
......
......@@ -24,7 +24,7 @@ Require Export dnegmod.KIbox_NaturalDeduction.
Ltac push_left := repeat (apply KIbox_impI).
Ltac push_right_in H := repeat (apply KIbox_impI in H).
(** %\noindent% TODO Ulrich *)
(** %\noindent% The [elim_false] tactic proves bottom by contradiction via [A] and [-! A]. [-! A] should be in the context before applying this tactic. [A] is left to prove afterwards. *)
Ltac elim_false A := apply KIbox_impE with (f1 := A); try contained (-! A);
try apply KIbox_impI.
......@@ -751,19 +751,12 @@ Qed.
(** * Map *)
(** TODO Ulrich *)
Ltac elim_f f I :=
repeat match goal with
| [H: KIbox _ (map f _) (f ?f) |- _ ] => eapply eq_ded in H; try (apply eq_sym; apply I)
| |- KIbox _ (map f _) ?f => eapply eq_ded; [ apply I | auto 0]
end.
Lemma map_eq:
forall Z G B f, (forall A G', KIbox Z G' (A <<->> f A)) ->
(KIbox Z (map f G) B -> KIbox Z G B).
Proof.
intros Z G B f H1 H2.
dependent induction G; elim_f f H1.
dependent induction G.
- apply H2.
- simpl in H2. push_right.
eapply IHG; trivial. push_left. push_right_in H2.
......
......@@ -29,17 +29,17 @@ The formalization contains a couple of hint databases, which are briefly explain
- [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 throught
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 theorem
from Oliva & Ferreira (TODO cite) and congruence for implication,
conjunction and disjuction respectivly. Using these
from Oliva & Ferreira ([[DNEG]]) and congruence for implication,
conjunction and disjunction respectively. Using these
databases, we could shorten proofs involving only simple
equivalances about double negations.
equivalences about double negations.
- [eq_triangle]: Also includes that equality is symmetric, transitive and
......@@ -52,44 +52,43 @@ The formalization contains a couple of hint databases, which are briefly explain
This section provides an overview of the tactics defined throughout the project.
** Solve Trivial Goals
- [contained A] soves 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.
- [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,
- [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
- [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].
- [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]
- [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.
- [elim_f f I] TODO Ulrich, ich hab keine Ahnung was das tut :D
** Proof by Contradiction
- [context_contradiction A] proves goal if the context contains [A] and [-! A].
- [elim_false A] TODO Ulrich, wie beschreibt man das am besten?
- [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
- [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].
- [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 formalisation of W. Ruitenburg JSL 1984 paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus"
-[[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]] Litak, Tadeusz. "Double Negation and Modality" ALCOP 2016. File "alcop2016slides_corrected_extended.pdf" in the projects repository.
*)
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment