From Coq Require Import Arith Ensembles List.

From hydras.Ackermann Require Export Languages folProof
  folProp folLogic3.
From LibHyps Require Import LibHyps.
From hydras Require Import MoreLibHyps NewNotations.

Definition Formula := Formula LNN.
Definition Formulas := Formulas LNN.
Definition System := System LNN.
Definition Sentence := Sentence LNN.
Definition Term := Term LNN.
Definition Terms := Terms LNN.
Definition SysPrf := SysPrf LNN.

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

 Module NNnotations.
 Export FolNotations.

Definition Plus (x y : Term) : Term :=
  apply LNN Plus_ (Tcons x (Tcons y (Tnil))).

Definition Times (x y : Term) : Term :=
  apply LNN Times_ (Tcons x (Tcons y (Tnil))).

Definition Succ (x : Term) : Term :=
  apply LNN Succ_ (Tcons x (Tnil)).

Definition Zero : Term := apply LNN Zero_ (Tnil).

Definition LT (x y : Term) : Formula :=
  atomic LNN LT_ (Tcons x (Tcons y (Tnil))).


Notation S_ t := (apply LNN Succ_ (Tcons t (Tnil))).

Infix "+" := Plus: fol_scope.
Notation "n + p" := (Plus n p) (in custom fol at level 50, left associativity).

Check f[ ∀ 1, {var 1} + {var 1} = {var 1} ]f.
Infix "×" := Times: fol_scope.
Notation "n * p" := (Times n p) (in custom fol at level 40, left associativity).

Infix "<" := LT: fol_scope.
End NNnotations.

Import NNnotations.

Lemma LNN_eqdec : language_decidable LNN.

Section Free_Variables.

Lemma freeVarPlus (x y : Term) :
 freeVarT (Plus x y) = freeVarT x ++ freeVarT y.

Lemma freeVarTimes (x y : Term):
 freeVarT (Times x y) = freeVarT x ++ freeVarT y.

Lemma freeVarSucc (x : Term):
  freeVarT (Succ x) = freeVarT x.

Lemma freeVarZero : freeVarT Zero = nil.

Lemma freeVarLT (x y : Term) :
 freeVarF (LT x y) = freeVarT x ++ freeVarT y.

End Free_Variables.

Section Logic.

Lemma Axm (T : System) (f : Formula): mem _ T f → SysPrf T f.

Lemma sysExtend (T U : System) (f : Formula):
 Included _ T U → SysPrf T f → SysPrf U f.

Lemma sysWeaken (T : System) (f g : Formula):
  SysPrf T f → SysPrf (Ensembles.Add _ T g) f.

Lemma impI (T : System) (f g : Formula):
 SysPrf (Ensembles.Add _ T g) f → SysPrf T (g → f)%fol.

Lemma impE (T : System) (f g : Formula):
  SysPrf T (g → f)%fol → SysPrf T g → SysPrf T f.

Lemma contradiction (T : System) (f g : Formula):
  SysPrf T f → SysPrf T (¬ f)%fol → SysPrf T g.

Lemma nnE (T : System) (f : Formula):
  SysPrf T (~~ f)%fol → SysPrf T f.

Lemma noMiddle (T : System) (f : Formula): SysPrf T (¬ f ∨ f)%fol.

Lemma nnI (T : System) (f : Formula):
  SysPrf T f → SysPrf T (¬ ¬ f)%fol.

Lemma cp1 (T : System) (f g : Formula) :
 SysPrf T (¬ f → ¬ g)%fol → SysPrf T (impH g f).

Lemma cp2 (T : System) (f g : Formula):
 SysPrf T (g → f)%fol → SysPrf T (¬ f → ¬ g)%fol.

Lemma orI1 (T : System) (f g : Formula):
  SysPrf T f → SysPrf T (f ∨ g)%fol.

Lemma orI2 (T : System) (f g : Formula):
  SysPrf T g → SysPrf T (f ∨ g)%fol.

Lemma orE (T : System) (f g h : Formula):
  SysPrf T (f ∨ g)%fol →
  SysPrf T (f → h)%fol → SysPrf T (g → h)%fol → SysPrf T h.

Lemma orSys (T : System) (f g h : Formula) :
 SysPrf (Ensembles.Add _ T f) h → SysPrf (Ensembles.Add _ T g) h →
 SysPrf (Ensembles.Add _ T (f ∨ g)%fol) h.

Lemma andI (T : System) (f g : Formula):
 SysPrf T f → SysPrf T g → SysPrf T (f ∧ g)%fol.

Lemma andE1 (T : System) (f g : Formula):
  SysPrf T (f ∧ g)%fol → SysPrf T f.

Lemma andE2 (T : System) (f g : Formula):
  SysPrf T (f ∧ g)%fol → SysPrf T g.

Lemma iffI (T : System) (f g : Formula):
 SysPrf T (f → g)%fol → SysPrf T (g → f)%fol →
 SysPrf T (f ↔ g)%fol.

Lemma iffE1 (T : System) (f g : Formula):
 SysPrf T (f ↔ g)%fol → SysPrf T (f → g)%fol.

