# Library PropiL

Require Export Base.

# Formulas and contexts

Definition var := nat.

Inductive form: Type :=
| Var: var form
| Fal: form
| Imp: form form form
| And: form form form
| Or: form form form.

Definition Not s := Imp s Fal.
Definition Equi s t : form := And (Imp s t) (Imp t s).

Instance form_eq_dec : s t: form, dec (s = t).

# Generic Entailment Relations

Section EntailmentRelationProperties.

Variable F: Type.
Variable E: list F F Prop.

(*** Generic Structural Properties ***)
Definition Monotonicity : Prop :=
A A' s, A <<= A' E A s E A' s.

Definition Reflexivity : Prop :=
A s, s el A E A s.

Definition Cut : Prop :=
A s t, E A s E (s::A) t E A t.

Definition Consistency : Prop :=
s:F, ¬E nil s.

End EntailmentRelationProperties.

Definition context := list form.

(*** Logical Properties ***)

Definition CharFal (E: context form Prop) : Prop :=
A, E A Fal s, E A s.

Definition CharImp (E: context form Prop) : Prop :=
A s t, E A (Imp s t) E (s::A) t.

Definition CharAnd (E: context form Prop) : Prop :=
A s t, E A (And s t) u, E (s::t::A) u E A u.

Definition CharOr (E: context form Prop) : Prop :=
A s t, E A (Or s t) u, E (s::A) u E (t::A) u E A u.

Fixpoint subst (sigma: var form) (s: form) : form :=
match s with
| Var xsigma x
| FalFal
| Imp s tImp (subst sigma s) (subst sigma t)
| And s tAnd (subst sigma s) (subst sigma t)
| Or s tOr (subst sigma s) (subst sigma t)
end.

Definition Substitution (E: context form Prop) :=
A s sigma, E A s E (map (subst sigma) A) (subst sigma s).

Definition EntailRelAllProps (E: context form Prop) :=
Reflexivity E Monotonicity E Cut E Consistency E
CharImp E CharFal E CharAnd E CharOr E
Substitution E.

Lemma EntailRelAllProps_ext E E':
EntailRelAllProps E ( A s, E A s E' A s) EntailRelAllProps E'.

# Intuitionistic Gentzen System

Inductive gen: context form Prop :=
| genV A x: Var x el A gen A (Var x)
| genF A u: Fal el A gen A u
| genIR A s t: gen (s::A) t gen A (Imp s t)
| genIL A s t u: (Imp s t) el A gen A s gen (t::A) u gen A u
| genAL A s t u: (And s t) el A gen (s::t::A) u gen A u
| genAR A s t: gen A s gen A t gen A (And s t)
| genOL A s t u: (Or s t) el A gen (s::A) u gen (t::A) u gen A u
| genOR1 A s t: gen A s gen A (Or s t)
| genOR2 A s t: gen A t gen A (Or s t).

(* Hints for auto to use rules of gen *)
Hint Constructors gen.

Assumption rule
Lemma genA: Reflexivity gen.

Hint Resolve genA.

Weakening rule
Lemma gen_mono: Monotonicity gen.

Lemma genW A B s: gen A s A <<= B gen B s.

Cut rule
Lemma gen_GCut A s B u:
gen A s gen B u gen (A ++ rem B s) u.
Lemma gen_cut: Cut gen.

Lemma genCW A s t: gen A s gen [s] t gen A t.

Lemma gen_NoFal: ¬ gen [] Fal.

Lemma gen_cons: Consistency gen.

Lemma gen_imp: CharImp gen.

Lemma gen_fal: CharFal gen.

Lemma gen_and: CharAnd gen.

Lemma gen_and_both A s t: gen A (And s t) gen A s gen A t.

Lemma gen_or: CharOr gen.

Lemma gen_subst: Substitution gen.

Lemma gen_EntailRelation: EntailRelAllProps gen.

Lemma gen_NoVar x:
¬ gen [] (Var x).

Lemma gen_NoNVar x:
¬ gen [] (Not (Var x)).

# Intuitionistic Natural Deduction System

Inductive nd : context form Prop :=
| ndA A s: s el A nd A s
| ndE A s: nd A Fal nd A s
| ndII A s t: nd (s::A) t nd A (Imp s t)
| ndIE A s t: nd A (Imp s t) nd A s nd A t
| ndAI A s t: nd A s nd A t nd A (And s t)
| ndAE A s t u: nd A (And s t) nd (s::t::A) u nd A u
| ndOIL A s t: nd A s nd A (Or s t)
| ndOIR A s t: nd A t nd A (Or s t)
| ndOE A s t u: nd A (Or s t) nd (s::A) u nd (t::A) u nd A u.

(* Hints for auto to use rules of nd *)
Hint Constructors nd.

(* nd satisfies Entailment Relation properties *)
Lemma nd_refl: Reflexivity nd.

Lemma nd_mono: Monotonicity nd.

Lemma ndW A B s: nd A s A <<= B nd B s.

Lemma nd_cut: Cut nd.

Lemma ndCW A s t: nd A s nd [s] t nd A t.

(* Lemma nd_cons: Consistency nd. --- will be proved using Gentzen *)

Lemma nd_imp: CharImp nd.

Lemma nd_fal: CharFal nd.

Lemma nd_and: CharAnd nd.

Lemma nd_or: CharOr nd.

Lemma nd_subst: Substitution nd.

# Equivalence of Ni and Gi

Lemma gen_nd A s: gen A s nd A s.

Lemma nd_gen A s: nd A s gen A s.

Theorem gen_iff_nd A s: gen A s nd A s.

Lemma nd_NoFal: ¬ nd [] Fal.

Lemma nd_cons: Consistency nd.

Lemma nd_EntailRelation: EntailRelAllProps nd.

(* One-sided ND *)
Fixpoint c2f A s: form :=
match A with
| []s
| s' :: A'c2f A' (Imp s' s)
end.

