Commit 947405a1 authored by litak's avatar litak

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

parents 28d67815 23a593fd
(** * ApplicativeSetup *)
(** 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_Rules.
(*** Contents *)
(** This file contains underlying definitions and the theory of a (turnstile-Hilbert-style) presentation of IPC
used in Ruitenburg's paper. *)
(*** Hilbert-style system for IPC *)
Reserved Notation "G '|--' A" (at level 79).
Require Export Coq.Lists.List.
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 *)
| 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
| hilC1 : forall Z G A B, hil Z G (A ->> B ->> A & B)
| hilC2 : forall Z G A B, hil Z G (A & B ->> A)
| hilC3 : forall Z G A B, hil Z G (A & B ->> B)
| hilA1 : forall Z G A B, hil Z G (A ->> A ||| B)
| hilA2 : forall Z G A B, hil Z G (B ->> A ||| B)
| hilA3 : forall Z G A B C, hil Z G ((A ->> C) ->> (B ->> C) ->> (A ||| B ->> C))
| hilNorm : forall Z G A, hil Z [] A -> hil Z G (|[]|A)
| hilKax : forall Z G A B, hil Z G (|[]|(A ->> B) ->> |[]|A ->> |[]|B)
| hiltt : forall Z G, hil Z G tt
| hilff : forall Z G A, hil Z G (ff ->> A).
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.
- intro H. induction H; eauto 3 with KIboxDB.
+ 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.
intros. inversion H0.
+ do 2 eapply KIbox_impI.
eapply (KIbox_boxIE _ _ _ [A; A ->> B]).
* intros. inversion H; subst.
** contained (|[]| f).
** inversion H0; subst. try contained (|[]| (A ->> B)). inversion H1.
* eapply KIbox_impE; try contained (A ->> B); try contained A.
Admitted.
\ 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