Lemma iffE2 (T : System) (f g : Formula):
 SysPrf T (f ↔ g)%fol → SysPrf T (g → f)%fol.

Lemma forallI (T : System) (f : Formula) (v : nat):
 ¬ In_freeVarSys LNN v T → SysPrf T f → SysPrf T (allH v, f)%fol.

Lemma forallE (T : System) (f : Formula) (v : nat) (t : Term):
 SysPrf T (allH v, f)%fol → SysPrf T (substF f v t).

Lemma forallSimp (T : System) (f : Formula) (v : nat) :
 SysPrf T (allH v, f)%fol → SysPrf T f.

Lemma existI (T : System) (f : Formula) (v : nat) (t : Term):
 SysPrf T (substF f v t) → SysPrf T (exH v, f)%fol.

Lemma existE (T : System) (f g : Formula) (v : nat):
  ¬ In_freeVarSys LNN v T →
  ¬ In v (freeVarF g) →
  SysPrf T (exH v, f)%fol → SysPrf T (f → g)%fol →
  SysPrf T g.

Lemma existSimp (T : System) (f : Formula) (v : nat):
  SysPrf T f → SysPrf T (exH v, f)%fol.

Lemma existSys (T : System) (f g : Formula) (v : nat):
  ¬ In_freeVarSys LNN v T →
  ¬ In v (freeVarF g) →
  SysPrf (SetAdds T f) g →
  SysPrf (SetAdds T (exH v, f)%fol) g.

Lemma absurd1 (T : System) (f : Formula):
 SysPrf T (f → ¬ f)%fol → SysPrf T (¬ f)%fol.

Lemma nImp (T : System) (f g : Formula):
 SysPrf T (f ∧ ¬ g)%fol → SysPrf T (¬ (f → g))%fol.

Lemma nOr (T : System) (f g : Formula):
 SysPrf T (¬ f ∧ ¬ g)%fol → SysPrf T (¬ (f ∨ g))%fol.

Lemma nAnd (T : System) (f g : Formula):
 SysPrf T (¬ f ∨ ¬ g)%fol → SysPrf T (¬ (f ∧ g))%fol.

Lemma nForall (T : System) (f : Formula) (v : nat):
 SysPrf T (exH v, ¬ f)%fol → SysPrf T (¬ (allH v, f))%fol.

Lemma nExist (T : System) (f : Formula) (v : nat):
 SysPrf T (allH v, ¬ f)%fol → SysPrf T (¬ (exH v, f))%fol.

Lemma impRefl (T : System) (f : Formula): SysPrf T (f → f)%fol.

Lemma impTrans (T : System) (f g h : Formula):
 SysPrf T (f → g)%fol → SysPrf T (g → h)%fol → SysPrf T (f → h)%fol.

Lemma orSym (T : System) (f g : Formula):
  SysPrf T (f ∨ g)%fol → SysPrf T (g ∨ f)%fol.

Lemma andSym (T : System) (f g : Formula):
SysPrf T (f ∧ g)%fol → SysPrf T (g ∧ f)%fol.

Lemma iffRefl (T : System) (f : Formula): SysPrf T (f ↔ f)%fol.

Lemma iffSym (T : System) (f g : Formula):
  SysPrf T (f ↔ g)%fol → SysPrf T (g ↔ f)%fol.

Lemma iffTrans (T : System) (f g h : Formula):
  SysPrf T (f ↔ g)%fol → SysPrf T (g ↔ h)%fol →
  SysPrf T (f ↔ h)%fol.

Lemma eqRefl (T : System) (a : Term): SysPrf T (a = a)%fol.

Lemma eqSym (T : System) (a b : Term):
 SysPrf T (a = b)%fol → SysPrf T (b = a)%fol.

Lemma eqTrans (T : System) (a b c : Term):
SysPrf T (a = b)%fol → SysPrf T (b = c)%fol → SysPrf T (a = c)%fol.

Lemma eqPlus (T : System) (a b c d : Term):
  SysPrf T (a = b)%fol → SysPrf T (c = d)%fol →
  SysPrf T (a + c = b + d)%fol.

Lemma eqTimes (T : System) (a b c d : Term):
 SysPrf T (a = b)%fol → SysPrf T (c = d)%fol →
 SysPrf T (a × c = b × d)%fol.

Lemma eqSucc (T : System) (a b : Term):
  SysPrf T (a = b)%fol → SysPrf T (Succ a = Succ b)%fol.

Lemma eqLT (T : System) (a b c d : Term):
 SysPrf T (a = b)%fol → SysPrf T (c = d)%fol →
 SysPrf T (a < c ↔ b < d)%fol.

End Logic.

Fixpoint natToTerm (n : nat) : Term :=
  match n with
  | O ⇒ Zero
  | S m ⇒ Succ (natToTerm m)
  end.

#[global] Notation n2t i := (natToTerm i).

Lemma closedNatToTerm :
 ∀ a v : nat, ¬ In v (freeVarT (natToTerm a)).