Trying to get simple example to compile

Stream: lean4

[Andrew Cann]

Hi people. I'm completely new to lean and I thought I'd try out lean 4 since it's the latest and greatest version. The first thing I've tried to do is define a pair of mutually-inductive types. However I can't figure out the syntax. The examples I've found online don't work (presumably because they're for older versions) and the relevant page of the documentation just says "TODO".

This is my code:

mutual
  inductive Ctx : Type where
    | CRoot : Ctx
    | CCons : (parent : Ctx) -> (Ty parent) -> Ctx
  inductive Ty : Ctx -> Type where
end

Obviously this is wrong (somehow), but hopefully it's clear what I'm trying to do. Can someone show me the correct way to write this? Right now I just get "error: unknown identifier 'Ctx'" (referring to Ty : Ctx -> Type).

[Huỳnh Trần Khanh]

If you are new to Lean, you should be using Lean 3 instead because many important features are not yet implemented in Lean 4. Also, there might be endgame bugs (such as this) that are not yet known.

[Huỳnh Trần Khanh]

It's very unlikely that you can find decent documentation about Lean 4 right now.

[Sebastian Ullrich]

@Andrew Cann That is not a mutually inductive type (by Lean's definition) but an inductive-inductive type. Those are not supported by Lean's kernel, though also see https://github.com/javra/iit (very much WIP) by @Jakob von Raumer

[Andrew Cann]

@Huỳnh Trần Khanh Ah thanks. Maybe I'll try lean 3 instead then ...

@Sebastian Ullrich ... or maybe not. Damn. So I gather it's not possible to express this in Lean 3 either then? I'm giving lean a shot because agda is getting on my nerves, but I definitely need inductive-inductive types since I'm trying to formalize a type theory.

[Jakob von Raumer]

Lean 3 doesn't have inductive-inductive types either. I'm using Agda besides Lean as well, and I think it's still ahead when it comes to type theory formalizations. Lean also doesn't have a definitional eta rule for record types, which makes some things more difficult, too.

[Jakob von Raumer]

What exactly is Agda doing to get on your nerves?

[Andrew Cann]

@Jakob von Raumer Thanks, I'll just go back to Agda then.

I have a few complaints but the things that made me want to give up on it today are:
(a) Having to repeat myself ad-nauseam when writing functions that take a lot of arguments and have a lot of cases.
(b) Those function no longer type-checking when I add a new case, with the error pointing at a case that was already type-checking.
(c) Errors of the form such-and-such != such-and-such when checking ... where "such-and-such" and "such-and-such" are identical.
(d) Automatic proof search not being able to finds proofs that are completely trivial. eg. where the proof term is something like Set.

But I'll keep working around these things I guess :/

[Huỳnh Trần Khanh]

Probably tangential but is there any proof of false in the current version of Agda? Agda sounds like neat stuff but I heard somewhere on the internet that it might not be as reliable as Lean.

[Huỳnh Trần Khanh]

I have a few complaints but the things that made me want to give up on it today are

Well Lean 3 has its own quirks! But it is decently usable for me.

[Sebastian Ullrich]

Huỳnh Trần Khanh said:

Probably tangential but is there any proof of false in the current version of Agda? Agda sounds like neat stuff but I heard somewhere on the internet that it might not be as reliable as Lean.

https://github.com/agda/agda/issues?q=is%3Aopen+is%3Aissue+label%3Afalse

[Kevin Buzzard]

boom : ⊥
boom = yeah (∷⁻¹ argh)

[Kevin Buzzard]

they seem to use a different naming convention to us

[Kevin Buzzard]

I heard from an Agda user that Agda is (amongst other things) a type theory playground, where people do experiments with exotic types, and occasional proofs of false are not really considered harmful, they are rather considered as useful data about what we can get away with.

[Joe Hendrix]

From a programming or math formalization standpoint, I personally wouldn't worry too much about inconsistencies in Lean or Agda if you are getting started with either system. There was some interesting discussion within the SMT community last summer related to this.
If you have proven a major result that's going to attract press attention or a critical system depends on the proof being right, that may be a different story, but even then I think there are a many other factors that come into play.. e.g, did you get the theorem(s) and all supporting definitions right? are there other properties you also need to prove to have the assurance you need?

[Mario Carneiro]

@Andrew Cann Could you give a more elaborated example of what you need inductive-inductive types for? Just how complicated is your type theory that it requires this? I'm always interested in collecting examples of exotic inductive types, and to see whether they can be simplified to work without needing large cardinals.

[Jakob von Raumer]

@Mario Carneiro It usually occurs, whenever you have a dependent type theory and want to avoid dealing with non-welltyped terms.

[Scott Morrison]

Is https://github.com/agda/agda/issues/1201 really saying that there has been a known proof of false in agda for the past 6 years?

[Mario Carneiro]

@Jakob von Raumer Yes, but unless the language being modeled is lean itself or something with equivalent strength, it should be possible to model without busting the axiomatic strength budget

[Jakob von Raumer]

It's now kind of proven [1] that all finitary IITs can be reduced to mutual induction, where "finitary" means we can't have something like a pi-type ranging over Lean's Nat in the modelled language. Once you want to quotient at the time of definition you usually need QIITs, which are not assumed to be reducible to mutual induction + quotients (unless you accept noncomputability due to postulating AC).
[1] https://drops.dagstuhl.de/opus/volltexte/2020/13070/pdf/LIPIcs-TYPES-2019-6.pdf

[Jakob von Raumer]

The size-wise axiomatic strength budget shouldn't be strained any more than with mutual induction though.

[Mario Carneiro]

unless you accept noncomputability due to postulating AC

I think that's a given in this context

[Jakob von Raumer]

Mario Carneiro said:

Jakob von Raumer Yes, but unless the language being modeled is lean itself or something with equivalent strength, it should be possible to model without busting the axiomatic strength budget

Yes, once you use sized types, I do think they need a special flag to properly check.

[Mario Carneiro]

From a programming or math formalization standpoint, I personally wouldn't worry too much about inconsistencies in Lean or Agda if you are getting started with either system.

Is https://github.com/agda/agda/issues/1201 really saying that there has been a known proof of false in agda for the past 6 years?

I think that while inconsistencies in a theorem prover are not that important, what is important is seeing how severe of a bug the language developers consider it. Lean has a very good track record in this regard: The developers have always said that consistency bugs are of the highest priority, and no such bug has been discovered since lean 0.1, except for the one recent issue in lean 4 which was in fact dealt with promptly.

Rust is another example of a language that takes soundness bugs seriously, and are willing to break stability guarantees in order to fix soundness problems.

Agda seems to have a more standard programming language model where soundness bugs aren't that big of a deal and backwards compatibility is, if not more important, at least of similar priority, and so soundness bugs can languish. Personally I don't think I would trust a system with such a laissez-faire attitude to soundness bugs for theorem proving for anything I actually care about, although that's not necessarily a problem for a "type theory experimentation" system like Agda.

[Andrew Cann]

@Andrew Cann Could you give a more elaborated example of what you need inductive-inductive types for? Just how complicated is your type theory that it requires this? I'm always interested in collecting examples of exotic inductive types, and to see whether they can be simplified to work without needing large cardinals.

@Mario Carneiro I'm trying to formalize a dependent type theory. So my type of types needs to take a context as an argument, but contexts also need to contains types. Pretty much what I wrote in my example, except obviously my real Ty type would have some constructors.

[Mario Carneiro]

I gathered as much, but I'm asking more specifically what's in the dependent type theory

[Mario Carneiro]

depending on your answer it might be possible to do this in lean despite the lack of direct support

[Jannis Limperg]

The problem with Agda's inconsistency is that the --safe flag, which is supposed to be the consistent subset, still allows the inconsistent --sized-types. And the inconsistency isn't even some obscure corner case, it's pretty much baked into the design. With that said, you can disable sized types to get a language with no known inconsistencies. Agda's track record is otherwise similar to Coq's: a few inconsistencies that have been swiftly addressed.

@Andrew Cann have you considered an extrinsically-typed formalisation of your language? I feel like intrinsic typing is generally a trap because you end up needing all these fancy constructions just to avoid a moderate amount of boilerplate.

[Jesper Cockx]

Hey everyone, I was pointed to this conversation by a colleague. It's true that the ongoing problems with sized types are very unfortunate, but that doesn't mean we don't care about safety. In fact for the next release we've decided to no longer allow --sized-types under --safe (admittedly much too late). In other cases we have definitely prioritized soundness over backwards compatability.

[Jesper Cockx]

Andrew Cann said:

I have a few complaints but the things that made me want to give up on it today are:
(a) Having to repeat myself ad-nauseam when writing functions that take a lot of arguments and have a lot of cases.
(b) Those function no longer type-checking when I add a new case, with the error pointing at a case that was already type-checking.
(c) Errors of the form such-and-such != such-and-such when checking ... where "such-and-such" and "such-and-such" are identical.
(d) Automatic proof search not being able to finds proofs that are completely trivial. eg. where the proof term is something like Set.

If you have concrete examples of these it would be very nice if you could report them (on github or on the agda zulip). We've especially tried to get rid of all problems of kind c), so if there's any of those left it would be good to fix them ASAP.

[Jannis Limperg]

Jesper Cockx said:

In fact for the next release we've decided to no longer allow --sized-types under --safe .

Ah, that's very good to hear. Thanks for clarifying!