Lemma nd_onesided A s: nd A s nd [] (c2f A s).

# Intuitionistic Hilbert System Hi

Definition FK (s t : form) : form :=
Imp s (Imp t s).

Definition FS (s t u : form) : form :=
(Imp (Imp s (Imp t u))
(Imp (Imp s t)
(Imp s u))).

Inductive hil (A : context): form Prop :=
| hilK s t: hil A (FK s t)
| hilS s t u: hil A (FS s t u)
| hilAL s t: hil A (Imp (And s t) s)
| hilAR s t: hil A (Imp (And s t) t)
| hilAI s t: hil A (Imp s (Imp t (And s t)))
| hilOL s t: hil A (Imp s (Or s t))
| hilOR s t: hil A (Imp t (Or s t))
| hilOE s t u: hil A (Imp (Imp s u) (Imp (Imp t u) (Imp (Or s t) u)))
| hilE s: hil A (Imp Fal s)
| hilA s: s el A hil A s
| hilMP s t: hil A (Imp s t) hil A s hil A t.

Equivalence of Ni and Hi
Lemma hil_nd A s :
hil A s nd A s.

Lemma hilAK A s t:
hil A s hil A (Imp t s).

Lemma hilAS A s t u :
hil A (Imp s (Imp t u)) hil A (Imp s t) hil A (Imp s u).

Lemma hilI A s: hil A (Imp s s).

Lemma hilD w A v :
hil (w::A) v hil A (Imp w v).

Lemma nd_hil A s :
nd A s hil A s.

Theorem hil_iff_nd A s:
hil A s nd A s.

# Intuitionistic Tableaux (Fitting's System)

Inductive tab (C D: list form): Prop :=
| tabF : Fal el C tab C D
| tabC x : Var x el C Var x el D tab C D
| tabIP s t: Imp s t el C tab C (s::D) tab (t::C) D tab C D
| tabIN s t: Imp s t el D tab (s :: C) [t] tab C D
| tabAP s t: And s t el C tab (s :: t :: C) D tab C D
| tabAN s t: And s t el D tab C (s :: D) tab C (t :: D) tab C D
| tabOP s t: Or s t el C tab (s :: C) D tab (t :: C) D tab C D
| tabON s t: Or s t el D tab C (s :: t :: D) tab C D.

Lemma tabLW C D: tab C D C', C <<= C' tab C' D.

Lemma tabRW C D: tab C D D', D <<= D' tab C D'.

