Library hydras.Ackermann.folReplace

From Coq Require Import Ensembles Lists.List Peano_dec.

From hydras.Ackermann
  Require Import ListExt folProof folLogic folProp.

Section Replacement.

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 reduceImp :
  ∀ (f1 f2 f3 f4 : Formula) (T : System),
    SysPrf T (iffH f1 f3) →
    SysPrf T (iffH f2 f4) →
    SysPrf T (iffH (impH f1 f2) (impH f3 f4)).

Lemma reduceNot (f1 f2 : Formula) (T : System):
 SysPrf T (iffH f1 f2) → SysPrf T (iffH (notH f1) (notH f2)).

Lemma impForall (f1 f2 : Formula) (v : nat) (T : System):
  ¬ In_freeVarSys _ v T →
  SysPrf T (impH f1 f2) → SysPrf T (impH (forallH v f1) (forallH v f2)).

Lemma reduceForall (f1 f2 : Formula) (v : nat) (T : System):
 ¬ In_freeVarSys _ v T →
 SysPrf T (iffH f1 f2) → SysPrf T (iffH (forallH v f1) (forallH v f2)).

Lemma reduceOr (f1 f2 f3 f4 : Formula) (T : System):
 SysPrf T (iffH f1 f3) →
 SysPrf T (iffH f2 f4) → SysPrf T (iffH (orH f1 f2) (orH f3 f4)).

Lemma reduceAnd (f1 f2 f3 f4 : Formula) (T : System):
    SysPrf T (iffH f1 f3) →
    SysPrf T (iffH f2 f4) → SysPrf T (iffH (andH f1 f2) (andH f3 f4)).

Lemma iffExist (f1 f2 : Formula) (v : nat) (T : System):
 ¬ In_freeVarSys _ v T →
 SysPrf T (impH f1 f2) → SysPrf T (impH (existH v f1) (existH v f2)).

Lemma reduceExist (f1 f2 : Formula) (v : nat) (T : System):
  ¬ In_freeVarSys _ v T →
  SysPrf T (iffH f1 f2) → SysPrf T (iffH (existH v f1) (existH v f2)).

Lemma reduceIff (f1 f2 f3 f4 : Formula) (T : System):
 SysPrf T (iffH f1 f3) →
 SysPrf T (iffH f2 f4) → SysPrf T (iffH (iffH f1 f2) (iffH f3 f4)).

Lemma reduceIfThenElse (f1 f2 f3 f4 f5 f6 : Formula) (T : System):
 SysPrf T (iffH f1 f4) →
 SysPrf T (iffH f2 f5) →
 SysPrf T (iffH f3 f6) →
 SysPrf T (iffH (ifThenElseH f1 f2 f3) (ifThenElseH f4 f5 f6)).

Lemma reduceSub (T : System) (v : nat) (s : Term) (f g : Formula):
 ¬ In_freeVarSys L v T →
 SysPrf T (iffH f g) →
 SysPrf T (iffH (substF f v s) (substF g v s)).

Lemma reduceCloseList (l : list nat) (f1 f2 : Formula) (T : System):
 (∀ v : nat, In v l → ¬ In_freeVarSys _ v T) →
 SysPrf T (iffH f1 f2) →
 SysPrf T (iffH (closeList L l f1) (closeList L l f2)).

End Replacement.