Spaces:
Running
Running
File size: 2,774 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 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 | import Std
universe u v
namespace BehavioralSemantics
abbrev Tuple (X : Type u) (n : Nat) := Fin n → X
abbrev Bundle (X : Type u) (n : Nat) (V : Type v) := Tuple X n → V
structure Coalgebra (F : Type u → Type u) (X : Type u) where
transition : X → F X
structure BundleLifting
(F : Type u → Type u) (n : Nat) (V : Type v) where
lift : {X : Type u} → Bundle X n V → Bundle (F X) n V
def pullTuple {X Y : Type u} {n : Nat}
(f : X → Y) (xs : Tuple X n) : Tuple Y n :=
fun i => f (xs i)
def pullBundle {X Y : Type u} {n : Nat} {V : Type v}
(f : X → Y) (h : Bundle Y n V) : Bundle X n V :=
fun xs => h (pullTuple f xs)
def closure {F : Type u → Type u} {X : Type u} {n : Nat} {V : Type v}
(system : Coalgebra F X)
(lifting : BundleLifting F n V)
(h : Bundle X n V) : Bundle X n V :=
fun xs => lifting.lift h (fun i => system.transition (xs i))
def BundleLE {X : Type u} {n : Nat} {V : Type v} [LE V]
(h k : Bundle X n V) : Prop :=
∀ xs, h xs ≤ k xs
def PostFixed {X : Type u} {n : Nat} {V : Type v} [LE V]
(operator : Bundle X n V → Bundle X n V)
(h : Bundle X n V) : Prop :=
BundleLE h (operator h)
def Fixed {X : Type u} {n : Nat} {V : Type v}
(operator : Bundle X n V → Bundle X n V)
(h : Bundle X n V) : Prop :=
h = operator h
def BehavioralStructure {X : Type u} {n : Nat} {V : Type v} [LE V]
(operator : Bundle X n V → Bundle X n V)
(h : Bundle X n V) : Prop :=
PostFixed operator h ∨ Fixed operator h
theorem claim1_bundle_total
{X : Type u} {n : Nat} {V : Type v}
(h : Bundle X n V) (xs : Tuple X n) :
∃ value, h xs = value ∧
∀ other, h xs = other → other = value := by
refine ⟨h xs, rfl, ?_⟩
intro other equality
exact equality.symm
theorem claim1_coalgebra_transition_total
{F : Type u → Type u} {X : Type u}
(system : Coalgebra F X) (x : X) :
∃ next, system.transition x = next ∧
∀ other, system.transition x = other → other = next := by
refine ⟨system.transition x, rfl, ?_⟩
intro other equality
exact equality.symm
theorem claim2_closure_pointwise
{F : Type u → Type u} {X : Type u} {n : Nat} {V : Type v}
(system : Coalgebra F X)
(lifting : BundleLifting F n V)
(h : Bundle X n V) (xs : Tuple X n) :
closure system lifting h xs =
lifting.lift h (fun i => system.transition (xs i)) :=
rfl
theorem claim2_fixed_is_postfixed
{X : Type u} {n : Nat} {V : Type v} [LE V]
(operator : Bundle X n V → Bundle X n V)
(h : Bundle X n V)
(le_refl : ∀ value : V, value ≤ value)
(fixed : Fixed operator h) :
PostFixed operator h := by
intro xs
rw [congrFun fixed xs]
exact le_refl (operator h xs)
end BehavioralSemantics
|