list unit

Stream: lean4

[Kevin Buzzard]

attribute [class] unit
attribute [instance] unit.star

inductive list_unit
| nil : list_unit
| cons [hd : unit] (tl : list_unit) : list_unit

When a mathematician writes $\N$ they do not mean nat. They mean any object whatsoever, in any type theory or set theory or whatever, which offers the interface of nat, i.e.

nat : Type -- or some more type object like `Type u`, I explicitly do not care about universes
nat.zero : nat
nat.succ : nat → nat
nat.rec : <principles of induction and recursion written in appropriate foundational theory>

An example of an object offering this interface is list unit, and the reason it offers this interface is that the internal structure of list unit is to my naive mathematician's eyes "literally exactly the same object" as the internal structure of nat. Am I completely naive in wanting the ring tactic to work "automatically" on list unit in Lean 4? I have no understanding of the issues here I'm afraid.

[Kevin Buzzard]

PS Lean 4:

attribute [class] Unit
-- invalid 'class', declaration 'Unit' must be inductive datatype or structure

[Kevin Buzzard]

Can we prove List Unit = Nat in Lean 4?

[Daniel Fabian]

I was dealing with a bit of related question not too long ago, and from what I understand, the CIC cannot prove two inductive types are the same. There is a special case where you can make a cardinality argument that you could prove Unit \ne Nat, but that only holds because of cardinality.

[Kevin Buzzard]

What is interesting in this particular case is that I am explicitly observing that what we in some sense are told is the implementation of Nat, namely

inductive Nat : Type
| Zero : Nat
| Succ : Nat -> Nat

is literally what we are told is the implementation of List Unit, modulo some noise which a machine (the type class inference system) can deal with.

[Kevin Buzzard]

Is there some way that Lean 4 can bolt these inductive types together under the hood?

[Daniel Fabian]

let me put it this way. I think there is no reason, why we couldn't write a meta-program that takes a proof w.r.t. Nat and turn it into one w.r.t. List Unit. On the other hand, you are asking, if we can prove \|- Nat = List Unit and I think the latter is not possible in CIC.

[Daniel Fabian]

in fact, I am doing something fairly simple with my construction for inductive predicates. The user writes a proof w.r.t. their inductive type. Then I introduce a new type which has more contextual information, I take the original prove and re-prove it w.r.t. my new type. After that I have enough contextual information to eliminate recursion. Thus proving structural recursion.

[Daniel Fabian]

your taking a Nat proof, turning it into List Unit proof should be simpler, in principle.

[Scott Morrison]

@Kevin Buzzard, I don't understand why you think anything might be different in Lean 4 vs Lean 3 here.

[Scott Morrison]

Nothing about the axiomatics is changing, is it?

[Daniel Fabian]

nope, the axioms are the same, afaik. The kernel is slightly different insofar as it does mutually recursive inductive types, but that doesn't change the set of provable theorems, I don't think.

[Kevin Buzzard]

@Daniel Fabian I sometimes want abel to work for commutative multiplicative groups (for example when I am doing calculations in commutative rings which ultimately reduce to explicit messy problems not containing zero or add). I was always told that in theory abel could work for multiplicative groups but AFAIK it still doesn't.

-- Lean 3
import tactic
import data.complex.basic -- or whatever one needs

example (X : Type) [add_comm_monoid X] (a b c d e : X) :
  a + (b + c + d + e) = (a + b + c) + (d + e) := by abel

instance foo (X : Type) [field X] : comm_monoid X := infer_instance


example (X : Type) [field X] (a b c d e : X) :
  a * (b * c * d * e) = (a * b * c) * (d * e) := by abel -- fails

[Daniel Fabian]

ah, I see. That kind of thing, I think should be possible to do. But it wouldn't something that's happening at the axiomatic level, but rather at the meta-programming level. I.e. the abel tactic would have to learn how to turn X into an add_comm_monoid and then it should work.

[Daniel Fabian]

presumably, already today, you could somehow get an add_comm_monoid X instance into the local context and then abel would be happy?

[Kevin Buzzard]

Scott Morrison said:

Kevin Buzzard, I don't understand why you think anything might be different in Lean 4 vs Lean 3 here.

Scott for me Lean 3 and Lean 4 _are_ the same, in the sense that I have literally zero understanding of the implementation of the Lean code in some other language e.g. C++ or C or whatever Lean is written in or compiles to or whatever. I am just observing that in some real way these objects are identical in the sense that they have been constructed using identical constructors. Interally why can't Lean just bolt its understanding of Nat onto List Unit is my question, but as I've said before, I don't know what I'm talking about. Lean 4 will only let me as a non-meta Lean user to talk about Nat via its interface, so any algorithm I have which works via the interface should work for any implementation of the interface, right?

