Questions tagged [lean]

Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.

10 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
17 votes
0 answers
149 views

Programming language metatheory in Lean 4?

I'm looking for developments of programming language metatheory done in Lean 4. We have a calculus with a lot of mutually recursive judgements and we want to formalise its denotational semantics. ...
13 votes
0 answers
322 views

How to speed up Lean?

I've recently been writing my first somewhat serious proof in Lean. While doing that, I noticed that Lean gets slower very fast with increasing length of the proof (slower in the sense that whenever I ...
  • 451
8 votes
0 answers
115 views

Has there been any work on automated translation of tactic proofs to everyday language?

There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
  • 363
5 votes
0 answers
196 views

An algorithm for the substitution of formulas for predicates in first order logic

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
5 votes
0 answers
169 views

What would a fully classical and fully univalent ITP and library look like?

Consider two developments in dependent type theory: Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
  • 5,748
3 votes
0 answers
130 views

Does Lean have a function that reads a file "at compile time"?

Is there some "pure" function that reads a file before the program is type-checked and returns its contents as a string or something, for example if the file ...
2 votes
0 answers
111 views

Does Lean 4 have syntax to refer to the current thing being defined?

If I am defining a function (using def for example) then is there some way to refer to the function being defined inside its definition without using the name of ...
  • 21
2 votes
0 answers
122 views

Proof of a certain proposition not using classical logic

I'm self-studying the textbook Theorem Proving in Lean, and there's one exercise from Section 3.7 that I'm stuck on. The exercise asks for a proof of the proposition ¬(p ↔ ¬p) that does not use ...
1 vote
1 answer
44 views

unexpected inductive type occurrence error for recursive inductive type

I want to declare a property that a recursive structure was constructed using a smart constructor. The smart constructor mainly constructs with hash field and the property would allow me to trust the ...
0 votes
1 answer
57 views

Well founded recursion through lists

I'm trying out Lean for programming, and I'm struggling with the termination checker. Here's the toy I'm playing with: ...
  • 263