nat = int

Stream: general

[Kenny Lau]

Is nat = int consistent with Lean?

[Mario Carneiro]

yes

[Mario Carneiro]

but it will make the VM not like you

[Kenny Lau]

good lord

[Kenny Lau]

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

[Kevin Buzzard]

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

[Mario Carneiro]

axiom nat_eq_int : nat = int

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

[Kevin Buzzard]

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

[Kevin Buzzard]

equiv of types -- that I understand.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

I'm not surprised

[Chris Hughes]

Did you teach them the truth table definition of implies?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

But this is somehow the same issue.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

This is bad because you can make the VM crash

[Kevin Buzzard]

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

[Kevin Buzzard]

If the kernel's happy, I'm happy

[Chris Hughes]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I have strong evidence in the direction of a proof

[Kevin Buzzard]

Fair enough.

[Mario Carneiro]

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

[Kevin Buzzard]

Aah I see equiv has popped up again

[Kenny Lau]

maybe we should add that as an axiom

[Kenny Lau]

just like how we added propext as an axiom

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

which has to do with the other thread

[Kenny Lau]

Type u even

[Chris Hughes]

It doesn't type check

[Kevin Buzzard]

oh yeah

[Kenny Lau]

oh

[Kevin Buzzard]

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

[Kenny Lau]

use \to

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Patrick Massot]

We all want the same tactic: rw_that_just_works

[Mario Carneiro]

this is a difficult research question

[Mario Carneiro]

the problem is always type dependency

[Kenny Lau]

What is type erasure?

[Kevin Buzzard]

this is a difficult research question

Mathematicians can do it in their heads!

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Andrew Ashworth]

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

[Chris Hughes]

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]

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]

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

[Mario Carneiro]

or type theory

[Patrick Massot]

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

[Patrick Massot]

That's the proper way for brave men

[Mario Carneiro]

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]

it is much easier to read the reference typecheckers like trepplein