Last active
March 21, 2025 01:57
-
-
Save kuruczgy/c8d638065bd189e7844f1785c5618b18 to your computer and use it in GitHub Desktop.
Proof that circular composition preserves the behavioral subset relation on nondeterministic Mealy automata
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| def Sequence α n := (j : Nat) → j < n → α | |
| def Sequence.map (f : α → β) (s : Sequence α n) : Sequence β n := fun j hj => f (s j hj) | |
| instance : GetElem (Sequence α n) Nat α fun _ j => j < n where | |
| getElem s j hj := s j hj | |
| structure NMealy (I O : Type) where | |
| S : Type | |
| S₀ : S → Prop | |
| Δ : S → I → O → S → Prop | |
| def NMealy.BehaviorSubset (M₁ M₂ : NMealy I O) : Prop := | |
| ∀ n (s : Sequence M₁.S (n + 1)), M₁.S₀ s[0] → | |
| ∃ (s' : Sequence M₂.S (n + 1)), M₂.S₀ s'[0] ∧ | |
| ∀ j (hj : j < n) i o, | |
| M₁.Δ s[j] i o s[j + 1] → M₂.Δ s'[j] i o s'[j + 1] | |
| instance : HasSubset (NMealy I O) := ⟨NMealy.BehaviorSubset⟩ | |
| def NMealy.circular_compose | |
| (M₁ : NMealy (I₁ × O₂) (O₁ × I₂)) | |
| (M₂ : NMealy I₂ O₂) | |
| : NMealy I₁ O₁ := | |
| { | |
| S := M₁.S × M₂.S, | |
| S₀ := fun (s₁, s₂) => M₁.S₀ s₁ ∧ M₂.S₀ s₂ | |
| Δ := fun (s₁, s₂) i₁ o₁ (s₁', s₂') => ∃ i₂ o₂, | |
| M₁.Δ s₁ (i₁, o₂) (o₁, i₂) s₁' ∧ M₂.Δ s₂ i₂ o₂ s₂' | |
| } | |
| theorem circular_compose_monotonic | |
| (M : NMealy (I₁ × O₂) (O₁ × I₂)) | |
| (U U' : NMealy I₂ O₂) | |
| (h_u_sub : U ⊆ U') | |
| : M.circular_compose U ⊆ M.circular_compose U' := by | |
| simp [NMealy.circular_compose] | |
| intros n s h_s₀ | |
| cases h_s₀ | |
| obtain ⟨su', ⟨hu'0, hu'⟩⟩ := h_u_sub n (s.map Prod.snd) (by assumption) | |
| exists (fun j hj => (s[j].fst, su'[j])) | |
| simp | |
| constructor | |
| · constructor <;> assumption | |
| · intros j hj i₁ o₁ i₂ o₂ hmd hud | |
| exists i₂, o₂ | |
| constructor | |
| · apply hmd | |
| · apply (hu' j hj) | |
| apply hud | |
| theorem NMealy.BehaviorSubset_reflexive (M : NMealy I O) : M ⊆ M := by | |
| intros n s hs0 | |
| exists s | |
| simp | |
| assumption | |
| theorem NMealy.BehaviorSubset_transitive (M₁ M₂ M₃ : NMealy I O) : M₁ ⊆ M₂ → M₂ ⊆ M₃ → M₁ ⊆ M₃ := by | |
| intros h12 h23 | |
| intros n s1 hs1_0 | |
| obtain ⟨s2, ⟨hs2_0, hd12⟩⟩ := h12 n s1 hs1_0 | |
| obtain ⟨s3, ⟨hs3_0, hd23⟩⟩ := h23 n s2 hs2_0 | |
| exists s3 | |
| constructor; assumption | |
| intros j hj i o hd1 | |
| apply (hd23 j hj) | |
| apply (hd12 j hj) | |
| apply hd1 | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment