Library hydras.Ackermann.LNN2LNT

LNN2LNT:

Translation of LNN-formulas and proofs into LNT by replacement of (t < t')%fol subformulas with (∃ v, t + Succ v = t')%nt.

Original file by Russel O'Connor

Translation of terms

Fixpoint LNN2LNT_term (t : fol.Term LNN) : fol.Term LNT:=
  match t with
  | var v ⇒ var v
  | apply f ts ⇒ apply LNT f (LNN2LNT_terms _ ts)
  end

with LNN2LNT_terms (n : nat) (ts : fol.Terms LNN n) {struct ts} :
Terms n :=
  match ts in (fol.Terms _ n0) return (Terms n0) with
  | Tnil ⇒ @Tnil LNT
  | Tcons m s ss ⇒ Tcons (LNN2LNT_term s) (LNN2LNT_terms m ss)
  end.

Inverse translation

Fixpoint LNT2LNN_term (t : Term) : fol.Term LNN :=
  match t with
  | var v ⇒ var v
  | apply f ts ⇒ apply LNN f (LNT2LNN_terms _ ts)
  end

with LNT2LNN_terms (n : nat) (ts : Terms n) {struct ts} :
fol.Terms LNN n :=
  match ts in (fol.Terms _ n0) return (fol.Terms LNN n0) with
  | Tnil ⇒ @Tnil LNN
  | Tcons m s ss ⇒ Tcons (LNT2LNN_term s) (LNT2LNN_terms m ss)
  end.

Lemma LNT2LNN_natToTerm (n: nat) :
  LNT2LNN_term (natToTerm n) = natToTermLNN n.

Lemma LNT2LNT_term (t : Term): LNN2LNT_term (LNT2LNN_term t) = t.

Translation of formulas

Translation of (v#0 < v#1)%fol

Definition LTFormula := (exH 2, v #0 + LNT.Succ v #2 = v #1)%nt.

Translation of (t < t')%fol

The function translateLT is defined by an interactive proof (omitted). It is specified by the lemma translateLT1

Definition translateLT (ts : fol.Terms LNN (arityR LNN LT_)) : Formula.

Lemma translateLT1 :
∀ a a0 b0,
translateLT (Tcons a (Tcons a0 b0)) =
subAllFormula LNT LTFormula
   (fun H : nat ⇒
    nat_rec (fun _ : nat ⇒ fol.Term LNT) (LNN2LNT_term a)
      (fun (H0 : nat) (_ : fol.Term LNT) ⇒
       nat_rec (fun _ : nat ⇒ fol.Term LNT) (LNN2LNT_term a0)
         (fun (H1 : nat) (_ : fol.Term LNT) ⇒ var H1) H0) H).

Translation of any LNN-formula

The translation of any LNN-formula is straigthforward, except for the special case of t_1 < t_2 (handled by translateLT )

Fixpoint LNN2LNT_formula (f : fol.Formula LNN) : Formula :=
  match f with
  | (t1 = t2)%fol ⇒ (LNN2LNT_term t1 = LNN2LNT_term t2)%nt
  | atomic r ts ⇒
      match
        r as l return (fol.Terms LNN (arityR LNN l) → Formula)
      with
      | LT_ ⇒ fun ts : fol.Terms LNN (arityR LNN LT_) ⇒ translateLT ts
      end ts
  | (A → B)%fol ⇒ (LNN2LNT_formula A → LNN2LNT_formula B)%nt
  | (¬ A)%fol ⇒ (¬ LNN2LNT_formula A)%nt
  | (allH v, A)%fol ⇒ (allH v, LNN2LNT_formula A)%nt
  end.

Helpful rewriting lemmas

Lemma LNN2LNT_or (a b : fol.Formula LNN):
  LNN2LNT_formula (orH a b) =
    orH (LNN2LNT_formula a) (LNN2LNT_formula b).

Lemma LNN2LNT_and (a b : fol.Formula LNN):
LNN2LNT_formula (andH a b) =
andH (LNN2LNT_formula a) (LNN2LNT_formula b).

Lemma LNN2LNT_iff (a b : fol.Formula LNN):
LNN2LNT_formula (iffH a b) =
   iffH (LNN2LNT_formula a) (LNN2LNT_formula b).

Lemma LNN2LNT_exist (v : nat) (a : fol.Formula LNN) :
LNN2LNT_formula (existH v a) = existH v (LNN2LNT_formula a).

Lemma LNN2LNT_freeVarF (f : fol.Formula LNN) (v : nat):
  In v (freeVarF (LNN2LNT_formula f)) ↔ In v (freeVarF f).

Lemma LNN2LNT_freeVarF1 (f : fol.Formula LNN) (v : nat):
In v (freeVarF (LNN2LNT_formula f)) →
In v (freeVarF f).

Lemma LNN2LNT_freeVarF2 (f : fol.Formula LNN) (v : nat):
  In v (freeVarF f) →
  In v (freeVarF (LNN2LNT_formula f)).

Lemma LNN2LNT_subFormula
(T : System) (f : fol.Formula LNN) (v : nat) (s : fol.Term LNN):
SysPrf T
   (iffH (LNN2LNT_formula (substF f v s))
      (substF (LNN2LNT_formula f) v (LNN2LNT_term s))).

Inverse translation

Fixpoint LNT2LNN_formula (f : Formula) : fol.Formula LNN :=
  match f with
  | (t1 = t2)%nt ⇒ (LNT2LNN_term t1 = LNT2LNN_term t2)%fol
  | atomic r ts ⇒ match r with
                   end
  | (A → B)%nt ⇒ (LNT2LNN_formula A → LNT2LNN_formula B)%fol
  | (¬ A)%nt ⇒ (¬ LNT2LNN_formula A)%fol
  | (allH v, A)%nt ⇒ (allH v, LNT2LNN_formula A)%fol
  end.

Commutation lemmas

Lemma LNT2LNT_formula (f : Formula):
LNN2LNT_formula (LNT2LNN_formula f) = f.

Lemma LNT2LNN_subTerm (t : Term) (v : nat) (s : Term):
  LNT2LNN_term (substT t v s) =
    substT (LNT2LNN_term t) v (LNT2LNN_term s).

Lemma LNT2LNN_freeVarT ( t : Term):
  freeVarT (LNT2LNN_term t) = freeVarT t.

Lemma LNT2LNN_freeVarF (f : Formula):
  freeVarF (LNT2LNN_formula f) = freeVarF f.

Lemma LNT2LNN_subFormula :
  ∀ (f : Formula) (v : nat) (s : Term),
    LNT2LNN_formula (substF f v s) =
      substF (LNT2LNN_formula f) v (LNT2LNN_term s).

Proof translation

If the translation of every axiom of a LNN-system U is provable in a closed LNT-system V, then the translation of any LNN-formula in U is provable in V.

Lemma translateProof (U : fol.System LNN) (V : System):
    ClosedSystem LNT V →
    (∀ f : fol.Formula LNN,
        mem (fol.Formula LNN) U f → SysPrf V (LNN2LNT_formula f)) →
    ∀ f : fol.Formula LNN,
      folProof.SysPrf LNN U f → SysPrf V (LNN2LNT_formula f).