Step
*
1
1
of Lemma
term-accum-induction
.....wf.....
1. opr : Type
2. P : Type
3. R : P ⟶ term(opr) ⟶ ℙ
4. Q : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P
5. ∀p:P. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . R[p;varterm(v)]
6. ∀p:P. ∀f:opr. ∀bts:bound-term(opr) List. ∀L:{L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))} \000C.
R[p;mkterm(f;bts)]
7. n : ℕ
8. ∀[m:ℕn]. ∀a:{a:term(opr)| term-size(a) ≤ m} . ∀p:P. R[p;a]
9. term(opr) ≡ coterm-fun(opr;term(opr))
10. f : opr
11. bts : (varname() List × term(opr)) List
12. inr <f, bts> ∈ term(opr)
13. (1 + Σ(term-size(snd(bt)) | bt ∈ bts)) ≤ n
14. p : P
15. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ bts))
16. g : ∀bt:{bt:varname() List × term(opr)| (bt ∈ bts)} . ∀p:P. R[p;snd(bt)]
⊢ accumulate (with value L and list item bt):
let p' = Q[p;f;fst(bt);L] in
L @ [<snd(bt), p', g bt p'>]
over list:
bts
with starting value:
[]) ∈ {L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))}
BY
{ ((Enough to prove ∀X:(varname() List × term(opr)) List. ∀LL:{L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||X|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(X[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||
((fst(snd(L[i])))
= Q[p;f;fst(X[i]);firstn(i;L)]
∈ P))} .
(accumulate (with value L and list item bt):
let p' = Q[p;f;fst(bt);L] in
L @ [<snd(bt), p', g bt p'>]
over list:
bts
with starting value:
LL) ∈ {L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||X @ bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(X @ bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(X @ bts[i]);firstn(i;L)] ∈ P))} )
Because (RepeatFor 2 ((D -1 With ⌜[]⌝ THENA Auto)) THEN Reduce -1 THEN Trivial))
THEN MoveToConcl (-1)
THEN All Thin
THEN ListInd (-2)
THEN Reduce 0
THEN Intros
THEN (Subst' X @ [] ~ X 0 THENA Auto)
THEN Try (Trivial)
THEN (D -4 With ⌜g⌝ THENA Auto)
THEN (Subst' X @ [u / v] ~ (X @ [u]) @ v 0 THENA ((RWO "append_assoc" 0 THENA Auto) THEN Reduce 0 THEN Auto))
THEN (BHyp -1 THENL [Auto; (Thin (-1) THEN D -1 THEN (MemTypeCD THENW Auto))])
THEN ((RepUR ``let`` 0 THEN ((RWO "length-append" 0 THENM Reduce 0) THENA Auto) THEN ParallelLast) ORELSE Auto)
THEN ParallelLast
THEN ((D 0 THENA Auto) THEN (RWO "select-append" 0 THENA Auto))
THEN RevHypSubst' (-4) 0
THEN AutoSplit
THEN (Subst' i - ||LL|| ~ 0 0 THENA Auto)
THEN Reduce 0
THEN Auto) }
1
1. opr : Type
2. P : Type
3. R : P ⟶ term(opr) ⟶ ℙ
4. Q : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P
5. f : opr
6. p : P
7. u : varname() List × term(opr)
8. v : (varname() List × term(opr)) List
9. g : ∀bt:{bt:varname() List × term(opr)| (bt ∈ [u / v])} . ∀p:P. R[p;snd(bt)]
10. X : (varname() List × term(opr)) List
11. LL : (t:term(opr) × p:P × R[p;t]) List
12. ||LL|| = ||X|| ∈ ℤ
13. ∀i:ℕ||LL||. ((fst(LL[i])) = (snd(X[i])) ∈ term(opr))
14. ∀i:ℕ||LL||. ((fst(snd(LL[i]))) = Q[p;f;fst(X[i]);firstn(i;LL)] ∈ P)
15. i : ℕ||LL|| + 1
16. ¬i < ||LL||
⊢ Q[p;f;fst(u);LL] = Q[p;f;fst(u);firstn(i;LL @ [<snd(u), Q[p;f;fst(u);LL], g u Q[p;f;fst(u);LL]>])] ∈ P
Latex:
Latex:
.....wf.....
1. opr : Type
2. P : Type
3. R : P {}\mrightarrow{} term(opr) {}\mrightarrow{} \mBbbP{}
4. Q : P {}\mrightarrow{} opr {}\mrightarrow{} (varname() List) {}\mrightarrow{} ((t:term(opr) \mtimes{} p:P \mtimes{} R[p;t]) List) {}\mrightarrow{} P
5. \mforall{}p:P. \mforall{}v:\{v:varname()| \mneg{}(v = nullvar())\} . R[p;varterm(v)]
6. \mforall{}p:P. \mforall{}f:opr. \mforall{}bts:bound-term(opr) List. \mforall{}L:\{L:(t:term(opr) \mtimes{} p:P \mtimes{} R[p;t]) List|
(||L|| = ||bts||)
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((fst(L[i])) = (snd(bts[i]))))
\mwedge{} (\mforall{}i:\mBbbN{}||L||
((fst(snd(L[i])))
= Q[p;f;fst(bts[i]);firstn(i;L)]))\} .
R[p;mkterm(f;bts)]
7. n : \mBbbN{}
8. \mforall{}[m:\mBbbN{}n]. \mforall{}a:\{a:term(opr)| term-size(a) \mleq{} m\} . \mforall{}p:P. R[p;a]
9. term(opr) \mequiv{} coterm-fun(opr;term(opr))
10. f : opr
11. bts : (varname() List \mtimes{} term(opr)) List
12. inr <f, bts> \mmember{} term(opr)
13. (1 + \mSigma{}(term-size(snd(bt)) | bt \mmember{} bts)) \mleq{} n
14. p : P
15. 1 \mleq{} (1 + \mSigma{}(term-size(snd(bt)) | bt \mmember{} bts))
16. g : \mforall{}bt:\{bt:varname() List \mtimes{} term(opr)| (bt \mmember{} bts)\} . \mforall{}p:P. R[p;snd(bt)]
\mvdash{} accumulate (with value L and list item bt):
let p' = Q[p;f;fst(bt);L] in
L @ [<snd(bt), p', g bt p'>]
over list:
bts
with starting value:
[]) \mmember{} \{L:(t:term(opr) \mtimes{} p:P \mtimes{} R[p;t]) List|
(||L|| = ||bts||)
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((fst(L[i])) = (snd(bts[i]))))
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)]))\}
By
Latex:
((Enough to prove \mforall{}X:(varname() List \mtimes{} term(opr)) List. \mforall{}LL:\{L:(t:term(opr) \mtimes{} p:P \mtimes{} R[p;t]) List|
(||L|| = ||X||)
\mwedge{} (\mforall{}i:\mBbbN{}||L||
((fst(L[i])) = (snd(X[i]))))
\mwedge{} (\mforall{}i:\mBbbN{}||L||
((fst(snd(L[i])))
= Q[p;f;fst(X[i]);firstn(i;L)]))\} \000C.
(accumulate (with value L and list item bt):
let p' = Q[p;f;fst(bt);L] in
L @ [<snd(bt), p', g bt p'>]
over list:
bts
with starting value:
LL) \mmember{} \{L:(t:term(opr) \mtimes{} p:P \mtimes{} R[p;t]) List|
(||L|| = ||X @ bts||)
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((fst(L[i])) = (snd(X @ bts[i]))))
\mwedge{} (\mforall{}i:\mBbbN{}||L||
((fst(snd(L[i]))) = Q[p;f;fst(X @ bts[i]);firstn(i;L)]))\} )
Because (RepeatFor 2 ((D -1 With \mkleeneopen{}[]\mkleeneclose{} THENA Auto)) THEN Reduce -1 THEN Trivial))
THEN MoveToConcl (-1)
THEN All Thin
THEN ListInd (-2)
THEN Reduce 0
THEN Intros
THEN (Subst' X @ [] \msim{} X 0 THENA Auto)
THEN Try (Trivial)
THEN (D -4 With \mkleeneopen{}g\mkleeneclose{} THENA Auto)
THEN (Subst' X @ [u / v] \msim{} (X @ [u]) @ v 0
THENA ((RWO "append\_assoc" 0 THENA Auto) THEN Reduce 0 THEN Auto)
)
THEN (BHyp -1 THENL [Auto; (Thin (-1) THEN D -1 THEN (MemTypeCD THENW Auto))])
THEN ((RepUR ``let`` 0 THEN ((RWO "length-append" 0 THENM Reduce 0) THENA Auto) THEN ParallelLast)
ORELSE Auto
)
THEN ParallelLast
THEN ((D 0 THENA Auto) THEN (RWO "select-append" 0 THENA Auto))
THEN RevHypSubst' (-4) 0
THEN AutoSplit
THEN (Subst' i - ||LL|| \msim{} 0 0 THENA Auto)
THEN Reduce 0
THEN Auto)
Home
Index