{-# OPTIONS --without-K #-}
module BarTheorem where
open import Basis
open import Spread.Baire
open import Securability
open import SystemT.Syntax
open import SystemT.Semantics
open import Dialogue as π hiding (module β’)
module BarTheorem (π
: Species) (π
-mono : monotone π
) where
bar-theorem
: (F : β’α΅ (nat β nat) β nat)
β F β© [] βα΅ π
β [] β π
bar-theorem F =
readback [] (π.norm (tmβͺ F β«β π.generic))
β eval F
where
eval
: (F : β’α΅ (nat β nat) β nat)
β F β© [] βα΅ π
β norm (tmβͺ F β«β generic) β© [] β π
eval F p Ξ± =
β‘.coe*
(Ξ» β β π
(Ξ± [ β + 0 ]))
(β‘.seq
(Coh.hauptsatzβ _ F _ generic Ξ» β¦nβ§ βͺnβ« β¦nβ§βΌβͺnβ« β
β‘.seq
(β‘.cong Ξ± β¦nβ§βΌβͺnβ«)
(π.β’.generic-diagram Ξ± βͺnβ«))
(π.β’.coh (tmβͺ F β«β generic) Ξ±))
(p Ξ±)
0β― : Point
0β― _ = 0
readback/Ξ·
: {U : Node}
β (k : β)
β spit k β© U β π
β U β π
readback/Ξ· zero f =
spit
(β‘.coe* π
(Point.β’.prepend-take-len _)
(f 0β―))
readback/Ξ· (suc n) f =
bite Ξ» x β
readback/Ξ· n Ξ» Ξ± β
β‘.coe* π
(Point.β’.take-cong
(Point.β’.su-+-transpose _ _)
(Ξ» _ β refl))
(f (x <β· Ξ±))
readback
: (U : Node)
β (m : π.π
β β)
β m β© U β π
β U β π
readback U (spit n) f =
readback/Ξ· n f
readback U (bite ΞΊ) f =
bite Ξ» x β
readback _ (ΞΊ x) Ξ» Ξ± β
β‘.coe*
(π
β U <++ x <β· Ξ± [_])
(Point.β’.su-+-transpose _ π
[ ΞΊ x β Ξ± ])
(π
-mono (f (x <β· Ξ±)))
module Induction
(π : Species)
(π
βπ : π
β π)
(π-hered : hereditary π)
where
relabel
: (U : Node)
β (U β π
)
β π U
relabel U (spit x) =
π
βπ U x
relabel U (bite m) =
π-hered Ξ» x β
relabel (U β’ x) (m x)
induction
: (F : β’α΅ (nat β nat) β nat)
β F β© [] βα΅ π
β π []
induction F =
relabel []
β bar-theorem F