Library hydras.Ackermann.folLogic3

From Coq Require Import Ensembles List Arith Lia.
From LibHyps Require Export LibHyps.

From hydras.Ackermann Require Import ListExt folProp folProof.
From hydras.Ackermann Require Export folLogic folLogic2.
From hydras.Ackermann Require Import subProp folReplace subAll misc.
From hydras Require Import Compat815.
From hydras Require Export MoreLibHyps.
Import FolNotations.

Section Equality_Logic_Rules.

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).

Let Prf := Prf L.
Let SysPrf := SysPrf L.

Lemma eqRefl (T : fol.System L) (a : fol.Term L):
  SysPrf T (a = a)%fol.

Lemma eqSym (T : fol.System L) (a b : fol.Term L):
  SysPrf T (a = b)%fol → SysPrf T (b = a)%fol.

Lemma eqTrans (T : fol.System L) (a b c : fol.Term L):
 SysPrf T (a = b)%fol → SysPrf T (b = c)%fol →
 SysPrf T (a = c)%fol.

Fixpoint PairwiseEqual (T : fol.System L) (n : nat) {struct n} :
 fol.Terms L n → fol.Terms L n → Prop :=
  match n return (fol.Terms L n → fol.Terms L n → Prop) with
  | O ⇒ fun ts ss : fol.Terms L 0 ⇒ True
  | S x ⇒
      fun ts ss : fol.Terms L (S x) ⇒
      let (a, b) := proj1_sig (consTerms L x ts) in
      let (c, d) := proj1_sig (consTerms L x ss) in
      SysPrf T (a = c)%fol ∧ PairwiseEqual T x b d
  end.

Let termsMap (m : nat) (ts ss : fol.Terms L m) : nat → fol.Term L.

Remark subAllnVars1 (a : nat) (ts ss : fol.Terms L a):
 ts = subAllTerms L _ (fst (nVars L a)) (termsMap a ts ss).

Remark subAllnVars2 (a : nat) (ts ss : fol.Terms L a):
 ss = subAllTerms L _ (snd (nVars L a)) (termsMap a ts ss).
    Opaque eq_nat_dec.
    Transparent eq_nat_dec.

Remark addPairwiseEquals (T : fol.System L) (n : nat) (ts ss : fol.Terms L n):
  PairwiseEqual T n ts ss →
  ∀ m0 : nat → fol.Term L,
    (∀ q : nat, q < n + n → m0 q = termsMap n ts ss q) →
    ∀ f0 : fol.Formula L,
      SysPrf T
        (subAllFormula L
           (nat_rec (fun _ : nat ⇒ fol.Formula L) f0
              (fun (n : nat) (Hrecn : fol.Formula L) ⇒
                 (v#(n + n) = v#(S (n + n)) → Hrecn)%fol
                 )
              n) m0) → SysPrf T (subAllFormula L f0 m0).

Lemma equalRelation (T : fol.System L) (r : Relations L) (ts ss : fol.Terms L _):
 PairwiseEqual T _ ts ss → SysPrf T (atomic r ts ↔ atomic r ss)%fol.

Lemma equalFunction (T : fol.System L) (f : Functions L) (ts ss : fol.Terms L _):
 PairwiseEqual T _ ts ss → SysPrf T (apply f ts = apply f ss)%fol.

Lemma subWithEqualsTerm (a b t : fol.Term L) (v : nat)
  (T : fol.System L):
 SysPrf T (a = b)%fol →
 SysPrf T (substT t v a = substT t v b)%fol.

Lemma subWithEqualsTerms (a b : fol.Term L) (n : nat) (ts : fol.Terms L n)
  (v : nat) (T : fol.System L):
  SysPrf T (a = b)%fol →
  PairwiseEqual T _ (substTs ts v a) (substTs ts v b).

Lemma subWithEquals :
  ∀ (f : fol.Formula L) (v : nat) (a b : fol.Term L) (T : fol.System L),
    SysPrf T (a = b)%fol →
    SysPrf T
      (substF f v a → substF f v b)%fol.

End Equality_Logic_Rules.