CPPsiteProjPackage.CPP_BiInt_GHC
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_gen.
Delimit Scope My_scope with M.
Open Scope My_scope.
Set Implicit Arguments.
Notation "x :: l" := (cons x l)
(at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
(* In this file we define the generalised Hilbert calculi based on sets for the propositonal
bi-intuitionistic logic BIL. *)
(* Definitions Language *)
(* First, let us define the propositional formulae we use here. *)
Inductive BPropF : Type :=
| Var : nat -> BPropF
| Bot : BPropF
| Top : BPropF
| And : BPropF -> BPropF -> BPropF
| Or : BPropF -> BPropF -> BPropF
| Imp : BPropF -> BPropF -> BPropF
| Excl : BPropF -> BPropF -> BPropF
.
Notation "# P" := (Var P) (at level 1) : My_scope.
Notation "A --> B" := (Imp A B) (at level 16, right associativity) : My_scope.
Definition wNeg (A : BPropF) := Excl Top A.
Definition Neg (A : BPropF) := Imp A Bot.
Fixpoint DN_form (n : nat) (A : (BPropF)) : (BPropF) :=
match n with
| 0 => A
| S m => Neg (wNeg (DN_form m A))
end.
Inductive DN_clos_set (Γ : @Ensemble (BPropF)): @Ensemble (BPropF) :=
| InitClo : forall A, In _ Γ A -> DN_clos_set Γ A
| IndClo : forall A, DN_clos_set Γ A -> DN_clos_set Γ (Neg (wNeg A)).
Lemma eq_dec_form : forall x y : BPropF, {x = y}+{x <> y}.
Proof.
decide equality. decide equality.
Qed.
Fixpoint size_form (A : BPropF) : nat :=
match A with
| # P => 1
| Bot => 1
| Top => 1
| And B C => 1 + (size_form B) + (size_form C)
| Or B C => 1 + (size_form B) + (size_form C)
| Imp B C => 1 + (size_form B) + (size_form C)
| Excl B C => 1 + (size_form B) + (size_form C)
end.
Fixpoint subst (f : nat -> (BPropF)) (A : (BPropF)) : (BPropF) :=
match A with
| # P => (f P)
| Bot => Bot
| Top => Top
| And B C => And (subst f B) (subst f C)
| Or B C => Or (subst f B) (subst f C)
| Imp B C => Imp (subst f B) (subst f C)
| Excl B C => Excl (subst f B) (subst f C)
end.
(* Now, we can define some properties of formulas. *)
Definition is_atomicT (A : BPropF) : Type :=
(exists (P : nat), A = # P) + (A = Bot) + (A = Top).
(* We can define some types of lists formulae. For example, we can define
lists of formulae which contain only propositional variables. *)
Definition is_Atomic (Γ : @Ensemble (BPropF)) : Type :=
forall (A : BPropF), (Γ A) -> ((exists (P : nat), A = # P) + (A = Bot) + (A = Top)).
(* We define here the axioms. *)
Definition RA1 (A B C : BPropF) : BPropF := (A --> B) --> ((B --> C) --> (A --> C)).
Definition RA2 (A B : BPropF) : BPropF := A --> (Or A B).
Definition RA3 (A B : BPropF) : BPropF := B --> (Or A B).
Definition RA4 (A B C : BPropF) : BPropF := (A --> C) --> ((B --> C) --> ((Or A B) --> C)).
Definition RA5 (A B : BPropF) : BPropF := (And A B) --> A.
Definition RA6 (A B : BPropF) : BPropF := (And A B) --> B.
Definition RA7 (A B C : BPropF) : BPropF := (A --> B) --> ((A --> C) --> (A --> (And B C))).
Definition RA8 (A B C : BPropF) : BPropF := (A --> (B --> C)) --> ((And A B) --> C).
Definition RA9 (A B C : BPropF) : BPropF := ((And A B) --> C) --> (A --> (B --> C)).
Definition RA10 (A B : BPropF) : BPropF := (A --> B) --> ((Neg B) --> (Neg A)).
Definition RA11 (A B : BPropF) : BPropF := A --> (Or B (Excl A B)).
Definition RA12 (A B : BPropF) : BPropF := (Excl A B) --> (wNeg (A --> B)).
Definition RA13 (A B C : BPropF) : BPropF := (Excl (Excl A B) C) --> (Excl A (Or B C)).
Definition RA14 (A B : BPropF) : BPropF := (Neg (Excl A B)) --> (A --> B).
Definition RA15 (A : BPropF) : BPropF := A --> Top.
Definition RA16 (A : BPropF) : BPropF := Bot --> A.
Inductive BIAxioms (A : BPropF) : Prop :=
| RA1_I : (exists B C D, A = (RA1 B C D)) -> BIAxioms A
| RA2_I : (exists B C, A = (RA2 B C)) -> BIAxioms A
| RA3_I : (exists B C, A = (RA3 B C)) -> BIAxioms A
| RA4_I : (exists B C D, A = (RA4 B C D)) -> BIAxioms A
| RA5_I : (exists B C, A = (RA5 B C)) -> BIAxioms A
| RA6_I : (exists B C, A = (RA6 B C)) -> BIAxioms A
| RA7_I : (exists B C D, A = (RA7 B C D)) -> BIAxioms A
| RA8_I : (exists B C D, A = (RA8 B C D)) -> BIAxioms A
| RA9_I : (exists B C D, A = (RA9 B C D)) -> BIAxioms A
| RA10_I : (exists B C, A = (RA10 B C)) -> BIAxioms A
| RA11_I : (exists B C, A = (RA11 B C)) -> BIAxioms A
| RA12_I : (exists B C, A = (RA12 B C)) -> BIAxioms A
| RA13_I : (exists B C D, A = (RA13 B C D)) -> BIAxioms A
| RA14_I : (exists B C, A = (RA14 B C)) -> BIAxioms A
| RA15_I : (exists B, A = (RA15 B)) -> BIAxioms A
| RA16_I : (exists B, A = (RA16 B)) -> BIAxioms A.
(* Finally, we can define the rules which constitute our calculi. We gather
them in cacluli in a definition appearing later.
We start by giving the rules common to both calculi. *)
Inductive IdRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| IdRule_I : forall A (Γ : @Ensemble _),
(Γ A) -> (IdRule [] (pair Γ A)).
Inductive AxRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| AxRule_I : forall Γ (A : BPropF),
(BIAxioms A) -> AxRule [] (pair Γ A)
.
Inductive MPRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| MPRule_I : forall A B Γ,
MPRule [(pair Γ (A --> B)); (pair Γ A)]
(pair Γ B)
.
(* Then we turn to the distinctive rule of BIH. *)
Inductive DNwRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| DNwRule_I : forall (A : BPropF) Γ,
DNwRule [(pair (@Empty_set (BPropF)) A)]
(pair Γ (Neg (wNeg A)))
.
(* At last we can define our calculus BIH. *)
Inductive BIH_rules (s : ((@Ensemble (BPropF)) * (BPropF))) : Prop :=
| Id : IdRule [] s -> BIH_rules s
| Ax : AxRule [] s -> BIH_rules s
| MP : forall ps, (forall prem, List.In prem ps -> BIH_rules prem) -> MPRule ps s -> BIH_rules s
| DNw : forall ps, (forall prem, List.In prem ps -> BIH_rules prem) -> DNwRule ps s -> BIH_rules s
.
(* Define the general notion of derivable pair. *)
Fixpoint list_disj (l : list (BPropF)) : BPropF :=
match l with
| nil => Bot
| h :: t => Or h (list_disj t)
end.
Definition pair_derrec (G : prod (@Ensemble (BPropF)) (@Ensemble (BPropF))) : Prop :=
exists (l : list (BPropF)), NoDup l /\ (forall A, List.In A l -> ((snd G) A)) /\
(BIH_rules (fst G, list_disj l)).
Definition complete (G : prod (@Ensemble (BPropF)) (@Ensemble (BPropF))) : Prop :=
forall (A : BPropF), (fst G) A \/ (snd G) A.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_gen.
Delimit Scope My_scope with M.
Open Scope My_scope.
Set Implicit Arguments.
Notation "x :: l" := (cons x l)
(at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
(* In this file we define the generalised Hilbert calculi based on sets for the propositonal
bi-intuitionistic logic BIL. *)
(* Definitions Language *)
(* First, let us define the propositional formulae we use here. *)
Inductive BPropF : Type :=
| Var : nat -> BPropF
| Bot : BPropF
| Top : BPropF
| And : BPropF -> BPropF -> BPropF
| Or : BPropF -> BPropF -> BPropF
| Imp : BPropF -> BPropF -> BPropF
| Excl : BPropF -> BPropF -> BPropF
.
Notation "# P" := (Var P) (at level 1) : My_scope.
Notation "A --> B" := (Imp A B) (at level 16, right associativity) : My_scope.
Definition wNeg (A : BPropF) := Excl Top A.
Definition Neg (A : BPropF) := Imp A Bot.
Fixpoint DN_form (n : nat) (A : (BPropF)) : (BPropF) :=
match n with
| 0 => A
| S m => Neg (wNeg (DN_form m A))
end.
Inductive DN_clos_set (Γ : @Ensemble (BPropF)): @Ensemble (BPropF) :=
| InitClo : forall A, In _ Γ A -> DN_clos_set Γ A
| IndClo : forall A, DN_clos_set Γ A -> DN_clos_set Γ (Neg (wNeg A)).
Lemma eq_dec_form : forall x y : BPropF, {x = y}+{x <> y}.
Proof.
decide equality. decide equality.
Qed.
Fixpoint size_form (A : BPropF) : nat :=
match A with
| # P => 1
| Bot => 1
| Top => 1
| And B C => 1 + (size_form B) + (size_form C)
| Or B C => 1 + (size_form B) + (size_form C)
| Imp B C => 1 + (size_form B) + (size_form C)
| Excl B C => 1 + (size_form B) + (size_form C)
end.
Fixpoint subst (f : nat -> (BPropF)) (A : (BPropF)) : (BPropF) :=
match A with
| # P => (f P)
| Bot => Bot
| Top => Top
| And B C => And (subst f B) (subst f C)
| Or B C => Or (subst f B) (subst f C)
| Imp B C => Imp (subst f B) (subst f C)
| Excl B C => Excl (subst f B) (subst f C)
end.
(* Now, we can define some properties of formulas. *)
Definition is_atomicT (A : BPropF) : Type :=
(exists (P : nat), A = # P) + (A = Bot) + (A = Top).
(* We can define some types of lists formulae. For example, we can define
lists of formulae which contain only propositional variables. *)
Definition is_Atomic (Γ : @Ensemble (BPropF)) : Type :=
forall (A : BPropF), (Γ A) -> ((exists (P : nat), A = # P) + (A = Bot) + (A = Top)).
(* We define here the axioms. *)
Definition RA1 (A B C : BPropF) : BPropF := (A --> B) --> ((B --> C) --> (A --> C)).
Definition RA2 (A B : BPropF) : BPropF := A --> (Or A B).
Definition RA3 (A B : BPropF) : BPropF := B --> (Or A B).
Definition RA4 (A B C : BPropF) : BPropF := (A --> C) --> ((B --> C) --> ((Or A B) --> C)).
Definition RA5 (A B : BPropF) : BPropF := (And A B) --> A.
Definition RA6 (A B : BPropF) : BPropF := (And A B) --> B.
Definition RA7 (A B C : BPropF) : BPropF := (A --> B) --> ((A --> C) --> (A --> (And B C))).
Definition RA8 (A B C : BPropF) : BPropF := (A --> (B --> C)) --> ((And A B) --> C).
Definition RA9 (A B C : BPropF) : BPropF := ((And A B) --> C) --> (A --> (B --> C)).
Definition RA10 (A B : BPropF) : BPropF := (A --> B) --> ((Neg B) --> (Neg A)).
Definition RA11 (A B : BPropF) : BPropF := A --> (Or B (Excl A B)).
Definition RA12 (A B : BPropF) : BPropF := (Excl A B) --> (wNeg (A --> B)).
Definition RA13 (A B C : BPropF) : BPropF := (Excl (Excl A B) C) --> (Excl A (Or B C)).
Definition RA14 (A B : BPropF) : BPropF := (Neg (Excl A B)) --> (A --> B).
Definition RA15 (A : BPropF) : BPropF := A --> Top.
Definition RA16 (A : BPropF) : BPropF := Bot --> A.
Inductive BIAxioms (A : BPropF) : Prop :=
| RA1_I : (exists B C D, A = (RA1 B C D)) -> BIAxioms A
| RA2_I : (exists B C, A = (RA2 B C)) -> BIAxioms A
| RA3_I : (exists B C, A = (RA3 B C)) -> BIAxioms A
| RA4_I : (exists B C D, A = (RA4 B C D)) -> BIAxioms A
| RA5_I : (exists B C, A = (RA5 B C)) -> BIAxioms A
| RA6_I : (exists B C, A = (RA6 B C)) -> BIAxioms A
| RA7_I : (exists B C D, A = (RA7 B C D)) -> BIAxioms A
| RA8_I : (exists B C D, A = (RA8 B C D)) -> BIAxioms A
| RA9_I : (exists B C D, A = (RA9 B C D)) -> BIAxioms A
| RA10_I : (exists B C, A = (RA10 B C)) -> BIAxioms A
| RA11_I : (exists B C, A = (RA11 B C)) -> BIAxioms A
| RA12_I : (exists B C, A = (RA12 B C)) -> BIAxioms A
| RA13_I : (exists B C D, A = (RA13 B C D)) -> BIAxioms A
| RA14_I : (exists B C, A = (RA14 B C)) -> BIAxioms A
| RA15_I : (exists B, A = (RA15 B)) -> BIAxioms A
| RA16_I : (exists B, A = (RA16 B)) -> BIAxioms A.
(* Finally, we can define the rules which constitute our calculi. We gather
them in cacluli in a definition appearing later.
We start by giving the rules common to both calculi. *)
Inductive IdRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| IdRule_I : forall A (Γ : @Ensemble _),
(Γ A) -> (IdRule [] (pair Γ A)).
Inductive AxRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| AxRule_I : forall Γ (A : BPropF),
(BIAxioms A) -> AxRule [] (pair Γ A)
.
Inductive MPRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| MPRule_I : forall A B Γ,
MPRule [(pair Γ (A --> B)); (pair Γ A)]
(pair Γ B)
.
(* Then we turn to the distinctive rule of BIH. *)
Inductive DNwRule : rls ((@Ensemble (BPropF)) * (BPropF)) :=
| DNwRule_I : forall (A : BPropF) Γ,
DNwRule [(pair (@Empty_set (BPropF)) A)]
(pair Γ (Neg (wNeg A)))
.
(* At last we can define our calculus BIH. *)
Inductive BIH_rules (s : ((@Ensemble (BPropF)) * (BPropF))) : Prop :=
| Id : IdRule [] s -> BIH_rules s
| Ax : AxRule [] s -> BIH_rules s
| MP : forall ps, (forall prem, List.In prem ps -> BIH_rules prem) -> MPRule ps s -> BIH_rules s
| DNw : forall ps, (forall prem, List.In prem ps -> BIH_rules prem) -> DNwRule ps s -> BIH_rules s
.
(* Define the general notion of derivable pair. *)
Fixpoint list_disj (l : list (BPropF)) : BPropF :=
match l with
| nil => Bot
| h :: t => Or h (list_disj t)
end.
Definition pair_derrec (G : prod (@Ensemble (BPropF)) (@Ensemble (BPropF))) : Prop :=
exists (l : list (BPropF)), NoDup l /\ (forall A, List.In A l -> ((snd G) A)) /\
(BIH_rules (fst G, list_disj l)).
Definition complete (G : prod (@Ensemble (BPropF)) (@Ensemble (BPropF))) : Prop :=
forall (A : BPropF), (fst G) A \/ (snd G) A.