Termination issue with List function

Stream: new members

[Bashar Hamade]

I starting a project to formalise CCS and i'm struggling to provide a working definition for the reachability of a list of states in LTS because Lean can't show termination on the arguments :

import Batteries.Data.List.Basic

structure State where
  val : String
deriving BEq

structure Action where
  val : String

structure LTS where
  states : List State
  actions : List Action
  transition : State → Action → List State
  s0 : State

def post_A (lts : LTS) (s : State) (actions : List Action) : List State :=
  actions.foldl (fun acc act => acc ++ post lts s act) []

def reach_aux (lts : LTS) (visited : List State) (to_visit : List State) (acc : List State): List State :=
  match to_visit with
  | [] => acc
  | s::ss =>
    if visited.indexOf? s == none then
      reach_aux lts visited ss acc
    else
      reach_aux lts (s::visited) (  (post_A lts s lts.actions)  ++ ss) ( (post_A lts s lts.actions) ++ acc )

Is there a way to bypass this termination failure issue?

[Kim Morrison]

You shouldn't think about "bypassing" termination, but instead explain (informally) why you think it does terminate, and then using termination_by to tell Lean the decreasing quantity, and then possibly decreasing_by to proof the proof that that quantity decreases, in the event that automation can't do it already.

[Bashar Hamade]

unfortunately I haven't dealt with termination at all in proof assistants.How would I clarify that finding all the reachable states in a LTS (or an automaton,the concept is basically the same) does indeed terminate ?
I know it terminates because i'm just iterating over a finite automaton like I would for a finite graph

[Markus Himmel]

I assume that you wanted to write if visited.indexOf? s != none then (with a != instead of a ==)?

[Markus Himmel]

If so, I think that your function doesn't actually terminate, because you don't constrain the transition function to only return states the are in the states list, so something like

def badLts : LTS where
  states := []
  actions := [⟨"a"⟩]
  transition s a := [⟨s.1 ++ a.1⟩]
  s0 := ⟨""⟩

#eval reach_aux badLts [] [⟨"s"⟩] []

should lead to infinite recursion.

[Chris Bailey]

Just as a side note, it is permissible to write and execute recursive functions without showing they terminate using partial def.

[Markus Himmel]

Here is one way to show termination using a fixed version of the LTS structure:

import Batteries.Data.List.Perm

open List

set_option autoImplicit true

@[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)

structure Action where
  val : String

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

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

