rewrite rules possible? similar as agda or lambdapi

Stream: lean4

[hahalol]

lean4 is advertised as also a programming language besides a proof assistant,
(0) is there a quick summary of how this works?
it suggests that rewrite rules (that is, a type theory with computational assumtions https://inria.hal.science/hal-02901011v2 ) are now possible, and this is the part of the proof assistant which is called "also as a programming language"... so in summary, as of today, rewrite rules are only possible in
(1) lambapi, agda (and coq for simple types) or
(2) lambdapi, agda, lean4 or
(3) many other proof assistants/logical frameworks too (which ones?)

[Mario Carneiro]

No, lean does not and AFAIK has no plans to support user-defined definitional rewrite rules

[Mario Carneiro]

You can of course rewrite with equality using the rw tactic

[Mario Carneiro]

I'm not sure how this is particularly relevant to "lean4 is advertised as also a programming language besides a proof assistant", this is not at all a required feature of programming language type systems (in fact, most programming languages have significantly simpler type systems than lean's)

[Mario Carneiro]

Generally speaking lean is quite conservative with regard to things that require kernel support, because that's the trusted core of the system and we have a proof of consistency (c.f. #leantt). Adding user-defined rewrite rules makes the whole thing have wildly different properties and generally become very undecidable (in practice, not just in theory / obscure edge cases no one ever runs into accidentally)

[hahalol]

I spent 5 minutes on your leantt slide.pdf and I am already puzzled by your conclusion that "prove unprovability of
f == g → x == y → f x == g y", what does that mean, did I misunderstand a notation? and you expect to prove strong normalization, isn't such proof nearly impossible to write in details?
anyway let's come back to the topic: "lean4 is advertised as also a programming language BESIDES the proof assistant" means that you should be ALLOWED TO MANUALLY write your ow inductive datatype copy of nat with its constructors/eliminator/computation rules; so my question comes down to this: can the end-user manually declare this code (stolen from your slides.pdf) in lean4?
zero : N
succ : N → N
recN : ∀(C : N → Ui). C zero →
(∀n : N. C n → C (succ n)) → ∀n : N. C n
recN C z s zero ≡ z
recN C z s (succ n) ≡ s n (recN C z s n)

if not then it is false advertisement and I want my afternoon back lol kthx for your attention to this matter.

[Mario Carneiro]

I spent 5 minutes on your leantt slide.pdf and I am already puzzled by your conclusion that "prove unprovability of
f == g → x == y → f x == g y", what does that mean, did I misunderstand a notation?

That's about the HEq relation, which was not defined in the slides but is a version of equality which asserts rather than requires that the values have the same type. This relation is poorly behaved, and in particular does not satisfy the listed congruence rule. This is a folk theorem about lean's type theory and other similar type theories, but it would be nice to have a formal proof of such.

you expect to prove strong normalization, isn't such proof nearly impossible to write in details?

Certainly it's complicated, but not particularly more complicated than the theorems already in the thesis, and strong normalization theorems have been proven for variants of lean's type theory, such as similar subsets of Coq and Agda. Since this paper was written, a counterexample to strong normalization was discovered by Abel and Coquand, but it requires reduction of proofs, which is not a part of lean's unification algorithm. The case of strong normalization for values which are not proofs is still open.

[Arthur Adjedj]

@hahalol You are perfectly able to redefine natural numbers, the language provides indexed nested/mutual datatypes, and you would have realised that had you spent a second looking at any ressource related to Lean. What you cannot do, however, is have a general rewriting system as described in the paper you sent. Terms, functions and recursors do have computational meaning, and the language is perfectly usable as programming language, but being usable as a programming language has nothing to do with having a general rewrite framework à la Agda/Dedukti.
Lastly, you should not expect people to spend time answering your questions if you keep on being unpleasant.

[Mario Carneiro]

As Arthur says, you can define your own natural numbers satisfying those rules. However, the language itself requires that the recursor have a particular form and that those computation rules have exactly that form - you as the user cannot modify them directly, other than by changing the inductive specification. For example, you cannot define addition by recursion on natural numbers and then assert that a + b ≡ b + a is a definitional equality, you only get the definitional equalities coming from the recursive cases themselves, that is a + 0 ≡ a and a + succ b ≡ succ (a + b).