How to define Pi data?

Stream: new members

[Malvin Gattinger]

How can I define values of a $\Pi$ type when I need to distinguish the elements? Whenever I do intros then I can no longer distinguish different cases. This might be more of a basic type theory and less of a lean question ;-)

import data.finset.basic
import data.finset.pimage

@[simp]
def mySets : finset (finset ℕ) := { {1,2}, {3,4} }

def multiThing : Π (ns : finset ℕ), ns ∈ mySets → ℕ := begin
  intros ns ns_in_mySets,
  cases ns_in_mySets,
  -- error: induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop
  -- wanted: if it is the first set, return this ... if it is the second set do this ...
end

[Kyle Miller]

This is is what decidable is for: it lets you take propositions and make decisions about what the value will be in a definition.

One solution is to use an if/then/else chain. For the final impossible case, you use exfalso, which turns the result into a Prop (false) and then you can do cases ns_in_mySets. This could be refined more, but it's just to demonstrate the idea:

def multiThing : Π (ns : finset ℕ), ns ∈ mySets → ℕ := begin
  intros ns ns_in_mySets,
  refine if h1 : ns = {1, 2} then _ else if h2 : ns = {3, 4} then _ else _,
  { exact 1, },
  { exact 2, },
  { exfalso,
    cases ns_in_mySets,
    { exact h1 ns_in_mySets, },
    { simp! at ns_in_mySets,
      exact h2 ns_in_mySets, } }
end

[Kyle Miller]

Here's another way I'd probably organize it:

def multiThing (ns : finset ℕ) (hns : ns ∈ mySets) : ℕ :=
if h1 : ns = {1, 2} then 1
else if h2 : ns = {3, 4} then 2
else begin
  exfalso,
  simp only [mySets, finset.mem_insert, finset.mem_singleton] at hns,
  cases hns; solve_by_elim,
end

[Malvin Gattinger]

Aha, many thanks!!