## Stream: new members

### Topic: Why can't I prove that my type is a fintype?

#### Saif Ghobash (Jan 02 2022 at 16:20):

I am trying to formalize some results on context free grammars. I am trying to construct a grammar using inductive types, and one of the conditions for a context free grammar is that the rules are finite. Consider the following example,

import data.fintype.basic

open sum

inductive v | s
inductive t | a | b
inductive rs : v → list (v ⊕ t) → Prop
| r1 : rs v.s [inr t.a, inl v.s, inr t.b]
| r2 : rs v.s [inr t.a, inr t.b]

example : fintype rs :=
begin
/-
type mismatch at application
fintype rs
term
rs
has type
v → list (v ⊕ t) → Prop : Type
but is expected to have type
Type ? : Type (?+1)
-/
end


Can someone help me understand what is going wrong here?

#### Huỳnh Trần Khanh (Jan 02 2022 at 16:25):

too bad I don't speak computer science even though I'm a programmer :joy: but fintype rs looks very very wrong to me, can you explain what you mean by that?

the reason you're getting the error is because rs lives in the Prop universe but fintype doesn't accept that

#### Yaël Dillies (Jan 02 2022 at 16:29):

fintype looks rights, but what you're trying to feed it looks wrong.

#### Henrik Böving (Jan 02 2022 at 16:29):

In the lean the amount of introduction rules of all inductive types are all finite. fintype formalizes another concept, namely that you can only construct finitely many distinct values of that type which is different of what you are trying to show @Saif Ghobash

#### Yaël Dillies (Jan 02 2022 at 16:30):

I would hazard guess that what you want is fintype {x : v × list (v ⊕ t) // rs x.1 x.2}.

#### Henrik Böving (Jan 02 2022 at 16:31):

That would be the statement that the language is finite though, not that the amount of rules is finite (which as I explained is trivially true) right?

#### Yaël Dillies (Jan 02 2022 at 16:31):

Okay, then I don't know how to do that!

#### Yaël Dillies (Jan 02 2022 at 16:33):

I don't exactly know what you mean by "rule" here, because if it's the stricto sensu introduction rules then there are two, just by reading the code.

#### Yaël Dillies (Jan 02 2022 at 16:35):

Huỳnh Trần Khanh said:

the reason you're getting the error is because rs lives in the Prop universe but fintype doesn't accept that

This is wrong. It lives in v → list (v ⊕ t) → Prop, not in Prop, and is expected to live in Type*.

#### Henrik Böving (Jan 02 2022 at 16:36):

Yaël Dillies said:

I don't exactly know what you mean by "rule" here, because if it's the stricto sensu introduction rules then there are two, just by reading the code.

If you really wanted to prove that statement you could probably do a meta proof about the lean type theory itself though although that seems like overkill...

#### Marcus Rossel (Jan 02 2022 at 16:37):

@Yaël Dillies I think this is also why rs isn't a fintype right? Because there are infinitely many functions for v -> list (sum v t) -> Prop.

#### Yaël Dillies (Jan 02 2022 at 16:39):

The error message says everything: fintype rs does not make sense. rs is a function, not a type. What you might be confused by is that v → list (v ⊕ t) → Prop is itself a type, but what we're interested in is the fact that its terms are themselves types.

#### Marcus Rossel (Jan 02 2022 at 16:45):

@Saif Ghobash Are you trying to express:

S ::= a S b | a b


with rs?

#### Saif Ghobash (Jan 02 2022 at 16:45):

@Marcus Rossel yes that is what I am trying to express

#### Saif Ghobash (Jan 02 2022 at 16:48):

@Yaël Dillies Yes essentially that is what I was confused by, v → list (v ⊕ t) → Prop is a type, so I was confused as to why I could prove that it is a fintype, I see now why it does not make any sense to show that rs is a fintype.

#### Reid Barton (Jan 02 2022 at 16:50):

In order to state that the set of rules is finite, you need a type which enumerates the rules. I think you want something like
inductive r | r1 | r2 (which you can prove is a fintype)
and then a function r -> (v × list (v ⊕ t)) (or two separate functions) which encodes the contents of the rules.

#### Saif Ghobash (Jan 02 2022 at 16:51):

@Reid Barton I think that makes more sense here. I'll try that, thank you!

Last updated: Dec 20 2023 at 11:08 UTC