Library hydras.Ackermann.subAll

From Coq Require Import Ensembles List Arith Peano_dec.

From hydras.Ackermann Require Import ListExt folProof folLogic
  folLogic2 folProp.
From hydras Require Import folReplace subProp Compat815.
From Coq Require Import Lia.
Import FolNotations.

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

Section SubAllVars.

Variable L : Language.
Notation Formula := (Formula L) (only parsing).
Notation Formulas := (Formulas L) (only parsing).
Notation System := (System L) (only parsing).
Notation Term := (Term L) (only parsing).
Notation Terms := (Terms L) (only parsing).
Notation SysPrf := (SysPrf L) (only parsing).

Fixpoint subAllTerm (t : fol.Term L) : (nat → fol.Term L) → fol.Term L :=
  match t return ((nat → fol.Term L) → fol.Term L) with
  | var x ⇒ fun m ⇒ m x
  | apply f ts ⇒ fun m ⇒ apply f (subAllTerms _ ts m)
  end
 
 with subAllTerms (n : nat) (ts : fol.Terms L n) {struct ts} :
 (nat → fol.Term L) → fol.Terms L n :=
  match
    ts in (fol.Terms _ n) return ((nat → fol.Term L) → fol.Terms L n)
  with
  | Tnil ⇒ fun _ ⇒ Tnil
  | Tcons n' t ss ⇒
      fun m ⇒ Tcons (subAllTerm t m) (subAllTerms _ ss m)
  end.

Lemma subAllTerm_ext (t : fol.Term L) :
  ∀ (m1 m2 : nat → fol.Term L),
    (∀ m : nat, In m (freeVarT t) → m1 m = m2 m) →
    subAllTerm t m1 = subAllTerm t m2.

Lemma subAllTerms_ext (n : nat) (ts : fol.Terms L n) (m1 m2 : nat → fol.Term L):
 (∀ m : nat, In m (freeVarTs ts) → m1 m = m2 m) →
 subAllTerms n ts m1 = subAllTerms n ts m2.

Fixpoint freeVarMap (l : list nat) : (nat → fol.Term L) → list nat :=
  match l with
  | nil ⇒ fun _ ⇒ nil
  | a :: l' ⇒ fun m ⇒ freeVarT (m a) ++ freeVarMap l' m
  end.

Lemma freeVarMap_ext (l : list nat) (f1 f2 : nat → fol.Term L):
 (∀ m : nat, In m l → f1 m = f2 m) →
 freeVarMap l f1 = freeVarMap l f2.

Lemma freeVarMap1 (l : list nat) (m : nat → fol.Term L) (v n : nat):
 In v (freeVarT (m n)) → In n l → In v (freeVarMap l m).

Fixpoint subAllFormula (f : Formula) (m : (nat → Term)) {struct f} : Formula :=
  match f with
  | (t = s)%fol ⇒ equal (subAllTerm t m) (subAllTerm s m)
  | atomic r ts ⇒ atomic r (subAllTerms _ ts m)
  | (f → g)%fol ⇒
      (subAllFormula f m → subAllFormula g m)%fol
  | (¬ f)%fol ⇒ (¬ subAllFormula f m)%fol
  | (allH n, f)%fol ⇒
      let nv :=
        newVar
          (freeVarF f ++
           freeVarMap (freeVarF (allH n, f)%fol) m) in
      (allH nv,
        (subAllFormula f
           (fun v : nat ⇒
            match eq_nat_dec v n with
            | left _ ⇒ var nv
            | right _ ⇒ m v
            end)))%fol
  end.

Lemma subAllFormula_ext :
 ∀ (f : fol.Formula L) (m1 m2 : nat → fol.Term L),
 (∀ m : nat, In m (freeVarF f) → m1 m = m2 m) →
 subAllFormula f m1 = subAllFormula f m2.

Lemma freeVarSubAllTerm1 (t : fol.Term L) (m : nat → fol.Term L) (v : nat):
 In v (freeVarT (subAllTerm t m)) →
 ∃ n : nat, In n (freeVarT t) ∧ In v (freeVarT (m n)).

Lemma freeVarSubAllTerms1 (n : nat) (ts : fol.Terms L n)
  (m : nat → fol.Term L) (v : nat):
 In v (freeVarTs (subAllTerms n ts m)) →
 ∃ a : nat, In a (freeVarTs ts) ∧ In v (freeVarT (m a)).

Lemma freeVarSubAllTerm2 (t : fol.Term L) (m : nat → fol.Term L) (v n : nat):
 In n (freeVarT t) →
 In v (freeVarT (m n)) → In v (freeVarT (subAllTerm t m)).

Lemma freeVarSubAllTerms2 (a : nat) (ts : fol.Terms L a)
  (m : nat → fol.Term L)
  (v n : nat):
  In n (freeVarTs ts) →
  In v (freeVarT (m n)) → In v (freeVarTs (subAllTerms a ts m)).

Lemma freeVarSubAllFormula1 :
 ∀ (f : fol.Formula L) (m : nat → fol.Term L) (v : nat),
 In v (freeVarF (subAllFormula f m)) →
 ∃ n : nat, In n (freeVarF f) ∧ In v (freeVarT (m n)).

Lemma freeVarSubAllFormula2 :
 ∀ (f : fol.Formula L) (m : nat → fol.Term L) (v n : nat),
 In n (freeVarF f) →
 In v (freeVarT (m n)) →
 In v (freeVarF (subAllFormula f m)).

