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.