Zulip Chat Archive

Stream: general

Topic: member of set used as member of corresponding type


view this post on Zulip Kris Brown (Jul 31 2020 at 08:59):

I'm a bit unclear about working with sets which are coerced to types. For instance, I have a finset which can be coerced to a set which can be coerced to a Type:

  @[simp] def finset_to_type {α: Type} (b: finset α): Type := ( b : set α)

I'm interested in this because I have an inductive type which would ideally look like this :

  with Struct: string  Type
   | mk (name: string) (fields: finset (string × PrimitiveType)):  Struct name

This won't compile, since the PrimitiveType is being mutually inductively defined and therefore cannot be inside a non-inductive-type like finset. So instead I could just have some finite type of string keys and a map from those to values.

  with Struct: string  Type
   | mk (name: string) (fields: finset string)
        (vals: (finset_to_type fields)  PrimitiveType): Struct name

In order for me to actually use this, I need a function like the following:

def finset_str_map: Π{s: finset string} {α: Type},
  (finset_to_type s  α)   string  option α
    | s α f key := if h: key  s
      then some (f (by {simp, rw finset.has_lift,
                        have h': key  s, by {sorry},
                     -- I don't actually know what to do here
                       -- rw set.mem_def at h',
                       --rw set.has_coe_to_sort.coe ↑s at h',
                        --exact h'
                         sorry}))
      else none

Is there a simple way to express that, if I have an element of a finite set, that I can treat it as a member of the corresponding type?

view this post on Zulip Kris Brown (Jul 31 2020 at 09:10):

MWE

import data.finset.basic

  @[simp] def finset_to_type {α: Type} (b: finset α): Type := ( b : set α)

  mutual inductive PrimType, Struct
  with PrimType: Type
   | pBool:  bool   PrimType
   | pInt:     PrimType
   | pStruct {s: string}: Struct s  PrimType
  with Struct: string  Type
   | mk (name: string) (fields: finset string)
        (vals: (finset_to_type fields)  PrimType): Struct name


def finset_str_map: Π{s: finset string} {α: Type},
  (finset_to_type s  α)   string  option α
    | s α f key := if h: key  s
      then some (f (by {sorry}))
      else none

view this post on Zulip Mario Carneiro (Jul 31 2020 at 09:36):

To slightly #xy your problem, I suggest using two foralls instead of a function over the subtype in the mutual inductive. You can do something like this:

mutual inductive PrimType, Struct
with PrimType : Type
| pBool : bool   PrimType
| pInt :   PrimType
| pStruct {s : string} : Struct s  PrimType
with Struct : string  Type
| mk (name : string) (fields : finset string)
  (vals :  s  fields, PrimType) : Struct name

def Struct.fields :  {s}, Struct s  finset string
| _ (Struct.mk _ f _) := f

def Struct.vals :  {s} (c : Struct s) (s  c.fields), PrimType
| _ (Struct.mk _ _ v) := v

def Struct.get {s} (c : Struct s) (key : string) : option PrimType :=
if h : key  c.fields then some (c.vals _ h) else none

view this post on Zulip Mario Carneiro (Jul 31 2020 at 09:38):

in the original question though you can replace the by {sorry} with ⟨key, h⟩

view this post on Zulip Kris Brown (Jul 31 2020 at 10:11):

Thanks!

view this post on Zulip Kris Brown (Aug 01 2020 at 00:14):

Does this strategy make it impossible to show that two Structs are decidably equal? The amount of data in the mapping is finite, but it looks like I have to prove equality for a function ranging over a (seemingly) infinite domain.

mutual def primtype_eq, struct_eq
with primtype_eq: ...

with struct_eq: Π(s: string), decidable_eq (Struct s)
 | _ ( Struct.mk a b c) (Struct.mk d e f) := by {
        simp,
        have p: decidable (a=d), by exact string.has_decidable_eq a d,
        have q: decidable (b=e), by exact finset.has_decidable_eq b e,
        cases p with pf pt,
            {simp [pf], exact decidable.false}, -- different names
        {rw pt, simp, cases q with qf qt,
            {simp [qf], exact decidable.false}, -- different fields
        subst qt,
        have r: decidable (c=f), by sorry, -- TODO prove maps are equal (will need primtype_eq)
        cases r with rf rt,
            {simp [rf], exact decidable.false}, -- different values

        subst rt, simp, exact decidable.true}} --

Right now the strategy seems like I should prove some lemmas saying that functions from a finite domain into a codomain (w/ decidable equality) have decidable equality, and then convince Lean that (due to the constraint imposed by the argument) that Struct.vals is effectively a function from a type with a finite domain. I didn't see anything directly related to these two goals in mathlib, but it seems in principle do-able.

view this post on Zulip Reid Barton (Aug 01 2020 at 00:20):

May I introduce you to classical.prop_decidable? :upside_down:

view this post on Zulip Reid Barton (Aug 01 2020 at 00:29):

This definitely should be possible though

view this post on Zulip Mario Carneiro (Aug 01 2020 at 00:39):

I think I should probably mention my usual advice at this point, which is that if you want to do nontrivial proofs with the type you should avoid mutual inductive and roll your own

view this post on Zulip Kris Brown (Aug 01 2020 at 00:53):

I'm interested but don't know what rolling my own would entail. Is there an example of what you mean by this?

view this post on Zulip Mario Carneiro (Aug 01 2020 at 01:05):

I managed this:

import data.finset.basic

inductive PrimType : Type
| pBool : bool   PrimType
| pInt :   PrimType
| pStruct' (name : string) (fields : finset string)
  (vals :  s  fields, PrimType) : PrimType

instance : decidable_eq PrimType :=
begin
  intros a b, induction a generalizing b; cases b;
  try {{ apply decidable.is_false, rintro ⟨⟩ }},
  { exact decidable_of_iff (a = b) (by simp) },
  { exact decidable_of_iff (a = b) (by simp) },
  { refine if h : a_name = b_name then _ else decidable.is_false (by simp [h]),
    refine if h2 : a_fields = b_fields then _ else decidable.is_false (by simp [h2]),
    resetI, refine decidable_of_iff ( x hx, a_vals x hx = b_vals x (by rwa  h2)) _,
    subst h, subst h2, simp [function.funext_iff] },
end

@[derive decidable_eq]
structure Struct (name : string) :=
(fields : finset string) (vals :  s  fields, PrimType)

def PrimType.pStruct :  {s}, Struct s  PrimType
| s f, v := PrimType.pStruct' s f v

def Struct.get {s} (c : Struct s) (key : string) : option PrimType :=
if h : key  c.fields then some (c.vals _ h) else none

view this post on Zulip Mario Carneiro (Aug 01 2020 at 01:06):

In this case it's pretty easy to avoid a mutual inductive because Struct is just a package around the arguments of pStruct


Last updated: May 16 2021 at 21:11 UTC