Zulip Chat Archive

Stream: general

Topic: nat = int


Kenny Lau (Oct 09 2018 at 19:24):

Is nat = int consistent with Lean?

Mario Carneiro (Oct 09 2018 at 19:29):

yes

Mario Carneiro (Oct 09 2018 at 19:29):

but it will make the VM not like you

Kenny Lau (Oct 09 2018 at 19:29):

good lord

Kenny Lau (Oct 09 2018 at 19:30):

so how can a constructor of an inductive type construct itself...

Kevin Buzzard (Oct 09 2018 at 19:30):

Equality of types is terrifying. I just stick to equality of terms.

Mario Carneiro (Oct 09 2018 at 19:30):

axiom nat_eq_int : nat = int

#eval cast nat_eq_int.symm (-5) -- 2147483643

Kevin Buzzard (Oct 09 2018 at 19:30):

I am not sure I have a good feeling as to what equality of types means.

Kevin Buzzard (Oct 09 2018 at 19:31):

equiv of types -- that I understand.

Mario Carneiro (Oct 09 2018 at 19:32):

Unfortunately, as a cast off from HoTT, univalence is consistent in some weak forms

Mario Carneiro (Oct 09 2018 at 19:32):

but the VM assumes something much stricter, in order for type erasure to be sound

Kevin Buzzard (Oct 09 2018 at 19:39):

So an interesting thing happened in my lecture today. It was an interactive lecture and the students could vote on the questions I was asking, on their phones. And I asked them if "not P" was equal to "P implies false" and a lot of them said that these things were not equal.

Patrick Massot (Oct 09 2018 at 19:40):

I'm not surprised

Chris Hughes (Oct 09 2018 at 19:40):

Did you teach them the truth table definition of implies?

Kevin Buzzard (Oct 09 2018 at 19:40):

But they were all happy that these things were equivalent. I didn't tell them Lean's definition of "not P", I was doing basic propositional calculus, so the definition of "not" was "not false = true" and "not true = false" and that's it

Patrick Massot (Oct 09 2018 at 19:40):

Did you try on a room full of professional mathematicians next?

Kevin Buzzard (Oct 09 2018 at 19:40):

But this is somehow the same issue.

Kevin Buzzard (Oct 09 2018 at 19:41):

Two propositions can be equivalent, but it's a bit weird saying they are equal.

Kevin Buzzard (Oct 09 2018 at 19:41):

Especially when I told them that 2+2=4 and Fermat's Last Theorem were both true, and asked them if they thought that they were hence equal.

Mario Carneiro (Oct 09 2018 at 19:41):

aha, here's an example of a lie proposition from that axiom:

axiom nat_eq_int : nat = int
def lie : bool := cast nat_eq_int.symm (-int.of_nat (2^31)) < 0
theorem not_lying : lie = ff := rfl
#eval lie -- tt

Mario Carneiro (Oct 09 2018 at 19:41):

This is bad because you can make the VM crash

Kevin Buzzard (Oct 09 2018 at 19:42):

That's not bad -- that just means that you shouldn't rely on the VM

Kevin Buzzard (Oct 09 2018 at 19:42):

If the kernel's happy, I'm happy

Chris Hughes (Oct 09 2018 at 19:42):

It means you shouldn't introduce axioms and then rely on the VM.

Chris Hughes (Oct 09 2018 at 19:43):

But you shouldn't introduce axioms and rely on the kernel either. So I don't think that's a problem.

Mario Carneiro (Oct 09 2018 at 19:43):

it means that some axioms are consistent with the VM and others aren't, even if they are consistent with lean itself

Kevin Buzzard (Oct 09 2018 at 19:43):

Mario do you _know_ that nat = int is consistent with Lean (assuming maths is consistent etc)

Mario Carneiro (Oct 09 2018 at 19:44):

I have strong evidence in the direction of a proof

Kevin Buzzard (Oct 09 2018 at 19:44):

Fair enough.

Mario Carneiro (Oct 09 2018 at 19:44):

the more general statement is that two types with the same cardinality are consistently equal

Kevin Buzzard (Oct 09 2018 at 19:45):

Aah I see equiv has popped up again

Kenny Lau (Oct 09 2018 at 19:45):

maybe we should add that as an axiom

Kenny Lau (Oct 09 2018 at 19:45):

just like how we added propext as an axiom

Mario Carneiro (Oct 09 2018 at 19:45):

But type erasure, used in the VM, assumes that the only provable equalities are between objects with the same runtime representation

Kevin Buzzard (Oct 09 2018 at 19:45):

