Equality problems for defined structures

Stream: new members

[Bashar Hamade]

I'm struggling to understand what type of equality proofs I need when trying to write (basic) function definitions.I'm implementing labelled transition systems and I wanna write a function that gets the predecessor states of a given state using a given action :

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

However I get this error :

failed to synthesize
  BEq { s // s ∈ lts.states }
use `set_option diagnostics true` to get diagnostic information

What is exactly BEq ? and why does Lean struggle with such equalities ?

[Bashar Hamade]

here is the full code :

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 ValidState (lts : LTS) :=
  { s : State // s ∈ lts.states }

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


def post_S {lts : LTS} (states : List { s : State // s ∈ lts.states }) (a : Action) : 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 Action) : 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 Action) : 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 Action) (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

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
  | cons b t ih =>
    simp [indexOf?] at ha ⊢
    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  s lts.actions)  ++ ss) ( (post_A  s lts.actions).map Subtype.val ++ acc )
termination_by (lts.states.length - visited.1.length, to_visit.length)


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




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

[Edward van de Meent]

from my memory, BEq is a typeclass which carries a bool-valued 2-ary function on the supplied type. furthermore, LawfulBEq says that this boolean value corresponds to the Prop-valued equality given by the Eq type.

the problem is that because {s:State // s \in lts.states} is a separate type from State, it doesn't automatically have a BEq instance. (in general these instances can't. consider what would happen if we automatically supplied add to {n:Nat//n<4}). however, in this case you can fix this:

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

local instance instLawfulBEqSubtype {α :Type _} [BEq α] [i:LawfulBEq α] (P : α → Prop) :
    LawfulBEq (Subtype P) where
  eq_of_beq := by
    intro a b
    dsimp [BEq.beq]
    intro h
    ext
    exact i.eq_of_beq h
  rfl := by
    intro a
    dsimp [BEq.beq]
    exact i.rfl

[Edward van de Meent]

the local is because i'm not familiar enough with Batteries and friends to know that these issues don't cause any issues

[Chris Bailey]

There's an instance to get BEq from DecidableEq, and there's a DecidableEq on Subtype, but I guess there's nothing separate for BEq.

I think in general if the type allows (as State does here), you want to derive DecidableEq since you get more stuff for free.

[Marcus Rossel]

Edward van de Meent said:

the problem is that because {s:State // s \in lts.states} is a separate type from State, it doesn't automatically have a BEq instance. (in general these instances can't.

You can easily automatically derive BEq for subtypes though.

[Bashar Hamade]

Edward van de Meent said:

however, in this case you can fix this:

Sorry for late reply,but this still does not work and I get the same error . Also as @Marcus Rossel said that BEq can be easily automatically derived,could you elaborate more on how to do so?

[Edward van de Meent]

Bashar Hamade said:

Sorry for late reply,but this still does not work and I get the same error

are you sure? because for me, it gives a notably different error.

[Bashar Hamade]

ah sorry,got mixed up as I was getting the error I currently got at a previous time too. So now the error is :

application type mismatch
  filter (fun st ↦ indexOf? s (lts.transition st.val a) != none) lts.states
argument
  lts.states
has type
  List State : Type
but is expected to have type
  List { s // s ∈ lts.states } : Type

so it still can't properly derive the fact that lts.states are also of type List { s // s ∈ lts.states }

[Bashar Hamade]

one problem I'm facing is Lean wanting me to prove that an element of a List that has been constructed actually exists in it, is there a painless way to deal with this?

def states : List State :=
  [State.mk "UNUSED", State.mk "BURNING", State.mk "EXTINCT"]

def actions : List Action :=
  [Action.mk "strike", Action.mk "extinguish"]

def transition (s : State) (a : Action) : List { s : State // s ∈ states } :=
  match (s.val, a.val) with
  | ("UNUSED", "strike") => [⟨State.mk "BURNING", by simp [states]⟩] -- here we use the constructor notation to provide a proof that State.mk "BURNING" is a member of `states`
  | ("BURNING", "extinguish") => [⟨State.mk "EXTINCT", by simp [states]⟩]
  | _ => []

def lts_example : LTS :=
  LTS.mk
    states
    actions
    transition
    <| State.mk "UNUSED"

-- the simp proof above doesn't work here for some reason
example : lts_example.post (⟨State.mk "UNUSED", sorry⟩) (Action.mk "strike") = [⟨State.mk "BURNING", sorry⟩] := sorry

[Bashar Hamade]

I was wondering if there is some instance that could be applied here that would make lean automatically understand this membership