Library hydras.Ackermann.codeSubTerm

From hydras.Ackermann Require Import primRec cPair folProp code
                        extEqualNat.
From Coq Require Import Arith.
From Coq Require Vector.
From hydras Require Import Compat815.
Import LispAbbreviations.
Require Import NewNotations.
Import PRNotations.

Section Code_Substitute_Term.

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 codeSubTermTerms : nat → nat → nat → nat :=
  evalStrongRec 2
    (fun t recs v s : nat ⇒
       cPair
         (switchPR (car t)
            (cPair (car t) (cdr (codeNth (t - S (cdr t)) recs)))
            (switchPR (charFunction 2 Nat.eqb (cdr t) v) s t))
         (switchPR t
            (S
               (cPair (car (codeNth (t - S (car (pred t))) recs))
                  (cdr (codeNth (t - S (cdr (pred t))) recs)))) 0)).

Definition codeSubTerm (t s v : nat) : nat :=
  car (codeSubTermTerms t s v).

Definition codeSubTerms (t s v : nat) : nat :=
  cdr (codeSubTermTerms t s v).

Lemma codeSubTermCorrect :
  ∀ (t : Term) (v : nat) (s : Term),
    codeSubTerm (codeTerm t) v (codeTerm s) =
      codeTerm (substT t v s).

Lemma codeSubTermsCorrect :
  ∀ (n : nat) (ts : Terms n) (v : nat) (s : Term),
    codeSubTerms (codeTerms ts) v (codeTerm s) =
      codeTerms (substTs ts v s).

#[export] Instance codeSubTermTermsIsPR : isPR 3 codeSubTermTerms.

#[export] Instance codeSubTermIsPR : isPR 3 codeSubTerm.

Lemma codeSubTermsIsPR : isPR 3 codeSubTerms.

End Code_Substitute_Term.