Lemma tabW C D C' D': tab C D C <<= C' D <<= D' tab C' D'.

Lemma tabCS C D s: s el C s el D tab C D.

Fixpoint OrAR (B: list form) : form :=
match B with
| []Fal
| s :: B'match B' with
| []s
| _Or s (OrAR B')
end
end.

Lemma OrAR_mono A B: A <<= B gen [OrAR A] (OrAR B).
Lemma tab_genG C D:
tab C D gen C (OrAR D).

Lemma tab_gen A s:
tab A [s] gen A s.

Lemma gen_tab A s:
gen A s tab A [s].

Theorem gen_iff_tab A s:
gen A s tab A [s].

Lemma OrAR_mono_nd A B: A <<= B nd [OrAR A] (OrAR B).
Lemma tab_ndG C D:
tab C D nd C (OrAR D).

Lemma tab_nd A s:
tab A [s] nd A s.

Lemma nd_OrCut A s t:
nd A (Or s t) nd (s::A) t nd A t.

Lemma nd_OrARcut A B s:
nd A (OrAR (s::B)) nd (s::A) (OrAR B) nd A (OrAR B).

# Decidability of Intuitionistic Gentzen

Subformula Closure

Definition sf_closed (A : context) : Prop :=
u, u el A match u with
| Imp s t | And s t | Or s ts el A t el A
| _True
end.

Lemma sf_closed_app A B:
sf_closed A sf_closed B sf_closed (A ++ B).

Lemma sf_closed_cons u s t A :
(u = Imp s t u = And s t u = Or s t)
s el A t el A sf_closed A sf_closed (u :: A).

Subformula-closed list

Fixpoint scl' (s : form) : context :=
s :: match s with
| Imp u v | And u v | Or u vscl' u ++ scl' v
| _nil
end.

Lemma scl'_in s: s el scl' s.

Lemma scl'_closed s: sf_closed (scl' s).

Fixpoint scl (A : context) : context :=
match A with
| nilnil
| s :: A'scl' s ++ scl A'
end.

Lemma scl_incl' A: A <<= scl A.

Lemma scl_incl A B: A <<= B A <<= scl B.

Lemma scl_closed A: sf_closed (scl A).

Definition goal := prod (context) form.

Instance goal_eq_dec (gamma delta: goal):
dec (gamma = delta).

Section Decidability.
Variable A0 : context.
Variable s0 : form.
Definition U := scl (s0::A0).
Definition U_sfc : sf_closed U := @scl_closed _.
Definition Gamma := list_prod (power U) U.

Definition step (Delta : list goal) (gamma : goal) : Prop :=
let (A,u) := gamma in
match u with
| Var _u el A
| Imp s t(rep (s::A) U, t) el Delta
| And s t(A, s) el Delta (A, t) el Delta
| Or s t(A, s) el Delta (A, t) el Delta
| _False
end

v, v el A
match v with
| FalTrue
| Imp s t(A, s) el Delta (rep (t::A) U, u) el Delta
| And s t(rep (s::t::A) U, u) el Delta
| Or s t(rep (s::A) U, u) el Delta (rep (t::A) U, u) el Delta
| _False
end.

Instance step_dec Delta gamma :
dec (step Delta gamma).

Definition Lambda : list goal :=
FCI.C (step := step) Gamma.

Lemma lambda_closure gamma:
gamma el Gamma step Lambda gamma gamma el Lambda.

Lemma lambda_ind (p : goal Prop) :
( Delta gamma, inclp Delta p gamma el Gamma
step Delta gamma p gamma)
inclp Lambda p.

Lemma gen_lambda A u:
A <<= U u el U gen A u (rep A U,u) el Lambda.

Lemma lambda_gen A u :
(A,u) el Lambda gen A u.

Theorem nd_dec: dec (nd A0 s0).

End Decidability.

Some underivablity results

Lemma gen_DN' A x s :
A <<= [Var x; Not (Not (Var x))] gen A s s Fal s Not (Var x).

Lemma gen_DN x :
¬ gen [Not (Not (Var x))] (Var x).

Formula size and depth

Fixpoint sizeF s : nat :=
match s with
| Imp s1 s2 | And s1 s2 | Or s1 s2 ⇒ 1 + sizeF s1 + sizeF s2
| _ ⇒ 1
end.

