Models for the propositional fragment
Require Export some_neg_form propositional_rules.
Section Propositional_models.
Variable V : Type.
Variable L : modal_operators.
Definition prop_model : Type := set V.
Fixpoint is_prop_model(m : prop_model)(f : lambda_formula V L)
(prop_f : propositional f) : Prop :=
match f return propositional f → Prop with
| lf_prop v ⇒ fun _ ⇒ m v
| lf_neg f1 ⇒ fun(H : propositional (lf_neg f1)) ⇒
not (is_prop_model m f1 (propositional_neg f1 H))
| lf_and f1 f2 ⇒ fun(H : propositional (lf_and f1 f2)) ⇒
is_prop_model m f1 (propositional_and_left f1 f2 H) ∧
is_prop_model m f2 (propositional_and_right f1 f2 H)
| lf_modal op args ⇒ fun(H : propositional (lf_modal op args)) ⇒
propositional_tcc_modal op args H
end prop_f.
Lemma is_prop_model_tcc_irr :
∀(m : prop_model)(f : lambda_formula V L)(p1 p2 : propositional f),
is_prop_model m f p1 → is_prop_model m f p2.
nonempty_v is in the wrong position here, but this way the
lemma can be used directly in prop_model_sequent_interpretation.
Lemma is_prop_model_false :
∀(m : prop_model)(nonempty_v : V)
(prop_false : propositional (lambda_false nonempty_v)),
is_prop_model m (lambda_false nonempty_v) prop_false → False.
Definition prop_valid(f : lambda_formula V L)
(prop_f : propositional f) : Prop :=
∀(m : prop_model), is_prop_model m f prop_f.
Definition prop_valid_sequent(nonempty_v : V)(s : sequent V L)
(prop_s : propositional_sequent s) : Prop :=
prop_valid (or_formula_of_sequent s nonempty_v)
(propositional_or_formula nonempty_v s prop_s).
∀(m : prop_model)(nonempty_v : V)
(prop_false : propositional (lambda_false nonempty_v)),
is_prop_model m (lambda_false nonempty_v) prop_false → False.
Definition prop_valid(f : lambda_formula V L)
(prop_f : propositional f) : Prop :=
∀(m : prop_model), is_prop_model m f prop_f.
Definition prop_valid_sequent(nonempty_v : V)(s : sequent V L)
(prop_s : propositional_sequent s) : Prop :=
prop_valid (or_formula_of_sequent s nonempty_v)
(propositional_or_formula nonempty_v s prop_s).
Definition prop_sequent_interpretation(m : prop_model)(s : sequent V L)
(prop_seq : propositional_sequent s) : Prop :=
some_neg_dep propositional (is_prop_model m) s prop_seq.
Lemma prop_sequent_interpretation_tcc_irr :
∀(m : prop_model)(s : sequent V L)(ps1 ps2 : propositional_sequent s),
prop_sequent_interpretation m s ps1 →
prop_sequent_interpretation m s ps2.
Lemma prop_sequent_interpretation_empty :
∀(m : prop_model)(prop : propositional_sequent []),
prop_sequent_interpretation m [] prop → False.
Lemma prop_sequent_interpretation_singleton :
∀(m : prop_model)(f : lambda_formula V L)
(prop_s : propositional_sequent [f]),
prop_sequent_interpretation m [f] prop_s ↔
is_prop_model m f (prop_s 0 (lt_0_Sn 0)).
Lemma prop_sequent_interpretation_nth_intro :
∀(m : prop_model)(s : sequent V L)(n : nat)(n_less : n < length s)
(prop_s : propositional_sequent s),
is_prop_model m (nth s n n_less) (prop_s n n_less) →
prop_sequent_interpretation m s prop_s.
Lemma prop_sequent_interpretation_cons_case_elim :
∀(m : prop_model)(f : lambda_formula V L)(s : sequent V L)
(prop_fs : propositional_sequent (f :: s)),
prop_sequent_interpretation m (f :: s) prop_fs →
((s = [] ∧ is_prop_model m f
(propositional_sequent_head _ _ prop_fs)) ∨
(s ≠ [] ∧
~(~is_prop_model m f
(propositional_sequent_head _ _ prop_fs) ∧
¬prop_sequent_interpretation m s
(propositional_sequent_tail _ _ prop_fs)))).
Lemma prop_sequent_interpretation_cons_cons_elim :
∀(m : prop_model)(f1 f2 : lambda_formula V L)(s : sequent V L)
(prop_s : propositional_sequent (f1 :: f2 :: s)),
prop_sequent_interpretation m (f1 :: f2 :: s) prop_s →
~(~is_prop_model m f1 (propositional_sequent_head _ _ prop_s) ∧
¬prop_sequent_interpretation m (f2 :: s)
(propositional_sequent_tail _ _ prop_s)).
Lemma prop_sequent_interpretation_length_case_intro :
∀(m : prop_model)(s : sequent V L)(prop_s : propositional_sequent s),
(length s = 1 → prop_sequent_interpretation m s prop_s) →
(length s ≠ 1 → ~~prop_sequent_interpretation m s prop_s) →
prop_sequent_interpretation m s prop_s.
Lemma prop_sequent_interpretation_cons_case_intro :
∀(m : prop_model)(f : lambda_formula V L)(s : sequent V L)
(prop_fs : propositional_sequent (f :: s)),
(s = [] → is_prop_model m f (propositional_sequent_head _ _ prop_fs))
→
(s ≠ [] → ~~prop_sequent_interpretation m (f :: s) prop_fs) →
prop_sequent_interpretation m (f :: s) prop_fs.
Lemma prop_sequent_interpretation_cons_cons_intro :
∀(m : prop_model)(f1 f2 : lambda_formula V L)(s : sequent V L)
(prop_fs : propositional_sequent (f1 :: f2 :: s)),
~~prop_sequent_interpretation m (f1 :: f2 :: s) prop_fs →
prop_sequent_interpretation m (f1 :: f2 :: s) prop_fs.
Lemma prop_sequent_interpretation_append :
∀(m : prop_model)(sl sr : sequent V L)
(prop_sl : propositional_sequent sl)
(prop_sr : propositional_sequent sr),
(prop_sequent_interpretation m sl prop_sl ∨
prop_sequent_interpretation m sr prop_sr) →
prop_sequent_interpretation m (sl ++ sr)
(propositional_sequent_append sl sr prop_sl prop_sr).
Lemma prop_sequent_interpretation_append_split :
∀(m : prop_model)(sl sr : sequent V L)
(prop_sl_sr : propositional_sequent (sl ++ sr)),
prop_sequent_interpretation m (sl ++ sr) prop_sl_sr →
~(~ (∀ (prop_sl : propositional_sequent sl),
prop_sequent_interpretation m sl prop_sl) ∧
¬ (∀ (prop_sr : propositional_sequent sr),
prop_sequent_interpretation m sr prop_sr)).
Lemma prop_sequent_interpretation_add_context :
∀(m : prop_model)(sl s sr : sequent V L)
(prop_sl : propositional_sequent sl)
(prop_s : propositional_sequent s)
(prop_sr : propositional_sequent sr),
(prop_sequent_interpretation m sl prop_sl ∨
prop_sequent_interpretation m s prop_s ∨
prop_sequent_interpretation m sr prop_sr) →
prop_sequent_interpretation m (add_context sl sr s)
(propositional_add_context sl sr s prop_sl prop_sr prop_s).
Lemma prop_sequent_interpretation_add_context_split :
∀(m : prop_model)(sl s sr : sequent V L)
(prop_sl_s_sr : propositional_sequent (add_context sl sr s)),
prop_sequent_interpretation m (add_context sl sr s) prop_sl_s_sr
→
~(~(∀(prop_sl : propositional_sequent sl),
prop_sequent_interpretation m sl prop_sl) ∧
~(∀(prop_s : propositional_sequent s),
prop_sequent_interpretation m s prop_s) ∧
~(∀(prop_sr : propositional_sequent sr),
prop_sequent_interpretation m sr prop_sr)).
Lemma is_prop_model_or :
∀(m : prop_model)(f1 f2 : lambda_formula V L)
(prop_f1 : propositional f1)(prop_f2 : propositional f2),
is_prop_model m (lambda_or f1 f2)
(propositional_lambda_or _ _ prop_f1 prop_f2)
↔
~(~is_prop_model m f1 prop_f1 ∧ ¬is_prop_model m f2 prop_f2).
Lemma prop_model_sequent_interpretation :
∀(nonempty_v : V)(m : prop_model)(s : sequent V L)
(prop_seq : propositional_sequent s),
prop_sequent_interpretation m s prop_seq
↔
is_prop_model m (or_formula_of_sequent s nonempty_v)
(propositional_or_formula nonempty_v _ prop_seq).
End Propositional_models.
Implicit Arguments is_prop_model [V L].
Implicit Arguments is_prop_model_tcc_irr [V L].
Implicit Arguments is_prop_model_false [V L].
Implicit Arguments prop_valid [V L].
Implicit Arguments prop_valid_sequent [V L].
Implicit Arguments prop_sequent_interpretation [V L].
Implicit Arguments prop_sequent_interpretation_tcc_irr [V L].
Implicit Arguments prop_sequent_interpretation_singleton [V L].
Implicit Arguments prop_sequent_interpretation_nth_intro [V L].
Implicit Arguments prop_model_sequent_interpretation [V L].
Implicit Arguments prop_sequent_interpretation_append [V L].
Implicit Arguments prop_sequent_interpretation_append_split [V L].
Implicit Arguments prop_sequent_interpretation_add_context [V L].
Implicit Arguments prop_sequent_interpretation_add_context_split [V L].