Lemma subSubAllTerm (t : fol.Term L) (m : nat → fol.Term L)
  (v : nat) (s : fol.Term L):
 substT (subAllTerm t m) v s =
 subAllTerm t (fun n : nat ⇒ substT (m n) v s).

Lemma subSubAllTerms (n : nat) (ts : fol.Terms L n) (m : nat → fol.Term L)
  (v : nat) (s : fol.Term L) :
  substTs (subAllTerms n ts m) v s =
    subAllTerms n ts (fun n : nat ⇒ substT (m n) v s).

Lemma subSubAllFormula :
  ∀ (T : fol.System L) (f : fol.Formula L) (m : nat → fol.Term L)
         (v : nat) (s : fol.Term L),
    folProof.SysPrf L T
      (iffH (substF (subAllFormula f m) v s)
         (subAllFormula f (fun n : nat ⇒ substT (m n) v s))).

Lemma subAllTermId (t : fol.Term L):
  subAllTerm t (fun x : nat ⇒ var x) = t.

Lemma subAllTermsId (n : nat) (ts : fol.Terms L n):
  subAllTerms n ts (fun x : nat ⇒ var x) = ts.

Lemma subAllFormulaId (T : fol.System L) (f : fol.Formula L):
 folProof.SysPrf L T
   (iffH (subAllFormula f (fun x : nat ⇒ var x)) f).

Lemma subAllSubAllTerm (t : fol.Term L) :
 ∀ (m1 m2 : nat → fol.Term L),
 subAllTerm (subAllTerm t m1) m2 =
 subAllTerm t (fun n : nat ⇒ subAllTerm (m1 n) m2).

Lemma subAllSubAllTerms (n : nat) (ts : fol.Terms L n) (m1 m2 : nat → fol.Term L):
 subAllTerms n (subAllTerms n ts m1) m2 =
 subAllTerms n ts (fun n : nat ⇒ subAllTerm (m1 n) m2).

Lemma subAllSubAllFormula (T : fol.System L) (f : fol.Formula L):
 ∀ (m1 m2 : nat → fol.Term L),
 folProof.SysPrf L T
   (iffH (subAllFormula (subAllFormula f m1) m2)
      (subAllFormula f (fun n : nat ⇒ subAllTerm (m1 n) m2))).

Section subAllCloseFrom.

Fixpoint closeFrom (a n : nat) (f : fol.Formula L) {struct n} :
 fol.Formula L :=
  match n with
  | O ⇒ f
  | S m ⇒ forallH (a + m) (closeFrom a m f)
  end.

Opaque le_lt_dec.

Lemma liftCloseFrom (n : nat) :
 ∀(f : fol.Formula L) (T : fol.System L) (m : nat),
 (∀ v : nat, In v (freeVarF f) → v < m) →
 n ≤ m →
 folProof.SysPrf L T (closeFrom 0 n f) →
 folProof.SysPrf L T
   (closeFrom m n
      (subAllFormula f
         (fun x : nat ⇒
          match le_lt_dec n x with
          | left _ ⇒ var x
          | right _ ⇒ var (m + x)
          end))).

Lemma subAllCloseFrom1 :
  ∀ (n m : nat) (map : nat → fol.Term L) (f : fol.Formula L)
         (T : fol.System L),
    (∀ v : nat,
        v < n → ∀ w : nat, In w (freeVarT (map (m + v))) → w < m) →
    folProof.SysPrf L T (closeFrom m n f) →
    folProof.SysPrf L T
      (subAllFormula f
         (fun x : nat ⇒
            match le_lt_dec m x with
            | left _ ⇒
                match le_lt_dec (m + n) x with
                | left _ ⇒ var x
                | right _ ⇒ map x
                end
            | right _ ⇒ var x
            end)).

Lemma subAllCloseFrom :
  ∀ (n : nat) (m : nat → fol.Term L) (f : fol.Formula L)
         (T : fol.System L),
    folProof.SysPrf L T (closeFrom 0 n f) →
    folProof.SysPrf L T
      (subAllFormula f
         (fun x : nat ⇒
            match le_lt_dec n x with
            | left _ ⇒ var x
            | right _ ⇒ m x
            end)).

Lemma reduceSubAll :
  ∀ (T : fol.System L) (map : nat → fol.Term L) (A B : fol.Formula L),
    (∀ v : nat, ¬ In_freeVarSys L v T) →
    folProof.SysPrf L T (iffH A B) →
    folProof.SysPrf L T (iffH (subAllFormula A map) (subAllFormula B map)).

End subAllCloseFrom.

Lemma subToSubAll (T : fol.System L) (A : fol.Formula L) (v : nat)
  (s : fol.Term L):
 folProof.SysPrf L T
   (iffH (substF A v s)
      (subAllFormula A
         (fun x : nat ⇒
          match eq_nat_dec v x with
          | left _ ⇒ s
          | right _ ⇒ var x
          end))).

Lemma subAllSubFormula :
  ∀ (T : fol.System L) (A : fol.Formula L) (v : nat)
         (s : fol.Term L) (map : nat → fol.Term L),
    folProof.SysPrf L T
      (iffH (subAllFormula (substF A v s) map)
         (subAllFormula A
            (fun x : nat ⇒
               match eq_nat_dec v x with
               | left _ ⇒ subAllTerm s map
               | right _ ⇒ map x
               end))).

End SubAllVars.