## Stream: new members

### Topic: How to define Pi data?

#### Malvin Gattinger (Feb 02 2022 at 16:08):

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 (Feb 02 2022 at 17:35):

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 (Feb 02 2022 at 17:40):

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 (Feb 02 2022 at 17:52):

Aha, many thanks!!

Last updated: Dec 20 2023 at 11:08 UTC