## Stream: new members

### Topic: ite types

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 18:31):

To make this work:

instance my_zero : has_zero (ite (2 ≤ 1) ℕ ℤ) := {zero := (0:ℤ)}


I guess I have to supply a proof that ¬ (2 ≤ 1), but where?

#### Mario Carneiro (Dec 17 2020 at 18:32):

by rw if_neg; [exact (0:int), norm_num]

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 18:35):

Hmm... this doesn't work

instance my_zero : has_zero (ite (2 ≤ 1) ℕ ℤ) := {
zero := by rw if_neg; [exact (0:int); norm_num]
}


#### Rob Lewis (Dec 17 2020 at 18:37):

I think it should be [exact (0:int), norm_num]

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 18:39):

exact (0:int); norm_num works. Thanks!

#### Reid Barton (Dec 17 2020 at 18:41):

You also don't have to do it this way, you could use the definition by exact {zero := (0 : ℤ)} or show has_zero ℤ, by apply_instance

#### Reid Barton (Dec 17 2020 at 18:43):

but this relies on definitional equality, so in some general situation, if you only have a proof of the condition of the ite, then these won't work

#### Kevin Buzzard (Dec 17 2020 at 18:44):

ite (2 ≤ 1) ℕ ℤ is definitionally ℤ?

So it is!

#### Reid Barton (Dec 17 2020 at 18:44):

as long as you're using the constructive decidable instance

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 18:46):

Ah... I actually do want something more complicated than 2 ≤ 1, more like this: 2^k ≤ 2^(2^(4-k)) - 1.

#### Reid Barton (Dec 17 2020 at 18:47):

I mean, it was always pretty unlikely someone would intentionally write ite (2 ≤ 1) ℕ ℤ.

#### Reid Barton (Dec 17 2020 at 18:47):

I think you'll find the system fighting you at every step if you go down this path

#### Reid Barton (Dec 17 2020 at 18:48):

probably a better approach is something like {x : \Z // 2^k ≤ 2^(2^(4-k)) - 1 -> x >= 0}

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 18:51):

Oh... so the x >= 0 is to choose between \N and \Z? How about choosing between arbitrary types there?

#### Reid Barton (Dec 17 2020 at 18:51):

well, I might be extracting the wrong assumptions from your choice of N and Z then

#### Reid Barton (Dec 17 2020 at 18:51):

like I'm assuming you're next going to ask how to define has_add, and then how to prove that x + 0 = x

#### Mario Carneiro (Dec 17 2020 at 18:52):

another option is to use an inductive type with constructors for N and Z

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 18:52):

I actually want more complicated types than N and Z, it was just a minimal (not) working example

or other types

#### Reid Barton (Dec 17 2020 at 18:52):

or maybe an inductive family that bakes this 2^k ≤ 2^(2^(4-k)) - 1 condition in somehow

#### Mario Carneiro (Dec 17 2020 at 18:53):

yeah that's what I mean

#### Mario Carneiro (Dec 17 2020 at 18:53):

in fact, you might find that the assumption isn't necessary in some situations

#### Mario Carneiro (Dec 17 2020 at 18:53):

which means that the inductive type is actually a union of several different types in general, which may or may not be a problem

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 18:56):

Say, if we replace N and Z by arbitrary types U and V, what becomes of the x >= 0 condition in

{x : \Z // 2^k ≤ 2^(2^(4-k)) - 1 -> x >= 0}


?

#### Reid Barton (Dec 17 2020 at 18:56):

this is an obviously useful condition which I don't think we have a way to express other than \ex (q : \Q), x = q

#### Reid Barton (Dec 17 2020 at 18:57):

apparently we have a definition irrational :thinking:

#### Reid Barton (Dec 17 2020 at 18:59):

oh with the new version you can't do it this way, of course

#### Reid Barton (Dec 17 2020 at 19:00):

this is a danger of "minimal", it encourages answerable questions, which is good, but they might not have too much relevance to the real question

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 19:00):

How about ite (2^k ≤ 2^(2^(4-k)) - 1) U V where U and V are types... is it bad to use ite here?
(Sorry for all the edits.)

#### Reid Barton (Dec 17 2020 at 19:01):

And of course the person with the question can't be expected to preserve exactly the relevant aspects of the question, otherwise they would probably be able to answer it themselves

#### Reid Barton (Dec 17 2020 at 19:03):

It's probably never a good idea to use ite on types

#### Eric Wieser (Dec 17 2020 at 19:05):

This sounds similar to my topic about using sum.elim U V as a type...

(deleted)

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 19:08):

