help with fintype

Stream: new members

[Matt Earnshaw]

I have a type of words over alphabets (which I am treating as enumerated types).

inductive Γ | X | Y

inductive word (α : Type) : Type
| ε {} : word
| nonempty : α → word → word
infixr ` ∙ ` :100 := word.nonempty

#check (Γ.X ∙ ε : word Γ)

I would like to have a matrix (word Γ) (word Γ) _, but this doesn't work as we would need instance : fintype (word Γ) (which surely is not constructible). So I started an attempt at finite words

def max_length := 1000
inductive finword (α : Type) : ℕ → Type
| empty : finword 0
| nonempty {n : ℕ} {h : n+1 <= max_length} : α → finword n → finword (n+1)

I have no idea really how to prove fintype for this. Maybe I need to rethink my approach. Thanks in advance for any suggestions. For reference I am trying to model what is called on slide 7 here "Closed and Consistent Finite Hankel Matrices", which as you can see are in the first instance finite matrices indexed by words in a language (hopefully once I have the correct type for such a matrix, then the closed & consistent predicates will be easy) https://borjaballe.github.io/slides/turing18.pdf

[Reid Barton]

I would just not use matrix

[Reid Barton]

A function seems fine

[Matt Earnshaw]

hm, yes I suppose a "partial" function word α -> word α -> option bool could work... I was thinking it would be useful to draw on the matrix methods, but actually it does not have the main thing I need which is some kind of add_row. let's see if I can define that...

[Matt Earnshaw]

so this is working well enough so far:

variables {α : Type} [decidable_eq α]
def table := word α → word α → option bool

def add_row (t : table) (row : word α) (entries : word α → option bool) :=
  function.update t row entries

def consistent (T : table) := ∀ p₁ p₂ : word α, ∀ a : α, T p₁ = T p₂ → T (a∙p₁) = T (a∙p₂)

now, ideally I would have a function that for any table, either proves consistency or gives a counterexample (or at least gives a bool answer for consistent or not). I should be able to construct that function as a term of some type right? I'm having trouble getting started

[Mario Carneiro]

You should probably make table a definition rather than a notation

[Mario Carneiro]

You can't decide consistent T unless word A is finite

[Mario Carneiro]

and A

[Mario Carneiro]

The type you want to construct is decidable (consistent T)

[Mario Carneiro]

although this is only the weaker form; for the stronger form you need some specialized proof-or-counterexample type

[Matt Earnshaw]

thanks. so I'm back to square one - I know how to deal with proving fintype A but word A just isn't finite (it is basically list A). so was my original finwordsketch possibly a non insane idea?

[Matt Earnshaw]

right, so I'm pretty happy with this

namespace x
inductive fin : ℕ → Type
| zero {n : ℕ} : fin (n+1)
| succ {n : ℕ} : fin n → fin (n+1)

inductive finword (α : Type) : Π n : ℕ, fin n → Type
| empty    {}      {n : ℕ}     : finword (n+1) fin.zero
| nonempty {n : ℕ} {len : fin n} : α → finword n len → finword (n+1) len.succ

infixr ` ∙ ` :100 := finword.nonempty
notation `ε` := finword.empty

but now I'm stuck on the type of tables:
def mytable : finword α 100 _ → finword α 100 _ → option bool | ε ε := tt ... clearly isn't valid, but neither is filling in any particular fin for the _. so it seems I would need to make that argument implicit in finword, but I'm not sure if that's possible...

[Matt Earnshaw]

this works, including the word lengths manually but is not very elegant

def mytable : Π {n m : fin 10}, finword Γ 10 n → finword Γ 10 m → option bool
| fin.zero  fin.zero  ε          ε := tt
| (fin.succ fin.zero) fin.zero (Γ.X∙ε) ε := tt
| _ _ _ _ := none

[Matt Earnshaw]

and further, for a moderately sized table, lean does not want to compile it (deep recursion was detected at 'replace')

[Mario Carneiro]

This is not what you want - each finword A n i is isomorphic to A, so it doesn't represent the type of words. You need empty and nonempty to be able to inhabit the same type for that. I suggest:

inductive finword (α : Type) : Π n : ℕ, Type
| empty {} {n : ℕ} : finword (n+1)
| nonempty {n : ℕ} : α → finword n → finword (n+1)

