Library hydras.Ackermann.codeList

From hydras.Ackermann Require Import primRec cPair.
From Coq Require Export Lists.List.
From hydras.Ackermann Require Import ListExt.
From Coq Require Import Arith.
From Coq Require Vector.
From hydras Require Import extEqualNat Compat815.

Definition codeLength : nat → nat :=
  evalStrongRec 0
    (fun n Hrecs : nat ⇒
     switchPR n (S (codeNth (n - S (cPairPi2 (pred n))) Hrecs)) 0).

Lemma codeLengthCorrect :
 ∀ l : list nat, codeLength (codeList l) = length l.

#[export] Instance codeLengthIsPR : isPR 1 codeLength.

Definition codeApp : nat → nat → nat :=
  evalStrongRec 1
    (fun n Hrecs p1 : nat ⇒
       switchPR n
         (S
            (cPair (cPairPi1 (pred n))
               (codeNth (n - S (cPairPi2 (pred n))) Hrecs))) p1).

Lemma codeAppCorrect (l1 l2 : list nat):
 codeApp (codeList l1) (codeList l2) = codeList (l1 ++ l2).

#[export] Instance codeAppIsPR : isPR 2 codeApp.

Definition codeListRemove (a l : nat) : nat :=
  evalStrongRec 1
    (fun n Hrecs p1 : nat ⇒
     switchPR n
       (switchPR (charFunction 2 Nat.eqb (cPairPi1 (pred n)) p1)
          (codeNth (n - S (cPairPi2 (pred n))) Hrecs)
          (S
             (cPair (cPairPi1 (pred n))
                (codeNth (n - S (cPairPi2 (pred n))) Hrecs))))
       (codeList nil)) l a.

Lemma codeListRemoveCorrect (a : nat) (l : list nat):
 codeListRemove a (codeList l) =
   codeList (List.remove eq_nat_dec a l).

#[export] Instance codeListRemoveIsPR : isPR 2 codeListRemove.

Definition codeIn (a l : nat) : nat :=
  evalStrongRec 1
    (fun n Hrecs p1 : nat ⇒
     switchPR n
       (switchPR (charFunction 2 Nat.eqb (cPairPi1 (pred n)) p1) 1
          (codeNth (n - S (cPairPi2 (pred n))) Hrecs)) 0) l a.

Lemma codeInCorrect (a : nat) (l : list nat) :
 codeIn a (codeList l) =
 match In_dec eq_nat_dec a l with
 | left _ ⇒ 1
 | right _ ⇒ 0
 end.

#[export] Instance codeInIsPR : isPR 2 codeIn.

Definition codeNoDup : nat → nat :=
  evalStrongRec 0
    (fun l recs : nat ⇒
       switchPR l
         (switchPR
            (codeIn (cPairPi1 (pred l))
               (codeNth (l - S (cPairPi2 (pred l))) recs))
            (codeNth (l - S (cPairPi2 (pred l))) recs)
            (S
               (cPair (cPairPi1 (pred l))
                  (codeNth (l - S (cPairPi2 (pred l))) recs)))) 0).

Lemma codeNoDupCorrect (l : list nat) :
 codeNoDup (codeList l) = codeList (List.nodup eq_nat_dec l).

#[export] Instance codeNoDupIsPR : isPR 1 codeNoDup.