Fixpoint depth (s: form): nat :=
match s with
| Var _ ⇒ 0
| Fal ⇒ 0
| Imp s1 s2 | And s1 s2 | Or s1 s2
1 + (if decision (depth s1 depth s2) then depth s2 else depth s1)
end.

Signed formulas and clauses

Inductive sform : Type :=
| Pos : form sform
| Neg : form sform.

Definition clause := list sform.

Notation "+ s" := (Pos s) (at level 35).
Notation "- s" := (Neg s).

Definition positive (S: sform): Prop :=
match S with +sTrue | -sFalse end.

Definition negative (S: sform): Prop :=
match S with +sFalse | -sTrue end.

Instance sform_eq_dec (S T: sform) : dec (S = T).

Definition uns S : form :=
match S with +ss | -sNot s end.

Fixpoint size C : nat :=
match C with
| nil ⇒ 0
| +s::C' | -s::C'sizeF s + size C'
end.

Lemma uns_pos A :
map uns (map Pos A) = A.

Incomplete formulas

Fixpoint FalFree u: Prop :=
match u with
| Var _True
| FalFalse
| Imp s t | And s t | Or s tFalFree s FalFree t
end.

Fixpoint ImpFree u: Prop :=
match u with
| Var _ | FalTrue
| Imp _ _False
| And s t | Or s tImpFree s ImpFree t
end.

Fixpoint AndFree u: Prop :=
match u with
| Var _ | FalTrue
| Imp s tAndFree s AndFree t
| And _ _False
| Or s tAndFree s AndFree t
end.

Fixpoint OrFree u: Prop :=
match u with
| Var _ | FalTrue
| Imp s t | And s tOrFree s OrFree t
| Or _ _False
end.

Section ssL.
Definition ss_closed' (S: sform) (C: clause): Prop :=
match S with
| +Imp s t-s el C +t el C
| -Imp s t+s el C -t el C
| +And s t+s el C +t el C
| -And s t-s el C -t el C
| +Or s t+s el C +t el C
| -Or s t-s el C -t el C
| _True
end.

Definition ss_closed (C: clause) : Prop :=
S, S el C ss_closed' S C.

Definition s2b (S: sform): (bool × form) :=
match S with | + s(true, s) | - s(false, s) end.

Definition b2s (sign: bool) (s: form) := if sign then +s else -s.

Fixpoint ssLb (sg: bool) (s: form): clause :=
b2s sg s ::
if sg then
match s with
| Imp s1 s2ssLb false s1 ++ ssLb true s2
| And s1 s2 | Or s1 s2ssLb true s1 ++ ssLb true s2
| _[]
end
else
match s with
| Imp s1 s2ssLb true s1 ++ ssLb false s2
| And s1 s2 | Or s1 s2ssLb false s1 ++ ssLb false s2
| _[]
end.

Definition ssL' (S: sform): clause := let (sg,s) := s2b S in ssLb sg s.

Fixpoint ssL (C: clause): clause :=
match C with
| [][]
| Sf :: C'ssL' Sf ++ ssL C'
end.

Lemma ss_closed'_mono S C C':
ss_closed' S C C <<= C' ss_closed' S C'.

Lemma ss_closed_app C C':
ss_closed C ss_closed C' ss_closed (C ++ C').

Lemma ssL'_self (S: sform): ss_closed' S (ssL' S).

Lemma ssL'_in (S: sform): S el (ssL' S).

Lemma ssL'_correct (S: sform): ss_closed (ssL' S).

Lemma ssL_correct C: ss_closed (ssL C) C <<= ssL C.

Lemma ssL_in C S: S el C S el ssL C.

Lemma ssL'_in_ssL S C S': S' el ssL' S S el C S' el ssL C.

Lemma ssL_mono C D: C <<= D ssL C <<= ssL D.

Lemma ssL_app C D: ssL (C ++ D) === ssL C ++ ssL D.

Lemma ssL_idempotent C: ssL C === ssL (ssL C).

Lemma ssL'_in_ssL2 S C S': S' el ssL' S S el ssL C S' el ssL C.

End ssL.