Library hydras.Ackermann.expressible

From Coq Require Import Arith List.
From hydras.Ackermann
  Require Import ListExt folProp subProp extEqualNat Languages LNN
  NewNotations.
Import NNnotations.

#[local] Arguments apply _ _ _ : clear implicits.

Section RepresentableExpressible.

Variable T : System.

Hypothesis closedT1: (ClosedSystem LNN T).

Remark closedT : ∀ v : nat, ¬ In_freeVarSys LNN v T.

Fixpoint RepresentableHalf1 (n : nat) :
  naryFunc n → Formula → Prop :=
  match n return (naryFunc n → Formula → Prop) with
  | O ⇒
      fun (f : naryFunc 0) (A : Formula) ⇒
      SysPrf T (A → v#0 = natToTerm f)%fol
  | S m ⇒
      fun (f : naryFunc (S m)) (A : Formula) ⇒
      ∀ a : nat,
      RepresentableHalf1 m (f a)
        (substF A (S m) (natToTerm a))
  end.

Fixpoint RepresentableHalf2 (n : nat) : naryFunc n → Formula → Prop :=
  match n return (naryFunc n → Formula → Prop) with
  | O ⇒
      fun (f : naryFunc 0) (A : Formula) ⇒
      SysPrf T (v#0 = natToTerm f → A)%fol
  | S m ⇒
      fun (f : naryFunc (S m)) (A : Formula) ⇒
      ∀ a : nat,
      RepresentableHalf2 m (f a)
        (substF A (S m) (natToTerm a))
  end.

Lemma RepresentableHalf1Alternate :
 ∀ (n : nat) (f : naryFunc n) (A B : Formula),
 SysPrf T (impH A B) → RepresentableHalf1 n f B →
 RepresentableHalf1 n f A.

Lemma RepresentableHalf2Alternate :
 ∀ (n : nat) (f : naryFunc n) (A B : Formula),
   SysPrf T (A → B)%fol → RepresentableHalf2 n f A →
   RepresentableHalf2 n f B.

Fixpoint RepresentableHelp (n : nat) : naryFunc n → Formula → Prop :=
  match n return (naryFunc n → Formula → Prop) with
  | O ⇒
      fun (f : naryFunc 0) (A : Formula) ⇒
      SysPrf T (A ↔ v#0 = natToTerm f)%fol
  | S m ⇒
      fun (f : naryFunc (S m)) (A : Formula) ⇒
      ∀ a : nat,
      RepresentableHelp m (f a)
        (substF A (S m) (natToTerm a))
  end.

Lemma RepresentableHalfHelp :
 ∀ (n : nat) (f : naryFunc n) (A : Formula),
 RepresentableHalf1 n f A →
 RepresentableHalf2 n f A → RepresentableHelp n f A.

Definition Representable (n : nat) (f : naryFunc n)
  (A : Formula) : Prop :=
  (∀ v : nat, In v (freeVarF A) → v ≤ n) ∧
  RepresentableHelp n f A.

Lemma RepresentableAlternate :
 ∀ (n : nat) (f : naryFunc n) (A B : Formula),
 SysPrf T (iffH A B) → RepresentableHelp n f A →
 RepresentableHelp n f B.

Lemma Representable_ext :
 ∀ (n : nat) (f g : naryFunc n) (A : Formula),
   extEqual n f g → RepresentableHelp n f A →
   RepresentableHelp n g A.

Fixpoint ExpressibleHelp (n : nat) : naryRel n → Formula → Prop :=
  match n return (naryRel n → Formula → Prop) with
  | O ⇒
      fun (R : naryRel 0) (A : Formula) ⇒
      match R with
      | true ⇒ SysPrf T A
      | false ⇒ SysPrf T ( ¬ A)%fol
      end
  | S m ⇒
      fun (R : naryRel (S m)) (A : Formula) ⇒
      ∀ a : nat,
      ExpressibleHelp m (R a)
        (substF A (S m) (natToTerm a))
  end.

Definition Expressible (n : nat) (R : naryRel n) (A : Formula) : Prop :=
  (∀ v : nat, In v (freeVarF A) →
                   v ≤ n ∧ v ≠ 0) ∧
  ExpressibleHelp n R A.

Lemma expressibleAlternate :
  ∀ (n : nat) (R : naryRel n) (A B : Formula),
    SysPrf T (iffH A B) → ExpressibleHelp n R A →
    ExpressibleHelp n R B.

Hypothesis nn1: SysPrf T (natToTerm 1 ≠ natToTerm 0)%fol.

Lemma Representable2Expressible :
 ∀ (n : nat) (R : naryRel n) (A : Formula),
 Representable n (charFunction n R) A →
 Expressible n R (substF A 0 (natToTerm 1)).

End RepresentableExpressible.