Library hydras.Ackermann.model

From Coq Require Import Ensembles List Vector Arith.

From hydras.Ackermann Require Import ListExt folProof folProp.
From Coq Require Import Peano_dec.
From hydras.Ackermann Require Import misc.
Import FolNotations.
From hydras.Ackermann Require Import NewNotations.

Section Model_Theory.

Variable L : Language.

Fixpoint naryFunc (A : Set) (n : nat) {struct n} : Set :=
  match n with
  | O ⇒ A
  | S m ⇒ A → naryFunc A m
  end.

Fixpoint naryRel (A : Set) (n : nat) {struct n} : Type :=
  match n with
  | O ⇒ Prop
  | S m ⇒ A → naryRel A m
  end.

Record Model : Type := model
  {U : Set;
   func : ∀ f : Functions L, naryFunc U (arityF L f);
   rel : ∀ r : Relations L, naryRel U (arityR L r)}.

Variable M : Model.

Fixpoint interpTerm (value : nat → U M) (t : Term L) {struct t} :
 U M :=
  match t with
  | var v ⇒ value v
  | apply f ts ⇒ interpTerms _ (func M f) value ts
  end
 
 with interpTerms (m : nat) (f : naryFunc (U M) m)
 (value : nat → U M) (ts : Terms L m) {struct ts} :
 U M :=
  match ts in (Terms _ n) return (naryFunc (U M) n → U M) with
  | Tnil ⇒ fun f ⇒ f
  | Tcons m t ts ⇒ fun f ⇒ interpTerms m (f (interpTerm value t)) value ts
  end f.

Fixpoint interpRels (m : nat) (r : naryRel (U M) m)
 (value : nat → U M) (ts : Terms L m) {struct ts} : Prop :=
  match ts in (Terms _ n) return (naryRel (U M) n → Prop) with
  | Tnil ⇒ fun r ⇒ r
  | Tcons m t ts ⇒ fun r ⇒ interpRels m (r (interpTerm value t)) value ts
  end r.

Definition updateValue (value : nat → U M) (n : nat)
  (v : U M) (x : nat) : U M :=
  match eq_nat_dec n x with
  | left _ ⇒ v
  | right _ ⇒ value x
  end.

Fixpoint interpFormula (value : nat → U M) (f : Formula L) {struct f} :
 Prop :=
  match f with
  | equal t s ⇒ interpTerm value t = interpTerm value s
  | atomic r ts ⇒ interpRels _ (rel M r) value ts
  | impH A B ⇒ interpFormula value A → interpFormula value B
  | notH A ⇒ interpFormula value A → False
  | forallH v A ⇒ ∀ x : U M, interpFormula (updateValue value v x) A
  end.

Lemma freeVarInterpTerm (v1 v2 : nat → U M) (t : Term L):
 (∀ x : nat, List.In x (freeVarT t) → v1 x = v2 x) →
 interpTerm v1 t = interpTerm v2 t.

Lemma freeVarInterpRel (v1 v2 : nat → U M) (n : nat)
  (ts : Terms L n) (r : naryRel (U M) n):
  (∀ x : nat, List.In x (freeVarTs ts) → v1 x = v2 x) →
  interpRels n r v1 ts → interpRels n r v2 ts.

Lemma freeVarInterpFormula (v1 v2 : nat → U M) (g : Formula L):
 (∀ x : nat, List.In x (freeVarF g) → v1 x = v2 x) →
 interpFormula v1 g → interpFormula v2 g.

Lemma subInterpTerm (value : nat → U M) (t : Term L) (v : nat) (s : Term L):
 interpTerm (updateValue value v (interpTerm value s)) t =
 interpTerm value (substT t v s).

Lemma subInterpRel (value : nat → U M) (n : nat) (ts : Terms L n)
  (v : nat) (s : Term L) (r : naryRel (U M) n):
  interpRels n r (updateValue value v (interpTerm value s)) ts ↔
    interpRels n r value (substTs ts v s).

Lemma subInterpFormula :
 ∀ (value : nat → U M) (f : Formula L) (v : nat) (s : Term L),
 interpFormula (updateValue value v (interpTerm value s)) f ↔
 interpFormula value (substF f v s).

Lemma subInterpFormula1 (value : nat → U M) (f : Formula L) (v : nat) (s : Term L):
 interpFormula (updateValue value v (interpTerm value s)) f →
 interpFormula value (substF f v s).

Lemma subInterpFormula2 (value : nat → U M) (f : Formula L) (v : nat) (s : Term L):
  interpFormula value (substF f v s) →
  interpFormula (updateValue value v (interpTerm value s)) f.

Fixpoint nnHelp (f : Formula L) : Formula L :=
  match f with
  | equal t s ⇒ equal t s
  | atomic r ts ⇒ atomic r ts
  | impH A B ⇒ impH (nnHelp A) (nnHelp B)
  | notH A ⇒ notH (nnHelp A)
  | forallH v A ⇒ (allH v, ¬ ¬ nnHelp A)%fol
  end.

Definition nnTranslate (f : Formula L) : Formula L :=
  notH (notH (nnHelp f)).

Lemma freeVarNNHelp (f : Formula L): freeVarF f = freeVarF (nnHelp f).

Lemma subNNHelp :
 ∀ (f : Formula L) (v : nat) (s : Term L),
 substF (nnHelp f) v s = nnHelp (substF f v s).

Section Consistent_Theory.

  Variable T : System L.

  Fixpoint interpTermsVector (value : nat → U M) (n : nat)
    (ts : Terms L n) {struct ts} : Vector.t (U M) n :=
    match ts in (Terms _ n) return (Vector.t (U M) n) with
    | Tnil ⇒ Vector.nil (U M)
    | Tcons m t ts ⇒
        Vector.cons (U M) (interpTerm value t) m (interpTermsVector value m ts)
    end.

Lemma preserveValue (value : nat → U M):
 (∀ f : Formula L,
  mem _ T f → interpFormula value (nnTranslate f)) →
 ∀ g : Formula L, SysPrf L T g → interpFormula value (nnTranslate g).

Lemma ModelConsistent (value : nat → U M):
  (∀ f : Formula L,
      mem _ T f → interpFormula value (nnTranslate f)) →
  Consistent L T.

End Consistent_Theory.

End Model_Theory.