How about this: how to implement types U_1, ... U_n where if (2^k ≤ 2^(2^(n-k)) - 1) then U_k= fin k(say) and otherwise U_k = finset (fin k) (say)

#### Reid Barton (Dec 17 2020 at 19:15):

well, hopefully you don't care about actual equality of types

#### Reid Barton (Dec 17 2020 at 19:16):

one possibility is

inductive U (n k : ℕ)
| mk₁ : (2^k ≤ 2^(2^(n-k)) - 1) → fin k → U n k
| mk₂ : ¬ (2^k ≤ 2^(2^(n-k)) - 1) → finset (fin k) → U n k


#### Reid Barton (Dec 17 2020 at 19:16):

but really, the question can't be answered from this perspective

#### Reid Barton (Dec 17 2020 at 19:17):

Types describe what you can do with something, and we have no idea what you want to do with these U_k

#### Reid Barton (Dec 17 2020 at 19:18):

It's hard enough to figure out the right definitions when you know what you're doing (literally)

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 19:20):

That looks promising, although I get invalid return type

#### Mario Carneiro (Dec 17 2020 at 19:20):

It should just be U there, not U n k

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 19:24):

@Reid Barton well briefly, I want to prove things about elements of the type Σ k, U k. Maybe your solution will do the trick!

#### Mario Carneiro (Dec 17 2020 at 19:28):

You can adapt the type reid gave to incorporate the sigma too:

inductive U (n : ℕ)
| mk₁ (k) : (2^k ≤ 2^(2^(n-k)) - 1) → fin k → U
| mk₂ (k) : ¬ (2^k ≤ 2^(2^(n-k)) - 1) → finset (fin k) → U


#### Reid Barton (Dec 17 2020 at 19:28):

if you only need this sigma type then you can just use off-the-shelf types

#### Reid Barton (Dec 17 2020 at 19:29):

(Σ k (H : 2^k ≤ 2^(2^(n-k)) - 1), fin k) ⊕ (Σ k (H : ¬ 2^k ≤ 2^(2^(n-k)) - 1), finset (fin k))

#### Reid Barton (Dec 17 2020 at 19:30):

That said, in a particular application you might want to use a custom type to get more meaningful names than sum.inr

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 20:54):

@Reid Barton that looks good although is there some typo?

#### Bjørn Kjos-Hanssen (Dec 17 2020 at 20:56):

Do you mean

(Σ k:ℕ, (2^k ≤ 2^(2^(n-k)) - 1)→ fin k) ⊕ (Σ k:ℕ, (¬ 2^k ≤ 2^(2^(n-k)) - 1) →  finset (fin k))


?

#### Floris van Doorn (Dec 18 2020 at 18:44):

You want to write your own definition that takes an x and returns the k. Here are some examples on how to do this, depending on how you choose to define the type:

import data.finset.basic

-- Reid's example (fixed)
def my_type (n : ℕ) : Type :=
(Σ' k (H : 2^k ≤ 2^(2^(n-k)) - 1), fin k) ⊕ (Σ' k (H : ¬ 2^k ≤ 2^(2^(n-k)) - 1), finset (fin k))

def my_k {n : ℕ} : ∀ (x : my_type n), ℕ
| (sum.inl ⟨k, H, x⟩) := k
| (sum.inr ⟨k, H, x⟩) := k

-- another way to define k
def my_k_alternate {n : ℕ} (x : my_type n) : ℕ :=
sum.elim psigma.fst psigma.fst x

-- maybe more convenient?
def my_type' (n : ℕ) : Type :=
Σ (k : ℕ), { x : fin k // 2^k ≤ 2^(2^(n-k)) - 1} ⊕ { x : finset (fin k) // ¬ 2^k ≤ 2^(2^(n-k)) - 1}

def my_k' {n : ℕ} (x : my_type' n) : ℕ :=
x.1

-- Mario's example
inductive U (n : ℕ)
| mk₁ (k) : (2^k ≤ 2^(2^(n-k)) - 1) → fin k → U
| mk₂ (k) : ¬ (2^k ≤ 2^(2^(n-k)) - 1) → finset (fin k) → U

open U

def U_k {n : ℕ} : ∀ (x : U n), ℕ
| (mk₁ k H x) := k
| (mk₂ k H x) := k


#### Bjørn Kjos-Hanssen (Dec 18 2020 at 20:25):

Awesome @Floris van Doorn . Had not heard of the modified Σ type Σ' before.

#### Eric Wieser (Dec 18 2020 at 21:37):

That syntax is docs#psigma, right?

Last updated: Dec 20 2023 at 11:08 UTC