From Coq Require Import Arith.
From hydras.Ackermann Require Import fol folProof cPair.

Section Code_Term_Formula_Proof.

Variable L : Language.
 Section LcodeDef.
   Variable cF : Functions L → nat.
   Variable cR : Relations L → nat.
   Class Lcode : Prop :=
     { codeFInj :
       ∀ f g : Functions L, cF f = cF g → f = g;
       codeRInj :
       ∀ R S : Relations L, cR R = cR S → R = S
     }.
  End LcodeDef.

 Definition codeF {cf : Functions L → nat} {cr : Relations L → nat} (c: Lcode cf cr) := cf.

 Definition codeR {cf : Functions L → nat} {cr : Relations L → nat} (c: Lcode cf cr) := cr.

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

Generalizable All Variables.
Section codeTermFormDef.

  Context `(cl : Lcode cf cr).
Fixpoint codeTerm (t : Term) : nat :=
  match t with
  | var n ⇒ cPair 0 n
  | apply f ts ⇒ cPair (S (codeF cl f)) (codeTerms _ ts)
  end
 
 with codeTerms (n : nat) (ts : Terms n) {struct ts} : nat :=
  match ts with
  | Tnil ⇒ 0
  | Tcons n t ss ⇒ S (cPair (codeTerm t) (codeTerms n ss))
  end.

Lemma codeTermInj :
  ∀ t s : Term, codeTerm t = codeTerm s → t = s.

Lemma codeTermsInj :
 ∀ (n : nat) (ts ss : Terms n),
 codeTerms n ts = codeTerms n ss → ts = ss.

Fixpoint codeFormula (f : Formula) : nat :=
  match f with
  | equal t1 t2 ⇒ cPair 0 (cPair (codeTerm t1) (codeTerm t2))
  | impH f1 f2 ⇒ cPair 1 (cPair (codeFormula f1) (codeFormula f2))
  | notH f1 ⇒ cPair 2 (codeFormula f1)
  | forallH n f1 ⇒ cPair 3 (cPair n (codeFormula f1))
  | atomic R ts ⇒ cPair (4 + codeR cl R) (codeTerms _ ts)
  end.

Lemma codeFormulaInj :
  ∀ f g : Formula, codeFormula f = codeFormula g → f = g.

Fixpoint codePrf (Z : Formulas) (f : Formula) (prf : Prf Z f) {struct prf} :
 nat :=
  match prf with
  | AXM A ⇒ cPair 0 (codeFormula A)
  | MP Axm1 Axm2 A B rec1 rec2 ⇒
      cPair 1
        (cPair
           (cPair (cPair 1 (cPair (codeFormula A) (codeFormula B)))
              (codePrf _ _ rec1)) (cPair (codeFormula A) (codePrf _ _ rec2)))
  | GEN Axm A v _ rec ⇒
      cPair 2 (cPair v (cPair (codeFormula A) (codePrf _ _ rec)))
  | IMP1 A B ⇒ cPair 3 (cPair (codeFormula A) (codeFormula B))
  | IMP2 A B C ⇒
      cPair 4 (cPair (codeFormula A) (cPair (codeFormula B) (codeFormula C)))
  | CP A B ⇒ cPair 5 (cPair (codeFormula A) (codeFormula B))
  | FA1 A v t ⇒ cPair 6 (cPair (codeFormula A) (cPair v (codeTerm t)))
  | FA2 A v _ ⇒ cPair 7 (cPair (codeFormula A) v)
  | FA3 A B v ⇒ cPair 8 (cPair (codeFormula A) (cPair (codeFormula B) v))
  | EQ1 ⇒ cPair 9 0
  | EQ2 ⇒ cPair 10 0
  | EQ3 ⇒ cPair 11 0
  | EQ4 r ⇒ cPair 12 (codeR cl r)
  | EQ5 f ⇒ cPair 13 (codeF cl f)
  end.

Lemma codePrfInjAxm :
 ∀ (a b : Formula) (A B : Formulas) (p : Prf A a) (q : Prf B b),
 codePrf A a p = codePrf B b q → A = B.

Definition codeImp (a b : nat) := cPair 1 (cPair a b).

Lemma codeImpCorrect :
 ∀ a b : Formula,
 codeImp (codeFormula a) (codeFormula b) = codeFormula (impH a b).

Definition codeNot (a : nat) := cPair 2 a.

Lemma codeNotCorrect :
 ∀ a : Formula, codeNot (codeFormula a) = codeFormula (notH a).

Definition codeForall (n a : nat) := cPair 3 (cPair n a).

Lemma codeForallCorrect :
 ∀ (n : nat) (a : Formula),
 codeForall n (codeFormula a) = codeFormula (forallH n a).

Definition codeOr (a b : nat) := codeImp (codeNot a) b.

Lemma codeOrCorrect :
 ∀ a b : Formula,
 codeOr (codeFormula a) (codeFormula b) = codeFormula (orH a b).

Definition codeAnd (a b : nat) := codeNot (codeOr (codeNot a) (codeNot b)).

Lemma codeAndCorrect :
 ∀ a b : Formula,
 codeAnd (codeFormula a) (codeFormula b) = codeFormula (andH a b).

Definition codeIff (a b : nat) := codeAnd (codeImp a b) (codeImp b a).

Lemma codeIffCorrect :
 ∀ a b : Formula,
 codeIff (codeFormula a) (codeFormula b) = codeFormula (iffH a b).

End codeTermFormDef.

End Code_Term_Formula_Proof.

Arguments codeTerm {L} {cf cr cl} _.
Arguments codeTerms {L} {cf cr cl n} _.
Arguments codeFormula {L} {cf cr cl} _.
Arguments codePrf {L} {cf cr cl} _ _ _.