Inversion, 3.12 - 3.13

This module proves the inversion lemmas 3.12 and 3.13. The first one, 3.12, states depth preserving inversion in G_n + H. This is the result which is needed inside the syntactic cut-elimination proof. It is therefore formalized completely here. The other, 3.13, states depth preserving inversion for GR_n. The paper does not proof the depth-preserving part and one would need a completely different proof for that. Because 3.13 is never used, I only formalize inversion without depth preservation.

Require Export weakening.

Section Inversion.

  Variable V : Type.
  Variable L : modal_operators.

Need decidable equality on propositional constants for the unused Lemma inversion_admissible_GR_n (3.13)
  Variable v_eq : eq_type V.

Towards Lemma 3.12, Inversion in G_n + H

Closure under inversion for hypothesis'


  Definition conj_head_inversion_closed(ss : set (sequent V L)) : Prop :=
    (sr : sequent V L)(f1 f2 : lambda_formula V L),
      ss ((lf_and f1 f2) :: sr) →
        ss (f1 :: sr) ss (f2 :: sr).

  Definition disj_head_inversion_closed(ss : set (sequent V L)) : Prop :=
    (sr : sequent V L)(f1 f2 : lambda_formula V L),
      ss ((lf_neg (lf_and f1 f2)) :: sr) →
        ss ((lf_neg f1) :: (lf_neg f2) :: sr).

  Definition neg_head_inversion_closed(ss : set (sequent V L)) : Prop :=
    (sr : sequent V L)(f : lambda_formula V L),
      ss ((lf_neg (lf_neg f)) :: sr) →
        ss (f :: sr).

  Definition head_inversion_closed(ss : set (sequent V L)) : Prop :=
    conj_head_inversion_closed ss
    disj_head_inversion_closed ss
    neg_head_inversion_closed ss.

  Lemma head_inversion_closed_empty :
    head_inversion_closed (empty_sequent_set V L).

