Library hydras.Ackermann.LNT

LNT.v : Language of Number Theory
Original version by Russel O'Connor

From Coq Require Import Arith Ensembles List.

From hydras.Ackermann
 Require Import Languages folProof folProp folLogic3.

Instantiations of a few generic constructs

To do perhaps these redefinitions should be deprecated, because they cause some issues in statements which mix LNN and LNT terms and formulas

Definition Formula := Formula LNT.
Definition Formulas := Formulas LNT.
Definition System := System LNT.
Definition Sentence := Sentence LNT.
Definition Term := Term LNT.
Definition Terms := Terms LNT.
Definition SysPrf := SysPrf LNT.
#[local] Arguments apply _ _ _ : clear implicits.

Module LNT.

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

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

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

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

End LNT.
Export LNT.

Notations for LNT formulas: experimental and unstable


Declare Scope nt_scope.
Delimit Scope nt_scope with nt.

Infix "=" := (equal _): nt_scope.
Infix "∨" := (orH): nt_scope.
Infix "∧" := (andH):nt_scope.
Infix "→" := (impH): nt_scope.
Notation "~ A" := (@notH _ A): nt_scope.
Notation "A <-> B" := (@iffH _ A B): nt_scope.

Notation "t = u" := (@equal _ t u): nt_scope.
Notation "t <> u" := (¬ t = u)%nt : nt_scope.
Notation "'v#' i" := (var i) (at level 3, format "'v#' i", i at level 0) : nt_scope.

Notation "'exH' x .. y , p" := (existH x .. (existH y p) ..)
  (x at level 0, y at level 0, at level 200, right associativity) : nt_scope.

Notation "'allH' x .. y , p" := (forallH x .. (forallH y p) ..)
  (x at level 0, y at level 0, at level 200, right associativity) : nt_scope.

Infix "+" := Plus :nt_scope.
Infix "×" := Times :nt_scope.
Notation S_ t := (apply LNT Succ_ (Tcons t (Tnil))).

Notations for printing computed formulas/terms with derived connectives


Reserved Notation "x '\/'' y" (at level 85, right associativity).
Reserved Notation "x '/\'' y" (at level 80, right associativity).
Reserved Notation "x '<->'' y" (at level 95, no associativity).
Reserved Notation "x '<->''' y" (at level 95, no associativity).

Notation "x \/' y" := (¬ x → y)%nt : nt_scope.
Notation "x /\' y" := (¬ (~ x \/' ¬ y))%nt : nt_scope.
Notation "x <->'' y" := ((x → y) ∧ (y → x))%nt: nt_scope.
Notation "x <->' y" := (¬ (~ (x → y) \/' ~(y → x)))%nt : nt_scope.
Notation exH' v A := (¬ (forallH v (¬ A)))%nt.

Examples


Section Examples.
Variable f : Formula.
Check (allH 0 1 , (f → v#0 = v#0 → v#1 = v#1))%nt.

Check (exH 0 1 , (v#0 = v#0 → v#1 = v#1))%nt.
End Examples.

Basic properties


Lemma LNT_eqdec : language_decidable LNT.

List of free variables of a formula


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 (S_ x)%nt = freeVarT x.

Lemma freeVarZero : freeVarT Zero = nil.

End Free_Variables.

Basic and derived proof rules


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)%nt.

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

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

Lemma nnE (T : System) (f : Formula):
  SysPrf T (¬ ¬ f)%nt → SysPrf T f.

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

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

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

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

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

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

Lemma orE (T : System) (f g h : Formula):
  SysPrf T (f ∨ g)%nt →
  SysPrf T (f → h)%nt → SysPrf T (g → h)%nt →
  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)%nt) h.

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

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

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

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

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

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

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

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

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

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

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

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

Lemma existSys (T : System) (f g : Formula) (v : nat):
  ¬ In_freeVarSys LNT v T →
  ¬ In v (freeVarF g) →
  SysPrf (Ensembles.Add _ T f) g →
  SysPrf (Ensembles.Add _ T (exH v, f)%nt) g.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

End Logic.

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

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