[Mario Carneiro]

Where fin comes in is that you can define a bijection between finword A n and fin n -> A

[Matt Earnshaw]

@Mario Carneiro that's perfect, thanks. I got into a subtle confusion but I see now

[Mario Carneiro]

Actually, I think empty needs type finword 0 if you want this to be like the type vector A n

[Matt Earnshaw]

true

[Matt Earnshaw]

I think the original should work for my purposes

[Matt Earnshaw]

I am proving decidable (consistent T) for a special case to get a feel for the general one. blanking on how to solve a goal of the form:

a_1 : f x  = f  y
⊢ f b = f c

where a_1 is false... it's late

[Bryan Gin-ge Chen]

If you can get a term t : false, then t.elim will solve the goal. Similarly, if you have ha : a and hna: ¬a, absurd ha hna will work.

[Mario Carneiro]

You can use exfalso to make the goal false explicitly, but it's rarely necessary. Once you prove the context is contradictory it usually doesn't matter what the goal is

[Matt Earnshaw]

cheers, remember these from the NNG but actually introducing the relevant term was tripping me up... got there in the end

[Matt Earnshaw]

I feel it will be brutal to generalize this proof to any table...

[Wojciech Nawrocki]

Hello! I'm trying to construct an object for all fintypes, i.e. I want a conclusion of the form ∀ (J: Type u) [fintype J], C J for some motive C. I scoured the chat for ways to construct stuff out of fintypes and it seems one way to do it is by induction on fintype.card, but the inductive step is really awkward since one needs to construct something like "a fintype-with-one-object-less-than-J given that fintype.card J = nat.succ n". Constructing my thing would be quite nice given the following recursion principle:

def myrec
  (C : Π (J: Type u) [fintype J], Sort v)
  (C0 : C pempty)
  (CS : ∀ (J': Type u) [fintype J'], C J' → C (unit ⊕ J'))
  : ∀ (J: Type u) [fintype J], by exactI C J

The problem is I'm not quite sure if this is provable, or even true. Might it be?

[Kevin Buzzard]

My guess is that this would only be provable if you can prove that C is constant on isomorphism classes, i.e. if there's a bijection between J and K then C(J)=C(K).

[Kevin Buzzard]

Because your assumptions will enable to you prove C(unit ⊕ unit ⊕ ... ⊕ unit) but where do you go from there unless you know C is constant on isomorphism classes?

[Wojciech Nawrocki]

Thank you, this does sound reasonable. So something like

def myrec
  (C : Π (J: Type u) [fintype J], Sort v)
  (C0 : C pempty)
  (CS : ∀ (J': Type u) [fintype J'], C J' → C (unit ⊕ J'))
  (h : ∀ (J J': Type u) [fintype J] [fintype J'], J ≃ J' → C J = C J')
  : ∀ (J: Type u) [fintype J], by exactI C J

might be true.

[Kevin Buzzard]

Yes it might be, but if C is really taking values in Sort v then the danger here is that it might be hard to prove C J = C J'. Equality of types is a thorny subject.

[Scott Morrison]

You should be able to do this with only the assumption J ≃ J' → C J ≃ C J'.

[Reid Barton]

But at this point you might as well just prove nonempty (C J)

[Reid Barton]

So you might as well just assume C takes values in Props

[Reid Barton]

This is assuming you don't intend to prove any lemmas about which value my_rec takes, but it's hard to see what kind of lemma you could expect to have.

[Wojciech Nawrocki]

@Reid Barton Wouldn't def myC (J: Type u) [fintype J] : Type := fin (fintype.card J) be a valid non-Prop example? It's fairly simple to prove that it respects isomorphisms.

[Reid Barton]

We could even take C J = J

[Reid Barton]

But to define myrec you will have to choose an isomorphism from J to the nested sum of units, and this choice won't be compatible with isomorphisms

[Wojciech Nawrocki]

Thank you, I don't really care about what it returns as long as it's in Type. For context, I'm trying to prove in the catthy library that binary products and terminal object imply finite products by recursion on the size of J where (discrete J) ⥤ C is the diagram. The return type is has_limit F which is not a Prop. Doing this on fin n doesn't seem to work because it's not universe-polymorphic and the category wants objects at level u, so perhaps what I really want is a polymorphic pfin.