Spaces:
Running
Running
File size: 2,260 Bytes
6bbcc6f | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 | import Formalization.Core
universe u v
namespace BehavioralSemantics
theorem pullBundle_order_reflecting
{S Z : Type u} {n : Nat} {V : Type v} [LE V]
(encoder : S → Z)
(surjective : Function.Surjective encoder)
{h k : Bundle Z n V}
(pulled : BundleLE (pullBundle encoder h) (pullBundle encoder k)) :
BundleLE h k := by
classical
intro zs
let ss : Tuple S n := fun i => Classical.choose (surjective (zs i))
have mapped : pullTuple encoder ss = zs := by
funext i
exact Classical.choose_spec (surjective (zs i))
have pointwise := pulled ss
change h (pullTuple encoder ss) ≤ k (pullTuple encoder ss) at pointwise
rw [mapped] at pointwise
exact pointwise
theorem claim3_safe_verification
{S Z : Type u} {n : Nat} {V : Type v} [LE V]
(le_transitive : ∀ {a b c : V}, a ≤ b → b ≤ c → a ≤ c)
(encoder : S → Z)
(surjective : Function.Surjective encoder)
(concreteClosure : Bundle S n V → Bundle S n V)
(abstractClosure : Bundle Z n V → Bundle Z n V)
(closureOplax :
∀ h, BundleLE
(concreteClosure (pullBundle encoder h))
(pullBundle encoder (abstractClosure h)))
(h : Bundle Z n V)
(concretePostfixed :
PostFixed concreteClosure (pullBundle encoder h)) :
PostFixed abstractClosure h := by
apply pullBundle_order_reflecting encoder surjective
intro ss
exact le_transitive (concretePostfixed ss) (closureOplax h ss)
theorem claim3_safe_construction
{S Z : Type u} {n : Nat} {V : Type v} [LE V]
(le_transitive : ∀ {a b c : V}, a ≤ b → b ≤ c → a ≤ c)
(pushforward : Bundle S n V → Bundle Z n V)
(concreteClosure : Bundle S n V → Bundle S n V)
(abstractClosure : Bundle Z n V → Bundle Z n V)
(pushforwardMonotone :
∀ {h k}, BundleLE h k →
BundleLE (pushforward h) (pushforward k))
(closureLax :
∀ h, BundleLE
(pushforward (concreteClosure h))
(abstractClosure (pushforward h)))
(h : Bundle S n V)
(concretePostfixed : PostFixed concreteClosure h) :
PostFixed abstractClosure (pushforward h) := by
intro zs
exact le_transitive
(pushforwardMonotone concretePostfixed zs)
(closureLax h zs)
end BehavioralSemantics
|