Questions tagged [lean4]
Lean 4 is the latest major version of the Lean theorem prover by Microsoft Research. Use this tag for questions specific to Lean 4; if it's about Lean in general, use the tag (lean).
174
questions
1
vote
1
answer
24
views
Passing functions to casesOn which do not depend on a pattern match
In Chapter 8 of Theorem Proving with Lean4, there's the following example of a tail function for dependent lists:
...
- 113
3
votes
1
answer
87
views
Stochastic calculus in Lean4?
Has anyone started looking into this? Measures and Probability theory look like a good place to start, but maybe there are other resources?
https://leanprover-community.github.io/undergrad.html
- 131
1
vote
0
answers
43
views
How to enter in Lean 4 the unicode for "LEFT SQUARE BRACKET WITH TICK IN TOP CORNER"
I am using Lean 4 (4.3) and trying to enter some stylized brackets in Unicode: ⦍ .
Per this question, I tried to hover the mouse in VS Code over its definition:
...
- 2,320
2
votes
1
answer
175
views
Could proof assistants fill in single theorems automatically?
Would it be possible to only write declarations and conclusions and write a program that automatically fill in theorems used to derive those conclusions in LEAN 4? From my understanding, proof ...
- 194
3
votes
2
answers
274
views
What is the unicode braces {| |} (⦃ ... ⦄) in lean 4?
I came across the use of a Unicode braces here ⦃ ... ⦄
In Lean the definition looks like this:
def Set.Subset (U V : Set α) : Prop := ∀ ⦃x⦄, x ∈ U → x ∈ V
I am not sure what it is exactly. I know ...
- 2,320
4
votes
0
answers
133
views
How do I write a definition/theorem with an arbitrary number $n$ of types?
I am trying to use mathlib to write the definition of a monoidally well-pointed monoidal category. This definition goes like: For all parallel pairs of morphisms $f, g : A_1 \otimes \cdots \otimes A_n ...
- 41
2
votes
1
answer
127
views
How to do recursive type coercion in Lean
I have a type
inductive Pair where
| zero
| pair (a b: Pair)
and I would like to use () for ...
- 470
4
votes
2
answers
111
views
How to make lean 4's rw tactic rewrite at a given position of ocurrence?
I am learning lean 4 and find it sometimes necessary to rewrite a specific instance of a term, but couldn't figure at how to do that.
In a fake example below, the rw...
- 2,320
3
votes
1
answer
194
views
1
vote
2
answers
112
views
why I cannot apply `ring` to `y = x * y / x`
I'm teaching myself about Lean4 using The Mechanics of Proof. I'm trying to solve one of the problems in the book 2.1.9 exercise 3
...
- 111
2
votes
0
answers
68
views
Proof Checking for State Machines Similar to TLA+
I'm wanting to find a modern proof assistant that I can use for modeling distributed systems or similar protocols/algorithms.
TLA+ is the most commonly used language in that field, but I recently ...
- 21
1
vote
1
answer
145
views
Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?
Remark 1. The following counting formula can be derived using arithmetic properties of inequalities, properties of floor / ceiling, inclusion-exclusion, sieve-of-Eratosthenes, and the inclusion-...
- 303
1
vote
1
answer
71
views
Lean Proving a Prop that has a match
I am working on making the surreal numbers in Lean from scratch. I came across a problem when trying to write proofs for propositions that are defined using match statements. I boiled down the problem ...
0
votes
0
answers
61
views
Arbitrary sorting of non-comparable elements? (Lean 4)
In Lean I'm working a lot with partial orders, and they have this property that not every element is necessarily comparable (i.e. for a, b in P where P is a partial order, it may not be true that ...
0
votes
1
answer
138
views
Defining a Finset in Lean4
I am currently trying to define a finset (of a collection of finite images of some function).
More specifically, given a fixed mapping between the maximal chains of a partially ordered set (of which ...
2
votes
2
answers
42
views
Determining the minimal index where lexicographically different lists diverge in Lean 4
I'm trying to define the smallest index at which two lexicographically different lists of equal length diverge. This is what I have so far:
...
2
votes
1
answer
140
views
Is there any way to approximate noncomputable functions in Lean4?
As you may know, there are some definitions in lean4 that can't be evaluated due to the noncomputable tag. Is there any way to approximate their value in lean4?
For ...
- 21
5
votes
1
answer
290
views
How to perform type conversion/coercion in Lean 4?
Does Lean 4 have a good way of handling data type conversion (e.g. between the natural and real numbers)?
I am trying to solve the following property from the Mechanics of Proof book:
$\forall a \in Z,...
- 2,320
1
vote
0
answers
23
views
Use of `by` on first line of lean proof - when to / when not to? [duplicate]
The following lean4 proof generates no warnings or errors.
...
- 119
2
votes
1
answer
57
views
Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?
I have a Lean 4 test project in C:\Temp\MyProject I open with Visual Studio. In that directory, I have a Main.lean file. And, in ...
0
votes
1
answer
61
views
How to combine the PROP of a list of PROP in lean 4?
I have the following structures:
structure MyElem where
identifier : Nat
acceptable : Prop
structure MyList where
elements : List ( MyElem )
I want to ...
1
vote
1
answer
54
views
Showing that elements match after reducing list (Lean 4)
I'm currently trying to show that the elements of a reduced list match the original list after applying List.take. It feels obvious but it doesn't seem to be ...
1
vote
1
answer
74
views
Lean4: Prove that ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) = ∑ x : Fin nn, k (Fin.castLE _ ↑↑x) (sums over Fin n)
Im working with sums over Fin n for some n : Nat, and I am stuck with two sums, that should be equal (and look exactly equal in ...
- 13
1
vote
2
answers
133
views
How can I reason backwards and assume the conclusion holds in Lean 4?
I was wondering how can one reason backwards in Lean 4, starting from an existentially quantified conclusion.
I know that I can reason about an existentially quantified variable in a hypothesis using <...
- 2,320
1
vote
0
answers
40
views
Obtaining Elements in Linked Lists in Lean4
I am currently working on a proof involving chains in partially ordered sets in Lean right now, and am facing some issues regarding obtaining an element from a chain of arbitrary length (e.g. given a ...
0
votes
1
answer
83
views
Transitivity of Implication in Lean 4
I'm trying to prove example (C A S: Prop) (h1 : C → A) (h2 : A → S) : C → S. It's this level in the Lean Intro to Logic game. So far I have
...
- 1
2
votes
1
answer
96
views
6
votes
2
answers
210
views
When is the lean 4 "by" required?
I am reading an introductory math/lean course here, and got confused about when the tactic/keyword by is required. It is used most of the time, but is occasionally ...
- 2,320
0
votes
0
answers
38
views
How does one install new dependencies to a Lean 4 programatically e.g., adding aesop by editing lakefile.lean in bash?
I have a github repo at (note it's not a Lean 4 project):
$HOME/learning_lean
with a Lean 4 project at:
...
- 333
3
votes
1
answer
172
views
How to prove termination of mutually recursive functions if only some decrease their arguments?
I need to prove termination of mutually recursive functions. However, only some of those functions actually (structurally) decrease their arguments, other functions do some other calculations and pass ...
- 470
1
vote
2
answers
142
views
How to write a proof of n + 0 = n in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?
I want to do the proof of n + 0 = n in Lean 4 using mathlib 4, my attempt:
...
- 333
5
votes
2
answers
437
views
Is there a complete index of Lean 4 tactics?
I'm wondering if Lean 4 tactics are documented anywhere, in a way comparable to the API documentation for mathlib.
(Sorry for brevity...will edit if this is unclear.)
- 433
3
votes
1
answer
134
views
How can I implement my own deriving in Lean4?
I have the following recursive data structures that I need ToJson and FromJson implementations:
...
- 6,346
1
vote
1
answer
62
views
Lean 4 program to insert element in binary tree shows error: failed to sythesize instance LT \alpha
I wrote a Lean 4 routine to insert a element into a binary tree and got the following error message: "failed to synthesize instance LT \alpha". Here is my program:
...
3
votes
1
answer
152
views
Help needed for Lean4 book Interlude exercise
In 3. Interlude of the Functional Programming in Lean book, one of the exercises asks the reader to prove by simp some few theorems, one of them is ...
- 133
0
votes
0
answers
29
views
Inductive assumption in inductive case
likely stupid question here, I'm sure, but I have been trying fruitlessly with little success to figure this problem out. Here is a toy example. Suppose we have this.
...
- 31
1
vote
1
answer
100
views
Define maximum of matrix entries in Lean4
In Lean4 I would like to define a function max that finds the largest entry of an $n\times n$ matrix with entries in a ...
- 193
2
votes
1
answer
81
views
Lean4 instance management
I have a group $G$ and $G$-sets $X$ and $Y$. I would like to let $G$ act on the type $(X\to Y)$ by the usual rule $(g\bullet u)(x)=g\bullet u(g^{-1}\bullet x)$. I define a ...
- 1,051
1
vote
1
answer
101
views
Applying universally quantified equalities to propositions
In Lean, given an equality eq: e0 = e1, one may rewrite either e0 or e1 with the other one ...
- 470
0
votes
1
answer
120
views
Using lean4 to prove subset properties
I'm learning Lean4.
I'm trying to prove in lean4 these basic properties of subsets:
$ X \subseteq X $
$ X \subseteq Y , Y \subseteq Z \Rightarrow X \subseteq Z$
$ X \subseteq Y , Y \subseteq X \...
- 3
1
vote
1
answer
85
views
Lean 4 directive to always include a section variable
Here is something that I think used to work in Lean 3, although I no longer have a working installation of Lean 3 with which to check that the details of this minimal example are precisely correct. I ...
- 1,051
2
votes
1
answer
101
views
Negating universal/existential quantifier in type theory, propositions on elements of the empty type
The universal/existential quantifier:
In classical logic, ~∀x P(x) is equivalent to ∃x ~P(x). Looking at the existential quantifier in Lean4, the object ∃ x:nat P(x) is essentially the tuple (x:nat, P(...
- 63
2
votes
1
answer
543
views
How does one import Natural numbers in Lean 4 -- unknown identifier 'ℕ'?
I found the definition of Nat's but lean still complains that it doesn't exist. Why is it?
...
- 333
2
votes
1
answer
53
views
3
votes
2
answers
149
views
Lean4: How to construct an HEq between dependent functions?
I have an extremely simple goal to prove:
HEq
(fun px rd =>
match px, rd with
| Sum.inr _ppos, dir => dir)
fun x => id
The reason the match ...
- 41
1
vote
1
answer
71
views
Termination for Wrapped Fin in Lean4
The following example type checks in Lean 4, but I am confused why the termination_by declaration is required.
...
- 165
2
votes
1
answer
80
views
How to find the data type of a Json value that in lean4, to perform type validation. (Functional programming in lean)
Basically I am taking in a json object in lean4 as input and I want to check whether a particular feild like 'age' should always be Nat not something else depending on the schema that the user has ...
- 21
4
votes
3
answers
228
views
For formal proofs of graph structures and algorithms, which proof assistant should I learn?
My goal is to be able to make formal proofs for graph structures and algorithms, proving i.e. for every vertex in a directed-acyclic-graph there exists a path from a source vertex to that vertex, or i....
- 63
0
votes
1
answer
85
views
How does one define a structure with the ext theorem in Lean 4?
I get this error:
unknown attribute [ext]
and my code is literally a copy paste of the code from mathematics in lean:
...
- 333
2
votes
1
answer
154
views
How to recover implicit arguments of inductive types in a match expression?
def IsEven: Nat → Prop
| Nat.zero => True
| Nat.succ pred => ¬IsEven pred
inductive Example: Nat → Prop
| IsExample: IsEven n → Example (n + 10)
Here, ...
- 470