finmap inside an inductive type

Stream: new members

[Guilherme Espada]

I'm trying to define an inductive type, of which one of the parameters is a finmap. Like this:

inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype
| ty_record (m: finmap (λ(x:string),ttype)): ttype

Lean reports inductive type being declared can only be nested inside the parameters of other inductive types. How can I work around this limitation?

[Guilherme Espada]

I tried working around it by defining my own map-like structure:

@[derive decidable_eq]
inductive recordmap (T : Type u)
| nil : recordmap
| cons (k:string) (v : T) (tl : recordmap) : recordmap

@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype
| ty_record (m: (recordmap ttype)): ttype

However, this errors out with:

tactic.mk_instance failed to generate instance for
  decidable_eq _nest_1_1.ttype

I definitely need decidable_eq. How can I fix this problem?

[Kenny Lau]

Looks like you would need to construct dec eq yourself

[Guilherme Espada]

Is there a document that details how to do so?

[Horatiu Cheval]

docs#decidable_eq, and more generally docs#decidable. In general, to prove p : Prop is decidable you need to provide a proof either for it or for its negation (as attested by the is_false and is_true constructors of decidable)

[Kevin Buzzard]

import tactic

@[derive decidable_eq]
inductive recordmap (T : Type u)
| nil : recordmap
| cons (k:string) (v : T) (tl : recordmap) : recordmap

inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype
| ty_record (m: (recordmap ttype)): ttype

namespace ttype

instance : decidable_eq ttype
| (ty_func l r) ty_bool := is_false (by simp)
...

That sort of thing.

[Guilherme Espada]

Alright, that's very helpful thanks. Another question: how can I prevent library_search from cheating by importing classical?

[Kevin Buzzard]

I'm afraid that mathlib has made a design decision to be resolutely classical and you're not the first person to ask for it to be switched off but it's difficult.

[Horatiu Cheval]

But I noticed that following (I am not sure whether it's a problem or not)

@[derive decidable_eq]
inductive recordmap (T : Type u)
| nil : recordmap
| cons (k:string) (v : T) (tl : recordmap) : recordmap

#check @recordmap.decidable_eq
-- recordmap.decidable_eq : Π (T : Type u_1) [a : decidable_eq T], decidable_eq (recordmap T)
-- only records of type with decidable_eq have decidable_eq


-- @[derive decidable_eq]
inductive ttype
-- | ty_func (l r:ttype): ttype
-- | ty_bool : ttype
| ty_record (m: (recordmap ttype)): ttype

instance (a b : ttype) : decidable (a = b) :=
begin
  cases a, cases b,
  -- it seems you need decidable_eq for records of ttype,
  -- but for that you need to already know that ttype has decidable_eq, i.e. what we're trying to prove
  have := recordmap.decidable_eq ttype, --doesn't work
end

Is this right?

[Kevin Buzzard]

Why not do induction instead of cases?

[Guilherme Espada]

It seems to me that induction should work here

[Guilherme Espada]

but I'm just cheating with classical for now

[Horatiu Cheval]

Kevin Buzzard said:

Why not do induction instead of cases?

Well, it seems that for me it doesn't generate a hypothesis of induction in that case, so it's the same as cases:

instance (a b : ttype) : decidable (a = b) :=
begin
  induction a; induction b,
  case ty_record ty_record
  {
--     case ttype.ty_record ttype.ty_record
--     ab: recordmap ttype
--     ⊢ decidable (ttype.ty_record a = ttype.ty_record b)
  }
end

[Horatiu Cheval]

Am I missing the right induction?

[Kevin Buzzard]

Perhaps the problem with your simplification is that your simplified type is empty? Or maybe I'm wrong?

[Horatiu Cheval]

If you mean that previously I commented out the ty_func and ty_bool cases, I uncommented them before writing the snippet, and it's the same behavior.

[Kevin Buzzard]

I am not an expert on these induction matters, I'm afraid.

[Horatiu Cheval]

I also noticed that if I try

@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype
| ty_record (m: (recordmap ttype)): ttype

then it fails with "'ttype' is not an inductive type", so maybe it has something to do with that.

[Kevin Buzzard]

I think that if you know what you're doing (and I don't) then it should be possible to prove this sort of thing by induction, perhaps with the equation compiler. It seems to me that you want to prove decidable equality of both ttype and recordmap ttype at once. The following failed attempt to prove decidable equality directly indicates this, at least: I'd be done if I also had a proof of decidable eq for the "simpler" recordmap terms. But as I say, I don't really know what the tricks are in this area, I'm a mathematician, I only do induction on nats.

instance (a b : ttype) : decidable (a = b) :=
begin
  induction a generalizing b,
  induction a generalizing b,
  { induction b,
    induction b,
    { apply is_true,
      refl },
    { apply is_false,
      simp } },
  induction b generalizing a_v a_tl,
  induction b generalizing a_v a_tl,
  { apply is_false,
    simp },
  -- now we're done if we can decide a_tl = b_tl
  sorry
end

[Horatiu Cheval]

Ok, I think I understand your point. Thanks for explaining the idea

[Mario Carneiro]

@Horatiu Cheval For these sorts of definitions, I always recommend not using nested inductives and instead rolling your own with a plain inductive type, which supports the correct induction principle

import logic.basic tactic.cache

inductive ttype_or_list : bool → Type
| ty_func (l r : ttype_or_list ff) : ttype_or_list ff
| ty_bool : ttype_or_list ff
| ty_record (m : ttype_or_list tt) : ttype_or_list ff
| tyl_nil : ttype_or_list tt
| tyl_cons (k:string) (v : ttype_or_list ff) (tl : ttype_or_list tt) : ttype_or_list tt

def ttype := ttype_or_list ff

instance {c} : decidable_eq (ttype_or_list c) :=
begin
  intros a b,
  induction a with al ar IH1 IH2 a _ ak av al generalizing b; cases b,
  case ty_func ty_func : bl br { exactI decidable_of_iff' (al = bl ∧ ar = br) (by simp) },
  case ty_bool ty_bool { exact decidable.is_true rfl },
  case ty_record ty_record : b { exactI decidable_of_iff' (a = b) (by simp) },
  case tyl_nil tyl_nil { exact decidable.is_true rfl },
  case tyl_cons tyl_cons : bk bv bl {
    exactI decidable_of_iff' (ak = bk ∧ av = bv ∧ al = bl) (by simp) },
  all_goals { apply decidable.is_false, simp },
end

instance : decidable_eq ttype := ttype_or_list.decidable_eq

[Horatiu Cheval]

Thanks for working out the example. Though the initial question was asked by @Guilherme Espada, it will certainly be, for me too, a good future reference on how to rearrange nested inductives