Is forall X Y : Type, equiv X Y iff X = Y consistent with Lean?

Mario Carneiro (Oct 09 2018 at 19:45):

which has to do with the other thread

Kenny Lau (Oct 09 2018 at 19:45):

Type u even

Chris Hughes (Oct 09 2018 at 19:45):

It doesn't type check

Kevin Buzzard (Oct 09 2018 at 19:46):

oh yeah

Kenny Lau (Oct 09 2018 at 19:46):

oh

Kevin Buzzard (Oct 09 2018 at 19:46):

nonempty (equiv X Y) iff X = Y or whatever

Kenny Lau (Oct 09 2018 at 19:46):

use \to

Mario Carneiro (Oct 09 2018 at 19:47):

You have to be careful not to run afoul of the counterexample to HoTT

Mario Carneiro (Oct 09 2018 at 19:49):

Consider the bnot : bool -> bool function, which swaps the two values. This is provably an equivalence in HoTT, so from univalence we get an equality ua bnot : bool = bool. It is provable in HoTT that cast (ua bnot) tt = ff, but cast rfl tt = tt and hence ua bnot != rfl, contradicting proof irrelevance

Kenny Lau (Oct 09 2018 at 19:50):

but you can't prove in lean that cast (ua bnot) tt = ff right

Mario Carneiro (Oct 09 2018 at 19:51):

In HoTT, this is provable because we know ua is the inverse of the natural function A = B -> A ~= B

Kevin Buzzard (Oct 09 2018 at 19:52):

@Patrick Massot this should sort out your heq problems:

import data.equiv.basic
axiom for_patrick :  (X Y : Type*), equiv X Y  X = Y

Kevin Buzzard (Oct 09 2018 at 19:52):

and apparently Mario thinks it's consistent, but just be careful with the VM OK?

Mario Carneiro (Oct 09 2018 at 19:53):

I strongly recommend against any axioms that don't obey type erasure

Chris Hughes (Oct 09 2018 at 19:53):

I don't think it helps. Patrick knows his Types are equal, he just can't rw using that equality.

Patrick Massot (Oct 09 2018 at 19:53):

We all want the same tactic: rw_that_just_works

Mario Carneiro (Oct 09 2018 at 19:54):

this is a difficult research question

Mario Carneiro (Oct 09 2018 at 19:54):

the problem is always type dependency

Kenny Lau (Oct 09 2018 at 19:54):

What is type erasure?

Kevin Buzzard (Oct 09 2018 at 19:54):

this is a difficult research question

Mathematicians can do it in their heads!

Patrick Massot (Oct 09 2018 at 19:56):

Then do you have example where all those subst or generalize tricks works? I haven't been able to find any math example

Kevin Buzzard (Oct 09 2018 at 19:58):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/Continuous.20Functions.20Preserve.20Limits/near/134675116

Kevin Buzzard (Oct 09 2018 at 19:58):

Rohan wanted to prove that if x0,x1,x2...x_0,x_1,x_2... tended to xx then x1,x2,x3,...x_1,x_2,x_3,... also tended to xx. We formalised the change of variables using filters and then Kenny proved it using subst

Mario Carneiro (Oct 09 2018 at 20:00):

the solution of course is extensional type theory but I might be contractually obligated to say that's silly

Andrew Ashworth (Oct 09 2018 at 20:02):

was OTT (https://github.com/leanprover/lean/issues/654) no good?

Chris Hughes (Oct 09 2018 at 20:07):

One thing I've wondered for a while is why does this work?

example : (0 : ) = eq.rec 0 (classical.choice eq.refl ℕ⟩) := rfl

Mario Carneiro (Oct 09 2018 at 20:15):

there is a kernel reduction rule eq.rec e h ~> e when h : a = a. Intuitively this is justified by using proof irrelevance to replace h with rfl and then iota reducing

Kevin Buzzard (Oct 09 2018 at 20:18):

Chris it looks like it's about time you learn C++

Mario Carneiro (Oct 09 2018 at 20:18):

or type theory

Patrick Massot (Oct 09 2018 at 20:22):

Kevin means learning type theory by reading C++ code of the Lean kernel

Patrick Massot (Oct 09 2018 at 20:23):

That's the proper way for brave men

Mario Carneiro (Oct 09 2018 at 20:30):

I should note that I have written a paper on this topic and I still haven't fully understood the kernel of lean

Mario Carneiro (Oct 09 2018 at 20:30):

it is much easier to read the reference typecheckers like trepplein


Last updated: Dec 20 2023 at 11:08 UTC