Skip to main content

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).

Filter by
Sorted by
Tagged with
0 votes
2 answers
49 views

How to write a proof of n + 0 = 0 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: ...
Charlie Parker's user avatar
3 votes
1 answer
126 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.)
Jon Bannon's user avatar
3 votes
1 answer
84 views

How can I implement my own deriving in Lean4?

I have the following recursive data structures that I need ToJson and FromJson implementations: ...
ice1000's user avatar
  • 6,186
1 vote
1 answer
34 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: ...
Ralph Trenkler's user avatar
3 votes
1 answer
139 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 ...
Leandro Caniglia's user avatar
0 votes
0 answers
26 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. ...
Mark Pock's user avatar
1 vote
1 answer
60 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 ...
Strichcoder's user avatar
2 votes
1 answer
64 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 ...
Neil Strickland's user avatar
1 vote
1 answer
97 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 ...
Jozef Mikušinec's user avatar
0 votes
1 answer
79 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 \...
teoobo's user avatar
  • 3
1 vote
1 answer
41 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 ...
Neil Strickland's user avatar
2 votes
1 answer
73 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(...
Snowybluesky's user avatar
2 votes
1 answer
377 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? ...
Charlie Parker's user avatar
2 votes
1 answer
51 views

Pattern Matching on List x Fin

So, here is the example I'm working on: ...
redjamjar's user avatar
  • 165
3 votes
2 answers
125 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 ...
André Muricy's user avatar
1 vote
1 answer
55 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. ...
redjamjar's user avatar
  • 165
2 votes
1 answer
77 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 ...
Ashmit's user avatar
  • 21
4 votes
3 answers
183 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....
Snowybluesky's user avatar
0 votes
1 answer
64 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: ...
Charlie Parker's user avatar
2 votes
1 answer
138 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, ...
Jozef Mikušinec's user avatar
1 vote
1 answer
110 views

How do I force Lean 4 to show me the rewrite rules and theorems simp is using -- error: unknown option 'trace.simplify.rewrite'?

I miraculously found this https://leanprover-community.github.io/extras/simp.html (which I think was for lean 3?) and it said: The simplifier is what is known as a conditional term rewriting system: ...
Charlie Parker's user avatar
0 votes
1 answer
85 views

Given some proposition in Lean 4, how do we state a theorem saying that we want that property to hold a number of times?

I have a definition of the form in Lean 4: ...
Charlie Parker's user avatar
2 votes
1 answer
90 views

How do I explicitly see the propositional or logical constructors in Lean 4?

I have the following goal: ⊢ ∃ δ, 0 < δ ∧ ∀ (x : ℝ), 0 < x - 0 ∧ x - 0 < δ → M < f x I am curious and want to see how the propositional constructors ...
Charlie Parker's user avatar
2 votes
1 answer
60 views

How do I construct a concrete real number in lean without errors? failed to synthesize instance OfScientific ℝ

How do I fix limit_linear_khan_academy.lean:22:16 Messages (1) limit_linear_khan_academy.lean:22:13 failed to synthesize instance OfScientific ℝ All Messages (4) ...
Charlie Parker's user avatar
1 vote
1 answer
109 views

Where does one find the keyword documentation for Lean4?

I find that Lean4 is rather hard to work to find keywords and related things. In coq the docs are pretty to search if I recall correctly. A quick search for Inductive send me to the grammer and lots ...
Charlie Parker's user avatar
0 votes
3 answers
107 views

Why can't Lean4 evaluate my function despite it being defined, Error: compiler IR check failed at '_eval', error: unknown declaration 'g'?

My lean4 code: def f (x : Real) : Real := x #check f #eval f 3 -- works noncomputable def g (x : ℝ) : ℝ := 1 / x #check g #eval g 3 -- fails but the second ...
Charlie Parker's user avatar
1 vote
1 answer
64 views

How do I write bitwise logic in lean4 with mathlib?

I want to prove that a circuit decomposition into Toffoli gates is correct. In order to do this, I'm trying to explain to Lean what it means to apply a Toffoli gate to bits (flip the target bit if the ...
Craig Gidney's user avatar
2 votes
1 answer
129 views

What is the official way to reinstall Lean4 from scratch on a Mac or Linux?

I want to install Lean from scratch to see if I can fix a previous issue related to the location where I can create lean projects (and a related issue). The official instructions don't seem to make it ...
Charlie Parker's user avatar
0 votes
0 answers
23 views

How does one create a lean project even if it already exists e.g., lake +leanprover/lean4:nightly-2023-02-04 new my_project math?

I want to initialize a lean project but the folder I have already exists. How do I do this? e.g., ...
Charlie Parker's user avatar
1 vote
2 answers
131 views

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

I want to create a lean project inside another folder besides the $HOME folder. So I was going through the official Creating a Lean project instructions on how to ...
Charlie Parker's user avatar
2 votes
1 answer
64 views

Inductively proving that a number is either even or odd in Lean

I have the following Lean definitions: def is_even (a : Nat) := ∃ m, a = 2 * m def is_odd (a: Nat) := ∃ m, a = 2 * m + 1 The following proof would be complete if I ...
Thanasis's user avatar
2 votes
1 answer
222 views

Using `decreasing_by` to prove termination in Lean 4

Warning: This was written for Lean v4.5.0. To make the accepted answer work, please use v4.6.0-rc1. I would like to define an elementary quicksort function for ...
Matematiflo's user avatar
2 votes
1 answer
120 views

Two steps induction in Lean4: how to obtain 2nd inductive hypothesis?

When trying to solve this example from "The Mechanics of Proof": ...
Eugen Lindorfer's user avatar
0 votes
1 answer
137 views

What am I doing wrong when proving the add_right_cancel theorem?

So, as mentioned in my previous two questions, I have been using The Natural Number Game to help me teach myself how to use the mathematical proof assistant Lean4. I am currently trying to complete ...
CrSb0001's user avatar
  • 145
2 votes
2 answers
216 views

How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?

So I have been using The Natural Number Game (as I have mentioned in my previous post) to learn Lean1. However, I am currently stuck on level 6/9 in the Algorithm world, where I am supposed to prove ...
CrSb0001's user avatar
  • 145
1 vote
1 answer
126 views

Need help with induction proof in Lean for $0+d=d$

So I have been trying to learn Lean and have managed to find this resource called the "Natural Number Game" which is supposed to help me learn Lean. I am learning Lean to help me understand ...
CrSb0001's user avatar
  • 145
3 votes
1 answer
92 views

How to lift a binary function to a quotient?

Kia ora :) I am trying to use Quot. in Lean4 to define the integers as the quotient of the Cartesian product of two copies of the natural numbers (type Peano) under the relation: ...
user avatar
2 votes
1 answer
144 views

