some_neg

Abstract sequent semantics

This module proves the correctness of the some_neg sequent semantics on an abstract level.

There are five semantics for formulas and sequents in the formalization: propositional semantics, the real semantics, the step semantics, the X,tau semantics and the TX,tau semantics. Each of them constructs the sequent semantics with a finite disjunction from the formula semantics. For each of these sequent semantics I need concatenation lemmas and some other utility results. The predicate some_neg provides a simplified sequent semantics, for which concatenation and other results can be proved easily. This model proves the equivalence of the finite-disjunction-semantics with the simplified semantics.

As in module some_neg I first prove the dependent version and derive the non-dependent version from it.

Require Export some_neg formulas.

Correctness of simplified some_neg_dep semantics I

This is the dependent version for nonempty sequents

Section Some_neg_dep_form.

  Variable V : Type.
  Variable L : modal_operators.
  Variable form_prop : lambda_formula V L → Prop.
  Variable P : ∀(f : lambda_formula V L), form_prop f → Prop.

  Definition sequent_prop(s : sequent V L) : Prop := a_list_prop form_prop s.

First hypothesis: well-formedness of formulas is closed under disjunction.

  Hypothesis form_prop_or :
    ∀(f1 f2 : lambda_formula V L),
      form_prop f1 → form_prop f2 → form_prop (lambda_or f1 f2).

This is more a parameter than an hypothesis. It declares the function that converts a proof for the well-formedness of a sequent into the well-formdness of its disjunction. This function is needed for the main statement below and will get instantiated.

  Hypothesis form_prop_or_formula_of_sequent_iter :
    ∀(f : lambda_formula V L)(s : sequent V L),
      sequent_prop (f :: s) →
        form_prop (or_formula_of_sequent_iter f s).

Second hypothesis: The well-formedness argument is irrelevant for the formula semantics.

  Hypothesis P_tcc_irr :
    ∀(f : lambda_formula V L)(tf1 tf2 : form_prop f),
      P f tf1 → P f tf2.

Third hypothesis: The formula semantics is closed under disjunction.

  Hypothesis P_or_formula :
    ∀(f1 f2 : lambda_formula V L)(tf1 : form_prop f1)(tf2 : form_prop f2),
      P (lambda_or f1 f2) (form_prop_or f1 f2 tf1 tf2)
      ↔ ~(~P f1 tf1 ∧ ¬P f2 tf2 ).

  Lemma a_list_prop_first_or :
    ∀(f1 f2 f3 : lambda_formula V L)(s : sequent V L),
      sequent_prop (f1 :: f2 :: f3 :: s) →
        sequent_prop ((lambda_or f1 f2 ) :: f3 :: s).

  Lemma p_or_formula_of_sequent_iter :
    ∀(s : sequent V L)(f1 f2 : lambda_formula V L)
          (t_f_s : sequent_prop (f1 :: f2 :: s)),
      P (or_formula_of_sequent_iter f1 (f2 :: s))
         (form_prop_or_formula_of_sequent_iter f1 (f2 :: s) t_f_s)
      ↔
      ~(~P f1 (a_list_prop_head t_f_s) ∧
        ¬P (or_formula_of_sequent_iter f2 s)
           (form_prop_or_formula_of_sequent_iter f2 s
                                      (a_list_prop_tail t_f_s))).

  Lemma some_neg_dep_cons_correct :
    ∀(s : sequent V L)(f : lambda_formula V L)
          (dep_s : sequent_prop (f :: s)),
      some_neg_dep form_prop P (f :: s) dep_s ↔
        P (or_formula_of_sequent_iter f s)
          (form_prop_or_formula_of_sequent_iter f s dep_s).

End Some_neg_dep_form.

Implicit Arguments sequent_prop [V L].

Correctness of simplified some_neg_dep semantics II

This is the dependent version for possibly empty sequents

Section Some_neg_dep_form_2.

  Variable V : Type.
  Variable L : modal_operators.
  Variable form_prop : lambda_formula V L → Prop.
  Variable P : ∀(f : lambda_formula V L), form_prop f → Prop.

first hypothesis

  Hypothesis form_prop_or :
    ∀(f1 f2 : lambda_formula V L),
      form_prop f1 → form_prop f2 → form_prop (lambda_or f1 f2).

Declaration of the well-formedness proof conversion function

  Hypothesis form_prop_or_formula_of_sequent :
    ∀(nonempty_v : V)(s : sequent V L),
      sequent_prop form_prop s →
        form_prop (or_formula_of_sequent s nonempty_v).

second hypothesis

  Hypothesis P_tcc_irr :
    ∀(f : lambda_formula V L)(tf1 tf2 : form_prop f),
      P f tf1 → P f tf2.

third hypothesis

  Hypothesis P_or_formula :
    ∀(f1 f2 : lambda_formula V L)(tf1 : form_prop f1)(tf2 : form_prop f2),
      P (lambda_or f1 f2) (form_prop_or f1 f2 tf1 tf2)
      ↔ ~(~P f1 tf1 ∧ ¬P f2 tf2 ).

Fourth hypothesis: The formula semantics is false for false.

  Hypothesis P_false :
    ∀(nonempty_v : V)(t_false : form_prop (lambda_false nonempty_v)),
      P (lambda_false nonempty_v) t_false → False.

  Lemma form_prop_or_formula_of_sequent_iter :
    ∀(nonempty_v : V)(f : lambda_formula V L)(s : sequent V L),
      sequent_prop form_prop (f :: s) →
        form_prop (or_formula_of_sequent_iter f s).

  Lemma some_neg_dep_correct :
    ∀(nonempty_v : V)(s : sequent V L)(dep_s : sequent_prop form_prop s),
      some_neg_dep form_prop P s dep_s ↔
        P (or_formula_of_sequent s nonempty_v)
          (form_prop_or_formula_of_sequent nonempty_v s dep_s).

End Some_neg_dep_form_2.

Section Some_neg_form.

Correctness of simplified some_neg semantics

This is the simple (non-dependent) version for arbitrary sequents.

  Variable V : Type.
  Variable L : modal_operators.
  Variable P : lambda_formula V L → Prop.

There remain only two hypothesis for the simple version.

  Hypothesis P_false :
    ∀(nonempty_v : V),
      P (lambda_false nonempty_v) → False.

  Hypothesis P_or_formula : ∀(f1 f2 : lambda_formula V L),
    P (lambda_or f1 f2) ↔ ~(~P f1 ∧ ¬P f2 ).

  Lemma noprop_or : ∀(f1 f2 : lambda_formula V L),
    noprop (lambda_formula V L) f1 →
    noprop (lambda_formula V L) f2 →
    noprop (lambda_formula V L) (lambda_or f1 f2).

  Lemma noprop_or_formula_of_sequnet :
    ∀(nonempty_v : V)(s : sequent V L),
      a_list_prop (noprop (lambda_formula V L)) s →
        noprop (lambda_formula V L) (or_formula_of_sequent s nonempty_v).

  Lemma some_neg_correct :
    ∀(nonempty_v : V)(s : sequent V L),
      some_neg P s ↔ P (or_formula_of_sequent s nonempty_v).

End Some_neg_form.