Library hydras.Ackermann.folProp
From Coq Require Import Wf_nat Arith Lists.List Peano_dec.
From hydras.Ackermann Require Import ListExt.
From hydras.Ackermann Require Export fol.
Import FolNotations.
Section Fol_Properties.
Variable L : Language.
Notation Formula := (Formula L) (only parsing).
Notation Formulas := (Formulas L) (only parsing).
Notation System := (System L) (only parsing).
Notation Term := (Term L) (only parsing).
Notation Terms := (Terms L) (only parsing).
Let lt_depth := lt_depth L.
Section Free_Variables.
Fixpoint freeVarT (s : fol.Term L) : list nat :=
match s with
| var v ⇒ v :: nil
| apply f ts ⇒ freeVarTs (arityF L f) ts
end
with freeVarTs (n : nat) (ss : fol.Terms L n) {struct ss} : list nat :=
match ss with
| Tnil ⇒ nil (A:=nat)
| Tcons m t ts ⇒ freeVarT t ++ freeVarTs m ts
end.
Lemma freeVarTApply :
∀ (f : Functions L) (ts : fol.Terms L _),
freeVarT (apply f ts) = freeVarTs _ ts.
Fixpoint freeVarF (A : fol.Formula L) : list nat :=
match A with
| equal t s ⇒ freeVarT t ++ freeVarT s
| atomic r ts ⇒ freeVarTs _ ts
| impH A B ⇒ freeVarF A ++ freeVarF B
| notH A ⇒ freeVarF A
| forallH v A ⇒ remove eq_nat_dec v (freeVarF A)
end.
Definition ClosedSystem (T : fol.System L) :=
∀ (v : nat) (f : fol.Formula L),
mem _ T f → ¬ In v (freeVarF f).
Definition closed (a : fol.Formula L):=
∀ v: nat, ¬ In v (freeVarF a).
Fixpoint closeList (l: list nat)(a : fol.Formula L) :=
match l with
nil ⇒ a
| cons v l ⇒ f[ ∀ v, {closeList l a} ]f
end.
Definition close (x : fol.Formula L) : fol.Formula L :=
closeList (nodup eq_nat_dec (freeVarF x)) x.
Lemma freeVarClosedList1 :
∀ (l : list nat) (v : nat) (x : fol.Formula L),
In v l → ¬ In v (freeVarF (closeList l x)).
Lemma freeVarClosedList2 :
∀ (l : list nat) (v : nat) (x : fol.Formula L),
In v (freeVarF (closeList l x)) →
In v (freeVarF x).
Lemma freeVarClosed :
∀ (x : fol.Formula L) (v : nat), ¬ In v (freeVarF (close x)).
Fixpoint freeVarListFormula (l : fol.Formulas L) : list nat :=
match l with
| nil ⇒ nil (A:=nat)
| f :: l ⇒ freeVarF f ++ freeVarListFormula l
end.
Lemma freeVarListFormulaApp :
∀ a b : fol.Formulas L,
freeVarListFormula (a ++ b) =
freeVarListFormula a ++ freeVarListFormula b.
Lemma In_freeVarListFormula :
∀ (v : nat) (f : fol.Formula L) (F : fol.Formulas L),
In v (freeVarF f) → In f F → In v (freeVarListFormula F).
Lemma In_freeVarListFormulaE :
∀ (v : nat) (F : fol.Formulas L),
In v (freeVarListFormula F) →
∃ f : fol.Formula L, In v (freeVarF f) ∧ In f F.
Definition In_freeVarSys (v : nat) (T : fol.System L) :=
∃ f : fol.Formula L, In v (freeVarF f) ∧ mem _ T f.
Lemma notInFreeVarSys :
∀ x, ¬ In_freeVarSys x (Ensembles.Empty_set (fol.Formula L)).
End Free_Variables.
Section Substitution.
Fixpoint substT (s : fol.Term L) (x : nat)
(t : fol.Term L) {struct s} : fol.Term L :=
match s with
| var v ⇒
match eq_nat_dec x v with
| left _ ⇒ t
| right _ ⇒ var v
end
| apply f ts ⇒ apply f (substTs _ ts x t)
end
with substTs (n : nat) (ss : fol.Terms L n)
(x : nat) (t : fol.Term L) {struct ss} : fol.Terms L n :=
match ss in (fol.Terms _ n0) return (fol.Terms L n0) with
| Tnil ⇒ Tnil
| Tcons m s ts ⇒
Tcons (substT s x t) (substTs m ts x t)
end.
Lemma subTermVar1 :
∀ (v : nat) (s : fol.Term L), substT (var v) v s = s.
Lemma subTermVar2 :
∀ (v x : nat) (s : fol.Term L),
v ≠ x → substT (var x) v s = var x.
Lemma subTermApply :
∀ (f : Functions L) (ts : fol.Terms L (arityF L f))
(v : nat) (s : fol.Term L),
substT (apply f ts) v s = apply f (substTs _ ts v s).
Definition newVar (l : list nat) : nat :=
fold_right Nat.max 0 (map S l).
Lemma newVar2 : ∀ (l : list nat) (n : nat), In n l → n < newVar l.
Lemma newVar1 : ∀ l : list nat, ¬ In (newVar l) l.
Definition substituteFormulaImp (f : fol.Formula L)
(frec : nat × fol.Term L → {y : fol.Formula L | depth L y = depth L f})
(g : fol.Formula L)
(grec : nat × fol.Term L → {y : fol.Formula L | depth L y = depth L g})
(p : nat × fol.Term L) :
{y : fol.Formula L | depth L y = depth L (impH f g)} :=
match frec p with
| exist f' prf1 ⇒
match grec p with
| exist g' prf2 ⇒
exist
(fun y : fol.Formula L ⇒
depth L y = S (Nat.max (depth L f) (depth L g)))
(impH f' g')
(eq_ind_r
(fun n : nat ⇒
S (Nat.max n (depth L g')) =
S (Nat.max (depth L f) (depth L g)))
(eq_ind_r
(fun n : nat ⇒
S (Nat.max (depth L f) n) =
S (Nat.max (depth L f) (depth L g)))
(refl_equal (S (Nat.max (depth L f) (depth L g))))
prf2) prf1)
end
end.
Remark substituteFormulaImpNice :
∀ (f g : fol.Formula L)
(z1 z2 : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L f}),
(∀ q : nat × fol.Term L, z1 q = z2 q) →
∀
z3 z4 : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L g},
(∀ q : nat × fol.Term L, z3 q = z4 q) →
∀ q : nat × fol.Term L,
substituteFormulaImp f z1 g z3 q =
substituteFormulaImp f z2 g z4 q.
Definition substituteFormulaNot (f : fol.Formula L)
(frec : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L f})
(p : nat × fol.Term L) :
{y : fol.Formula L | depth L y = depth L (notH f)} :=
match frec p with
| exist f' prf1 ⇒
exist (fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(notH f')
(eq_ind_r (fun n : nat ⇒ S n = S (depth L f))
(refl_equal (S (depth L f))) prf1)
end.
Remark substituteFormulaNotNice :
∀ (f : fol.Formula L)
(z1 z2 : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L f}),
(∀ q : nat × fol.Term L, z1 q = z2 q) →
∀ q : nat × fol.Term L,
substituteFormulaNot f z1 q = substituteFormulaNot f z2 q.
Definition substituteFormulaForall (n : nat) (f : fol.Formula L)
(frec : ∀ b : fol.Formula L,
lt_depth b (forallH n f) →
nat × fol.Term L → {y : fol.Formula L | depth L y = depth L b})
(p : nat × fol.Term L) :
{y : fol.Formula L | depth L y = depth L (forallH n f)} :=
match p with
| (v, s) ⇒
match eq_nat_dec n v with
| left _ ⇒
exist (fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(forallH n f) (refl_equal (depth L (forallH n f)))
| right _ ⇒
match In_dec eq_nat_dec n (freeVarT s) with
| left _ ⇒
let nv := newVar (v :: freeVarT s ++ freeVarF f) in
match frec f (depthForall L f n) (n, var nv) with
| exist f' prf1 ⇒
match
frec f'
(eqDepth L f' f (forallH n f)
(sym_eq prf1) (depthForall L f n)) p
with
| exist f'' prf2 ⇒
exist
(fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(forallH nv f'')
(eq_ind_r (fun n : nat ⇒ S n = S (depth L f))
(refl_equal (S (depth L f)))
(trans_eq prf2 prf1))
end
end
| right _ ⇒
match frec f (depthForall L f n) p with
| exist f' prf1 ⇒
exist (fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(forallH n f')
(eq_ind_r (fun n : nat ⇒ S n = S (depth L f))
(refl_equal (S (depth L f))) prf1)
end
end
end
end.
Remark substituteFormulaForallNice :
∀ (v : nat) (a : fol.Formula L)
(z1 z2 : ∀ b : fol.Formula L,
lt_depth b (forallH v a) →
nat × fol.Term L → {y : fol.Formula L | depth L y = depth L b}),
(∀ (b : fol.Formula L) (q : lt_depth b (forallH v a))
(r : nat × fol.Term L), z1 b q r = z2 b q r) →
∀ q : nat × fol.Term L,
substituteFormulaForall v a z1 q = substituteFormulaForall v a z2 q.
Definition substituteFormulaHelp (f : fol.Formula L)
(v : nat) (s : fol.Term L) :
{y : fol.Formula L | depth L y = depth L f}.
Definition substF (f : fol.Formula L) (v : nat) (s : fol.Term L) :
fol.Formula L := proj1_sig (substituteFormulaHelp f v s).
Lemma subFormulaEqual :
∀ (t1 t2 : fol.Term L) (v : nat) (s : fol.Term L),
substF (t1 = t2)%fol v s =
(substT t1 v s = substT t2 v s)%fol.
Lemma subFormulaRelation :
∀ (r : Relations L) (ts : fol.Terms L (arityR L r))
(v : nat) (s : fol.Term L),
substF (atomic r ts) v s =
atomic r (substTs (arityR L r) ts v s).
Lemma subFormulaImp :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (f1 → f2)%fol v s =
(substF f1 v s → substF f2 v s)%fol.
Lemma subFormulaNot :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
substF (¬ f)%fol v s = (¬ substF f v s)%fol.
Lemma subFormulaForall :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
let nv := newVar (v :: freeVarT s ++ freeVarF f) in
substF (allH x, f)%fol v s =
match eq_nat_dec x v with
| left _ ⇒ forallH x f
| right _ ⇒
match In_dec eq_nat_dec x (freeVarT s) with
| right _ ⇒ (allH x, substF f v s)%fol
| left _ ⇒ (allH nv, substF (substF f x (v# nv) ) v s)%fol
end
end.
Section Extensions.
Lemma subFormulaOr :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (f1 ∨ f2)%fol v s =
(substF f1 v s ∨ substF f2 v s)%fol.
Lemma subFormulaAnd :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (f1 ∧ f2)%fol v s =
(substF f1 v s ∧ substF f2 v s)%fol.
Lemma subFormulaExist :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
let nv := newVar (v :: freeVarT s ++ freeVarF f) in
substF (existH x f) v s =
match eq_nat_dec x v with
| left _ ⇒ existH x f
| right _ ⇒
match In_dec eq_nat_dec x (freeVarT s) with
| right _ ⇒ existH x (substF f v s)
| left _ ⇒
existH nv (substF
(substF f x (var nv)) v s)
end
end.
Lemma subFormulaIff :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (iffH f1 f2) v s =
iffH (substF f1 v s) (substF f2 v s).
Lemma subFormulaIfThenElse :
∀ (f1 f2 f3 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (ifThenElseH f1 f2 f3) v s =
ifThenElseH (substF f1 v s) (substF f2 v s)
(substF f3 v s).
End Extensions.
Lemma subFormulaDepth :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
depth L (substF f v s) = depth L f.
Section Substitution_Properties.
Lemma subTermId :
∀ (t : fol.Term L) (v : nat), substT t v (var v) = t.
Lemma subTermsId :
∀ (n : nat) (ts : fol.Terms L n) (v : nat),
substTs n ts v (var v) = ts.
Lemma subFormulaId :
∀ (f : fol.Formula L) (v : nat), substF f v (var v) = f.
Lemma subFormulaForall2 :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
∃ nv : nat,
¬ In nv (freeVarT s) ∧
nv ≠ v ∧
¬ In nv (remove eq_nat_dec x (freeVarF f)) ∧
substF (forallH x f) v s =
match eq_nat_dec x v with
| left _ ⇒ forallH x f
| right _ ⇒
forallH nv (substF (substF f x (var nv)) v s)
end.
Lemma subFormulaExist2 :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
∃ nv : nat,
¬ In nv (freeVarT s) ∧
nv ≠ v ∧
¬ In nv (remove eq_nat_dec x (freeVarF f)) ∧
substF (existH x f) v s =
match eq_nat_dec x v with
| left _ ⇒ existH x f
| right _ ⇒
existH nv (substF (substF f x (var nv)) v s)
end.
Lemma substExHC (A : Formula) (v x : nat)(t: Term):
v ≠ x → ¬ In v (freeVarT t) →
substF (existH v A) x t =
existH v (substF A x t).
End Substitution_Properties.
End Substitution.
Definition Sentence (f:Formula) :=
(∀ v : nat, ¬ In v (freeVarF f)).
End Fol_Properties.
Arguments closed {L} _.
#[global] Arguments substF {L} _ _.
#[global] Arguments substT {L} _ _.
#[global] Arguments substTs {L n} _ _ _ .
From hydras.Ackermann Require Import ListExt.
From hydras.Ackermann Require Export fol.
Import FolNotations.
Section Fol_Properties.
Variable L : Language.
Notation Formula := (Formula L) (only parsing).
Notation Formulas := (Formulas L) (only parsing).
Notation System := (System L) (only parsing).
Notation Term := (Term L) (only parsing).
Notation Terms := (Terms L) (only parsing).
Let lt_depth := lt_depth L.
Section Free_Variables.
Fixpoint freeVarT (s : fol.Term L) : list nat :=
match s with
| var v ⇒ v :: nil
| apply f ts ⇒ freeVarTs (arityF L f) ts
end
with freeVarTs (n : nat) (ss : fol.Terms L n) {struct ss} : list nat :=
match ss with
| Tnil ⇒ nil (A:=nat)
| Tcons m t ts ⇒ freeVarT t ++ freeVarTs m ts
end.
Lemma freeVarTApply :
∀ (f : Functions L) (ts : fol.Terms L _),
freeVarT (apply f ts) = freeVarTs _ ts.
Fixpoint freeVarF (A : fol.Formula L) : list nat :=
match A with
| equal t s ⇒ freeVarT t ++ freeVarT s
| atomic r ts ⇒ freeVarTs _ ts
| impH A B ⇒ freeVarF A ++ freeVarF B
| notH A ⇒ freeVarF A
| forallH v A ⇒ remove eq_nat_dec v (freeVarF A)
end.
Definition ClosedSystem (T : fol.System L) :=
∀ (v : nat) (f : fol.Formula L),
mem _ T f → ¬ In v (freeVarF f).
Definition closed (a : fol.Formula L):=
∀ v: nat, ¬ In v (freeVarF a).
Fixpoint closeList (l: list nat)(a : fol.Formula L) :=
match l with
nil ⇒ a
| cons v l ⇒ f[ ∀ v, {closeList l a} ]f
end.
Definition close (x : fol.Formula L) : fol.Formula L :=
closeList (nodup eq_nat_dec (freeVarF x)) x.
Lemma freeVarClosedList1 :
∀ (l : list nat) (v : nat) (x : fol.Formula L),
In v l → ¬ In v (freeVarF (closeList l x)).
Lemma freeVarClosedList2 :
∀ (l : list nat) (v : nat) (x : fol.Formula L),
In v (freeVarF (closeList l x)) →
In v (freeVarF x).
Lemma freeVarClosed :
∀ (x : fol.Formula L) (v : nat), ¬ In v (freeVarF (close x)).
Fixpoint freeVarListFormula (l : fol.Formulas L) : list nat :=
match l with
| nil ⇒ nil (A:=nat)
| f :: l ⇒ freeVarF f ++ freeVarListFormula l
end.
Lemma freeVarListFormulaApp :
∀ a b : fol.Formulas L,
freeVarListFormula (a ++ b) =
freeVarListFormula a ++ freeVarListFormula b.
Lemma In_freeVarListFormula :
∀ (v : nat) (f : fol.Formula L) (F : fol.Formulas L),
In v (freeVarF f) → In f F → In v (freeVarListFormula F).
Lemma In_freeVarListFormulaE :
∀ (v : nat) (F : fol.Formulas L),
In v (freeVarListFormula F) →
∃ f : fol.Formula L, In v (freeVarF f) ∧ In f F.
Definition In_freeVarSys (v : nat) (T : fol.System L) :=
∃ f : fol.Formula L, In v (freeVarF f) ∧ mem _ T f.
Lemma notInFreeVarSys :
∀ x, ¬ In_freeVarSys x (Ensembles.Empty_set (fol.Formula L)).
End Free_Variables.
Section Substitution.
Fixpoint substT (s : fol.Term L) (x : nat)
(t : fol.Term L) {struct s} : fol.Term L :=
match s with
| var v ⇒
match eq_nat_dec x v with
| left _ ⇒ t
| right _ ⇒ var v
end
| apply f ts ⇒ apply f (substTs _ ts x t)
end
with substTs (n : nat) (ss : fol.Terms L n)
(x : nat) (t : fol.Term L) {struct ss} : fol.Terms L n :=
match ss in (fol.Terms _ n0) return (fol.Terms L n0) with
| Tnil ⇒ Tnil
| Tcons m s ts ⇒
Tcons (substT s x t) (substTs m ts x t)
end.
Lemma subTermVar1 :
∀ (v : nat) (s : fol.Term L), substT (var v) v s = s.
Lemma subTermVar2 :
∀ (v x : nat) (s : fol.Term L),
v ≠ x → substT (var x) v s = var x.
Lemma subTermApply :
∀ (f : Functions L) (ts : fol.Terms L (arityF L f))
(v : nat) (s : fol.Term L),
substT (apply f ts) v s = apply f (substTs _ ts v s).
Definition newVar (l : list nat) : nat :=
fold_right Nat.max 0 (map S l).
Lemma newVar2 : ∀ (l : list nat) (n : nat), In n l → n < newVar l.
Lemma newVar1 : ∀ l : list nat, ¬ In (newVar l) l.
Definition substituteFormulaImp (f : fol.Formula L)
(frec : nat × fol.Term L → {y : fol.Formula L | depth L y = depth L f})
(g : fol.Formula L)
(grec : nat × fol.Term L → {y : fol.Formula L | depth L y = depth L g})
(p : nat × fol.Term L) :
{y : fol.Formula L | depth L y = depth L (impH f g)} :=
match frec p with
| exist f' prf1 ⇒
match grec p with
| exist g' prf2 ⇒
exist
(fun y : fol.Formula L ⇒
depth L y = S (Nat.max (depth L f) (depth L g)))
(impH f' g')
(eq_ind_r
(fun n : nat ⇒
S (Nat.max n (depth L g')) =
S (Nat.max (depth L f) (depth L g)))
(eq_ind_r
(fun n : nat ⇒
S (Nat.max (depth L f) n) =
S (Nat.max (depth L f) (depth L g)))
(refl_equal (S (Nat.max (depth L f) (depth L g))))
prf2) prf1)
end
end.
Remark substituteFormulaImpNice :
∀ (f g : fol.Formula L)
(z1 z2 : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L f}),
(∀ q : nat × fol.Term L, z1 q = z2 q) →
∀
z3 z4 : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L g},
(∀ q : nat × fol.Term L, z3 q = z4 q) →
∀ q : nat × fol.Term L,
substituteFormulaImp f z1 g z3 q =
substituteFormulaImp f z2 g z4 q.
Definition substituteFormulaNot (f : fol.Formula L)
(frec : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L f})
(p : nat × fol.Term L) :
{y : fol.Formula L | depth L y = depth L (notH f)} :=
match frec p with
| exist f' prf1 ⇒
exist (fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(notH f')
(eq_ind_r (fun n : nat ⇒ S n = S (depth L f))
(refl_equal (S (depth L f))) prf1)
end.
Remark substituteFormulaNotNice :
∀ (f : fol.Formula L)
(z1 z2 : nat × fol.Term L →
{y : fol.Formula L | depth L y = depth L f}),
(∀ q : nat × fol.Term L, z1 q = z2 q) →
∀ q : nat × fol.Term L,
substituteFormulaNot f z1 q = substituteFormulaNot f z2 q.
Definition substituteFormulaForall (n : nat) (f : fol.Formula L)
(frec : ∀ b : fol.Formula L,
lt_depth b (forallH n f) →
nat × fol.Term L → {y : fol.Formula L | depth L y = depth L b})
(p : nat × fol.Term L) :
{y : fol.Formula L | depth L y = depth L (forallH n f)} :=
match p with
| (v, s) ⇒
match eq_nat_dec n v with
| left _ ⇒
exist (fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(forallH n f) (refl_equal (depth L (forallH n f)))
| right _ ⇒
match In_dec eq_nat_dec n (freeVarT s) with
| left _ ⇒
let nv := newVar (v :: freeVarT s ++ freeVarF f) in
match frec f (depthForall L f n) (n, var nv) with
| exist f' prf1 ⇒
match
frec f'
(eqDepth L f' f (forallH n f)
(sym_eq prf1) (depthForall L f n)) p
with
| exist f'' prf2 ⇒
exist
(fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(forallH nv f'')
(eq_ind_r (fun n : nat ⇒ S n = S (depth L f))
(refl_equal (S (depth L f)))
(trans_eq prf2 prf1))
end
end
| right _ ⇒
match frec f (depthForall L f n) p with
| exist f' prf1 ⇒
exist (fun y : fol.Formula L ⇒ depth L y = S (depth L f))
(forallH n f')
(eq_ind_r (fun n : nat ⇒ S n = S (depth L f))
(refl_equal (S (depth L f))) prf1)
end
end
end
end.
Remark substituteFormulaForallNice :
∀ (v : nat) (a : fol.Formula L)
(z1 z2 : ∀ b : fol.Formula L,
lt_depth b (forallH v a) →
nat × fol.Term L → {y : fol.Formula L | depth L y = depth L b}),
(∀ (b : fol.Formula L) (q : lt_depth b (forallH v a))
(r : nat × fol.Term L), z1 b q r = z2 b q r) →
∀ q : nat × fol.Term L,
substituteFormulaForall v a z1 q = substituteFormulaForall v a z2 q.
Definition substituteFormulaHelp (f : fol.Formula L)
(v : nat) (s : fol.Term L) :
{y : fol.Formula L | depth L y = depth L f}.
Definition substF (f : fol.Formula L) (v : nat) (s : fol.Term L) :
fol.Formula L := proj1_sig (substituteFormulaHelp f v s).
Lemma subFormulaEqual :
∀ (t1 t2 : fol.Term L) (v : nat) (s : fol.Term L),
substF (t1 = t2)%fol v s =
(substT t1 v s = substT t2 v s)%fol.
Lemma subFormulaRelation :
∀ (r : Relations L) (ts : fol.Terms L (arityR L r))
(v : nat) (s : fol.Term L),
substF (atomic r ts) v s =
atomic r (substTs (arityR L r) ts v s).
Lemma subFormulaImp :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (f1 → f2)%fol v s =
(substF f1 v s → substF f2 v s)%fol.
Lemma subFormulaNot :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
substF (¬ f)%fol v s = (¬ substF f v s)%fol.
Lemma subFormulaForall :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
let nv := newVar (v :: freeVarT s ++ freeVarF f) in
substF (allH x, f)%fol v s =
match eq_nat_dec x v with
| left _ ⇒ forallH x f
| right _ ⇒
match In_dec eq_nat_dec x (freeVarT s) with
| right _ ⇒ (allH x, substF f v s)%fol
| left _ ⇒ (allH nv, substF (substF f x (v# nv) ) v s)%fol
end
end.
Section Extensions.
Lemma subFormulaOr :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (f1 ∨ f2)%fol v s =
(substF f1 v s ∨ substF f2 v s)%fol.
Lemma subFormulaAnd :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (f1 ∧ f2)%fol v s =
(substF f1 v s ∧ substF f2 v s)%fol.
Lemma subFormulaExist :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
let nv := newVar (v :: freeVarT s ++ freeVarF f) in
substF (existH x f) v s =
match eq_nat_dec x v with
| left _ ⇒ existH x f
| right _ ⇒
match In_dec eq_nat_dec x (freeVarT s) with
| right _ ⇒ existH x (substF f v s)
| left _ ⇒
existH nv (substF
(substF f x (var nv)) v s)
end
end.
Lemma subFormulaIff :
∀ (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (iffH f1 f2) v s =
iffH (substF f1 v s) (substF f2 v s).
Lemma subFormulaIfThenElse :
∀ (f1 f2 f3 : fol.Formula L) (v : nat) (s : fol.Term L),
substF (ifThenElseH f1 f2 f3) v s =
ifThenElseH (substF f1 v s) (substF f2 v s)
(substF f3 v s).
End Extensions.
Lemma subFormulaDepth :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
depth L (substF f v s) = depth L f.
Section Substitution_Properties.
Lemma subTermId :
∀ (t : fol.Term L) (v : nat), substT t v (var v) = t.
Lemma subTermsId :
∀ (n : nat) (ts : fol.Terms L n) (v : nat),
substTs n ts v (var v) = ts.
Lemma subFormulaId :
∀ (f : fol.Formula L) (v : nat), substF f v (var v) = f.
Lemma subFormulaForall2 :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
∃ nv : nat,
¬ In nv (freeVarT s) ∧
nv ≠ v ∧
¬ In nv (remove eq_nat_dec x (freeVarF f)) ∧
substF (forallH x f) v s =
match eq_nat_dec x v with
| left _ ⇒ forallH x f
| right _ ⇒
forallH nv (substF (substF f x (var nv)) v s)
end.
Lemma subFormulaExist2 :
∀ (f : fol.Formula L) (x v : nat) (s : fol.Term L),
∃ nv : nat,
¬ In nv (freeVarT s) ∧
nv ≠ v ∧
¬ In nv (remove eq_nat_dec x (freeVarF f)) ∧
substF (existH x f) v s =
match eq_nat_dec x v with
| left _ ⇒ existH x f
| right _ ⇒
existH nv (substF (substF f x (var nv)) v s)
end.
Lemma substExHC (A : Formula) (v x : nat)(t: Term):
v ≠ x → ¬ In v (freeVarT t) →
substF (existH v A) x t =
existH v (substF A x t).
End Substitution_Properties.
End Substitution.
Definition Sentence (f:Formula) :=
(∀ v : nat, ¬ In v (freeVarF f)).
End Fol_Properties.
Arguments closed {L} _.
#[global] Arguments substF {L} _ _.
#[global] Arguments substT {L} _ _.
#[global] Arguments substTs {L n} _ _ _ .
compatibility with older names
#[deprecated(note="use substF")]
Notation substituteFormula := substF (only parsing).
#[deprecated(note="use substT")]
Notation substituteTerm := substT (only parsing).
#[deprecated(note="use substTs")]
Notation substituteTerms := substTs (only parsing).
#[deprecated(note="use freeVarF")]
Notation freeVarFormula := freeVarF (only parsing).
#[deprecated(note="use freeVarT")]
Notation freeVarTerm := freeVarT (only parsing).
#[deprecated(note="use freeVarTs")]
Notation freeVarTerms := freeVarTs (only parsing).
About substF.
Search substF.
to replace with a single recursive custom notation ?
#[global] Notation substF2 e v1 t1 v2 t2 :=
(substF (substF e v1 t1) v2 t2).
#[global] Notation substF3 e v1 t1 v2 t2 v3 t3 :=
(substF (substF2 e v1 t1 v2 t2) v3 t3).
#[global] Notation substF4 e v1 t1 v2 t2 v3 t3 v4 t4 :=
(substF (substF3 e v1 t1 v2 t2 v3 t3) v4 t4).
#[global] Notation substF5 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 :=
(substF (substF4 e v1 t1 v2 t2 v3 t3 v4 t4) v5 t5).
#[global] Notation substF6 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 v6 t6 :=
(substF (substF5 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5) v6 t6).
#[global] Notation substF7 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 v6 t6 v7 t7:=
(substF (substF6 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 v6 t6) v7 t7).
#[global] Notation
substF8 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 v6 t6 v7 t7 v8 t8 :=
(substF2 (substF6 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 v6 t6)
v7 t7 v8 t8).
#[global] Notation
substF9 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 v6 t6 v7 t7 v8 t8 v9 t9:=
(substF3 (substF6 e v1 t1 v2 t2 v3 t3 v4 t4 v5 t5 v6 t6)
v7 t7 v8 t8 v9 t9).
#[global] Arguments freeVarF {L} _.
#[global] Arguments freeVarT {L} _.
#[global] Arguments freeVarTs {L n} _.