member of set used as member of corresponding type

Stream: general

[Kris Brown]

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?

[Kris Brown]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kris Brown]

Thanks!

[Kris Brown]

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.

[Reid Barton]

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

[Reid Barton]

This definitely should be possible though

[Mario Carneiro]

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

[Kris Brown]

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

[Mario Carneiro]

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

[Mario Carneiro]

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