Library hydras.Ackermann.codeFreeVar

From hydras.Ackermann Require Import primRec cPair.
From Coq Require Import List Arith.
From hydras.Ackermann Require Import ListExt.
From hydras.Ackermann Require Export codeList.
From hydras Require Import folProp code Compat815.
Import LispAbbreviations.
Import PRNotations.

Section Code_Free_Vars.

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

Let Formula := Formula L.
Let Formulas := Formulas L.
Let System := System L.
Let Term := Term L.
Let Terms := Terms L.

Definition codeFreeVarTermTerms : nat → nat :=
  evalStrongRec 0
    (fun t recs : nat ⇒
     cPair
       (switchPR (car t) (cdr (codeNth (t - S (cdr t)) recs))
          (S (cPair (cdr t) 0)))
       (switchPR t
          (codeApp (car (codeNth (t - S (car (pred t))) recs))
             (cdr (codeNth (t - S (cdr (pred t))) recs))) 0)).

Definition codeFreeVarTerm (t : nat) : nat :=
  car (codeFreeVarTermTerms t).

Definition codeFreeVarTerms (t : nat) : nat :=
  cdr (codeFreeVarTermTerms t).

Lemma codeFreeVarTermCorrect (t: Term) :
 codeFreeVarTerm (codeTerm t) = codeList (freeVarT t).

Lemma codeFreeVarTermsCorrect (n : nat) (ts : Terms n):
 codeFreeVarTerms (codeTerms ts) = codeList (freeVarTs ts).

#[export]
  Instance codeFreeVarTermTermsIsPR : isPR 1 codeFreeVarTermTerms.

Lemma codeFreeVarTermIsPR : isPR 1 codeFreeVarTerm.

#[export]
  Instance codeFreeVarTermsIsPR : isPR 1 codeFreeVarTerms.

Definition codeFreeVarFormula : 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))))
                (codeFreeVarTerms (cdr f))
                (codeListRemove (cadr f)
                   (codeNth (f - S (cddr f)) recs)))
             (codeNth (f - S (cdr f)) recs))
          (codeApp (codeNth (f - S (cadr f)) recs)
             (codeNth (f - S (cddr f)) recs)))
       (codeApp (codeFreeVarTerm (cadr f))
          (codeFreeVarTerm (cddr f)))).

Lemma codeFreeVarFormulaCorrect (f : Formula) :
  codeFreeVarFormula (codeFormula f) =
    codeList (freeVarF f).

#[export]
  Instance codeFreeVarFormulaIsPR : isPR 1 codeFreeVarFormula.

Definition codeFreeVarListFormula : nat → nat :=
  evalStrongRec 0
    (fun l recs : nat ⇒
     switchPR l
       (codeApp (codeFreeVarFormula (car (pred l)))
          (codeNth (l - S (cdr (pred l))) recs)) 0).

Lemma codeFreeVarListFormulaCorrect (l : list Formula):
 codeFreeVarListFormula (codeList (map (codeFormula) l)) =
 codeList (freeVarListFormula L l).

#[export]
  Instance codeFreeVarListFormulaIsPR : isPR 1 codeFreeVarListFormula.

End Code_Free_Vars.