Non-valid inductive type constructor argument

Stream: lean4

[Avi Craimer]

I'm trying to make some types that check if some finite set of arrows follow the end-to-end composability rules. I tried several approaches with no luck. Finally, I realized the domain and codomain could be stored in the types which helped with the type inference, but I'm still getting an error.

structure Arrow {ObjNames: Set String} (dom: ObjNames) (cod: ObjNames)  :=
  name: String

inductive ComposablePath {ObjNames: Set String} (dom: ObjNames) (cod: ObjNames)  :=
 -- Paths of length zero still have domains and codomains assigned in the type
 | empty
 -- The codomain of the path matches the domain of the new arrow being added to form a new path
 | path {x : ObjNames} (a: Arrow dom cod) (prev: ComposablePath x dom)

The Error is:

(kernel) arg #6 of 'ComposiblePath.path' contains a non valid occurrence of the datatypes being declared

I'm guessing that ComposablePath x dom is the non-valid occurance. It seems to assume that any term with in the type family of CompasiblePath which is inside one of the constructor arguments, must be parameterized the same way as the type of the value being constructed.

Is this a general requirement inductive types in Lean or is there some mistake in the code?

[James Gallicchio]

So, there are type parameters and type indices. Syntactically they are distinguished by putting parameters before the : in the type declaration and indices after. Parameters need to be the same throughout the inductive declaration, indices can vary.

If you make the inductive

inductive ComposablePath {ObjNames : Set String} : ObjNames -> ObjNames -> Type
| ...

that should work!

[Avi Craimer]

Wow that's awesome to know. I was never sure if there was a difference between putting arguments before the : or after.

Is there only a difference when dealing with type definitions? Or is there also a difference when defining constructors and regular functions?

[Avi Craimer]

As a follow up on this.

I figure out how to construct a value when using Set as a type.

When I try to do it the naive way it fails.

def SetOfStrings : Set String := {"A", "B", "C"}

def ElementInSetOfStrings : SetOfStrings :=  "A"

Error:

type mismatch
  "A"
has type
  String : Type
but is expected to have type
  ↑SetOfStrings : Type

↑SetOfStrings is some kind of type, but I can't figure out how to inspect the guts of it to see what the structure of a value of this type actually is.

I tried reading the definitions of Set in MathLib4 but Set itself is defined as a function def Set (α : Type u) := α → Prop and I can't find where the ↑ operation is defined for Set.

[Henrik Böving]

Quite simply Set's are not types, Set String is a type and SetOfStrings is a value of type Set String. The statement String : SetOfStrings does not make sense in a Lean context. But you can say that a value is in a set with the classical membership operator that you know from math.

[Avi Craimer]

But the error message says ↑SetOfStrings : Type so evidently there is some kind of mechanism with the ↑ that turns a set into a type. I'm trying to figure out what is happening there.

[Henrik Böving]

There might be a coercion (docs#Coe.coe) set up to do this but even then your idea wouldn't work out as you would then be saying that "A" which has type String is of type SetOfStrings which is still wrong (which is what the error message is telling you)

[Avi Craimer]

I realize that String: SetOfStrings doesn't make sense. Sometimes Lean interprets the value of literal symbols from the context of the type annotations (e.g., 4: Nat vs 4: Real) so I thought that def ElementInSetOfStrings : SetOfStrings := "A" might be one of those cases where Lean automatically turns the literal "A" into the appropriate value for the type ↑SetOfStrings, but it doesn't do it.

So I'm just asking how I would explicitly construct a value of type ↑SetOfStrings.

[Richard Copley]

Check out docs#Subtype. A value of type {x // x ∈ SetOfStrings} is (like) a pair of a value x of type String and a proof of x ∈ SetOfStrings. Here are a few ways to construct one.

def SetOfStrings : Set String := {"A", "B", "C"}
theorem isElement : "A" ∈ SetOfStrings := Set.mem_insert "A" {"B", "C"}

def ElementInSetOfStrings₁ : SetOfStrings :=  ⟨"A", isElement⟩
def ElementInSetOfStrings₂ : {x // x ∈ SetOfStrings} :=  Subtype.mk "A" isElement
def ElementInSetOfStrings₃ : Subtype (fun x => x ∈ SetOfStrings) := { val := "A", property := isElement }

[Avi Craimer]

Thanks for your answer @Richard Copley

I'm familiar with the subtype notation, I just didn't know the relationship between this and the coerced Set types.

It sounds like you are saying that when a S: Set α is coerced to a type ↑S, this type is equal to { x:α // x ∈ S }. Is that correct?

If so it would be very helpful if the infoview displayed the subtype notation rather than ↑S.

[Richard Copley]

• Yes.
• You can use set_option pp.coercions true set_option pp.coercions false to bring that about.

[Avi Craimer]

Richard Copley said:

• Yes.
• You can use set_option pp.coercions true set_option pp.coercions false to bring that about.

That's great. There is nothing more frustrating than being unable to see what is really going on with types so that option is pure gold to me!

[Richard Copley]

It's useful sometimes, but not an unalloyed pleasure! I agree that it's frustrating when the a term is delaborated with an up-arrow and its type is not obvious, and also when those expressions don't round-trip (can't be elaborated as input).

[James Gallicchio]

Avi Craimer said:

Is there only a difference when dealing with type definitions?

I believe it's the only place where the difference matters in the type theory, yeah!