Library Goedel.codeSysPrf

TO DO: Define abbreviations and re-indent !!!

From Coq Require Import Ensembles.
From Coq Require Import List.
From hydras.Ackermann Require Import checkPrf.
From hydras.Ackermann Require Import code.
From hydras.Ackermann Require Import Languages.
From hydras.Ackermann Require Import folProp.
From hydras.Ackermann Require Import folProof.
From hydras.Ackermann Require Import folLogic3.
From hydras.Ackermann Require Import folReplace.
From Goedel Require Import PRrepresentable.
From hydras.Ackermann Require Import expressible.
From hydras.Ackermann Require Import primRec.
From Coq Require Import Arith Lia.
From hydras.Ackermann Require Import PA.
From hydras.Ackermann Require Import NNtheory.
From hydras.Ackermann Require Import codeList.
From hydras.Ackermann Require Import subProp.
From hydras.Ackermann Require Import ListExt.
From hydras.Ackermann Require Import cPair.
From hydras.Ackermann Require Import wellFormed.
From hydras.Ackermann Require Import prLogic.

From hydras Require Import Compat815.
Import NNnotations.

Section code_SysPrf.

Generalizable All Variables.
Variable L : Language.
Context `(cL: Lcode L cf cr).

Variable codeArityF : nat → nat.
Variable codeArityR : nat → nat.
Context (codeArityFIsPR : isPR 1 codeArityF).
Hypothesis
  codeArityFIsCorrect1 :
    ∀ f : Functions L, codeArityF (cf f) = S (arityF L f).
Hypothesis
  codeArityFIsCorrect2 :
    ∀ n : nat, codeArityF n ≠ 0 → ∃ f : Functions L , cf f = n.
Context (codeArityRIsPR : isPR 1 codeArityR).
Hypothesis
  codeArityRIsCorrect1 :
    ∀ r : Relations L, codeArityR (cr r) = S (arityR L r).
Hypothesis
  codeArityRIsCorrect2 :
    ∀ n : nat, codeArityR n ≠ 0 → ∃ r : Relations L , cr r = n.

Import LNN NN.
Import NNnotations.

Section LNN.

Variable T : System.
Hypothesis TextendsNN : Included _ NN T.

Variable U : fol.System L.
Variable fU : Formula.
Variable v0 : nat.
Hypothesis freeVarfU : ∀ v : nat, In v (freeVarF fU) → v = v0.
Hypothesis
  expressU1 :
    ∀ f : fol.Formula L,
    mem _ U f →
    SysPrf T
      (substF fU v0 (natToTerm (codeFormula f))).
Hypothesis
  expressU2 :
    ∀ f : fol.Formula L,
    ¬ mem _ U f →
    SysPrf T
      (notH (substF fU v0 (natToTerm (codeFormula f)))).

Definition codeSysPrf : Formula :=
  let nv := newVar (2 :: 1 :: 0 :: v0 :: nil) in
  existH nv
    (andH
       (substF
          (substF
             (primRecFormula 2
                (proj1_sig
                   (checkPrfIsPR L cL codeArityF codeArityR
                      codeArityFIsPR codeArityRIsPR))) 0
             (Succ (var nv))) 2 (var 0))
       (forallH (S nv)
          (impH (LT (var (S nv)) (var nv))
             (orH
                (substF
                   (substF
                      (substF
                         (primRecFormula 2 (proj1_sig codeInIsPR)) 2
                         (var (S nv))) 1 (var nv)) 0 Zero)
                (substF fU v0 (var (S nv))))))).

Lemma codeSysPrfCorrect1 :
∀ (f : fol.Formula L) (A : list (fol.Formula L)) (p : Prf L A f),
(∀ g : fol.Formula L, In g A → mem _ U g ) →
SysPrf T
   (substF
      (substF codeSysPrf 0
         (natToTerm (codeFormula f))) 1
      (natToTerm (codePrf A f p))).

Lemma codeSysPrfCorrect2 :
  ∀ (f : fol.Formula L) (A : fol.Formulas L),
    (∃ g : fol.Formula L , In g A ∧ ¬ mem _ U g ) →
    ∀ p : Prf L A f,
      SysPrf T
        (notH
           (substF
              (substF codeSysPrf 0
                 (natToTerm (codeFormula f))) 1
              (natToTerm (codePrf A f p)))).

Lemma codeSysPrfCorrect3 :
  ∀ (f : fol.Formula L) (n : nat),
    (∀ (A : list (fol.Formula L)) (p : Prf L A f),
        n ≠ codePrf A f p ) →
    SysPrf T
      (notH
         (substF
            (substF codeSysPrf 0
               (natToTerm (codeFormula f))) 1
            (natToTerm n))).

Lemma freeVarCodeSysPrf :
∀ v : nat, In v (freeVarF codeSysPrf) → v ≤ 1.

Definition codeSysPf : Formula := existH 1 codeSysPrf.

Lemma freeVarCodeSysPf :
∀ v : nat, In v (freeVarF codeSysPf) → v = 0.

Lemma codeSysPfCorrect :
∀ f : fol.Formula L,
folProof.SysPrf L U f →
SysPrf T
   (substF codeSysPf 0
      (natToTerm (codeFormula f))).

Definition codeSysPrfNot :=
  existH 2
    (andH (substF codeSysPrf 0 (var 2))
       (substF
          (substF (primRecFormula 1 (proj1_sig codeNotIsPR)) 0
             (var 2)) 1 (var 0))).

Lemma freeVarCodeSysPrfN :
∀ v : nat, In v (freeVarF codeSysPrfNot) → v ≤ 1.

Lemma codeSysPrfNCorrect1 :
  ∀ (f : fol.Formula L) (A : fol.Formulas L) (p : Prf L A (notH f)),
    (∀ g : fol.Formula L, In g A → mem _ U g ) →
    SysPrf T
      (substF
         (substF codeSysPrfNot 0
            (natToTerm (codeFormula f))) 1
         (natToTerm (codePrf A (notH f) p))).

Lemma codeSysPrfNCorrect2 :
  ∀ (f : fol.Formula L) (A : fol.Formulas L),
    (∃ g : fol.Formula L , In g A ∧ ¬ mem _ U g ) →
    ∀ p : Prf L A (notH f),
      SysPrf T
        (notH
           (substF
              (substF codeSysPrfNot 0
                 (natToTerm (codeFormula f))) 1
              (natToTerm (codePrf A (notH f) p)))).

Lemma codeSysPrfNCorrect3 :
∀ (f : fol.Formula L) (n : nat),
(∀ (A : fol.Formulas L) (p : Prf L A (notH f)),
  n ≠ codePrf A (notH f) p ) →
SysPrf T
   (notH
      (substF
         (substF codeSysPrfNot 0
            (natToTerm (codeFormula f))) 1
         (natToTerm n))).

End LNN.

End code_SysPrf.