Proof for sectioning reachablity to a certain power

Stream: new members

[Bashar Hamade]

Hello,I'm trying to prove the following property for successor states in a Labelled transition system in my lean code :

$$$$ $$s' \in \text{Post}^{n+1}(\{s\})$$ $$\iff \exists s'' : s'' \in \text{Post}^n(\{s\}) \land s' \in \text{Post}(\{s''\})$$

I have been going through multiple steps in the proof with no success, although I feel like it could be proven in a much better easier way using some built-in Lean Lemmas. Here is the proof I have so far :

theorem post_n_plus_1_equiv_post_n_post {lts : LTS} (s : { s : State // s ∈ lts.states }) (n : Nat) :
  ∀ s', s' ∈ (post_S_n [s] (map_lts_actionsList lts) (n + 1)).map Subtype.val ↔
    ∃ s'', s'' ∈ (post_S_n [s] (map_lts_actionsList lts) n).map Subtype.val ∧
           s' ∈ (post_S_A [⟨s'', by sorry⟩] (map_lts_actionsList lts)).map Subtype.val := by
  intro s'
  apply Iff.intro
  intro h_post_n_plus_1
    -- Forward direction proof
  have h_eq : post_S_n [s] (map_lts_actionsList lts) (n + 1) =
                post_S_A (post_S_n [s] (map_lts_actionsList lts) n) (map_lts_actionsList lts) := by
    rw [post_S_n_succ_eq_post_S_n_post_S_n]
    rfl
  unfold post_S_n at h_post_n_plus_1
  sorry

I don't feel like my approach has been proper,so I would really appreciate recieving help to better approach this proof

[Damiano Testa]

The code that you posted is missing previous definitions, though.

[Bashar Hamade]

Damiano Testa said:

The code that you posted is missing previous definitions, though.

here is the full code (My laptop crashed :( ) :

import Batteries.Data.List.Perm
import Mathlib.Tactic.NthRewrite

open List

@[ext]
structure State where
  val : String
deriving BEq

theorem State.beq_iff {s t : State} : (s == t) ↔ s.val = t.val := by
  rw [show s == t ↔ s.val == t.val from Iff.rfl, beq_iff_eq]

instance : LawfulBEq State where
  rfl := by simp [State.beq_iff]
  eq_of_beq h := State.ext _ _ (State.beq_iff.1 h)

@[ext]
structure Action where
  val : String
deriving BEq

theorem Action.beq_iff {a b : Action} : (a == b) ↔ a.val = b.val := by
  rw [show a == b ↔ a.val == b.val from Iff.rfl, beq_iff_eq]

instance : LawfulBEq Action where
  rfl := by simp [Action.beq_iff]
  eq_of_beq h := Action.ext _ _ (Action.beq_iff.1 h)

structure LTS where
  states : List State
  actions : List Action
  transition : { s : State // s ∈ states } → { a : Action // a ∈ actions } → List { s : State // s ∈ states }
  s0 : { s : State // s ∈ states }

def post {lts : LTS} (s : { s : State // s ∈ lts.states }) (a : {a : Action // a ∈ lts.actions }) : List { s : State // s ∈ lts.states } :=
  lts.transition s a




def post_S {lts : LTS} (states : List { s : State // s ∈ lts.states }) (a : { a : Action // a ∈ lts.actions }) : List { s : State // s ∈ lts.states } :=
  states.foldl (fun acc state => acc ++ post state a) []

def post_A {lts : LTS} (s : { s : State // s ∈ lts.states }) (actions : List { a : Action // a ∈ lts.actions }) : List { s : State // s ∈ lts.states } :=
  actions.foldl (fun acc act => acc ++ post s act) []

def post_S_A {lts : LTS} (states : List { s : State // s ∈ lts.states }) (actions : List { a : Action // a ∈ lts.actions }) : List { s : State // s ∈ lts.states } :=
  actions.foldl (fun acc act => acc ++ post_S states act) []

def post_S_n {lts : LTS} (states : List { s : State // s ∈ lts.states }) (actions : List { a : Action // a ∈ lts.actions }) (n : Nat) : List { s : State // s ∈ lts.states } :=
  match n with
  | 0 => states
  | n' + 1 => post_S_A (post_S_n states actions n') actions













def map_lts_actionsList (lts : LTS) : List { a : Action // a ∈ lts.actions } :=
  lts.actions.filterMap fun a ↦ if h : a ∈ lts.actions then some ⟨a, h⟩ else none




theorem post_S_n_succ_eq_post_S_n_post_S_n {lts : LTS}
  (states : List { s : State // s ∈ lts.states })
  (actions : List { a : Action // a ∈ lts.actions })
  (n : Nat) :
  post_S_n states actions (n + 1) = post_S_n (post_S_n states actions n) actions 1 := by
  rfl

-- Assuming this function is already defined in your code
def map_lts_statesList (lts : LTS) : List { s : State // s ∈ lts.states } :=
  lts.states.filterMap fun s ↦ if h : s ∈ lts.states then some ⟨s, h⟩ else none

-- BEq instance for subtypes
instance instBEqSubtype {α : Type _} [BEq α] (P : α → Prop) : BEq (Subtype P) where
  beq a b := a.val == b.val

-- BEq instance for states in LTS
instance {lts : LTS} : BEq { s : State // s ∈ lts.states } := instBEqSubtype _

-- Pre function
def pre {lts : LTS} (s : { s : State // s ∈ lts.states }) (a : { a : Action // a ∈ lts.actions }) : List { s : State // s ∈ lts.states } :=
  List.filter (fun st => (lts.transition st a).indexOf? s != none) (map_lts_statesList lts)

-- Pre_A function
def pre_A (lts : LTS) (s : State) (actions : List { a : Action // a ∈ lts.actions }) : List State :=
  let s_subtype : Option { s : State // s ∈ lts.states } :=
    if h : s ∈ lts.states then some ⟨s, h⟩ else none
  match s_subtype with
  | none => []
  | some s' =>
    actions.foldl (fun acc a => acc ++ (pre s' a).map Subtype.val) []

-- Pre_S function
def pre_S (lts : LTS) (states : List State) (a : { a : Action // a ∈ lts.actions }) : List State :=
  states.foldl (fun acc s =>
    let s_subtype : Option { s : State // s ∈ lts.states } :=
      if h : s ∈ lts.states then some ⟨s, h⟩ else none
    match s_subtype with
    | none => acc
    | some s' => acc ++ (pre s' a).map Subtype.val
  ) []

-- Pre_S_A function
def pre_S_A (lts : LTS) (states : List State) (actions : List { a : Action // a ∈ lts.actions }) : List State :=
  actions.foldl (fun acc action => acc ++ pre_S lts states action) []

-- Pre_S_n function
def pre_S_n (lts : LTS) (states : List State) (actions : List { a : Action // a ∈ lts.actions }) (n : Nat) : List State :=
  match n with
  | 0 => states
  | n' + 1 => pre_S_A lts (pre_S_n lts states actions n') actions

theorem post_n_plus_1_equiv_post_n_post {lts : LTS} (s : { s : State // s ∈ lts.states }) (n : Nat) :
  ∀ s', s' ∈ (post_S_n [s] (map_lts_actionsList lts) (n + 1)).map Subtype.val ↔
    ∃ s'', s'' ∈ (post_S_n [s] (map_lts_actionsList lts) n).map Subtype.val ∧
           s' ∈ (post_S_A [⟨s'', by sorry⟩] (map_lts_actionsList lts)).map Subtype.val := by
  intro s'
  apply Iff.intro
  intro h_post_n_plus_1
    -- Forward direction proof
  have h_eq : post_S_n [s] (map_lts_actionsList lts) (n + 1) =
                post_S_A (post_S_n [s] (map_lts_actionsList lts) n) (map_lts_actionsList lts) := by
    rw [post_S_n_succ_eq_post_S_n_post_S_n]
    rfl
  unfold post_S_n at h_post_n_plus_1
  sorry

[Bashar Hamade]

Here is also a clear image of the theorem as latex didn't seem to render in my message :
image.png

[Damiano Testa]

Oh, that is way more code than I can reasonably debug, sorry! :smile:

[Bashar Hamade]

Damiano Testa said:

Oh, that is way more code than I can reasonably debug, sorry! :smile:

I've edited the code so that its more concise,the foucs is mainly the theorem written at the end

[Kevin Buzzard]

What's the maths proof?

[Bashar Hamade]

Kevin Buzzard said:

What's the maths proof?

Unfortunately there is not much of a proof provided in my lecture,this proof I'm writing is part of a bigger proof as you can see in this image (the proof i'm writing is basically the first 2 lines in the image)
image.png

[Bashar Hamade]

so originally I would like to write this whole proof,but first I though I provide a theorem for the first steps of the proof

[Bashar Hamade]

Kevin Buzzard said:

What's the maths proof?

I re-uploaded the image as it wasn't really complete

[Eric Wieser]

Bashar Hamade said:

as latex didn't seem to render in my message :

Write the latex in a ```math environment not a ```latex one, and without the preamble or \[s (you can edit your original post)

[Pieter Cuijpers]

Hi @Bashar Hamade , how did this story unfold? I'm looking into formalizing some LTS theorems myself and was wondering why you used lists of states rather than sets.