ite types

Stream: new members

[Bjørn Kjos-Hanssen]

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]

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

[Bjørn Kjos-Hanssen]

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]

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

[Bjørn Kjos-Hanssen]

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

[Reid Barton]

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]

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]

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

[Kevin Buzzard]

So it is!

[Reid Barton]

as long as you're using the constructive decidable instance

[Bjørn Kjos-Hanssen]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Bjørn Kjos-Hanssen]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Bjørn Kjos-Hanssen]

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

[Mario Carneiro]

or other types

[Reid Barton]

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

[Mario Carneiro]

yeah that's what I mean

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

apparently we have a definition irrational :thinking:

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

(deleted)

[Bjørn Kjos-Hanssen]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Bjørn Kjos-Hanssen]

That looks promising, although I get invalid return type

[Mario Carneiro]

It should just be U there, not U n k

[Bjørn Kjos-Hanssen]

@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]

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]

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

[Reid Barton]

(Σ 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]

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]

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

[Bjørn Kjos-Hanssen]

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]

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]

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

[Eric Wieser]

That syntax is docs#psigma, right?