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

Stream: new members

[Saif Ghobash]

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]

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]

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

[Henrik Böving]

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]

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

[Henrik Böving]

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]

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

[Yaël Dillies]

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]

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]

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]

@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]

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]

@Saif Ghobash Are you trying to express:

S ::= a S b | a b

with rs?

[Saif Ghobash]

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

[Saif Ghobash]

@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]

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]

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