Definition: simple-game
SimpleGame == Pos:Type × Pos × Pos ⟶ Pos ⟶ ℙ × (Pos ⟶ Pos ⟶ ℙ)
Lemma: simple-game_wf
SimpleGame ∈ 𝕌'
Definition: sg-pos
Pos(g) == fst(g)
Lemma: sg-pos_wf
∀[g:SimpleGame]. (Pos(g) ∈ Type)
Definition: sg-init
InitialPos(g) == fst(snd(g))
Lemma: sg-init_wf
∀[g:SimpleGame]. (InitialPos(g) ∈ Pos(g))
Definition: sg-legal1
Legal1(x;y) == (fst(snd(snd(g)))) x y
Lemma: sg-legal1_wf
∀[g:SimpleGame]. ∀[x,y:Pos(g)]. (Legal1(x;y) ∈ ℙ)
Definition: sg-legal2
Legal2(x;y) == (snd(snd(snd(g)))) x y
Lemma: sg-legal2_wf
∀[g:SimpleGame]. ∀[x,y:Pos(g)]. (Legal2(x;y) ∈ ℙ)
Definition: play-item
moves[i] == moves[i]
Definition: play-len
||moves|| == ||moves||
Definition: play-truncate
play-truncate(f;m) == seq-truncate(f;m)
Definition: win2strat
A strategy that allows player two to respond to n plays by player one.
Anything is such a strategy for n=0.
For 0 < n, the strategy must also work for n-1, and for any play of the
game of length 2*n that has followed that strategy, the strategy
gives a legal move for player two that extends that play.⋅
win2strat(g;n) ==
if (n =z 0)
then Top
else s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)}
fi
Definition: strat2play
A play of game g of length at least 2*n that follows strategy s
on the first n moves by player two.⋅
strat2play(g;n;s) ==
if (n =z 0)
then {moves:sequence(Pos(g))| (2 ≤ ||moves||) ∧ (moves[0] = InitialPos(g) ∈ Pos(g)) ∧ Legal1(moves[0];moves[1])}
else f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}
fi
Lemma: win2strat-strat2play-wf
∀[g:SimpleGame]. ∀[n:ℕ].
((win2strat(g;n) ∈ Type)
∧ (∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type))
∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. (||f|| ∈ ℤ))
∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
(play-truncate(f;k) ∈ strat2play(g;n;s))))
Lemma: win2strat_wf
∀[g:SimpleGame]. ∀[n:ℕ]. (win2strat(g;n) ∈ Type)
Lemma: strat2play_wf
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
Lemma: play-len_wf
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. (||f|| ∈ ℤ)
Lemma: win2strat-properties
∀g:SimpleGame. ∀n:ℕ+. ∀s:win2strat(g;n).
((s ∈ win2strat(g;n - 1))
∧ (s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} ))
Lemma: win2strat_subtype
∀[g:SimpleGame]. ∀[n,m:ℕ]. win2strat(g;n) ⊆r win2strat(g;m) supposing m ≤ n
Lemma: strat2play_subtype
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)].
(strat2play(g;n;s) ⊆r {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} )
Lemma: strat2play_subtype_le
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[j:ℕn + 1]. (strat2play(g;n;s) ⊆r strat2play(g;j;s))
Lemma: play-truncate_wf
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
(play-truncate(f;k) ∈ {moves:strat2play(g;n;s)| ||moves|| = k ∈ ℤ} )
Lemma: play-truncate-trivial
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:ℤ].
play-truncate(f;k) ~ f supposing k = ||f|| ∈ ℤ
Lemma: play-item_wf
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[i:ℕ(2 * n) + 2]. (moves[i] ∈ Pos(g))
Lemma: strat2play-invariant-1
∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s).
((moves[0] = InitialPos(g) ∈ Pos(g))
∧ (∀i:ℕn + 1
((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
∧ (i < n
⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g)))))))
Lemma: truncate-strat2play
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[j:ℕ].
play-truncate(moves;2 * (j + 1)) ∈ strat2play(g;j;s) supposing j < n
Lemma: strat2play-invariant-type
∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s).
(∀i:ℕn + 1
((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
∧ (i < n
⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g))))) ∈ ℙ)
Lemma: strat2play-invariant
∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s). ∀i:ℕ(2 * n) + 1.
((((i mod 2) = 0 ∈ ℤ) ⇒ (↓Legal1(moves[i];moves[i + 1])))
∧ (((i mod 2) = 1 ∈ ℤ) ⇒ (↓Legal2(moves[i];moves[i + 1]))))
Lemma: strat2play-longer
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[x:sequence(Pos(g))].
((x ∈ strat2play(g;n;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n;s))) supposing
((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and
(||moves|| ≤ ||x||))
Lemma: strat2play-add1
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[x:Pos(g)].
(seq-add(moves;x) ∈ strat2play(g;n;s))
Lemma: strat2play-add
∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n + 1)]. ∀[moves:strat2play(g;n;s)].
∀[x,y:Pos(g)].
(seq-add(seq-add(moves;x);y) ∈ strat2play(g;n + 1;s)) supposing ((x = (s moves) ∈ Pos(g)) and Legal1(x;y))
supposing ||moves|| = ((2 * n) + 2) ∈ ℤ
Definition: win2
A winning strategy for player two in game g is a (very dependent) function
that uniformly for all n, allows player two to respond to n moves
by player one.⋅
win2(g) == ∀[n:ℕ]. win2strat(g;n)
Lemma: win2_wf
∀[g:SimpleGame]. (win2(g) ∈ ℙ)
Definition: sg-reachable
sg-reachable(g;x;y) ==
∃f:sequence(Pos(g))
(0 < ||f||
∧ (f[0] = x ∈ Pos(g))
∧ (f[||f|| - 1] = y ∈ Pos(g))
∧ (∀i:ℕ. ((2 * i) + 1 < ||f|| ⇒ (↓Legal1(f[2 * i];f[(2 * i) + 1]))))
∧ (∀i:ℕ+. (2 * i < ||f|| ⇒ (↓Legal2(f[(2 * i) - 1];f[2 * i])))))
Lemma: sg-reachable_wf
∀[g:SimpleGame]. ∀[x,y:Pos(g)]. (sg-reachable(g;x;y) ∈ ℙ)
Lemma: sg-reachable_self
∀[g:SimpleGame]. ∀x:Pos(g). sg-reachable(g;x;x)
Lemma: play-item-reachable
∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s). ∀i:ℕ(2 * n) + 2.
(moves[i] ∈ {p:Pos(g)| sg-reachable(g;InitialPos(g);p)} )
Lemma: strat2play-reachable
∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s).
((||moves|| ≤ ((2 * n) + 2)) ⇒ (moves ∈ sequence({p:Pos(g)| sg-reachable(g;InitialPos(g);p)} )))
Definition: isom-games
g1 ≅ g2 ==
∃f:Pos(g1) ⟶ Pos(g2)
∃g:Pos(g2) ⟶ Pos(g1)
((∀x,y:Pos(g1). (Legal1(x;y) ⇒ Legal1(f x;f y)))
∧ (∀x,y:Pos(g1). (Legal2(x;y) ⇒ Legal2(f x;f y)))
∧ (∀x,y:Pos(g2). (Legal1(x;y) ⇒ Legal1(g x;g y)))
∧ (∀x,y:Pos(g2). (Legal2(x;y) ⇒ Legal2(g x;g y)))
∧ (∀x:Pos(g2). ((f (g x)) = x ∈ Pos(g2)))
∧ (∀x:Pos(g1). ((g (f x)) = x ∈ Pos(g1)))
∧ ((f InitialPos(g1)) = InitialPos(g2) ∈ Pos(g2))
∧ ((g InitialPos(g2)) = InitialPos(g1) ∈ Pos(g1)))
Lemma: isom-games_wf
∀[g1,g2:SimpleGame]. (g1 ≅ g2 ∈ ℙ)
Lemma: isom-games_inversion
∀[g1,g2:SimpleGame]. (g1 ≅ g2 ⇒ g2 ≅ g1)
Lemma: isom-preserves-win2
∀g1,g2:SimpleGame. (g1 ≅ g2 ⇒ win2(g1) ⇒ win2(g2))
Lemma: isom-win2
∀g1,g2:SimpleGame. (g1 ≅ g2 ⇒ {win2(g1) ⇐⇒ win2(g2)})
Definition: goodAux
goodAux(g0;G;moves) ==
if (||moves|| =z 2)
then g0
else let g = goodAux(g0;G;play-truncate(moves;||moves|| - 2)) in
G moves[||moves|| - 4] moves[||moves|| - 3] g
fi
Lemma: good-sg-win2
∀g:SimpleGame
((∃Good:Pos(g) ⟶ ℙ'
(Good[InitialPos(g)] ∧ (∀p:Pos(g). ∀q:{q:Pos(g)| Legal1(p;q)} . ∀gd:Good[p]. ∃r:{r:Pos(g)| Legal2(q;r)} . Good[r])\000C))
⇒ win2(g))
Lemma: implies-sg-win2
∀g:SimpleGame
((∃Good:Pos(g) ⟶ ℙ'
∃F:p:{p:Pos(g)| Good[p]} ⟶ q:{q:Pos(g)| Legal1(p;q)} ⟶ Pos(g)
(Good[InitialPos(g)] ∧ (∀p:{p:Pos(g)| Good[p]} . ∀q:{q:Pos(g)| Legal1(p;q)} . (Good[F[p;q]] ∧ Legal2(q;F[p;q]))))\000C)
⇒ win2(g))
Definition: sg-change-init
g@j == let p,i,l1,l2 = g in <{y:p| sg-reachable(g;j;y)} , j, l1, l2>
Lemma: sg-change-init_wf
∀[g:SimpleGame]. ∀[j:Pos(g)]. (g@j ∈ SimpleGame)
Definition: sg-normalize
sg-normalize(g) == g@InitialPos(g)
Lemma: sg-normalize_wf
∀[g:SimpleGame]. (sg-normalize(g) ∈ SimpleGame)
Lemma: sg-pos-change-init
∀[g:SimpleGame]. ∀[j:Top]. (Pos(g@j) ~ {p:Pos(g)| sg-reachable(g;j;p)} )
Lemma: sg-pos-normalize
∀[g:SimpleGame]. (Pos(sg-normalize(g)) ~ {p:Pos(g)| sg-reachable(g;InitialPos(g);p)} )
Lemma: sg-legal1-change-init
∀[g:SimpleGame]. ∀[x,y,j:Top]. (Legal1(x;y) ~ Legal1(x;y))
Lemma: sg-legal1-normalize
∀[g:SimpleGame]. ∀[x,y:Top]. (Legal1(x;y) ~ Legal1(x;y))
Lemma: sg-legal2-change-init
∀[g:SimpleGame]. ∀[x,y,j:Top]. (Legal2(x;y) ~ Legal2(x;y))
Lemma: sg-legal2-normalize
∀[g:SimpleGame]. ∀[x,y:Top]. (Legal2(x;y) ~ Legal2(x;y))
Lemma: sg-init-change-init
∀[g:SimpleGame]. ∀[j:Top]. (InitialPos(g@j) ~ j)
Lemma: sg-init-normalize
∀[g:SimpleGame]. (InitialPos(sg-normalize(g)) ~ InitialPos(g))
Lemma: sg-normalize-win2
∀[g:SimpleGame]. win2(g) ≡ win2(sg-normalize(g))
Lemma: respond-implies-win2
∀g:SimpleGame. ((∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∃q:{q:Pos(g)| Legal2(p;q)} . win2(g@q)) ⇒ win2(g))
Lemma: win2-iff
∀g:SimpleGame. (win2(g) ⇐⇒ ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∃q:{q:Pos(g)| Legal2(p;q)} . win2(g@q))
Definition: coW
coW(A;a.B[a]) == pco-W ⋅
Lemma: coW_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (coW(A;a.B[a]) ∈ Type)
Lemma: W-subtype-coW
∀[A:𝕌']. ∀[B:A ⟶ Type]. (W(A;a.B[a]) ⊆r coW(A;a.B[a]))
Lemma: coW-ext
∀[A:Type]. ∀[B:A ⟶ Type]. coW(A;a.B[a]) ≡ a:A × (B[a] ⟶ coW(A;a.B[a]))
Lemma: coW-subtype1
∀[A:Type]. ∀[B:A ⟶ Type]. ((a:A × (B[a] ⟶ coW(A;a.B[a]))) ⊆r coW(A;a.B[a]))
Lemma: coW-corec
∀[A:𝕌']. ∀[B:A ⟶ Type]. coW(A;a.B[a]) ≡ corec(C.a:A × (B[a] ⟶ C))
Lemma: fix_wf_coW
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[G:⋂W:𝕌'. (W ⟶ (a:A × (B[a] ⟶ W)))]. (fix(G) ∈ coW(A;a.B[a]))
Lemma: fix_wf_coW_parameter
∀[P:Type]. ∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[G:⋂W:𝕌'. ((P ⟶ W) ⟶ P ⟶ (a:A × (B[a] ⟶ W)))]. ∀[p:P].
(fix(G) p ∈ coW(A;a.B[a]))
Definition: coW-dom
coW-dom(a.B[a];w) == B[fst(w)]
Lemma: coW-dom_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. (coW-dom(a.B[a];w) ∈ Type)
Definition: coW-item
coW-item(w;b) == (snd(w)) b
Lemma: coW-item_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[b:coW-dom(a.B[a];w)]. (coW-item(w;b) ∈ coW(A;a.B[a]))
Definition: coWsup
coWsup(a;f) == <a, f>
Lemma: coWsup_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[f:B[a] ⟶ coW(A;a.B[a])]. (coWsup(a;f) ∈ coW(A;a.B[a]))
Definition: coPath
coPath(a.B[a];w;n) == if (n =z 0) then Top else t:coW-dom(a.B[a];w) × coPath(a.B[a];coW-item(w;t);n - 1) fi
Lemma: coPath_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. (coPath(a.B[a];w;n) ∈ Type)
Lemma: coPath_subtype
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. ∀[m:ℕ]. coPath(a.B[a];w;m) ⊆r coPath(a.B[a];w;n) supposing n ≤ m
Definition: coPathAgree
coPathAgree(a.B[a];n;w;p;q) ==
if (n =z 0)
then True
else let t,p' = p
in let t',q' = q
in (t = t' ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n - 1;coW-item(w;t);p';q')
fi
Lemma: coPathAgree_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. ∀[p,q:coPath(a.B[a];w;n)]. (coPathAgree(a.B[a];n;w;p;q) ∈ ℙ)
Lemma: coPathAgree0_lemma
∀q,p,w,B:Top. (coPathAgree(a.B[a];0;w;p;q) ~ True)
Lemma: coPathAgree_refl
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀n:ℕ. ∀[w:coW(A;a.B[a])]. ∀p:coPath(a.B[a];w;n). coPathAgree(a.B[a];n;w;p;p)
Lemma: sq_stable__coPathAgree
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀n:ℕ. ∀[w:coW(A;a.B[a])]. ∀p,q:coPath(a.B[a];w;n). SqStable(coPathAgree(a.B[a];n;w;p;q))
Lemma: coPathAgree_le
∀[A:𝕌']. ∀[B:A ⟶ Type].
∀n:ℕ
∀[w:coW(A;a.B[a])]
∀p,q:coPath(a.B[a];w;n). (coPathAgree(a.B[a];n;w;p;q) ⇒ (∀m:ℕ. ((m ≤ n) ⇒ coPathAgree(a.B[a];m;w;p;q))))
Lemma: coPathAgree_transitivity
∀[A:𝕌']. ∀[B:A ⟶ Type].
∀n:ℕ
∀[w:coW(A;a.B[a])]
∀p,q,r:coPath(a.B[a];w;n).
(coPathAgree(a.B[a];n;w;p;q) ⇒ coPathAgree(a.B[a];n;w;q;r) ⇒ coPathAgree(a.B[a];n;w;p;r))
Definition: coPath-at
coPath-at(n;w;p) == if (n =z 0) then w else let t,q = p in coPath-at(n - 1;coW-item(w;t);q) fi
Lemma: coPath-at_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. ∀[p:coPath(a.B[a];w;n)]. (coPath-at(n;w;p) ∈ coW(A;a.B[a]))
Definition: coPath-extend
coPath-extend(n;p;t) == if (n =z 0) then <t, ⋅> else let x,y = p in <x, coPath-extend(n - 1;y;t)> fi
Lemma: coPath-extend_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. ∀[p:coPath(a.B[a];w;n)]. ∀[t:coW-dom(a.B[a];coPath-at(n;w;p))].
(coPath-extend(n;p;t) ∈ coPath(a.B[a];w;n + 1))
Definition: copath
copath(a.B[a];w) == n:ℕ × coPath(a.B[a];w;n)
Lemma: copath_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. (copath(a.B[a];w) ∈ Type)
Definition: copath-at
copath-at(w;p) == let n,q = p in coPath-at(n;w;q)
Lemma: copath-at_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. (copath-at(w;p) ∈ coW(A;a.B[a]))
Lemma: copath-at-W
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:W(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. (copath-at(w;p) ∈ W(A;a.B[a]))
Definition: copath-extend
copath-extend(q;t) == let n,p = q in <n + 1, coPath-extend(n;p;t)>
Lemma: copath-extend_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. ∀[t:coW-dom(a.B[a];copath-at(w;p))].
(copath-extend(p;t) ∈ copath(a.B[a];w))
Lemma: copath-at-extend
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. ∀[t:Top].
(copath-at(w;copath-extend(p;t)) ~ coW-item(copath-at(w;p);t))
Definition: copath-length
copath-length(p) == fst(p)
Lemma: copath-length_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. (copath-length(p) ∈ ℕ)
Definition: copath-nil
() == <0, ⋅>
Lemma: copath-nil_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. (() ∈ copath(a.B[a];w))
Lemma: copath_length_nil_lemma
copath-length(()) ~ 0
Definition: copath-hd
copath-hd(p) == fst(snd(p))
Lemma: copath-hd_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
copath-hd(p) ∈ coW-dom(a.B[a];w) supposing 0 < copath-length(p)
Definition: copath-tl
copath-tl(x) == let n,p = x in <n - 1, snd(p)>
Lemma: copath-tl_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
copath-tl(p) ∈ copath(a.B[a];coW-item(w;copath-hd(p))) supposing 0 < copath-length(p)
Definition: copath-cons
copath-cons(b;x) == let n,p = x in <n + 1, b, p>
Lemma: copath-cons_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[b:coW-dom(a.B[a];w)]. ∀[p:copath(a.B[a];coW-item(w;b))].
(copath-cons(b;p) ∈ copath(a.B[a];w))
Lemma: copath-hd-cons
∀[b:Top]. ∀[p:Top × Top]. (copath-hd(copath-cons(b;p)) ~ b)
Lemma: copath-tl-cons
∀[b:Top]. ∀[p:ℕ × Top]. (copath-tl(copath-cons(b;p)) ~ p)
Lemma: copath-cons-hd-tl
∀[p:ℕ × Top × Top]. (copath-cons(copath-hd(p);copath-tl(p)) ~ p)
Lemma: length-copath-extend
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. ∀[t:Top].
(copath-length(copath-extend(p;t)) = (copath-length(p) + 1) ∈ ℤ)
Lemma: copath-eta
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
(0 < copath-length(p) ⇒ (copath-cons(copath-hd(p);copath-tl(p)) = p ∈ copath(a.B[a];w)))
Lemma: copath-eta2
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. ∀[q:coW-dom(a.B[a];w)].
(0 < copath-length(p)
⇒ (q = copath-hd(p) ∈ coW-dom(a.B[a];w))
⇒ (copath-cons(q;copath-tl(p)) = p ∈ copath(a.B[a];w)))
Lemma: length-copath-cons
∀[b:Top]. ∀[p:Top × Top]. (copath-length(copath-cons(b;p)) ~ copath-length(p) + 1)
Lemma: length-copath-tl
∀[p:Top × Top]. (copath-length(copath-tl(p)) ~ copath-length(p) - 1)
Definition: copath-last
copath-last(w;p) ==
if (copath-length(p) =z 1) then <w, copath-hd(p)> else copath-last(coW-item(w;copath-hd(p));copath-tl(p)) fi
Lemma: copath-last_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
copath-last(w;p) ∈ w':coW(A;a.B[a]) × coW-dom(a.B[a];w') supposing 0 < copath-length(p)
Definition: copathAgree
copathAgree(a.B[a];w;x;y) ==
let n,p = x
in let m,q = y
in if (n) < (m) then coPathAgree(a.B[a];n;w;p;q) else coPathAgree(a.B[a];m;w;p;q)
Lemma: copathAgree_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[x,y:copath(a.B[a];w)]. (copathAgree(a.B[a];w;x;y) ∈ ℙ)
Lemma: copathAgree_refl
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀x:copath(a.B[a];w). copathAgree(a.B[a];w;x;x)
Lemma: copathAgree_transitivity
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].
∀x,y,z:copath(a.B[a];w).
((copath-length(x) ≤ copath-length(y))
⇒ (copath-length(y) ≤ copath-length(z))
⇒ copathAgree(a.B[a];w;x;y)
⇒ copathAgree(a.B[a];w;y;z)
⇒ copathAgree(a.B[a];w;x;z))
Lemma: sq_stable__copathAgree
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀x,y:copath(a.B[a];w). SqStable(copathAgree(a.B[a];w;x;y))
Lemma: hd-copathAgree
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[x,y:copath(a.B[a];w)].
(copath-hd(x) = copath-hd(y) ∈ coW-dom(a.B[a];w)) supposing
(0 < copath-length(y) and
0 < copath-length(x) and
copathAgree(a.B[a];w;x;y))
Lemma: copathAgree-cons
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[b:coW-dom(a.B[a];w)].
∀p,q:copath(a.B[a];coW-item(w;b)).
(copathAgree(a.B[a];coW-item(w;b);p;q) ⇒ copathAgree(a.B[a];w;copath-cons(b;p);copath-cons(b;q)))
Lemma: copathAgree-tl
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].
∀p,q:copath(a.B[a];w).
(copathAgree(a.B[a];w;p;q)
⇒ 0 < copath-length(p)
⇒ 0 < copath-length(q)
⇒ copathAgree(a.B[a];coW-item(w;copath-hd(p));copath-tl(p);copath-tl(q)))
Lemma: copathAgree-nil
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀p:copath(a.B[a];w). copathAgree(a.B[a];w;();p)
Lemma: copath-nil-Agree
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀p:copath(a.B[a];w). copathAgree(a.B[a];w;p;())
Lemma: copathAgree-last
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
(((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing
((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and
copathAgree(a.B[a];w;p;q))
Lemma: copathAgree-extend
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].
∀p:copath(a.B[a];w). ∀b:coW-dom(a.B[a];copath-at(w;p)). copathAgree(a.B[a];w;p;copath-extend(p;b))
Definition: pcw-path-coPath
pcw-path-coPath(n;p) ==
if (n =z 0)
then ()
else let param,w',d = p (n - 1) in
case d
of inl(b) =>
let pp = pcw-path-coPath(n - 1;p) in
if (copath-length(pp) =z n - 1) then copath-extend(pp;b) else () fi
| inr(x) =>
()
fi
Lemma: pcw-path-coPath_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:Path].
∀[n:ℕ]
((pcw-path-coPath(n;p) ∈ copath(a.B[a];w))
∧ ((copath-length(pcw-path-coPath(n;p)) = n ∈ ℤ)
⇒ (copath-at(w;pcw-path-coPath(n;p)) = (fst(snd((p n)))) ∈ coW(A;a.B[a]))))
supposing StepAgree(p 0;⋅;w)
Lemma: pcw-path-copathAgree
∀[A:𝕌']. ∀[B:A ⟶ Type].
∀w:coW(A;a.B[a]). ∀path:Path.
(StepAgree(path 0;⋅;w)
⇒ (∀i:ℕ
((copath-length(pcw-path-coPath(i + 1;path)) = (i + 1) ∈ ℤ)
⇒ (copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ)
⇒ copathAgree(a.B[a];w;pcw-path-coPath(i;path);pcw-path-coPath(i + 1;path)))))
Definition: coW-wfdd
coW-wfdd(a.B[a];w) ==
∀p:{p:n:ℕ ⟶ copath(a.B[a];w)|
∀i:ℕ
((copath-length(p i) = i ∈ ℤ)
⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ)
⇒ copathAgree(a.B[a];w;p i;p (i + 1)))}
(↓∃i:ℕ. (¬(copath-length(p i) = i ∈ ℤ)))
Lemma: coW-wfdd_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. (coW-wfdd(a.B[a];w) ∈ ℙ)
Lemma: sq_stable__coW-wfdd
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. SqStable(coW-wfdd(a.B[a];w))
Lemma: W-wfdd
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:W(A;a.B[a])]. coW-wfdd(a.B[a];w)
Lemma: coW-is-W
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. w ∈ W(A;a.B[a]) supposing coW-wfdd(a.B[a];w)
Definition: coW-game
coW-game(a.B[a];w;w') ==
<copath(a.B[a];w) × copath(a.B[a];w')
, <(), ()>
, λx,y. let u,v = x
in let u',v' = y
in ((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w;u;u')
∧ (v = v' ∈ copath(a.B[a];w')))
∨ ((u = u' ∈ copath(a.B[a];w))
∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w';v;v'))
, λx,y. let u,v = x
in let u',v' = y
in (((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w;u;u')
∧ (v = v' ∈ copath(a.B[a];w')))
∨ ((u = u' ∈ copath(a.B[a];w))
∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w';v;v')))
∧ (copath-length(u') = copath-length(v') ∈ ℤ)>
Lemma: coW-game_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. (coW-game(a.B[a];w;w') ∈ SimpleGame)
Lemma: sq-stable-coW-game-legal1
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. ∀p,q:Pos(coW-game(a.B[a];w;w')). SqStable(Legal1(p;q))
Lemma: sq-stable-coW-game-legal2
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. ∀p,q:Pos(coW-game(a.B[a];w;w')). SqStable(Legal2(p;q))
Definition: coW-equiv
The bisimulation relation on coW-types is defined to be
a winning strategy for the second player in the game ⌜coW-game(a.B[a];w;w')⌝.
This is an equivalence relation on the coW-type ⌜coW(A;a.B[a])⌝.⋅
coW-equiv(a.B[a];w;w') == win2(coW-game(a.B[a];w;w'))
Lemma: coW-equiv_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. (coW-equiv(a.B[a];w;w') ∈ ℙ)
Lemma: coW-equiv_weakening
∀[A:𝕌']. ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). coW-equiv(a.B[a];w;w') supposing w = w' ∈ coW(A;a.B[a])
Lemma: coW-equiv_inversion
∀[A:𝕌']. ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). (coW-equiv(a.B[a];w;w') ⇒ coW-equiv(a.B[a];w';w))
Definition: coW-pos-lens
coW-pos-lens(p;i;j) == let u,v = p in (copath-length(u) = i ∈ ℤ) ∧ (copath-length(v) = j ∈ ℤ)
Lemma: coW-pos-lens_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. ∀[p:Pos(coW-game(a.B[a];w;w'))]. ∀[i,j:ℤ]. (coW-pos-lens(p;i;j) ∈ ℙ)
Definition: coW-pos-agree
coW-pos-agree(a.B[a];w;w';p;q) ==
let u,v = p
in let u',v' = q
in ((copath-length(u) ≤ copath-length(u')) ∧ copathAgree(a.B[a];w;u;u'))
∧ (copath-length(v) ≤ copath-length(v'))
∧ copathAgree(a.B[a];w';v;v')
Lemma: coW-pos-agree_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. ∀[p,q:Pos(coW-game(a.B[a];w;w'))]. (coW-pos-agree(a.B[a];w;w';p;q) ∈ ℙ)
Lemma: sq_stable__coW-pos-agree
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])].
∀p,q:Pos(coW-game(a.B[a];w;w')). SqStable(coW-pos-agree(a.B[a];w;w';p;q))
Lemma: coW-pos-agree_refl
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. ∀p:Pos(coW-game(a.B[a];w;w')). coW-pos-agree(a.B[a];w;w';p;p)
Definition: coW-game2
coW-game2(a.B[a];w;w'';w') ==
<copath(a.B[a];w) × copath(a.B[a];w'') × copath(a.B[a];w')
, <(), (), ()>
, λx,y. let u,z,v = x in
let u',z',v' = y in
((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w;u;u')
∧ (v = v' ∈ copath(a.B[a];w'))
∧ (z = z' ∈ copath(a.B[a];w'')))
∨ (((u = u' ∈ copath(a.B[a];w)) ∧ (z = z' ∈ copath(a.B[a];w'')))
∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w';v;v'))
, λx,y. let u,z,v = x in
let u',z',v' = y in
((copath-length(z') = (copath-length(z) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w'';z;z')
∧ (((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w;u;u')
∧ (v = v' ∈ copath(a.B[a];w')))
∨ ((u = u' ∈ copath(a.B[a];w))
∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w';v;v'))))
∧ (copath-length(u') = copath-length(v') ∈ ℤ)
∧ (copath-length(z') = copath-length(v') ∈ ℤ)>
Lemma: coW-game2_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w',w'':coW(A;a.B[a])]. (coW-game2(a.B[a];w;w'';w') ∈ SimpleGame)
Lemma: coW-pos-agree_transitivity
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])].
∀p,q,r:Pos(coW-game(a.B[a];w;w')).
(coW-pos-agree(a.B[a];w;w';p;q) ⇒ coW-pos-agree(a.B[a];w;w';q;r) ⇒ coW-pos-agree(a.B[a];w;w';p;r))
Lemma: coW-play-invariant
∀[A:𝕌']
∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). ∀n:ℕ. ∀s:win2strat(coW-game(a.B[a];w;w');n).
∀moves:strat2play(coW-game(a.B[a];w;w');n;s). ∀i:ℕ.
(((i ≤ n)
⇒ (coW-pos-lens(moves[2 * i];i;i)
∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i))))
∧ ((i ≤ ((2 * n) + 1)) ⇒ (∀j:ℕi + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i]))))
Definition: coWtransInvariant
coWtransInvariant(x.B[x];w1;w2;w3;k;X;Y;a;b;moves) ==
(||a|| = ((2 * k) + 2) ∈ ℤ)
∧ (||b|| = ((2 * k) + 2) ∈ ℤ)
∧ (moves[(2 * k) + 1] = <fst(a[(2 * k) + 1]), snd(b[(2 * k) + 1])> ∈ Pos(coW-game(a.B[a];w1;w3)))
∧ ((snd((X a))) = (fst((Y b))) ∈ copath(a.B[a];w2))
∧ (((copath-length(snd(a[(2 * k) + 1])) = (copath-length(fst(b[(2 * k) + 1])) + 1) ∈ ℤ)
∧ (copath-length(snd(a[(2 * k) + 1])) = (copath-length(fst(a[(2 * k) + 1])) + 1) ∈ ℤ))
∨ ((copath-length(fst(b[(2 * k) + 1])) = (copath-length(snd(a[(2 * k) + 1])) + 1) ∈ ℤ)
∧ (copath-length(fst(b[(2 * k) + 1])) = (copath-length(snd(b[(2 * k) + 1])) + 1) ∈ ℤ)))
Lemma: coWtransInvariant_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w1,w2,w3:coW(A;a.B[a])]. ∀[k:ℕ]. ∀[X:win2strat(coW-game(a.B[a];w1;w2);k + 1)].
∀[Y:win2strat(coW-game(a.B[a];w2;w3);k + 1)]. ∀[a:strat2play(coW-game(a.B[a];w1;w2);k;X)].
∀[b:strat2play(coW-game(a.B[a];w2;w3);k;Y)]. ∀[m1:sequence(Pos(coW-game(a.B[a];w1;w3)))].
coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;m1) ∈ ℙ supposing ((2 * k) + 2) ≤ ||m1||
Definition: coW-trans
coW-trans(X; Y) == λmoves.let a,b = transMoves(X;Y;moves) in let u,x = X a in let x,v = Y b in <u, v>
Definition: transMoves
transMoves(X;Y;moves) ==
if (||moves|| =z 0)
then <seq-nil(), seq-nil()>
else let a,b = transMoves(X;Y;seq-truncate(moves;||moves|| - 2))
in let x,z1 = if (||moves|| =z 2) then <(), ()> else X a fi
in let z2,y = if (||moves|| =z 2) then <(), ()> else Y b fi
in let u,v = moves[||moves|| - 1]
in if copath-length(x) <z copath-length(u)
then let M1 = seq-add(seq-add(a;<x, z1>);<u, z1>) in
let M2 = seq-add(seq-add(b;<z2, y>);<snd((X M1)), y>) in
<M1, M2>
else let M2 = seq-add(seq-add(b;<z2, y>);<z2, v>) in
let M1 = seq-add(seq-add(a;<x, z1>);<x, fst((Y M2))>) in
<M1, M2>
fi
fi
Lemma: coW-trans_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w1,w2,w3:coW(A;a.B[a])]. ∀[n:ℕ]. ∀[X:win2strat(coW-game(a.B[a];w1;w2);n)].
∀[Y:win2strat(coW-game(a.B[a];w2;w3);n)].
(coW-trans(X; Y) ∈ win2strat(coW-game(a.B[a];w1;w3);n))
Lemma: coW-equiv_transitivity
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w1,w2,w3:coW(A;a.B[a])].
(coW-equiv(a.B[a];w1;w2) ⇒ coW-equiv(a.B[a];w2;w3) ⇒ coW-equiv(a.B[a];w1;w3))
Lemma: coW-equiv-equiv_rel
∀[A:𝕌']. ∀B:A ⟶ Type. EquivRel(coW(A;a.B[a]);w,w'.coW-equiv(a.B[a];w;w'))
Definition: coWmem
coWmem(a.B[a];z;w) == ∃b:coW-dom(a.B[a];w). coW-equiv(a.B[a];z;coW-item(w;b))
Lemma: coWmem_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])]. (coWmem(a.B[a];w;w') ∈ ℙ)
Lemma: coW-item-coWmem
∀[A:𝕌']. ∀B:A ⟶ Type. ∀w:coW(A;a.B[a]). ∀t:coW-dom(a.B[a];w). coWmem(a.B[a];coW-item(w;t);w)
Lemma: coW-game-reachable
∀[A:𝕌']
∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). ∀p,q:Pos(coW-game(a.B[a];w;w')).
(sg-reachable(coW-game(a.B[a];w;w');p;q) ⇒ coW-pos-agree(a.B[a];w;w';p;q))
Lemma: coW-game-step-isom
∀[A:𝕌']
∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). ∀t:coW-dom(a.B[a];w). ∀b:coW-dom(a.B[a];w').
sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))) ≅ coW-game(a.B[a];w;w')@<copath-cons(t;())
, copath-cons(b;())
>
Lemma: coW-equiv-implies
∀[A:𝕌']
∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
(coW-equiv(a.B[a];w;w') ⇒ (∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇒ coWmem(a.B[a];z;w'))))
Lemma: coW-equiv-iff
∀[A:𝕌']
∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
(coW-equiv(a.B[a];w;w') ⇐⇒ ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w')))
Lemma: coW-equiv-iff2
∀[A:𝕌']
∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
(coW-equiv(a.B[a];w;w')
⇐⇒ ∀p:copath(a.B[a];w')
∃q:copath(a.B[a];w)
((copath-length(q) = copath-length(p) ∈ ℤ) ∧ coW-equiv(a.B[a];copath-at(w';p);copath-at(w;q))))
Definition: maximal-copath
maximal-copath(a.B[a];w) ==
{p:ℕ ⟶ copath(a.B[a];w)|
∀n:ℕ. ((∀i:ℕn. (copath-length(p i) = i ∈ ℤ)) ⇒ (∀i:ℕn - 1. copathAgree(a.B[a];w;p i;p (i + 1))))}
Lemma: maximal-copath_wf
∀[A:𝕌']. ∀B:A ⟶ Type. ∀w:coW(A;a.B[a]). (maximal-copath(a.B[a];w) ∈ Type)
Lemma: coW-equiv-iff3
∀[A:𝕌']
∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
(coW-equiv(a.B[a];w;w')
⇐⇒ ∀p:maximal-copath(a.B[a];w')
∃q:maximal-copath(a.B[a];w)
∀n:ℕ
((∀i:ℕn. (copath-length(p i) = i ∈ ℤ))
⇒ (∀i:ℕn. ((copath-length(q i) = i ∈ ℤ) ∧ coW-equiv(a.B[a];copath-at(w;q i);copath-at(w';p i))))))
Lemma: coW-wfdd_functionality
∀[A:𝕌']. ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). (coW-equiv(a.B[a];w;w') ⇒ (coW-wfdd(a.B[a];w) ⇐⇒ coW-wfdd(a.B[a];w')))
Lemma: sqeq-copath1
∀[a,b,n:Top]. (λm.if (m) < (n - 1) then a[m] else b[m] ~ λm.if (m + 1) < (n) then a[m] else b[m])
Lemma: sqeq-copath2
∀[a,b,n,m:Top]. (if n + 1=m then a else b ~ if n=m - 1 then a else b)
Lemma: sqeq-copath3
∀[a,b,c,f:Top]. ∀[n,m:ℤ].
(λx.if (x) < (m) then f if x=n then a[x] else b[x] else c[x] ~ λx.if (x) < (m)
then if x=n then f a[x] else (f b[x])
else c[x])
Lemma: sqeq-copath4
∀[a,b,c,m:Top].
(λx.if (x) < (m) then if (x) < (m) then a[x] else b[x] else c[x] ~ λx.if (x) < (m) then a[x] else c[x])
Lemma: sqeq-copath5
∀[n,m:Top]. ((m + 1) - n - 1 ~ m - n - 1 - 1)
Definition: altW
We defined the W-type as a special case of the parameterized family
of W-types, so the proof of the induction principle is somewhat
complicated. Here we give an alternate definition as the
subtype of w ∈ coW(A;a.B[a]) for which ⌜coW-wfdd(a.B[a];w)⌝.
Then the induction operator is
altWind(h;w) == h w (λb.altWind(h;coW-item(w;b)))
and we directly prove that altWind(h;w) witnesses the induction
principle for altW(A;a.B[a]) by using bar induction
(see altWind_wf)⋅
altW(A;a.B[a]) == {w:coW(A;a.B[a])| coW-wfdd(a.B[a];w)}
Lemma: altW_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. (altW(A;a.B[a]) ∈ 𝕌')
Definition: altW-item
altW-item(w;b) == coW-item(w;b)
Lemma: altW-item_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:altW(A;a.B[a])]. ∀[b:coW-dom(a.B[a];w)]. (altW-item(w;b) ∈ altW(A;a.B[a]))
Definition: altWind
altWind(h;w) == h w (λb.altWind(h;coW-item(w;b)))
Lemma: altWind_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[P:altW(A;a.B[a]) ⟶ ℙ]. ∀[h:∀w:altW(A;a.B[a])
((∀b:coW-dom(a.B[a];w). P[altW-item(w;b)]) ⇒ P[w])].
∀[w:altW(A;a.B[a])].
(altWind(h;w) ∈ P[w])
Lemma: altWind-induction
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[P:altW(A;a.B[a]) ⟶ ℙ].
((∀w:altW(A;a.B[a]). ((∀b:coW-dom(a.B[a];w). P[altW-item(w;b)]) ⇒ P[w])) ⇒ (∀w:altW(A;a.B[a]). P[w]))
Definition: k-subtype
A ⊆ B == ∀i:ℕk. ((A i) ⊆r (B i))
Lemma: k-subtype_wf
∀[k:ℕ]. ∀[A,B:ℕk ⟶ Type]. (A ⊆ B ∈ ℙ)
Definition: k-ext
A ≡ B == A ⊆ B ∧ B ⊆ A
Lemma: k-ext_wf
∀[k:ℕ]. ∀[A,B:ℕk ⟶ Type]. (A ≡ B ∈ ℙ)
Lemma: k-ext-iff
∀[k:ℕ]. ∀[A,B:ℕk ⟶ Type]. uiff(A ≡ B;∀i:ℕk. A i ≡ B i)
Definition: k-monotone
k-Monotone(T.F[T]) == ∀[A,B:ℕk ⟶ Type]. F[A] ⊆ F[B] supposing A ⊆ B
Lemma: k-monotone_wf
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. (k-Monotone(T.F[T]) ∈ ℙ')
Definition: k-intersection
⋂n. X[n] == λi.⋂n:ℕ. (X[n] i)
Lemma: k-intersection_wf
∀[k:ℕ]. ∀[X:ℕ ⟶ ℕk ⟶ Type]. (⋂n. X[n] ∈ ℕk ⟶ Type)
Definition: k-1-continuous
k-1-continuous{i:l}(k;T.F[T]) == ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ. X (n + 1) ⊆ X n) ⇒ ((⋂n:ℕ. F[X n]) ⊆r F[⋂n. X n]))
Lemma: k-1-continuous_wf
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ Type]. (k-1-continuous{i:l}(k;T.F[T]) ∈ ℙ')
Definition: k-continuous
k-Continuous(T.F[T]) == ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ. X (n + 1) ⊆ X n) ⇒ ⋂n. F[X n] ⊆ F[⋂n. X n])
Lemma: k-continuous_wf
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. (k-Continuous(T.F[T]) ∈ ℙ')
Lemma: k-continuous-iff-all-k-1
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. (k-Continuous(T.F[T]) ⇐⇒ ∀i:ℕk. k-1-continuous{i:l}(k;T.F[T] i))
Lemma: implies-k-1-continuous
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ Type].
((∀[A,B:ℕk ⟶ Type]. F[A] ⊆r F[B] supposing A ⊆ B)
⇒ (∀j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ]))
⇒ k-1-continuous{i:l}(k;T.F[T]))
Lemma: implies-k-continuous
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
(k-Monotone(T.F[T])
⇒ (∀i,j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i))
⇒ k-Continuous(T.F[T]))
Definition: mutual-corec
mutual-corec(T.F[T]) == ⋂n. primrec(n;λi.Top;λ,T. F[T])
Lemma: mutual-corec_wf
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. (mutual-corec(T.F[T]) ∈ ℕk ⟶ Type)
Lemma: mutual-corec-ext
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
(mutual-corec(T.F[T]) ≡ F[mutual-corec(T.F[T])]) supposing (k-Monotone(T.F[T]) and k-Continuous(T.F[T]))
Lemma: mutual-corec-ext2
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
(mutual-corec(T.F[T]) ≡ F[mutual-corec(T.F[T])]) supposing
((∀i,j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i)) and
k-Monotone(T.F[T]))
Definition: m-corec
m-corec(T.F[T];i) == mutual-corec(T.F[T]) i
Lemma: m-corec_wf
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. ∀[i:ℕk]. (m-corec(T.F[T];i) ∈ Type)
Lemma: fix-mutual-corec-partial1
∀[A:Type]
(∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. ∀[f:(i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A))
⟶ i:ℕk
⟶ m-corec(T.F[T];i)
⟶ partial(A)].
(fix(f) ∈ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A))) supposing
(mono(A) and
value-type(A))
Lemma: fix_wf_mutual-corec-partial1
∀[A:Type]
(∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
∀[f:⋂T:ℕk ⟶ Type. ((i:ℕk ⟶ (T i) ⟶ partial(A)) ⟶ i:ℕk ⟶ (F[T] i) ⟶ partial(A))]
(fix(f) ∈ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A))
supposing k-Monotone(T.F[T])
∧ (∀i,j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i))) supposing
(mono(A) and
value-type(A))
Lemma: fix_wf_mutual-corec-partial-nat
∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
∀[f:⋂T:ℕk ⟶ Type. ((i:ℕk ⟶ (T i) ⟶ partial(ℕ)) ⟶ i:ℕk ⟶ (F[T] i) ⟶ partial(ℕ))]
(fix(f) ∈ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(ℕ))
supposing k-Monotone(T.F[T]) ∧ (∀i,j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i))
Definition: nat-prop
nat-prop{i:l}(n) == if (n) < (1) then Top else P:nat-prop{i:l}(n - 1) ⋂ j:ℕn ⟶ ℙ supposing dep-all(j;i.P i)
Definition: dep-all
dep-all(n;i.P[i]) == if (n) < (1) then True else :dep-all(n - 1;i.P[i]) ⋂ P[n - 1]
Lemma: nat-prop-dep-all-wf
∀[n:ℕ]. ((nat-prop{i:l}(n) ∈ 𝕌') ∧ (∀P:nat-prop{i:l}(n). ∀j:ℕn + 1. (dep-all(j;i.P[i]) ∈ ℙ)))
Lemma: nat-prop_wf
∀[n:ℕ]. (nat-prop{i:l}(n) ∈ 𝕌')
Lemma: dep-all_wf
∀[n:ℕ]. ∀[P:nat-prop{i:l}(n)]. (dep-all(n;i.P[i]) ∈ ℙ)
Definition: vdf-eq
vdf-eq(A;f;L) == dep-all(||L||;i.let a,b,c = L[i] in a = (f firstn(i;L) b) ∈ A)
Definition: vdf
vdf(A;B;a,b.C[a; b];n) ==
if n <z 1
then {L:(a:A × b:B × C[a; b]) List| ||L|| = 0 ∈ ℤ} ⟶ B ⟶ A
else f:vdf(A;B;a,b.C[a; b];n - 1) ⋂ {L:(a:A × b:B × C[a; b]) List| (||L|| ≤ n) ∧ vdf-eq(A;f;L)} ⟶ B ⟶ A
fi
Lemma: vdf-wf+
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type].
∀n:ℕ
((vdf(A;B;a,b.C[a;b];n) ∈ Type)
∧ (∀f:vdf(A;B;a,b.C[a;b];n). ∀L:(a:A × b:B × C[a;b]) List.
((||L|| ≤ (n + 1))
⇒ ((vdf-eq(A;f;L) ∈ ℙ)
∧ (vdf-eq(A;f;L) ⊆r (∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A)))))))
Lemma: vdf-wf
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type].
∀n:ℕ
((vdf(A;B;a,b.C[a;b];n) ∈ Type)
∧ (∀f:vdf(A;B;a,b.C[a;b];n). ∀L:(a:A × b:B × C[a;b]) List. ((||L|| ≤ (n + 1)) ⇒ (vdf-eq(A;f;L) ∈ ℙ))))
Lemma: vdf_wf
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[n:ℤ]. (vdf(A;B;a,b.C[a;b];n) ∈ Type)
Definition: very-dep-fun
We want to descibe a process "f,g" where "f" assignin to b ∈ B
a term a ∈ A and "g" computes a value r ∈ C[a;b] to get a triple
<a, b, r> ∈ a:A × b:B × C[a;b].
Given a list bs ∈ B List, this process "f,g" thus accumulates a list of
triples L ∈ (a:A × b:B × C[a;b]) List, but on each new b ∈ bs, f can use
the list L accumuated so far -- i.e. if b = bs[i], f can uses the list
accumulated by "f,g" from firstn(i;bs).
The type of "g" is simply a:A ⟶ b:B ⟶ C[a;b].
The type of "f" could simply be ((a:A × b:B × C[a;b]) List) ⟶ B ⟶ A
but that would require ⌜f L b ∈ A⌝ for any list of triples L, and b ∈ B.
Instead, we only need ⌜f L b ∈ A⌝ for lists L where if
<a, b, r> = L[i] then a = (f firstn(i;L) b).
We write ⌜vdf-eq(A;f;L)⌝ for this constraint on L.
Then the type of f should be
f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)} ⟶ B ⟶ A
So the type of the domain of f mentions f itself.
This is what we call a very dependent function type.
To define this type we use the dependent intersection type.
We define, by induction on n, the type vdf(A;B;a,b.C[a; b];n) of very dependent
functions that can accept input lists L of length upto n.
Then the very dependent function type is the intersection of these.
very-dep-fun(A;B;a,b.C[a; b]) == ⋂n:ℤ. vdf(A;B;a,b.C[a; b];n)
The constraint vdf-eq(A;f;L) is also defined by induction on the length of L
using dependent intersection.
By induction on n we can prove vdf-wf+ which proves (jointly) that
vdf-eq(A;f;L) is a proposition and vdf(A;B;a,b.C[a;b];n) is a type,
and also that vdf-eq(A;f;L) ⊆r (∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))))).
We get a kind of elimination rule for very-dep-fun(A;B;a,b.C[a; b])
very-dep-fun-subtype that says that for
f ∈ very-dep-fun(A;B;a,b.C[a; b]) we have
f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)} ⟶ B ⟶ A
For an introduction rule, we have a tactic VeryDepFunCD that reduces
proving f ∈ very-dep-fun(A;B;a,b.C[a;b]) to proving that
f [] ∈ B ⟶ A and f L ∈ B ⟶ A under the assumption
∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))))
To use the elimination rule, we will need to verify that a list of triples
L satisfies ⌜vdf-eq(A;f;L)⌝. For that, we have a tactic ProveVdfEq
that reduces that to proving
(fst(L[j])) = (f firstn(j;L) (fst(snd(L[j]))))
under the assumption
∀[i:ℕj]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))))
So the upshot is that we should be able to treat the type
very-dep-fun(A;B;a,b.C[a; b]) as an abstract, primitive type using only
the lemma very-dep-fun-subtype and the tactics
VeryDepFunCD and ProveVdfEq.
⋅
very-dep-fun(A;B;a,b.C[a; b]) == ⋂n:ℤ. vdf(A;B;a,b.C[a; b];n)
Lemma: very-dep-fun_wf
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. (very-dep-fun(A;B;a,b.C[a;b]) ∈ Type)
Lemma: very-dep-fun-subtype-domain
∀[A,B1,B2:Type]. ∀[C:A ⟶ B2 ⟶ Type].
very-dep-fun(A;B2;a,b.C[a;b]) ⊆r very-dep-fun(A;B1;a,b.C[a;b]) supposing B1 ⊆r B2
Lemma: vdf-eq_wf1
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[L:(a:A × b:B × C[a;b]) List]. ∀[m:ℤ]. ∀[f:vdf(A;B;a,b.C[a;b];m - 1)].
vdf-eq(A;f;L) ∈ Type supposing ||L|| ≤ m
Lemma: vdf-eq_wf
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀L:(a:A × b:B × C[a;b]) List. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. (vdf-eq(A;f;L) ∈ ℙ)
Lemma: very-dep-fun-eta
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. (f = (λL,b. (f L b)) ∈ very-dep-fun(A;B;a,b.C[a;b]\000C))
Lemma: vdf-eq-firstn
∀A:Type. ∀f:Top. ∀L:(a:Top × b:Top × Top) List. ∀i:ℕ||L||.
(vdf-eq(A;f;firstn(i + 1;L)) ~ x:vdf-eq(A;f;firstn(i;L)) ⋂ let tr = L[i] in
(fst(tr)) = (f firstn(i;L) (fst(snd(tr)))) ∈ A)
Lemma: vdf-eq-firstn-general
∀A:Type. ∀f:Top. ∀L:(a:Top × b:Top × Top) List. ∀i:ℕ||L|| + 1.
(vdf-eq(A;f;firstn(i;L)) ~ if (i =z 0)
then True
else x:vdf-eq(A;f;firstn(i - 1;L)) ⋂ let tr = L[i - 1] in
(fst(tr)) = (f firstn(i - 1;L) (fst(snd(tr)))) ∈ A
fi )
Lemma: vdf-eq-append1
∀A:Type. ∀f:Top. ∀L:(a:Top × b:Top × Top) List. ∀a,b,c:Top.
(vdf-eq(A;f;L @ [<a, b, c>]) ~ x:vdf-eq(A;f;L) ⋂ a = (f L b) ∈ A)
Lemma: vdf-eq-witness
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[L:(a:A × b:B × C[a;b]) List].
Ax ∈ vdf-eq(A;f;L) supposing vdf-eq(A;f;L)
Lemma: sq_stable__vdf-eq
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[L:(a:A × b:B × C[a;b]) List].
SqStable(vdf-eq(A;f;L))
Lemma: vdf-eq-subtype
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[n:ℕ]. ∀[f:vdf(A;B;a,b.C[a;b];n)]. ∀[L:(a:A × b:B × C[a;b]) List].
vdf-eq(A;f;L) ⊆r (∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A)) supposing ||L|| ≤ (n + 1)
Lemma: vdf-eq-implies
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[n:ℕ]. ∀[f:vdf(A;B;a,b.C[a;b];n)]. ∀[L:(a:A × b:B × C[a;b]) List].
vdf-eq(A;f;L) ⇒ (∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A)) supposing ||L|| ≤ (n + 1)
Lemma: vdf-eq-implies2
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[L:(a:A × b:B × C[a;b]) List].
(vdf-eq(A;f;L) ⇒ {∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A)})
Lemma: vdf-eq-firstn-implies
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[L:(a:A × b:B × C[a;b]) List]. ∀[j:ℕ||L||].
(vdf-eq(A;f;firstn(j;L)) ⇒ {∀[i:ℕj]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A)})
Lemma: implies-vdf-eq
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[L:(a:A × b:B × C[a;b]) List].
vdf-eq(A;f;L) supposing ∀i:ℕ||L|| + 1. ((∀j:ℕi. vdf-eq(A;f;firstn(j;L))) ⇒ vdf-eq(A;f;firstn(i;L)))
Lemma: very-dep-fun-subtype
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])].
(f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)} ⟶ B ⟶ A)
Lemma: implies-vdf-eq-append1
∀A,B:Type. ∀C:A ⟶ B ⟶ Type. ∀f:very-dep-fun(A;B;a,b.C[a;b]). ∀L:(a:A × b:B × C[a;b]) List. ∀a:A. ∀b:B. ∀c:Top.
(vdf-eq(A;f;L) ⇒ (a = (f L b) ∈ A) ⇒ vdf-eq(A;f;L @ [<a, b, c>]))
Home
Index