Library hydras.Ackermann.wellFormed

From hydras.Ackermann Require Import primRec cPair.
From Coq Require Import Arith Lia.
From hydras.Ackermann Require Import code folProp
  extEqualNat codeList.
From hydras Require Import Compat815.
Import LispAbbreviations.

Section Well_Formed_Term.

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

Variable codeArityF : 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.

Let Term := Term L.
Let Terms := Terms L.

Definition wellFormedTermTerms : nat → nat :=
  evalStrongRec 0
    (fun t recs : nat ⇒
     cPair
       (switchPR (cPairPi1 t)
          (charFunction 2 Nat.eqb (codeArityF (pred (cPairPi1 t)))
             (S (codeLength (cPairPi2 t))) ×
           cPairPi2 (codeNth (t - S (cPairPi2 t)) recs)) 1)
       (switchPR t
          (cPairPi1 (codeNth (t - S (cPairPi1 (pred t))) recs) ×
           cPairPi2 (codeNth (t - S (cPairPi2 (pred t))) recs)) 1)).

Definition wellFormedTerm (t : nat) : nat := cPairPi1 (wellFormedTermTerms t).

Definition wellFormedTerms (ts : nat) : nat :=
  cPairPi2 (wellFormedTermTerms ts).

Lemma lengthTerms :
 ∀ (n : nat) (ts : Terms n), codeLength (codeTerms ts) = n.

Lemma wellFormedTermCorrect1 :
  ∀ t : Term, wellFormedTerm (codeTerm t) = 1.

Lemma wellFormedTermsCorrect1 (n : nat) (ts : Terms n):
  wellFormedTerms (codeTerms ts) = 1.

Lemma multLemma1 : ∀ a b : nat, a × b ≠ 0 → a ≠ 0.

Lemma multLemma2 : ∀ a b : nat, a × b ≠ 0 → b ≠ 0.

Remark wellFormedTermTermsCorrect2 :
 ∀ n : nat,
 (wellFormedTerm n ≠ 0 → ∃ t : Term, codeTerm t = n) ∧
 (wellFormedTerms n ≠ 0 →
  ∃ m : nat, (∃ ts : Terms m, codeTerms ts = n)).

Lemma wellFormedTermCorrect2 :
  ∀ n : nat,
    wellFormedTerm n ≠ 0 → ∃ t : Term, codeTerm t = n.

Lemma wellFormedTermsCorrect2 :
  ∀ n : nat,
    wellFormedTerms n ≠ 0 →
    ∃ m : nat, (∃ ts : Terms m, codeTerms ts = n).

#[local] Instance wellFormedTermTermsIsPR :
  isPR 1 wellFormedTermTerms.

#[export] Instance wellFormedTermIsPR : isPR 1 wellFormedTerm.

#[export] Instance wellFormedTermsIsPR : isPR 1 wellFormedTerms.

Section Well_Formed_Formula.

Variable codeArityR : nat → nat.
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.

Let Formula := Formula L.

Definition wellFormedFormula : nat → nat :=
  evalStrongRec 0
    (fun f recs : nat ⇒
     switchPR (cPairPi1 f)
       (switchPR (pred (cPairPi1 f))
          (switchPR (pred (pred (cPairPi1 f)))
             (switchPR (pred (pred (pred (cPairPi1 f))))
                (charFunction 2 Nat.eqb
                   (codeArityR (pred (pred (pred (pred (cPairPi1 f))))))
                   (S (codeLength (cPairPi2 f))) ×
                 wellFormedTerms (cPairPi2 f))
                (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs))
             (codeNth (f - S (cPairPi2 f)) recs))
          (codeNth (f - S (cPairPi1 (cPairPi2 f))) recs ×
           codeNth (f - S (cPairPi2 (cPairPi2 f))) recs))
       (wellFormedTerm (cPairPi1 (cPairPi2 f)) ×
        wellFormedTerm (cPairPi2 (cPairPi2 f)))).

Lemma wellFormedFormulaCorrect1 :
 ∀ f : Formula, wellFormedFormula (codeFormula f) = 1.

Lemma wellFormedFormulaCorrect2 :
  ∀ n : nat,
    wellFormedFormula n ≠ 0 →
    ∃ f : Formula, codeFormula f = n.

#[export] Instance wellFormedFormulaIsPR : isPR 1 wellFormedFormula.

End Well_Formed_Formula.

End Well_Formed_Term.