Prod of inhabited is inhabited, TPIL Ch 7

Stream: new members

[Quinn Culver]

Following the advice in Chapter 7 of Theorem Proving in Lean, I'm trying to show that the product of inhabited types is inhabited. Thus I've written the following theorem.

theorem prod_inhab (a : inhabited α) (b : inhabited β): (inhabited (α × β))  :=
begin
 sorry
end

exact prod.inhabited works, but I'd rather construct the inhabitants myself (as suggested here).

I think something like exact (a,b) ought to work, but I can't get it to.

The output of #reduce prod .inhabited suggests somehow using default, but I cannot get that to work either.

[Kevin Buzzard]

inhabited is not a prop so this should not be a theorem. Is this Lean 3 or Lean 4? Did you read how to make instances of a structure? You want

:=
{ field1 := term1,
  field2 := term2,
  ... }

[Quinn Culver]

Doesn't the goal ⊢ inhabited (α × β) mean I'm trying to construct a term of type inhabited (α × β)? And isn't that just what I should be wanting to do?

[Quinn Culver]

This is Lean 3.

[Eric Wieser]

Kevin's remark above meant "this should not be a theorem, it should instead be a def"

[Eric Wieser]

exact (a,b) doesn't work because this is a term of type inhabited α × inhabited β not inhabited (α × β)

[Bulhwi Cha]

Quinn Culver said:

I think something like exact (a,b) ought to work, but I can't get it to.

This works:

def prod_inhab {α β : Type*} [inst_α : inhabited α] [inst_β : inhabited β] :
  inhabited (α × β) :=
match inst_α, inst_β with
| inhabited.mk a, inhabited.mk b := inhabited.mk (a, b)
end

[Eric Wieser]

That's still a pretty weird way to spell it. src#prod.inhabited is the best way to spell it, or the slightly more verbose

instance [inhabited α] [inhabited β] : inhabited (α × β) :=
{ default := (default, default) }

[Eric Wieser]

Hopefully it should be obvious what's going on when compared to docs#prod.has_zero,

instance [has_zero α] [has_zero β] : has_zero (α × β) :=
{ zero := (0, 0) }

[Bulhwi Cha]

Eric Wieser said:

That's still a pretty weird way to spell it. src#prod.inhabited is the best way to spell it, or the slightly more verbose

instance [inhabited α] [inhabited β] : inhabited (α × β) :=
{ default := (default, default) }

I think this looks confusing. The two defaults of the pair aren't necessarily the same, but they look the same.

[Patrick Massot]

It still looks much clearer than your version.

[Bulhwi Cha]

It does only when a learner understands that the pair is the same as (@default α inst_α, @default β inst_β). If they know this, then I have no problem with them using default to solve the exercise.

[Bulhwi Cha]

Chapter 7 of #tpil presents inhabited as follows:

inductive inhabited (α : Type*)
| mk : α → inhabited

It doesn't seem to mention anything about default.

[Eric Wieser]

Bulhwi Cha said:

I think this looks confusing. The two defaults of the pair aren't necessarily the same, but they look the same.

Would you make the same complaint about my 0s in the other example?

[Eric Wieser]

Bulhwi Cha said:

Chapter 7 of #tpil presents inhabited as follows:

inductive inhabited (α : Type*)
| mk : α → inhabited

Ah, then this is not the same as src#inhabited, so I guess your approach is the only one available

[Bulhwi Cha]

Yes. Maybe that's why my solution, which I wrote in January, looked the way it is.

[Bulhwi Cha]

Eric Wieser said:

Would you make the same complaint about my 0s in the other example?

I'd be happy if there were an option to make the zeros look different. Sometimes I want it, and sometimes I don't.

[Eric Wieser]

Well (default : α) and (0 : α) are an option

[Bulhwi Cha]

Hmm, I also want to see things like $0_\N$ and $0_\verb!Pos!$ from the Lean Infoview.

[Eric Wieser]

set_option pp.numeral_types true or something

[Quinn Culver]

It seems all of the suggested methods/solutions use techniques that come after chapter 7 in #tpil. Is there a (good) solution that doesn't?

[Bulhwi Cha]

I read #tpil4, so I'm not certain this is fine:

def prod_inhab {α β : Type*} [inst_α : inhabited α] [inst_β : inhabited β] :
  inhabited (α × β) :=
let ⟨a⟩ := inst_α in
let ⟨b⟩ := inst_β in
⟨(a, b)⟩

This proof was adapted from https://github.com/mccorvie/tpil4/blob/0cc46c02ac2336628ce86b334b21a9ab909d3ea5/TPIL4-ch7.lean#L104-L108.

[Kyle Miller]

Generally naming instance arguments doesn't feel like good style, but what you write works. Also, usually destructuring objects suggests that code isn't using the correct interface (unless it's something like and where destructuring is considered to be part of the interface). In tactic proofs in Lean 3, destructuring instance arguments is disallowed unless you wrap it in unfreezingI { ... } to update the instance cache.

I think the "right" answer is what Eric wrote:

instance [inhabited α] [inhabited β] : inhabited (α × β) :=
{ default := (default, default) }

This is because it's using the main interface to inhabited, which is the default function. If you don't like that it doesn't show types, then you're free to write

instance [inhabited α] [inhabited β] : inhabited (α × β) :=
{ default := (@default α, @default β) }

or

instance [inhabited α] [inhabited β] : inhabited (α × β) :=
{ default := ((default : α), (default : β)) }

The fact the type is implicit isn't a key feature of the interface, and I'd say it's mostly a convenience since often you'd otherwise write default _.

[Kyle Miller]

Variations on this is fine too:

instance [inhabited α] [inhabited β] : inhabited (α × β) := ⟨(default, default)⟩

[Kyle Miller]

But I'm just saying all this from the perspective of working with things in common practice.

[Kyle Miller]

Hmm, how quickly things change. I forgot that there was ever a time when the argument to default was explicit, but it was just a year ago: https://github.com/leanprover-community/lean/commit/7cb84a2a93c1e2d37b3ad5017fc5372973dbb9fb

[Kyle Miller]

If for exercise reasons you are stuck with inhabited as an inductive instead of a structure, then I would suggest defining default yourself (which does use destructuring, but that's ok because it's internal to an API you're defining) and then use that.