Library hydras.Ackermann.subProp

From Coq Require Import Ensembles List Peano_dec.
From hydras.Ackermann Require Import ListExt.
From Coq Require Import Arith.

From hydras.Ackermann
  Require Import folProof folLogic folProp folReplace.

From LibHyps Require Export LibHyps.
From hydras Require Export MoreLibHyps NewNotations.

Section Substitution_Properties.

Variable L : Language.
Let Formula := Formula L.
Let Formulas := Formulas L.
Let System := System L.
Let Term := Term L.
Let Terms := Terms L.
Let SysPrf := SysPrf L.

Lemma freeVarSubTerm1 (t : Term):
  ∀ (v : nat) (s : Term) (x : nat),
    In x (freeVarT t) →
    v ≠ x → In x (freeVarT (substT t v s)).

Lemma freeVarSubTerms1 (n : nat) (ts : Terms n) (v : nat) (s : Term) (x : nat):
  In x (freeVarTs ts) →
  v ≠ x → In x (freeVarTs (substTs ts v s)).

Lemma freeVarSubFormula1 (f : Formula):
 ∀ (v : nat) (s : Term) (x : nat),
 v ≠ x →
 In x (freeVarF f) →
 In x (freeVarF (substF f v s)).

Lemma freeVarSubTerm2 (t : Term) :
  ∀ (v : nat) (s : Term) (x : nat),
    In x (freeVarT s) →
    In v (freeVarT t) → In x (freeVarT (substT t v s)).

Lemma freeVarSubTerms2 (n : nat) (ts : Terms n) (v : nat) (s : Term) (x : nat):
 In x (freeVarT s) →
 In v (freeVarTs ts) →
 In x (freeVarTs (substTs ts v s)).

Lemma freeVarSubFormula2 (f : Formula):
  ∀ (v : nat) (s : Term) (x : nat),
    In x (freeVarT s) →
    In v (freeVarF f) →
    In x (freeVarF (substF f v s)).

Lemma freeVarSubTerm3 (t : Term):
  ∀ (v : nat) (s : Term) (x : nat),
    In x (freeVarT (substT t v s)) →
    In x (List.remove eq_nat_dec v (freeVarT t)) ∨
      In x (freeVarT s).

Lemma freeVarSubTerms3 (n : nat) (ts : fol.Terms L n) (v : nat)
  (s : Term) (x : nat):
  In x (freeVarTs (substTs ts v s)) →
  In x (List.remove eq_nat_dec v (freeVarTs ts)) ∨
    In x (freeVarT s).

Lemma freeVarSubFormula3 (f : Formula):
 ∀ (v : nat) (s : Term) (x : nat),
 In x (freeVarF (substF f v s)) →
 In x (List.remove eq_nat_dec v (freeVarF f)) ∨
 In x (freeVarT s).

Lemma freeVarSubTerm4 (t : Term) :
 ∀ (v : nat) (s : Term) (x : nat),
 In x (freeVarT (substT t v s)) →
 ¬ In v (freeVarT t) → In x (freeVarT t).

Lemma freeVarSubTerms4 (n : nat) (ts : Terms n) (v : nat)
  (s : Term) (x : nat):
  In x (freeVarTs (substTs ts v s)) →
  ¬ In v (freeVarTs ts) → In x (freeVarTs ts).

Lemma freeVarSubFormula4 (f : Formula) :
 ∀ (v : nat) (s : Term) (x : nat),
 In x (freeVarF (substF f v s)) →
 ¬ In v (freeVarF f) → In x (freeVarF f).

Lemma subTermNil (t : Term) (v : nat) (s : Term):
 ¬ In v (freeVarT t) → substT t v s = t.

Lemma subTermTrans (t : Term) (v1 v2 : nat) (s : Term):
 ¬ In v2 (List.remove eq_nat_dec v1 (freeVarT t)) →
 substT (substT t v1 (var v2)) v2 s = substT t v1 s.

Lemma subTermExch (t : Term) (v1 v2 : nat) (s1 s2 : Term):
 v1 ≠ v2 →
 ¬ In v2 (freeVarT s1) →
 ¬ In v1 (freeVarT s2) →
 substT (substT t v1 s1) v2 s2 =
 substT (substT t v2 s2) v1 s1.

Lemma subTermsNil (n : nat) (ts : Terms n) (v : nat) (s : Term):
 ¬ In v (freeVarTs ts) → substTs ts v s = ts.

Lemma subTermsTrans (n : nat) (ts : Terms n) (v1 v2 : nat) (s : Term):
 ¬ In v2 (List.remove eq_nat_dec v1 (freeVarTs ts)) →
 substTs (substTs ts v1 (var v2)) v2 s =
 substTs ts v1 s.

Lemma subTermsExch (n : nat) (ts : Terms n) (v1 v2 : nat)
  (s1 s2 : Term):
  v1 ≠ v2 →
  ¬ In v2 (freeVarT s1) →
  ¬ In v1 (freeVarT s2) →
  substTs (substTs ts v1 s1) v2 s2 =
    substTs (substTs ts v2 s2) v1 s1.

Remark subFormulaNTEHelp (f g : Formula) (v : nat) (s : Term):
 SysPrf (Ensembles.Add _ (Empty_set Formula) f) g →
 SysPrf (Ensembles.Add _ (Empty_set Formula) (substF f v s))
   (substF g v s).

Remark subFormulaNTE (f : Formula):
  ∀ (T : System),
    (∀ (v : nat) (s : Term),
        ¬ In v (freeVarF f) →
        SysPrf T (iffH (substF f v s) f)) ∧
      (∀ (v1 v2 : nat) (s : Term),
          ¬ In v2 (List.remove eq_nat_dec v1 (freeVarF f)) →
          SysPrf T
            (iffH (substF (substF f v1 (var v2)) v2 s)
               (substF f v1 s))) ∧
      (∀ (v1 v2 : nat) (s1 s2 : Term),
          v1 ≠ v2 →
          ¬ In v2 (freeVarT s1) →
          ¬ In v1 (freeVarT s2) →
          SysPrf T
            (iffH (substF (substF f v1 s1) v2 s2)
               (substF (substF f v2 s2) v1 s1))).

Lemma subFormulaNil :
  ∀ (f : Formula) (T : System) (v : nat) (s : Term),
    ¬ In v (freeVarF f) → SysPrf T (iffH (substF f v s) f).

Lemma subFormulaTrans :
  ∀ (f : Formula) (T : System) (v1 v2 : nat) (s : Term),
    ¬ In v2 (List.remove eq_nat_dec v1 (freeVarF f)) →
    SysPrf T
      (iffH (substF (substF f v1 (var v2)) v2 s)
         (substF f v1 s)).

Lemma subFormulaExch :
 ∀ (f : Formula) (T : System) (v1 v2 : nat) (s1 s2 : Term),
 v1 ≠ v2 →
 ¬ In v2 (freeVarT s1) →
 ¬ In v1 (freeVarT s2) →
 SysPrf T
   (iffH (substF (substF f v1 s1) v2 s2)
      (substF (substF f v2 s2) v1 s1)).

End Substitution_Properties.