In Lean 4 how to substitute equals in an expression with other variables?

I can use 'subst' to prove that if a=b and a is positive then b is positive: example (a b : Peano) (h1 : a = b) (h2 : pos a) : pos b := Eq.subst h1 h2 How do I ...
Lewis Baxter's user avatar
1 vote
1 answer
127 views

How to see the value under Exists in Lean?

My understanding of dependent typing is that it allows typing functions to constrain their behavior. Say I have a Lean object ...
antilope's user avatar
0 votes
1 answer
105 views

Shortcut proof by calculation for addition/subtraction, "The Mechanics of Proof", and mathlib4

In Macbeth's book 'The Mechanics of Proof,' the author provides a tactic called addarith to eliminate the need to write calc ...
probablygrigsby's user avatar
0 votes
1 answer
144 views

In Lean 4 how to use an implication in a hypothesis?

I am experimenting with my own "natural numbers" (Peano), so I don't want to use Lean 4's natural number tactics (such as add_comm or cancellation). How can the following be proved? It ...
Lewis Baxter's user avatar
0 votes
1 answer
183 views

An installation error in "Mathematics in Lean"

I have just started learning Lean 4 using Mathematics in Lean in Visual Studio Code, and I ran into a problem right away. I get the following error message: ...
Blankino's user avatar
2 votes
1 answer
174 views

Verifying a basic function with Lean4

I have this simple structure to represent a person: structure Person where age: Nat lifespan: Nat deriving Repr This function takes a Person and either (a) ...
probablygrigsby's user avatar
2 votes
1 answer
167 views

Are type universes related to proper classes from set theory?

I'm currently learning Lean 4, and in the book they mention that the type hierarchy was introduced to avoid a version of Russell's paradox. From reading a bit about set theory a while ago, I remember ...
Sasha Krassovsky's user avatar
0 votes
1 answer
292 views

How to use the most bare essentials of Lean 4?

As a learning exercise I want to use Lean 4 to prove theorems about natural numbers, but WITHOUT Mathlib (or as little as possible). I want to start with 2 Peano theorems s(x) != 0, and s(x)=s(y) ->...
Lewis Baxter's user avatar
1 vote
1 answer
156 views

Lean 4 exercise: Why can't I write this function definition inside an instance declaration?

In Lean 4.3.0, I'm solving an exercise from section 4.5 "Standard Classes" of the excellent book "Functional Programming in Lean". Given the structure ...
Adam Dingle's user avatar
1 vote
0 answers
61 views

Peano Arithmetic in LEAN4 [duplicate]

Kia ora! I am trying to implement the Peano axioms and prove some simple theorems about the natural numbers in LEAN4. However, I am not sure how to encode the first two (as presented here) axioms in ...
user avatar
2 votes
1 answer
160 views

Lean 4: How can I specify that out of two universe variables, one is larger than the other?

Before Mathlib 4 was finished, I decided to implement my own ordinals, but this was as I was learning Lean 4, so my Ordinal type had type Type 1 instead of the ...
Jozef Mikušinec's user avatar
0 votes
1 answer
125 views

In lean 4, how do I give names to variables when using `split`?

Sort of related to In lean 4, how do I refer to variables with names like `a✝` When I use split to pull apart a match, I get a ...
Craig Gidney's user avatar
1 vote
1 answer
224 views

In lean 4, how do I refer to variables with names like `a✝`

When I have a tactic state that mentions a variable name like a✝, is there a way to refer to it? When I use this variable name in my code, it says it doesn't exist. ...
Craig Gidney's user avatar