From Coq Require Import Arith List.
From hydras.Ackermann Require Import fol primRec code.

Inductive LNTFunction : Set :=
  | Plus_ : LNTFunction
  | Times_ : LNTFunction
  | Succ_ : LNTFunction
  | Zero_ : LNTFunction.

Inductive LNTRelation : Set :=.

Definition LNTFunctionArity (x : LNTFunction) : nat :=
  match x with
  | Plus_ ⇒ 2
  | Times_ ⇒ 2
  | Succ_ ⇒ 1
  | Zero_ ⇒ 0
  end.


Definition LNTRelationR (x : LNTRelation) : nat :=
  match x with bot ⇒ LNTRelation_rec (fun _ ⇒ nat) bot end.

Definition LNT : Language := language LNTRelation LNTFunction LNTRelationR LNTFunctionArity.

Inductive LNNRelation : Set :=
    LT_ : LNNRelation.

Definition LNNArityR (x : LNNRelation) : nat :=
 match x with LT_ ⇒ 2 end.

Definition LNNArityF (f : LNTFunction) :=
     LNTFunctionArity f.

Definition LNN : Language := language LNNRelation LNTFunction
                               LNNArityR LNNArityF.

Definition codeLNTFunction (f : LNTFunction) : nat :=
  match f with
  | Plus_ ⇒ 0
  | Times_ ⇒ 1
  | Succ_ ⇒ 2
  | Zero_ ⇒ 3
  end.

Definition codeLNTRelation (R : LNTRelation) : nat :=
  match R return nat with
  end.

Lemma codeLNTFunctionInj :
 ∀ f g : LNTFunction, codeLNTFunction f = codeLNTFunction g → f = g.

Lemma codeLNTRelationInj :
 ∀ R S : LNTRelation, codeLNTRelation R = codeLNTRelation S → R = S.


Definition codeArityLNTR (r : nat) := 0.

#[export]Instance codeArityLNTRIsPR : isPR 1 codeArityLNTR.

Lemma codeArityLNTRIsCorrect1 :
 ∀ r : Relations LNT,
 codeArityLNTR (codeLNTRelation r) = S (arityR LNT r).

Lemma codeArityLNTRIsCorrect2 :
 ∀ n : nat,
 codeArityLNTR n ≠ 0 → ∃ r : Relations LNT, codeLNTRelation r = n.

Definition codeArityLNTF (f : nat) :=
  switchPR f
    (switchPR (pred f)
       (switchPR (pred (pred f)) (switchPR (pred (pred (pred f))) 0 1) 2) 3)
    3.

#[export]Instance codeArityLNTFIsPR : isPR 1 codeArityLNTF.

Lemma codeArityLNTFIsCorrect1 :
 ∀ f : Functions LNT,
 codeArityLNTF (codeLNTFunction f) = S (arityF LNT f).

Lemma codeArityLNNFIsCorrect1 :
 ∀ f : Functions LNN,
 codeArityLNTF (codeLNTFunction f) = S (arityF LNN f).

Lemma codeArityLNTFIsCorrect2 :
 ∀ n : nat,
 codeArityLNTF n ≠ 0 →
 ∃ f : Functions LNT, codeLNTFunction f = n.

Definition codeLNNRelation (R : LNNRelation) : nat := 0.

Lemma codeLNNRelationInj :
 ∀ R S : LNNRelation, codeLNNRelation R = codeLNNRelation S → R = S.

Definition codeArityLNNR (r : nat) := switchPR r 0 3.

#[export]Instance codeArityLNNRIsPR : isPR 1 codeArityLNNR.

Lemma codeArityLNNRIsCorrect1 :
  ∀ r : Relations LNN,
    codeArityLNNR (codeLNNRelation r) = S (arityR LNN r).

Lemma codeArityLNNRIsCorrect2 :
 ∀ n : nat,
 codeArityLNNR n ≠ 0 → ∃ r : Relations LNN, codeLNNRelation r = n.

Lemma codeArityLNNFIsCorrect2 :
  ∀ n : nat,
    codeArityLNTF n ≠ 0 → ∃ f : Functions LNN, codeLNTFunction f = n.