Library hydras.Ackermann.codePA

From Coq Require Import Ensembles List Arith Lia.
From Coq Require Vector.
Import Bool.

From hydras
  Require Import primRec cPair folProp code codeList codeFreeVar
  extEqualNat prLogic codeNatToTerm Compat815.

Import LispAbbreviations.

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


Let Formula := Formula L .
Let codeFormula := codeFormula (cl:=cL).

Definition codeCloseList : nat → nat → nat :=
  evalStrongRec 1
    (fun l recs f : nat ⇒
     switchPR l
       (cPair 3
          (cPair (car (pred l))
             (codeNth (l - S (cdr (pred l))) recs))) f).

Lemma codeCloseListCorrect (l : list nat) (f : Formula):
 codeCloseList (codeList l) (codeFormula f) =
   codeFormula (closeList L l f).

#[export] Instance codeCloseListIsPR : isPR 2 codeCloseList.

Definition codeClose (f : nat) : nat :=
  codeCloseList (codeNoDup (codeFreeVarFormula f)) f.

Lemma codeCloseCorrect (f : Formula) :
  codeClose (codeFormula f) = codeFormula (close L f).

#[export] Instance codeCloseIsPR : isPR 1 codeClose.

End close.

From hydras.Ackermann Require Import PA codeSubFormula.

Section Code_PA.

Let codeTerm := codeTerm (cl :=LcodeLNT).
Let codeFormula := codeFormula (cl:=LcodeLNT).
Let codeFormulaInj := codeFormulaInj LNT LcodeLNT.

Definition codeOpen : nat → nat :=
  evalStrongRec 0
    (fun f recs : nat ⇒
     switchPR (car f)
       (switchPR (pred (car f))
          (switchPR (pred (pred (car f)))
             (switchPR (pred (pred (pred (car f)))) f
                (codeNth (f - S (cdr (cdr f))) recs)) f) f) f).

Lemma codeOpenCorrect (f : Formula):
  codeOpen (codeFormula f) = codeFormula (open f).

#[export] Instance codeOpenIsPR : isPR 1 codeOpen.

Definition codeInductionSchema (f : nat) : bool :=
  let n :=
    car (cdr (cddddr (codeOpen f))) in
  let g := cdr (cdr (cddddr (codeOpen f))) in
  Nat.eqb
    (codeClose
       (codeImp (codeSubFormula g n (codeTerm Zero))
          (codeImp
             (codeForall n
                (codeImp g (codeSubFormula g n
                              (codeTerm (Succ (var n))))))
             (codeForall n g)))) f.

Lemma codeInductionSchemaCorrect1 (f : Formula) :
 InductionSchema f → codeInductionSchema (codeFormula f) = true.

Lemma codeInductionSchemaCorrect2 (f : Formula):
 codeInductionSchema (codeFormula f) = true → InductionSchema f.
        Opaque cPairPi1.
        Opaque cPairPi2.

Lemma codeInductionSchemaCorrect3 (f : Formula):
 ¬ InductionSchema f → codeInductionSchema (codeFormula f) = false.

#[local] Instance codeInductionSchemaIsPR : isPRrel 1 codeInductionSchema.

Definition codePA : nat → bool :=
  orRel 1 (Nat.eqb (codeFormula PA6))
    (orRel 1 (Nat.eqb (codeFormula PA5))
       (orRel 1 (Nat.eqb (codeFormula PA4))
          (orRel 1 (Nat.eqb (codeFormula PA3))
             (orRel 1 (Nat.eqb (codeFormula PA2))
                (orRel 1 (Nat.eqb (codeFormula PA1))
                   codeInductionSchema))))).

Lemma codePAcorrect1 (f : Formula):
 codePA (codeFormula f) = true → mem Formula PA f.

Lemma codePAcorrect2 (f : Formula):
 ¬ mem Formula PA f → codePA (codeFormula f) = false.

Lemma codePAcorrect3 (f : Formula):
  mem Formula PA f → codePA (codeFormula f) = true.

#[export] Instance codePAIsPR : isPRrel 1 codePA.

End Code_PA.