Why doesn't exists.intro give err for witness of wrong type

Stream: new members

[Kevin Sullivan]

Here's a proof that 7 is even. Why does exists.intro accept 3.5 as an argument, given that m is declared to be of type nat?

def isEven (n: ℕ) : Prop :=
  ∃ m : ℕ, n / m = 2

theorem sevenIsEven : (isEven 7) :=
begin
unfold isEven,
apply exists.intro 3.5,
apply rfl,
end

[Johan Commelin]

Try it with 3 instead. Should work.

[Johan Commelin]

Probably 3.5 is coerced into 3 : nat or something like that.

[Johan Commelin]

Note that your definition of isEven is not what we usually mean with being even, because n / m is not what we usually mean with n / m.

[Simon Hudon]

If you use set_option pp.numerals false you see that 3.5 gets encoded as bit1 (bit1 (has_one.one ℕ)) / bit0 (has_one.one ℕ), which, as Johan points out, is a natural number because of rounded division.

[Simon Hudon]

((bit1 (bit1 (has_one.one ℕ)) / bit0 (has_one.one ℕ)) is 7 / 2)

[Johan Commelin]

I must say that I would rather get a syntax error at this point.

[Simon Hudon]

One way to make this happen is to look at one of @Kevin Buzzard suggestions and distinguish between proper division (/) and integer division (÷) (and the same can be said for subtraction vs pointed subtraction) and make sure that integers and natural numbers are only equipped with integer division. This way, expressing fractional numbers as division wouldn't work when fractional numbers aren't available.

[Kevin Buzzard]

Here's a proof that 7 is even.

Just to be clear, what's happening here is that division is maybe not what you think it is. 7 / 3 = 2, because 7 / 3 is declared to be of type nat.

[Simon Hudon]

Right. And somehow, integer division doesn't seem to mesh with fractional numbers. If we were to express integer division as ÷ and a separate type class, 3.5 would not be a valid natural number

[Kevin Sullivan]

Right. And somehow, integer division doesn't seem to mesh with fractional numbers. If we were to express integer division as ÷ and a separate type class, 3.5 would not be a valid natural number

Ok. Yes. This is slightly disturbing, but I understand.

def x : nat := 3.5

x is now 3.