Commit 3b68d0f6 authored by Ulrich's avatar Ulrich

started with hilbert style equality

parent 28fe2386
(** * 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_NaturalDeduction.
(*** 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.
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.
+ 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 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