Constructors and constants

Stream: new members

[Logan Murphy]

Hello! Trying to formalize labelled transition systems by building some types and structures. If I write something like

constant foo : Type
structure bar :=
mk :: (x : foo)

constant f : foo
def baz := bar.mk f

Lean complains that 'baz' is noncomputable and depends on 'f'. What is the problem?
As a counterexample, I can write

structure bar' := mk ::
(x : nat)

def baz' := bar'.mk 10

which behaves as expected. Why can Lean do this with nat's but not with constants of type foo?

[Scott Morrison]

I suspect constant doesn't mean what you think it means.

[Scott Morrison]

Using constant is adding a new axiom to your logical foundations.

[Scott Morrison]

In particular, one without a computational interpretation, and hence anything using it becomes noncomputable.

[Scott Morrison]

Generally, I would avoid entirely using constant or parameter.

[Scott Morrison]

variables is probably better

[Logan Murphy]

Ah, thank you very much Scott.

[Logan Murphy]

I was able to get the desired behavior just using an enumerated type.
If I can ask another question about building structures, let's say I define an LTS structure as follows.

inductive state
| s₁
| s₂
| s₃
| s₄
open state

inductive label
| l₁
| l₂
| l₃
| l₄
open label

structure LTS :=
mk :: (S : set state) (A : set label) (Δ : set (state × label × state))
open LTS

def M₁ : LTS :=  mk {s₁, s₂, s₃, s₄} {l₁, l₂, l₃, l₄} {(s₁, l₂, s₃), (s₃, l₁, s₄)}

When I query #reduce M₁, the result is abstracted over the arguments I've provided to the mk constructor. The result is

{S := λ (b : state), b = s₁ ∨ b = s₂ ∨ b = s₃ ∨ b = s₄,
 A := λ (b : label), b = l₁ ∨ b = l₂ ∨ b = l₃ ∨ b = l₄,
 Δ := λ (b : state × label × state), b = (s₁, l₂, s₃) ∨ b = (s₃, l₁, s₄)}

when I would expect something like
{ S := { s₁, s₂, s₃, s₄ }
A := { l₁, l₂, l₃, l₄ },
Δ := { (s₁, l₂, s₃), (s₃, l₁, s₄) } }

[Reid Barton]

λ (b : state), b = s₁ ∨ b = s₂ ∨ b = s₃ ∨ b = s₄ is the reduced form of { s₁, s₂, s₃, s₄ }, and so on.

[Logan Murphy]

Ok great, thank you very much!

[Logan Murphy]

Based on what I've read, it seems like to only way to have a structure's fields refer to one another is to use inheritance. For instance, I can define the structure

structure LTS  :=
mk :: (S : set state) (A : set label) (TransRel : set (state × label × state))

but I want to be able to limit TransRel to those triples formed of the sets S and A. One approach I tried was

structure foo := (S : set state) (A : set label)
structure LTS extends foo := (TransRel : S × A × S)

but it seems I can't form Cartesian products in this way. Is it clear at all what I could do to achieve this?

[Reid Barton]

structure LTS  :=
mk :: (S : set state) (A : set label) (TransRel : set (S × A × S))

works for me (with appropriate context)

[Reid Barton]

though I would guess (S : set state) (A : set label) is likely a mistranslation of what you actually want

[Reid Barton]

for example, maybe you actually want

structure LTS  :=
mk :: (S : Type) (A : Type) (TransRel : set (S × A × S))

[Logan Murphy]

You're probably right. Thank you!

[Logan Murphy]

(deleted)

[Logan Murphy]

The reason I wanted to define a type of state and use sets thereof was so I could do things like

def M₁ : LTS :=  mk {s₁, s₂, s₃, s₄} {l₁, l₂, l₃, l₄}
{(s₁, l₂, s₃), (s₃, l₁, s₄), (s₄, l₃ , s₂), (s₂, l₄, s₅)}

is there a way to do such a thing with the presentation you offered? Sorry for the noob questions, I'm still getting used to using dependent TT this way

[Reid Barton]

looks like

def M₁ : LTS :=  mk state label
{(s₁, l₂, s₃), (s₃, l₁, s₄), (s₄, l₃ , s₂), (s₂, l₄, s₅)}

[Reid Barton]

(I'm assuming you might want to define other LTSs with other state and label types.)

[Logan Murphy]

Definitely better. Thanks!

[Logan Murphy]

Ok, now I think the only other reason I'd be tempted to use sets of states and labels is so that I can use membership to inductively define executions within an LTS, in the (general) sense of

structure sl_pair :=
makepair :: (s : state) (l : label)

-- Given any Labelled Transition System M,
-- given any state s₀ ∈ M.S, (init s₀) is an execution
-- given any execution e which "finishes" at a state s,
--      can form an execution e' by appending
--      state-label pair (s', l) to e such that
--      (s, l, s') ∈ M.TransRel

/- skeleton of inductive definition -/
inductive execution {M : LTS}
| init : state → execution
| cons : sl_pair → execution → execution

So I'm trying to implement the logic in the comments into this definition, and one approach I guess would be to supply membership-propositions as arguments to the constructors, if I use the set-theoretic definition of LTS. But there may very well be an approach using the simpler type-theoretic definition as well.

[Reid Barton]

It looks like it will just be the same, but without any set membership involved.

[Logan Murphy]

Ok, will play around. Thanks again!