Commit ff26261e by Miriam

### Merge branch 'master' of cal8.cs.fau.de:dnegmod

parents e3583c2c 3d92ffa5
 ... ... @@ -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,9 @@ (** 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]]. *) (** * Formulas *) ... ... @@ -33,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. ... ...
 ... ... @@ -2,7 +2,7 @@ ## v # The Coq Proof Assistant ## ## "\$@" || ( RV=\$\$?; rm -f "\$@"; exit \$\${RV} ) ... ...