Commit 23a593fd authored by Ulrich's avatar Ulrich

only box case left

parent 3b68d0f6
......@@ -3,7 +3,7 @@
(** This file is the first part of Tadeusz Litak's formalisation of W. Ruitenburg JSL 1984 paper
"On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" *)
Require Export dnegmod.KIbox_NaturalDeduction.
Require Export dnegmod.KIbox_Rules.
(*** Contents *)
......@@ -23,7 +23,7 @@ Export ListNotations.
Inductive hil : form -> (list form) -> form -> Prop :=
| hilst : forall Z G A, In A G -> hil Z G A
| hilAx : forall Z G s, hil Z G (sub s Z)
| hilPerm : forall Z G G' A, hil Z G A -> Permutation G G' -> hil Z G' A
(*| hilPerm : forall Z G G' A, hil Z G A -> Permutation G G' -> hil Z G' A *)
| hilI1 : forall Z G A B, hil Z G (A ->> B ->> A)
| hilI2 : forall Z G A B C, hil Z G ((A ->> B ->> C) ->> (A ->> B) ->> A ->> C)
| hilMP : forall Z G A B, hil Z G (A ->> B) -> hil Z G A -> hil Z G B
......@@ -40,22 +40,79 @@ Inductive hil : form -> (list form) -> form -> Prop :=
Hint Constructors hil : hilDB.
Lemma hil_weakening: forall A B G Z, hil Z G B -> hil Z (A :: G) B.
Proof.
intros. induction H; eauto 3 with hilDB.
- apply hilst. simpl. right. assumption.
Qed.
Lemma hil_clear_context: forall G Z A, hil Z [] A ->
hil Z G A.
Proof.
induction G; intuition.
- eauto using hil_weakening.
Qed.
Example hil_deriv_id: forall Z G A, hil Z G (A ->> A).
Proof.
intros Z G A.
pose proof (hilI2 Z G A (A ->> A) A) as H1.
pose proof (hilI1 Z G A (A ->> A)) as H2.
pose proof (hilI1 Z G A A) as H3.
eapply hilMP. eapply hilMP.
- apply H1.
- apply H2.
- apply H3.
Defined.
Lemma hil_ded: forall Z G (A B : form), hil Z (A :: G) B -> hil Z G (A ->> B).
Proof.
intros.
remember (A :: G) as G'.
induction H; eauto 3 with hilDB.
- rewrite HeqG' in H. simpl in H. destruct H.
+ rewrite H. apply hil_deriv_id.
+ eauto 3 with hilDB.
- subst. eapply hilMP. eapply hilMP. eapply hilI2.
eapply IHhil1; trivial. apply IHhil2; trivial.
Defined.
Lemma hil_permute1 : forall Z G G' A, (hil Z G A) -> (forall B, In B G <-> In B G') -> (hil Z G' A).
Proof.
intros. generalize dependent G'. induction H; eauto 3 with hilDB.
- intros. apply H0 in H. eauto 3 with hilDB.
- intros. pose proof (IHhil2 G' H1) as H2. pose proof (IHhil1 G' H1) as H3.
eauto 3 with hilDB.
Defined.
Lemma hil_permute2 : forall Z G G' A, (hil Z G A) -> Permutation G G' -> (hil Z G' A).
Proof.
intros. eapply hil_permute1.
- apply H.
- intros. clear H. induction H0.
+ split; trivial.
+ simpl. inversion IHPermutation. split; intro; inversion H2; auto.
+ simpl. split; intro; inversion H; auto; inversion H0; auto.
+ rewrite IHPermutation1. rewrite IHPermutation2; split; auto.
Defined.
Theorem NaturalDeduction_eq_to_Hilbert:
forall G Z A, KIbox Z G A <-> hil Z G A.
Proof.
intros. split.
- intro H. induction H; eauto 3 with hilDB.
+ eapply hil_permute2; eauto.
+ eapply hil_ded in IHKIbox2. eapply hil_ded in IHKIbox3.
eapply hilMP; try apply IHKIbox1.
eapply hilMP; try apply IHKIbox3.
eapply hilMP; try apply IHKIbox2.
eapply hilA3.
+ eapply hil_ded; trivial.
+ admit.
+ admit.
+ admit.
- intro H. induction H; eauto 3 with KIboxDB.
+ do 3 eapply KIbox_impI.
eapply KIbox_impE.
* eapply KIbox_impE; try contained (A ->> B ->> C); try contained A.
* eapply KIbox_impE; try contained (A ->> B); try contained A.
+ do 2 eapply KIbox_impI. eapply box_andI; try contained A; try contained B.
+ do 3 eapply KIbox_impI. eapply KIbox_orE.
* contained (A ||| B).
+ eapply hilbert_axiom.
+ do 2 eapply KIbox_impI. eapply box_andI; perm_contained.
+ do 3 eapply KIbox_impI. eapply KIbox_orE; try perm_contained.
* eapply KIbox_impE; try contained (A ->> C); try contained A.
* eapply KIbox_impE; try contained (B ->> C); try contained B.
+ eapply (KIbox_boxIE _ _ _ []); trivial.
......
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