Prove first that inversion is admissible at head position


  Lemma sequent_other_axiom_G_n_set :
    (n : nat)(f1 : lambda_formula V L)(s1 s2 : sequent V L),
      simple_tautology (f1 :: s1) →
      rank_sequent n (f1 :: s1) →
      (rank_formula n f1rank_sequent n s2) →
      (not (neg_form_maybe prop_form f1)) →
        G_n_set V L n {| assumptions := []; conclusion := s2 ++ s1 |}.

  Lemma other_axiom_G_n_set :
    (n : nat)(f1 f2 : lambda_formula V L)(s : sequent V L),
      simple_tautology (f1 :: s) →
      rank_sequent n (f1 :: s) →
      (rank_formula n f1rank_formula n f2) →
      (not (neg_form_maybe prop_form f1)) →
        G_n_set V L n {| assumptions := []; conclusion := f2 :: s |}.

  Lemma list_subproofs_head_admissible :
    (hyp : set (sequent V L))(n d : nat)
          (f : lambda_formula V L)(sl sr new_ass : sequent V L)
          (ass : list (sequent V L))
          (pl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
                  (map (add_context (f :: sl) sr) ass)),
      every_dep_nth
        (fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
            proof_depth p d)
        (map (add_context (f :: sl) sr) ass) pl
      every_dep_nth
        (fun(a : sequent V L)(p_a : proof (G_n_set V L n) hyp a) ⇒
           (d : nat)(a_tl : sequent V L),
             a = f :: a_tl
             proof_depth p_a d
             (op : proof (G_n_set V L n) hyp (new_ass ++ a_tl)),
               proof_depth op d)
        (map (add_context (f :: sl) sr) ass)
        pl
      →
        (opl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
                              (map (add_context (new_ass ++ sl) sr) ass)),
          every_dep_nth
            (fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
                proof_depth p d)
            (map (add_context (new_ass ++ sl) sr) ass) opl.

  Lemma subproofs_head_admissible :
    (hyp : set (sequent V L))(n d : nat)
          (f1 f2 : lambda_formula V L)(sl sr : sequent V L)
          (ass : list (sequent V L))
          (pl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
                  (map (add_context (f1 :: sl) sr) ass)),
      every_dep_nth
        (fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
            proof_depth p d)
        (map (add_context (f1 :: sl) sr) ass) pl
      every_dep_nth
        (fun(a : sequent V L)(p_a : proof (G_n_set V L n) hyp a) ⇒
           (d : nat)(a_tl : sequent V L),
             a = f1 :: a_tl
             proof_depth p_a d
             (op : proof (G_n_set V L n) hyp (f2 :: a_tl)),
               proof_depth op d)
        (map (add_context (f1 :: sl) sr) ass)
        pl
      →
        (opl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
                              (map (add_context (f2 :: sl) sr) ass)),
          every_dep_nth
            (fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
                proof_depth p d)
            (map (add_context (f2 :: sl) sr) ass) opl.

  Lemma conj_left_head_Gn_admissible :
    (n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
          (f1 f2 : lambda_formula V L),
      conj_head_inversion_closed hyp
        (p_and : proof (G_n_set V L n) hyp gamma)
              (d : nat)(gamma_tl : sequent V L),
          gamma = (lf_and f1 f2) :: gamma_tl
          proof_depth p_and d
            (p : proof (G_n_set V L n) hyp (f1 :: gamma_tl)),
              proof_depth p d.

  Lemma conj_right_head_Gn_admissible :
    (n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
          (f1 f2 : lambda_formula V L),
      conj_head_inversion_closed hyp
        (p_and : proof (G_n_set V L n) hyp gamma)
              (d : nat)(gamma_tl : sequent V L),
          gamma = (lf_and f1 f2) :: gamma_tl
          proof_depth p_and d
            (p : proof (G_n_set V L n) hyp (f2 :: gamma_tl)),
              proof_depth p d.

  Lemma neg_and_inv_head_Gn_admissible_ind :
    (n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
          (f1 f2 : lambda_formula V L),
      disj_head_inversion_closed hyp
        (p_or : proof (G_n_set V L n) hyp gamma)
              (d : nat)(gamma_tl : sequent V L),
          gamma = (lf_neg (lf_and f1 f2)) :: gamma_tl
          proof_depth p_or d
            (p : proof (G_n_set V L n) hyp
                             ((lf_neg f1) :: (lf_neg f2) :: gamma_tl)),
              proof_depth p d.

  Lemma neg_and_inv_head_Gn_depth_admissible :
    (hyp : set (sequent V L))(n d : nat)
          (f1 f2 : lambda_formula V L)(s : sequent V L),
      disj_head_inversion_closed hyp
      provable_at_depth (G_n_set V L n) hyp d ((lf_neg (lf_and f1 f2)) :: s) →
        provable_at_depth (G_n_set V L n) hyp d
                          ((lf_neg f1) :: (lf_neg f2) :: s).

  Lemma neg_and_inv_head_G_n_hyp_admissible :
    (hyp : set (sequent V L))(n : nat)
          (f1 f2 : lambda_formula V L)(s : sequent V L),
      disj_head_inversion_closed hyp
      provable (G_n_set V L n) hyp ((lf_neg (lf_and f1 f2)) :: s) →
        provable (G_n_set V L n) hyp ((lf_neg f1) :: (lf_neg f2) :: s).

  Lemma neg_inv_head_Gn_depth_admissible_ind :
    (n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
          (f : lambda_formula V L),
          neg_head_inversion_closed hyp
        (p_neg : proof (G_n_set V L n) hyp gamma)
              (d : nat)(gamma_tl : sequent V L),
          gamma = (lf_neg (lf_neg f)) :: gamma_tl
          proof_depth p_neg d
            (p : proof (G_n_set V L n) hyp (f :: gamma_tl)),
              proof_depth p d.

  Lemma neg_inv_head_Gn_depth_admissible :
    (hyp : set (sequent V L))(n d : nat)
          (f : lambda_formula V L)(s : sequent V L),
      neg_head_inversion_closed hyp
      provable_at_depth (G_n_set V L n) hyp d ((lf_neg (lf_neg f)) :: s) →
        provable_at_depth (G_n_set V L n) hyp d (f :: s).

  Lemma neg_inv_head_Gn_hyp_admissible :
    (hyp : set (sequent V L))(n : nat)
          (f : lambda_formula V L)(s : sequent V L),
      neg_head_inversion_closed hyp
      provable (G_n_set V L n) hyp ((lf_neg (lf_neg f)) :: s) →
        provable (G_n_set V L n) hyp (f :: s).


  Lemma inversion_depth_preserving_admissible_Gn_H :
    (n : nat)(hyp : set (sequent V L)),
      sequent_multiset hyp
      head_inversion_closed hyp
        depth_preserving_admissible_rule_set (G_n_set V L n) hyp
          (inversion_rules V L).

  Lemma inversion_admissible_Gn_H :
    (n : nat)(hyp : set (sequent V L)),
      sequent_multiset hyp
      head_inversion_closed hyp
        admissible_rule_set (G_n_set V L n) hyp (inversion_rules V L).

Towards Inversion Lemma 3.13 for GR_n

I prove only simple admissibility here, because the depth-preserving part is not needed and the proof for depth preservation is missing in the paper.
prove first that the set of hypothesis in 3.9, provable_subst_n_conclusions, is closed under inversion at head position. This is slightly more difficult than indicated in the paper, because invertable formulas might occur in the the delta part.

  Lemma non_modal_weaken_subst_formula :
    (sigma : lambda_subst V L)(r : sequent_rule V L)
          (f : lambda_formula V L)(s delta : sequent V L),
      one_step_rule r
      not (top_modal_form f) →
      list_reorder (f :: s) (subst_sequent sigma (conclusion r) ++ delta) →
        (delta_l delta_r : sequent V L),
          delta = delta_l ++ f :: delta_r.

  Lemma change_sequent_provable_subst_n_conclusion :
    (rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
          (f : lambda_formula V L)(s1 s2 : sequent V L),
      one_step_rule_set rules
      not (top_modal_form f) →
      provable_subst_n_conclusions rules n npos (f :: s1) →
      rank_sequent n s2
        provable_subst_n_conclusions rules n npos (s2 ++ s1).

  Lemma change_form_provable_subst_n_conclusion :
    (rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
          (f1 f2 : lambda_formula V L)(s : sequent V L),
      one_step_rule_set rules
      not (top_modal_form f1) →
      provable_subst_n_conclusions rules n npos (f1 :: s) →
      rank_formula n f2
        provable_subst_n_conclusions rules n npos (f2 :: s).

  Lemma provable_subst_n_conclusions_rank_non_modal :
    (rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
          (f : lambda_formula V L)(s : sequent V L),
      one_step_rule_set rules
      not (top_modal_form f) →
      provable_subst_n_conclusions rules n npos (f :: s) →
        rank_formula n f.

  Lemma head_inversion_provable_subst_n_conclusion :
    (rules : set (sequent_rule V L))(n : nat)(npos : 0 < n),
      one_step_rule_set rules
        head_inversion_closed (provable_subst_n_conclusions rules n npos).


  Lemma inversion_admissible_GR_n :
    (nonempty_V : V)(rules : set (sequent_rule V L))(n : nat),
      0 < n
      one_step_rule_set rules
        admissible_rule_set
          (GR_n_set rules n) (empty_sequent_set V L)
          (rank_rules n (inversion_rules V L)).

Inversion Lemma for GR

comment on page 15
  Theorem inversion_admissible_GR :
    (nonempty_V : V)(rules : set (sequent_rule V L)),
      one_step_rule_set rules
        admissible_rule_set
          (GR_set rules) (empty_sequent_set V L)
          (inversion_rules V L).

End Inversion.

Implicit Arguments conj_head_inversion_closed [V L].
Implicit Arguments disj_head_inversion_closed [V L].
Implicit Arguments neg_head_inversion_closed [V L].
Implicit Arguments head_inversion_closed [V L].
Implicit Arguments conj_left_head_Gn_admissible [V L].
Implicit Arguments conj_right_head_Gn_admissible [V L].