theorem List.not_mem_of_indexOf?_eq_none [BEq α] [LawfulBEq α] (l : List α) (a : α) (ha : l.indexOf? a = none) : ¬a ∈ l := by
  induction l with
  | nil => simp [indexOf?]
  | cons b t ih =>
    simp [indexOf?] at *
    split at ha
    · simp at ha
    · rw [Option.map_eq_none'] at ha
      refine ⟨Ne.symm ?_, ih ha⟩
      next h =>
      rintro rfl
      exact h LawfulBEq.rfl

def reach_aux (lts : LTS) (visited : { l : List State // l <+~ lts.states } ) (to_visit : List { s : State // s ∈ lts.states }) (acc : List State): List State :=
  match to_visit with
  | [] => acc
  | s::ss =>
    if h : visited.1.indexOf? s.1 != none then
      reach_aux lts visited ss acc
    else
      have hx : (s.1 :: visited.1) <+~ lts.states := by
        refine List.cons_subperm_of_not_mem_of_mem ?_ s.2 visited.2
        rw [Bool.not_eq_true, bne_eq_false_iff_eq] at h
        exact List.not_mem_of_indexOf?_eq_none _ _ h
      have : lts.states.length - (visited.1.length + 1) < lts.states.length - visited.1.length := by
        refine Nat.sub_add_lt_sub ?_ Nat.zero_lt_one
        simpa using hx.length_le
      reach_aux lts ⟨s::visited, hx⟩ (  (post_A lts s lts.actions)  ++ ss) ( (post_A lts s lts.actions).map Subtype.val ++ acc )
termination_by (lts.states.length - visited.1.length, to_visit.length)

[Notification Bot]

7 messages were moved here from #general > Beginner Questions by Patrick Massot.

[Patrick Massot]

@Bashar Hamade I moved this discussion that used to be in a six years old thread with a very generic title in the general channel. The new members channel is specifically followed by people who are actively willing to help beginners, so you have a higher probability to get an answer there. Then the more specific thread title helps future people who will have a similar question.

[Bashar Hamade]

Markus Himmel said:

Here is one way to show termination using a fixed version of the LTS structure:

import Batteries.Data.List.Perm

open List

set_option autoImplicit true

@[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)

structure Action where
  val : String

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

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

theorem List.not_mem_of_indexOf?_eq_none [BEq α] [LawfulBEq α] (l : List α) (a : α) (ha : l.indexOf? a = none) : ¬a ∈ l := by
  induction l with
  | nil => simp [indexOf?]
  | cons b t ih =>
    simp [indexOf?] at *
    split at ha
    · simp at ha
    · rw [Option.map_eq_none'] at ha
      refine ⟨Ne.symm ?_, ih ha⟩
      next h =>
      rintro rfl
      exact h LawfulBEq.rfl

def reach_aux (lts : LTS) (visited : { l : List State // l <+~ lts.states } ) (to_visit : List { s : State // s ∈ lts.states }) (acc : List State): List State :=
  match to_visit with
  | [] => acc
  | s::ss =>
    if h : visited.1.indexOf? s.1 != none then
      reach_aux lts visited ss acc
    else
      have hx : (s.1 :: visited.1) <+~ lts.states := by
        refine List.cons_subperm_of_not_mem_of_mem ?_ s.2 visited.2
        rw [Bool.not_eq_true, bne_eq_false_iff_eq] at h
        exact List.not_mem_of_indexOf?_eq_none _ _ h
      have : lts.states.length - (visited.1.length + 1) < lts.states.length - visited.1.length := by
        refine Nat.sub_add_lt_sub ?_ Nat.zero_lt_one
        simpa using hx.length_le
      reach_aux lts ⟨s::visited, hx⟩ (  (post_A lts s lts.actions)  ++ ss) ( (post_A lts s lts.actions).map Subtype.val ++ acc )
termination_by (lts.states.length - visited.1.length, to_visit.length)

Thanks a lot for the provided code :) . this auxiliary function is to be used in another main reach function that starts with an empty list for 'visited' ,however that would lead to a type mismatch error as the case in this function:

def reach {lts : LTS} (initial_states : List { s : State // s ∈ lts.states }) : List { s : State // s ∈ lts.states } :=
  reach_aux lts [] initial_states []

[Bashar Hamade]

can I specify an empty list while specifying the exact type it should return to fix the problem?

[Bashar Hamade]

also how can I abbreviate { s : State // s ∈ lts.states },I've been repeating it in all my definitions and it gets too tedious quickly

[Markus Himmel]

Bashar Hamade said:

can I specify an empty list while specifying the exact type it should return to fix the problem?

The parameter (visited : { l : List State // l <+~ lts.states } ) is a pair of a list and a proof that the list is a subpermutation (docs#List.Subperm) of the states, so the correct invocation would be

def reach {lts : LTS} (initial_states : List { s : State // s ∈ lts.states }) : List { s : State // s ∈ lts.states } :=
  reach_aux lts ⟨[], nil_subperm⟩ initial_states []

[Markus Himmel]

Bashar Hamade said:

also how can I abbreviate { s : State // s ∈ lts.states },I've been repeating it in all my definitions and it gets too tedious quickly

You could define something like

def ValidState (lts : LTS) :=
  { s : State // s ∈ lts.states }

[Bashar Hamade]

perfect.Thanks a lot for your help :)