Library hydras.Ackermann.codeSubFormula
codeSubFormula:
Original file by Russel O'Connor
From Coq Require Import Arith Vector Lia.
From Coq Require Vector.
From hydras.Ackermann
Require Import primRec cPair folProp code extEqualNat codeSubTerm
codeFreeVar.
Import LispAbbreviations.
Import PRNotations.
From LibHyps Require Export LibHyps.
From hydras Require Export MoreLibHyps NewNotations Compat815.
Import Bool.
Section Code_Substitute_Formula.
Generalizable All Variables.
Variable L : Language.
Context `(cL : Lcode L cf cr).
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 codeFormula := codeFormula (cl := cL).
Let codeTerm := codeTerm (cl := cL).
Definition codeNewVar (l : nat) : nat :=
evalStrongRec 0
(fun n Hrecs : nat ⇒
switchPR n
(Nat.max (S (car (pred n)))
(codeNth (n - S (cdr (pred n))) Hrecs)) 0) l.
Lemma codeNewVarCorrect (l : list nat) :
codeNewVar (codeList l) = newVar l.
#[export] Instance codeNewVarIsPR : isPR 1 codeNewVar.
Definition checkSubFormulaTrace : nat → nat :=
evalStrongRec 0
(fun trace recs : nat ⇒
let v := cTriplePi1 (cTriplePi1 trace) in
let s := cTriplePi2 (cTriplePi1 trace) in
let input := cTriplePi3 (cTriplePi1 trace) in
let output := cTriplePi2 trace in
let rest := cTriplePi3 trace in
let type := cPairPi1 input in
switchPR type
(switchPR (pred type)
(switchPR (pred (pred type))
(switchPR (pred (pred (pred type)))
(charFunction 2 Nat.eqb output
(cPair type (codeSubTerms (cdr input) v s)))
(switchPR
(charFunction 2 Nat.eqb v (car (cdr input)))
(charFunction 2 Nat.eqb input output)
(switchPR
(codeIn (car (cdr input)) (codeFreeVarTerm s))
(let nv :=
codeNewVar
(S
(cPair v
(codeApp (codeFreeVarTerm s)
(codeFreeVarFormula
(cdr (cdr input)))))) in
charFunction 0
(Nat.eqb output
(cPair 3 (cPair nv (cTriplePi2 (cdr rest)))) &&
(Nat.eqb (cTriple v s (cTriplePi2 (car rest)))
(cTriplePi1 (cdr rest)) &&
Nat.eqb
(cTriple (car (cdr input))
(cPair 0 nv) (cdr (cdr input)))
(cTriplePi1 (car rest)))) ×
(codeNth (trace - S (car rest)) recs ×
codeNth (trace - S (cdr rest)) recs))
(charFunction 0
(Nat.eqb output
(cPair 3
(cPair (car (cdr input))
(cTriplePi2 rest))) &&
Nat.eqb (cTriple v s (cdr (cdr input)))
(cTriplePi1 rest)) ×
codeNth (trace - S rest) recs))))
(charFunction 0
(Nat.eqb output (cPair 2 (cTriplePi2 rest)) &&
Nat.eqb (cTriple v s (cdr input)) (cTriplePi1 rest)) ×
codeNth (trace - S rest) recs))
(charFunction 0
(Nat.eqb output
(cPair 1
(cPair (cTriplePi2 (car rest))
(cTriplePi2 (cdr rest)))) &&
(Nat.eqb (cTriple v s (car (cdr input)))
(cTriplePi1 (car rest)) &&
Nat.eqb (cTriple v s (cdr (cdr input)))
(cTriplePi1 (cdr rest)))) ×
(codeNth (trace - S (car rest)) recs ×
codeNth (trace - S (cdr rest)) recs)))
(charFunction 2 Nat.eqb output
(cPair 0
(cPair (codeSubTerm (car (cdr input)) v s)
(codeSubTerm (cdr (cdr input)) v s))))).
Definition makeTraceImp (f1 : fol.Formula L)
(f1rec : nat × fol.Term L → nat) (f2 : fol.Formula L)
(f2rec : nat × fol.Term L → nat) (p : nat × fol.Term L) : nat :=
let v := fst p in
let s := snd p in
cTriple (cTriple v (codeTerm s) (codeFormula (impH f1 f2)))
(codeFormula (substF (impH f1 f2) v s))
(cPair (f1rec p) (f2rec p)).
Definition makeTraceNot
(f : fol.Formula L) (frec : nat × fol.Term L → nat)
(p : nat × fol.Term L) : nat :=
let v := fst p in
let s := snd p in
cTriple (cTriple v (codeTerm s) (codeFormula (notH f)))
(codeFormula (substF (notH f) v s))
(frec p).
Definition makeTraceForall (n : nat) (f : fol.Formula L)
(rec : ∀ b : fol.Formula L,
lt_depth L b (forallH n f) → nat × fol.Term L → nat)
(p : nat × fol.Term L) : nat.
Definition makeTrace : fol.Formula L → nat × fol.Term L → nat :=
Formula_depth_rec2 L (fun _ : fol.Formula L ⇒ nat × fol.Term L → nat)
(fun (t t0 : fol.Term L) (p : nat × fol.Term L) ⇒
let v := fst p in
let s := snd p in
cTriple (cTriple v (codeTerm s) (codeFormula (equal t t0)))
(codeFormula (substF (equal t t0) v s)) 0)
(fun (r : Relations L) t (p : nat × fol.Term L) ⇒
let v := fst p in
let s := snd p in
cTriple (cTriple v (codeTerm s) (codeFormula (atomic r t)))
(codeFormula (substF (atomic r t) v s)) 0)
makeTraceImp
makeTraceNot makeTraceForall.
Lemma makeTraceImpNice (f2 g : fol.Formula L)
(z1 z2 : nat × fol.Term L → nat):
(∀ q : nat × fol.Term L, z1 q = z2 q) →
∀ z3 z4 : nat × fol.Term L → nat,
(∀ q : nat × fol.Term L, z3 q = z4 q) →
∀ q : nat × fol.Term L,
makeTraceImp f2 z1 g z3 q = makeTraceImp f2 z2 g z4 q.
Lemma makeTraceNotNice (f2 : fol.Formula L)
(z1 z2 : nat × fol.Term L → nat) :
(∀ q : nat × fol.Term L, z1 q = z2 q) →
∀ q : nat × fol.Term L,
makeTraceNot f2 z1 q = makeTraceNot f2 z2 q.
Lemma makeTraceForallNice
(v0 : nat) (a : fol.Formula L)
(z1 z2 : ∀ b : fol.Formula L,
lt_depth L b (forallH v0 a) → nat × fol.Term L → nat):
(∀ (b : fol.Formula L) (q : lt_depth L b (forallH v0 a))
(r : nat × fol.Term L), z1 b q r = z2 b q r) →
∀ q : nat × fol.Term L,
makeTraceForall v0 a z1 q = makeTraceForall v0 a z2 q.
Remark makeTrace1 (f : fol.Formula L) (v : nat) (s : fol.Term L):
cTriplePi1 (makeTrace f (v, s)) = cTriple v (codeTerm s) (codeFormula f).
Remark makeTrace2 (f : fol.Formula L) (v : nat) (s : fol.Term L):
cTriplePi2 (makeTrace f (v, s)) = codeFormula (substF f v s).
Lemma makeTraceCorrect :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
checkSubFormulaTrace (makeTrace f (v, s)) = 1.
Lemma checkTraceCorrect :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L) (n m : nat),
checkSubFormulaTrace (cTriple (cTriple v (codeTerm s) (codeFormula f)) n m) ≠
0 → codeFormula (substF f v s) = n.
Lemma switch5IsPR :
∀ (f1 f2 f3 f4 f5 : nat → nat → nat) (g : nat → nat),
isPR 2 f1 →
isPR 2 f2 →
isPR 2 f3 →
isPR 2 f4 →
isPR 2 f5 →
isPR 1 g →
isPR 2
(fun n recs : nat ⇒
switchPR (g n)
(switchPR (pred (g n))
(switchPR (pred (pred (g n)))
(switchPR (pred (pred (pred (g n)))) (f1 n recs) (f2 n recs))
(f3 n recs)) (f4 n recs)) (f5 n recs)).
#[export] Instance checkTraceIsPR : isPR 1 checkSubFormulaTrace.
Definition ReplaceTermTermsTerm : nat → nat → nat :=
evalStrongRec 1
(fun t recs s : nat ⇒
cPair
(switchPR (car t)
(cPair (car t) (cdr (codeNth (t - S (cdr t)) recs)))
(cPair 0 s))
(switchPR t
(S
(cPair (car (codeNth (t - S (car (pred t))) recs))
(cdr (codeNth (t - S (cdr (pred t))) recs)))) 0)).
#[local] Instance ReplaceTermTermsTermIsPR : isPR 2 ReplaceTermTermsTerm.
Definition ReplaceTermTerm (t s : nat) : nat :=
car (ReplaceTermTermsTerm t s).
Definition ReplaceTermsTerm (t s : nat) : nat :=
cdr (ReplaceTermTermsTerm t s).
#[export] Instance ReplaceTermTermIsPR : isPR 2 ReplaceTermTerm.
#[export] Instance ReplaceTermsTermIsPR : isPR 2 ReplaceTermsTerm.
Remark ReplaceTermTermsTermMonotone :
∀ a s1 s2 : nat,
s1 ≤ s2 →
ReplaceTermTerm a s1 ≤ ReplaceTermTerm a s2 ∧
ReplaceTermsTerm a s1 ≤ ReplaceTermsTerm a s2.
Lemma ReplaceTermTermMonotone :
∀ a s1 s2 : nat,
s1 ≤ s2 → ReplaceTermTerm a s1 ≤ ReplaceTermTerm a s2.
Lemma ReplaceTermsTermMonotone :
∀ a s1 s2 : nat,
s1 ≤ s2 → ReplaceTermsTerm a s1 ≤ ReplaceTermsTerm a s2.
Remark maxLemma :
∀ a b c d : nat, a ≤ b → c ≤ d → Nat.max a c ≤ Nat.max b d.
Remark maxLemma2 :
∀ a b : list nat,
fold_right Nat.max 0 a ≤ fold_right Nat.max 0 (a ++ b).
Remark maxLemma3 :
∀ a b : list nat,
fold_right Nat.max 0 b ≤ fold_right Nat.max 0 (a ++ b).
Remark maxApp :
∀ a b : list nat,
{fold_right Nat.max 0 (a ++ b) = fold_right Nat.max 0 a} +
{fold_right Nat.max 0 (a ++ b) = fold_right Nat.max 0 b}.
Lemma boundSubTerm :
∀ (t : fol.Term L) (v : nat) (s : fol.Term L),
codeTerm (substT t v s) ≤
ReplaceTermTerm (codeTerm t)
(fold_right Nat.max 0 (codeTerm s :: freeVarT t)).
Lemma boundSubTerms :
∀ (n : nat) (ts : fol.Terms L n) (v : nat) (s : fol.Term L),
codeTerms (substTs ts v s) ≤
ReplaceTermsTerm (codeTerms ts)
(fold_right Nat.max 0 (codeTerm s :: freeVarTs ts)).
Lemma ReplaceTermTermSub :
∀ (t : fol.Term L) (v w s2 : nat),
ReplaceTermTerm (codeTerm (substT t v (var w))) s2 =
ReplaceTermTerm (codeTerm t) s2.
Lemma ReplaceTermsTermSub :
∀ (n : nat) (ts : fol.Terms L n) (v w s2 : nat),
ReplaceTermsTerm (codeTerms (substTs ts v (var w))) s2 =
ReplaceTermsTerm (codeTerms ts) s2.
Definition ReplaceFormulaTerm : nat → nat → nat :=
evalStrongRec 1
(fun f recs s : nat ⇒
switchPR (car f)
(switchPR (pred (car f))
(switchPR (pred (pred (car f)))
(switchPR (pred (pred (pred (car f))))
(cPair (car f) (ReplaceTermsTerm (cdr f) s))
(cPair 3
(cPair s (codeNth (f - S (cdr (cdr f))) recs))))
(cPair 2 (codeNth (f - S (cdr f)) recs)))
(cPair 1
(cPair (codeNth (f - S (car (cdr f))) recs)
(codeNth (f - S (cdr (cdr f))) recs))))
(cPair 0
(cPair (ReplaceTermTerm (car (cdr f)) s)
(ReplaceTermTerm (cdr (cdr f)) s)))).
#[export] Instance ReplaceFormulaTermIsPR : isPR 2 ReplaceFormulaTerm.
Lemma ReplaceFormulaTermMonotone :
∀ a s1 s2 : nat,
s1 ≤ s2 → ReplaceFormulaTerm a s1 ≤ ReplaceFormulaTerm a s2.
Fixpoint varFormula (f : fol.Formula L) : list nat :=
match f with
| equal t s ⇒ freeVarT t ++ freeVarT s
| atomic r ts ⇒ freeVarTs ts
| impH A B ⇒ varFormula A ++ varFormula B
| notH A ⇒ varFormula A
| forallH v A ⇒ v :: varFormula A
end.
Lemma ReplaceFormulaTermSub :
∀ (f : fol.Formula L) (v w s2 : nat),
ReplaceFormulaTerm (codeFormula (substF f v (var w))) s2 =
ReplaceFormulaTerm (codeFormula f) s2.
Remark codeTermFreeVar :
∀ s : fol.Term L, fold_right Nat.max 0 (freeVarT s) ≤ codeTerm s.
Remark maxVarFreeVar :
∀ f : fol.Formula L,
fold_right Nat.max 0 (freeVarF f) ≤
fold_right Nat.max 0 (varFormula f).
Remark maxSubTerm (t : fol.Term L) (v : nat) (s : fol.Term L):
fold_right Nat.max 0 (freeVarT (substT t v s)) ≤
fold_right Nat.max 0 (freeVarT s ++ freeVarT t).
Remark maxSubTerms (n : nat) (ts : fol.Terms L n) (v : nat) (s : fol.Term L):
fold_right Nat.max 0 (freeVarTs (substTs ts v s)) ≤
fold_right Nat.max 0 (freeVarT s ++ freeVarTs ts).
3 ^ n
Definition pow3 : nat → nat :=
nat_rec (fun _ ⇒ nat) 1 (fun _ rec : nat ⇒ rec + (rec + rec)).
#[export] Instance pow3IsPR : isPR 1 pow3.
Lemma pow3Monotone : ∀ a b : nat, a ≤ b → pow3 a ≤ pow3 b.
Lemma pow3Min : ∀ a : nat, 1 ≤ pow3 a.
Remark mapListLemma :
∀ l : list nat,
fold_right Nat.max 0 (map S l) ≤ S (fold_right Nat.max 0 l).
Remark boundSubFormulaHelp2 (a : fol.Formula L) (v0 : nat) (s : fol.Term L):
newVar (v0 :: freeVarT s ++ freeVarF a) ≤
S
(fold_right Nat.max 0
(v0 :: fold_right Nat.max 0 (freeVarT s) :: varFormula a)).
Remark boundSubFormulaHelp1 :
∀ (b a : fol.Formula L) (v0 v : nat) (s : fol.Term L),
fold_right Nat.max 0
(varFormula
(substF b v
(var (newVar (v0 :: freeVarT s ++ freeVarF a))))) ≤
pow3 (depth L b) + pow3 (depth L b) +
Nat.max v0
(Nat.max (fold_right Nat.max 0 (freeVarT s))
(Nat.max v
(Nat.max (fold_right Nat.max 0 (varFormula b))
(fold_right Nat.max 0 (varFormula a))))).
Remark boundSubFormulaHelp :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
codeFormula (substF f v s) ≤
ReplaceFormulaTerm (codeFormula f)
(Nat.max (codeTerm s)
(pow3 (depth L f) +
fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))).
Definition boundComputation (d p1 p2 : nat) : nat :=
nat_rec (fun _ ⇒ nat) (cTriple p1 p2 0)
(fun _ rec : nat ⇒ cTriple p1 p2 (cPair rec rec)) d.
#[export] Instance boundComputationIsPR : isPR 3 boundComputation.
Lemma boundComputationMonotone :
∀ a1 a2 b1 b2 c1 c2 : nat,
a1 ≤ a2 →
b1 ≤ b2 →
c1 ≤ c2 → boundComputation a1 b1 c1 ≤ boundComputation a2 b2 c2.
Lemma boundMakeTrace :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
let C :=
Nat.max (codeTerm s)
(cPair 0
(pow3 (depth L f) +
fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))) in
makeTrace f (v, s) ≤
boundComputation (depth L f)
(cTriple C C (ReplaceFormulaTerm (codeFormula f) C))
(ReplaceFormulaTerm (codeFormula f) C).
Definition codeSubFormula (f v s : nat) : nat :=
let C := cPair 0 (pow3 f + (v + (s + f))) in
car
(boundedSearch
(fun p x : nat ⇒
ltBool 0 (checkSubFormulaTrace (cPair (car p) x)))
(cPair (cTriple v s f)
(S
(boundComputation f (cTriple C C (ReplaceFormulaTerm f C))
(ReplaceFormulaTerm f C))))).
Lemma codeSubFormulaCorrect (f : Formula) (v : nat) (s : Term):
codeSubFormula (codeFormula f) v (codeTerm s) =
codeFormula (substF f v s).
#[export] Instance codeSubFormulaIsPR : isPR 3 codeSubFormula.
End Code_Substitute_Formula.
nat_rec (fun _ ⇒ nat) 1 (fun _ rec : nat ⇒ rec + (rec + rec)).
#[export] Instance pow3IsPR : isPR 1 pow3.
Lemma pow3Monotone : ∀ a b : nat, a ≤ b → pow3 a ≤ pow3 b.
Lemma pow3Min : ∀ a : nat, 1 ≤ pow3 a.
Remark mapListLemma :
∀ l : list nat,
fold_right Nat.max 0 (map S l) ≤ S (fold_right Nat.max 0 l).
Remark boundSubFormulaHelp2 (a : fol.Formula L) (v0 : nat) (s : fol.Term L):
newVar (v0 :: freeVarT s ++ freeVarF a) ≤
S
(fold_right Nat.max 0
(v0 :: fold_right Nat.max 0 (freeVarT s) :: varFormula a)).
Remark boundSubFormulaHelp1 :
∀ (b a : fol.Formula L) (v0 v : nat) (s : fol.Term L),
fold_right Nat.max 0
(varFormula
(substF b v
(var (newVar (v0 :: freeVarT s ++ freeVarF a))))) ≤
pow3 (depth L b) + pow3 (depth L b) +
Nat.max v0
(Nat.max (fold_right Nat.max 0 (freeVarT s))
(Nat.max v
(Nat.max (fold_right Nat.max 0 (varFormula b))
(fold_right Nat.max 0 (varFormula a))))).
Remark boundSubFormulaHelp :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
codeFormula (substF f v s) ≤
ReplaceFormulaTerm (codeFormula f)
(Nat.max (codeTerm s)
(pow3 (depth L f) +
fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))).
Definition boundComputation (d p1 p2 : nat) : nat :=
nat_rec (fun _ ⇒ nat) (cTriple p1 p2 0)
(fun _ rec : nat ⇒ cTriple p1 p2 (cPair rec rec)) d.
#[export] Instance boundComputationIsPR : isPR 3 boundComputation.
Lemma boundComputationMonotone :
∀ a1 a2 b1 b2 c1 c2 : nat,
a1 ≤ a2 →
b1 ≤ b2 →
c1 ≤ c2 → boundComputation a1 b1 c1 ≤ boundComputation a2 b2 c2.
Lemma boundMakeTrace :
∀ (f : fol.Formula L) (v : nat) (s : fol.Term L),
let C :=
Nat.max (codeTerm s)
(cPair 0
(pow3 (depth L f) +
fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))) in
makeTrace f (v, s) ≤
boundComputation (depth L f)
(cTriple C C (ReplaceFormulaTerm (codeFormula f) C))
(ReplaceFormulaTerm (codeFormula f) C).
Definition codeSubFormula (f v s : nat) : nat :=
let C := cPair 0 (pow3 f + (v + (s + f))) in
car
(boundedSearch
(fun p x : nat ⇒
ltBool 0 (checkSubFormulaTrace (cPair (car p) x)))
(cPair (cTriple v s f)
(S
(boundComputation f (cTriple C C (ReplaceFormulaTerm f C))
(ReplaceFormulaTerm f C))))).
Lemma codeSubFormulaCorrect (f : Formula) (v : nat) (s : Term):
codeSubFormula (codeFormula f) v (codeTerm s) =
codeFormula (substF f v s).
#[export] Instance codeSubFormulaIsPR : isPR 3 codeSubFormula.
End Code_Substitute_Formula.