[Daniel Fabian]

but the point is you are not coding against an interface, but against the concrete Nat type. In a sense if you defined a class of Nat-like things with a base case and a successor case, only then would you be coding against the interface.

And in this latter scenario, we definitely would hope that two instances, one for Nat and one List Unit would, indeed, be able to re-use the same proof.

[Kevin Buzzard]

I genuinely have no idea what you mean by "the concrete Nat type". By a Type I mean "a closed box of information", or "What a ZFC person calls a set"

[Daniel Fabian]

the "concrete Nat type" is that one inductive definition inductive Nat ..., not something isomorphic to it, but literally just that one. A second definition inductive Nat' that has exactly the same structure is distinct from it. And they are not provably same or provably distinct.

Your theorems talk about properties of the first definition of Nat. They talk about what are the properties of that one definition only.

[Daniel Fabian]

When you want to transfer your knowledge, you must not mention Nat in the theorem statement anywhere. So your first example about monoids is a good example of something that is not specific.

[Eric Wieser]

Right; even in lean 3, you can't prove unit1 = unit2 given inductive unit1 | star and inductive unit2 | star

[Daniel Fabian]

Just out of pure interest, does anyone here know if adding an axiom saying that two types are the same, if there is a bijection between them is inconsistent? To me, without knowing much at all about HoTT, it seems related to the univalence axiom which I think is known to be inconsistent with the rest of CIC.

[Eric Wieser]

If that is inconsistent, is there a weaker axiom that says two types are equal if their constructors match?

[François G. Dorais]

I think @Mario Carneiro 's reduction to W-types can answer this. I think two types with the exact same constructors, in the same order, would map to the same W-type, but Mario is much more aware of the technical details for this reduction.

[Mario Carneiro]

Yes, that axiom is consistent, because it is validated by the cardinality model (where types are cardinalities and all the term constructors go through chosen bijections)

[Mario Carneiro]

You can't require that the bijection has any particular properties though; this is where HoTT fails, because it wants the bijections to be coherent with each other

[Mario Carneiro]

Eric Wieser said:

If that is inconsistent, is there a weaker axiom that says two types are equal if their constructors match?

This axiom is already validated by the model I construct in the lean type theory paper, because inductive types are represented using a mu operator and these would get mapped to the same expression. To recover nominal types you have to stick a natural number index on the mu operator which serves no purpose except to make unit1 and unit2 different expressions

[Mac]

Mario Carneiro said:

To recover nominal types you have to stick a natural number index on the mu operator which serves no purpose except to make unit1 and unit2 different expressions

Couldn't one just wrap the inductive in a structure to create distinct types? Because, if I am not mistaken, structures and inductive are distinct notions in Lean 4. If so, being able to prove equality between inductive types while permitting nominal distinction through structures seems like it could be a great extension to Lean.

[Mario Carneiro]

I'm talking about the mathematical modeling of lean's type system, structure doesn't exist at that level

[Mario Carneiro]

In lean as implemented, the "useless natural number index" that I mention is represented as the name of the inductive type itself. You can't have two distinct inductive types with the same name in lean

[Mario Carneiro]

Also, your proposed method wouldn't work because structure is just a wrapper around inductive in the kernel, so if inductive is a structural type then structure won't be a nominal type because it's the same thing

[Daniel Fabian]

So using this construction you get nominal types, which would mean String \ne Nat becomes provable... But that definitely won't prove that Unit1 = Unit2. Quite the opposite in fact

[Mac]

Mario Carneiro said:

Also, your proposed method wouldn't work because structure is just a wrapper around inductive in the kernel, so if inductive is a structural type then structure won't be a nominal type because it's the same thing

Ah. So in order to support inductive equality and nominal types, some kind of special attribute / type would need to be added to mark a given type as nominal and the rest could then ignore there nominal differences. Unfortunately, that does sound like to large of an undertaking. :(

[Mario Carneiro]

The larger undertaking would be adding "mu types" to lean, actually

[Mario Carneiro]

there is no term constructor for making inductive types

[Mario Carneiro]

instead you have to wrap every application of that term constructor behind a new declaration

[Mario Carneiro]

Having it as a term constructor makes it much more reasonable why it should be considered a "no axioms" construction even though it quite clearly adds constants to the system

[Mario Carneiro]

I'm not sure structural inductive types is a good idea in practice though. Inductive specs are complicated and I would hate for yet another big and complicated thing to get involved in defeq determinations

[Mario Carneiro]

I would much rather see eta for structures, which is useful in practice, rather than unit1 = unit2 which is something you would only write down if you are probing lean's axioms