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
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.
...
- 1,853
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 ...
- 399
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 ...
- 101
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 ...
- 21
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 ...
- 307
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