Require Export formulas list_set functions.
Section Substitutions.
Variable V : Type.
Variable L : modal_operators.
need a decidable equality on propositional constants for limit_subst
Definition lambda_subst : Type := V → lambda_formula V L.
Definition subst_form(sigma : lambda_subst)(f : lambda_formula V L) :
lambda_formula V L :=
lambda_formula_rec sigma lf_neg lf_and lf_modal f.
Lemma subst_form_char :
∀(sigma : lambda_subst)(f : lambda_formula V L),
subst_form sigma f =
match f with
| lf_prop v ⇒ sigma v
| lf_neg f ⇒ lf_neg (subst_form sigma f)
| lf_and f1 f2 ⇒ lf_and (subst_form sigma f1) (subst_form sigma f2)
| lf_modal op args ⇒
lf_modal op (counted_map (subst_form sigma) args)
end.
Lemma subst_form_or :
∀(f1 f2 : lambda_formula V L)(sigma : lambda_subst),
subst_form sigma (lambda_or f1 f2) =
lambda_or (subst_form sigma f1) (subst_form sigma f2).
Lemma subst_form_rank_increase :
∀(f : lambda_formula V L)(sigma : lambda_subst),
modal_rank f ≤ modal_rank (subst_form sigma f).
Definition id_subst(v : V) : lambda_formula V L := lf_prop v.
Lemma subst_form_id : ∀(f : lambda_formula V L),
subst_form id_subst f = f.
Definition subst_compose(sigma_1 sigma_2 : lambda_subst) : lambda_subst :=
fun(v : V) ⇒ subst_form sigma_1 (sigma_2 v).
Lemma subst_form_compose :
∀(f : lambda_formula V L)(sigma_1 sigma_2 : lambda_subst),
subst_form (subst_compose sigma_1 sigma_2) f =
subst_form sigma_1 (subst_form sigma_2 f).
Lemma subst_compose_id_right :
∀(sigma : lambda_subst),
subst_compose sigma id_subst ≡ sigma.
Lemma subst_compose_assoc :
∀(sigma1 sigma2 sigma3 : lambda_subst),
subst_compose (subst_compose sigma1 sigma2) sigma3 ≡
subst_compose sigma1 (subst_compose sigma2 sigma3).
Definition subst_sequent(sigma : lambda_subst)(s : sequent V L) :
sequent V L :=
map (subst_form sigma) s.
Lemma length_subst_sequent : ∀(sigma : lambda_subst)(s : sequent V L),
length (subst_sequent sigma s) = length s.
Lemma subst_sequent_id :
∀(s : sequent V L), subst_sequent id_subst s = s.
Lemma subst_sequent_append :
∀(sigma : lambda_subst)(s1 s2 : sequent V L),
subst_sequent sigma (s1 ++ s2) =
(subst_sequent sigma s1) ++ (subst_sequent sigma s2).
Lemma neg_sequent_subst_sequent :
∀(sigma : lambda_subst)(s : sequent V L),
every_nth neg_form s → every_nth neg_form (subst_sequent sigma s).
Lemma nth_subst_sequent :
∀(sigma : lambda_subst)(s : sequent V L)
(n : nat)(n_less_subst : n < length (subst_sequent sigma s))
(n_less_s : n < length s),
nth (subst_sequent sigma s) n n_less_subst =
subst_form sigma (nth s n n_less_s).
Lemma list_reorder_subst_sequent :
∀(sigma : lambda_subst)(s1 s2 : sequent V L),
list_reorder s1 s2 →
list_reorder (subst_sequent sigma s1) (subst_sequent sigma s2).
Lemma or_formula_subst_sequent_tcc :
∀(s : sequent V L)(sigma : lambda_subst),
s ≠ [] → subst_sequent sigma s ≠ [].
Lemma or_formula_subst_sequent :
∀(s : sequent V L)(sigma : lambda_subst)(nonempty_s : s ≠ []),
or_formula_of_ne_sequent (subst_sequent sigma s)
(or_formula_subst_sequent_tcc s sigma nonempty_s) =
subst_form sigma (or_formula_of_ne_sequent s nonempty_s).
Lemma subst_sequent_rank_increase :
∀(n : nat)(s : sequent V L)(sigma : lambda_subst),
rank_sequent n (subst_sequent sigma s) → rank_sequent n s.
Lemma subst_sequent_compose :
∀(s : sequent V L)(sigma_1 sigma_2 : lambda_subst),
subst_sequent (subst_compose sigma_1 sigma_2) s =
subst_sequent sigma_1 (subst_sequent sigma_2 s).
Definition rank_subst(n : nat)(sigma : lambda_subst) : Prop :=
∀(v : V), rank_formula n (sigma v).
Lemma nonempty_rank_subst : ∀(v : V)(n : nat)(sigma : lambda_subst),
rank_subst n sigma → 0 < n.
Lemma rank_subst_ge :
∀(n1 n2 : nat),
n1 ≤ n2 →
subset (rank_subst n1) (rank_subst n2).
Lemma rank_subst_update :
∀(sigma : lambda_subst)(n : nat)(v : V)(f : lambda_formula V L),
rank_formula n f →
rank_subst n sigma →
rank_subst n (function_update v_eq sigma v f).
Lemma rank_formula_subst_formula_add :
∀(f : lambda_formula V L)(sigma : lambda_subst)(n k : nat),
1 ≤ k →
rank_formula n f →
rank_subst k sigma →
rank_formula (n + k - 1) (subst_form sigma f).
Lemma rank_sequent_subst_add :
∀(s : sequent V L)(sigma : lambda_subst)(n k npk : nat),
rank_sequent n s →
rank_subst k sigma →
1 ≤ k →
n + k - 1 = npk →
rank_sequent npk (subst_sequent sigma s).
Lemma rank_sequent_subst_prop_sequent :
∀(s : sequent V L)(sigma : lambda_subst)(n : nat),
prop_sequent s →
rank_subst n sigma →
rank_sequent n (subst_sequent sigma s).
Lemma rank_subst_subst_compose :
∀(n k npk : nat)(sigma_1 sigma_2 : lambda_subst),
rank_subst (S n) sigma_1 →
rank_subst (S k) sigma_2 →
S (n + k) = npk →
rank_subst npk (subst_compose sigma_1 sigma_2).
Definition subst_sequent_set(sigma : lambda_subst)(ss : set (sequent V L))
: set (sequent V L) :=
fun(s : sequent V L) ⇒
∃(o : sequent V L),
ss o ∧ s = subst_sequent sigma o.
Lemma subst_sequent_set_empty :
∀(sigma : lambda_subst),
set_equal (subst_sequent_set sigma (empty_sequent_set V L))
(empty_sequent_set V L).
Definition subst_sequent_rule(sigma : lambda_subst)(r : sequent_rule V L)
: sequent_rule V L :=
{| assumptions := map (subst_sequent sigma) (assumptions r);
conclusion := subst_sequent sigma (conclusion r)
|}.
Lemma rule_has_rank_subst_rule :
∀(sigma : lambda_subst)(r : sequent_rule V L)(n k : nat),
rule_has_rank n r →
rank_subst (S k) sigma →
rule_has_rank (n + k) (subst_sequent_rule sigma r).
Definition subst_closed_rule_set(rules : set (sequent_rule V L)) : Prop :=
∀(sigma : lambda_subst)(r : sequent_rule V L),
rules r → rules (subst_sequent_rule sigma r).
Lemma rank_formula_id_subst : ∀(n : nat)(v : V),
0 < n → rank_formula n (id_subst v).
Lemma rank_subst_id_subst : ∀(n : nat),
0 < n → rank_subst n id_subst.
Definition limit_subst(pv : list V)(sigma : lambda_subst) : lambda_subst :=
fun(v : V) ⇒
if member v_eq v pv
then sigma v
else id_subst v.
Lemma rank_subst_limit_lf_modal :
∀(n : nat)(v : V)(sigma : lambda_subst)
(op : operator L)
(args : counted_list (lambda_formula V L) (arity L op)),
every_nth prop_form (list_of_counted_list args) →
In v (prop_var_formula (lf_modal op args)) →
rank_formula n (subst_form sigma (lf_modal op args)) →
rank_formula (pred n) (sigma v).
Definition subst_eq_on_vars(sigma1 sigma2 : lambda_subst)(pv : list V)
: Prop :=
∀(v : V), In v pv → sigma1 v = sigma2 v.
Lemma subst_eq_on_vars_empty :
∀(sigma1 sigma2 : lambda_subst),
subst_eq_on_vars sigma1 sigma2 [].
Lemma subst_eq_on_vars_symm :
∀(sigma1 sigma2 : lambda_subst)(pv : list V),
subst_eq_on_vars sigma1 sigma2 pv →
subst_eq_on_vars sigma2 sigma1 pv.
Lemma subst_eq_on_vars_trans :
∀(sigma1 sigma2 sigma3: lambda_subst)(pv : list V),
subst_eq_on_vars sigma1 sigma2 pv →
subst_eq_on_vars sigma2 sigma3 pv →
subst_eq_on_vars sigma1 sigma3 pv.
Lemma subst_eq_on_vars_trans_rev :
∀(sigma1 sigma2 sigma3: lambda_subst)(pv : list V),
subst_eq_on_vars sigma3 sigma2 pv →
subst_eq_on_vars sigma1 sigma2 pv →
subst_eq_on_vars sigma1 sigma3 pv.
Lemma subst_eq_on_vars_seq :
∀(sigma1 sigma2 : lambda_subst)(pv : list V),
sigma1 ≡ sigma2 →
subst_eq_on_vars
sigma1
sigma2
pv.
Lemma subst_eq_on_vars_compose_right_change :
∀(subst1 subst2 subst3 : lambda_subst)(pv : list V),
subst_eq_on_vars subst2 subst3 pv →
subst_eq_on_vars
(subst_compose subst1 subst2)
(subst_compose subst1 subst3) pv.
Lemma subst_eq_on_vars_append :
∀(pv1 pv2 : list V)(sigma1 sigma2 : lambda_subst),
subst_eq_on_vars sigma1 sigma2 pv1 →
subst_eq_on_vars sigma1 sigma2 pv2 →
subst_eq_on_vars sigma1 sigma2 (pv1 ++ pv2).
Lemma subst_formula_eq :
∀(sigma1 sigma2 : lambda_subst)
(f : lambda_formula V L)(prop_vars : list V),
incl (prop_var_formula f) prop_vars →
subst_eq_on_vars sigma1 sigma2 prop_vars →
subst_form sigma1 f = subst_form sigma2 f.
Proof the case for modal arguments again, because it is needed
separately.
Lemma subst_modal_args_eq :
∀(sigma1 sigma2 : lambda_subst)
(n : nat)(args : counted_list (lambda_formula V L) n)
(prop_vars : list V),
incl (prop_var_modal_args n args) prop_vars →
subst_eq_on_vars sigma1 sigma2 prop_vars →
counted_map (subst_form sigma1) args =
counted_map (subst_form sigma2) args.
Lemma subst_sequent_eq :
∀(sigma1 sigma2 : lambda_subst)(s : sequent V L)(prop_vars : list V),
incl (prop_var_sequent s) prop_vars →
subst_eq_on_vars sigma1 sigma2 prop_vars →
subst_sequent sigma1 s = subst_sequent sigma2 s.
∀(sigma1 sigma2 : lambda_subst)
(n : nat)(args : counted_list (lambda_formula V L) n)
(prop_vars : list V),
incl (prop_var_modal_args n args) prop_vars →
subst_eq_on_vars sigma1 sigma2 prop_vars →
counted_map (subst_form sigma1) args =
counted_map (subst_form sigma2) args.
Lemma subst_sequent_eq :
∀(sigma1 sigma2 : lambda_subst)(s : sequent V L)(prop_vars : list V),
incl (prop_var_sequent s) prop_vars →
subst_eq_on_vars sigma1 sigma2 prop_vars →
subst_sequent sigma1 s = subst_sequent sigma2 s.
Lemma subst_eq_on_vars_limit :
∀(sigma : lambda_subst)(pv : list V),
subst_eq_on_vars (limit_subst pv sigma) sigma pv.
Lemma subst_sequent_limit_eq :
∀(s : sequent V L)(sigma : lambda_subst)(prop_vars : list V),
incl (prop_var_sequent s) prop_vars →
subst_sequent (limit_subst prop_vars sigma) s = subst_sequent sigma s.
Lemma map_subst_sequent_limit_eq :
∀(ss : list (sequent V L))(sigma : lambda_subst)(prop_vars : list V),
incl (flatten (map prop_var_sequent ss)) prop_vars →
map (subst_sequent (limit_subst prop_vars sigma)) ss =
map (subst_sequent sigma) ss.
End Substitutions.
Implicit Arguments subst_form [V L].
Implicit Arguments subst_form_char [V L].
Implicit Arguments subst_compose [V L].
Implicit Arguments subst_sequent [V L].
Implicit Arguments rank_subst [V L].
Implicit Arguments rank_formula_subst_formula_add [V L].
Implicit Arguments or_formula_subst_sequent_tcc [V L].
Implicit Arguments nonempty_rank_subst [V L].
Implicit Arguments rank_subst_ge [V L].
Implicit Arguments rank_sequent_subst_add [V L].
Implicit Arguments subst_sequent_set [V L].
Implicit Arguments subst_sequent_rule [V L].
Implicit Arguments subst_closed_rule_set [V L].
Implicit Arguments id_subst [[V] [L]].
Implicit Arguments subst_eq_on_vars [V L].
Implicit Arguments limit_subst [V L].