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
1 vote
1 answer
40 views

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

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 ...
Charlie Parker's user avatar
0 votes
0 answers
18 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
0 votes
1 answer
61 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
1 vote
1 answer
41 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
1 vote
1 answer
97 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
89 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
69 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
164 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
98 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
71 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
88 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
94 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
88 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
91 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
89 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
158 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
149 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
208 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
127 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
59 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
112 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
65 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
0 votes
1 answer
121 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
1 vote
1 answer
81 views

What do I need to import from MathLib to make `induction a with d hd` work?

I know that I need to import Mathlib to make rewrite [x] at h work. But induction a with d hd...
Craig Gidney's user avatar
5 votes
1 answer
421 views

Why is lean 4 behaving differently on my machine vs in the natural number game?

In the lean 4 version of the natural number game at https://adam.math.hhu.de/#/g/leanprover-community/NNG4/ , I can use tactics like apply x at h and ...
Craig Gidney's user avatar
3 votes
1 answer
100 views

Print the version of lean that is running

In python, I can get the version of python I am using like this: import sys print(sys.version) ...
Craig Gidney's user avatar
0 votes
1 answer
84 views

In lean4 why is induction only rewriting the goal, and not the known facts?

When I do induction over a variable $x$ in lean 4, why isn't $x=0$ available as a fact in the base case of the induction? Without this fact, I can't rewrite other facts in order to make the induction ...
Craig Gidney's user avatar
2 votes
1 answer
89 views

Apply `unfold` once, instead of many times, in lean4

I have code that is similar in spirit to this: ...
Craig Gidney's user avatar
1 vote
1 answer
31 views

Case assumption missing from tactic state in lean4

I'm trying to prove a <= max(a, b) by case. I have this: ...
Craig Gidney's user avatar
2 votes
1 answer
211 views

How do I make the rational numbers 0 and 1/2 in lean4?

I'm trying to define a function that in python I would write: def f(x: bool) -> float: if x: return 0.5 return 0.0 In lean 4 I tried writing ...
Craig Gidney's user avatar
3 votes
2 answers
76 views

Shortening a 4-levels-of-match lean4 proof of the CHSH inequality

In the CHSH game, Alice (Bob) is given the value $x$ ($y$) and needs to pick a value $a$ ($b$) such that $a \oplus b = xy$. The CHSH inequality proves they can win at most 75% of the time with ...
Craig Gidney's user avatar
1 vote
1 answer
119 views

Rewriting certain terms in Lean4

I want to prove the following theorem using a single axiom (https://mathworld.wolfram.com/WolframAxiom.html): ...
swish's user avatar
  • 113
1 vote
2 answers
153 views

How to introduce assumption in lean4

This is probably a trivial question, but I've been googling for hours and can't find the syntax I'm looking for. I'm trying to write a proof of ...
basicLeanWoes's user avatar
1 vote
2 answers
161 views

How to run lean4 with mathlib manually

I have a file which contents are: import Mathlib.Data.Rat.Basic I save it as file.lean in a lean project and run it like this ...
Rainb's user avatar
  • 151
2 votes
1 answer
209 views

How to understand the sigma types example from "Theorem Proving in Lean 4"?

In the Lean 4 book called "Theorem Proving in Lean 4" (https://lean-lang.org/theorem_proving_in_lean4/title_page.html), I don't understand a code example about cartesian product types in ...
Ludovic Kuty's user avatar
2 votes
1 answer
181 views

How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?

I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, ...
Rainb's user avatar
  • 151
1 vote
1 answer
182 views

how to prove 2+2+a=4+a in lean4?

It should be simple but dig it for a while and still not successful. theorem example (a : R) : 2 + 2 + a = 4 + a := ... can someone help to figure out how to do next? many thanks
Tim Eric's user avatar
2 votes
1 answer
211 views

How to handle data from json files in lean 4?

I don't know how mature or efficient Lean 4.1.0's standard feature support is. However, I did enjoy an interesting case about benchmarking data processing languages.The challenge is to read a json ...
Matheus C. França's user avatar
2 votes
2 answers
99 views

Simplifying Array Access

I'm confused how to show the second example here: ...
redjamjar's user avatar
  • 123
7 votes
1 answer
435 views

Benefits of HoTT compared with dependent type theory like what Lean does?

I am not an expert in type theory, so I wonder what will HoTT bring to theorem proving (ITP/ATP), compared with dependent type theory? More specially, imagine Lean is implemented using HoTT, I would ...
ch271828n's user avatar
  • 171
2 votes
0 answers
124 views

Highschool level linear algebra

I would like to be able to do high-school level linear algebra in Lean/Mathlib. However, it seems pretty hard. I do understand that mathematicians don't care about being able to do this basic stuff ...
Adomas Baliuka's user avatar
3 votes
1 answer
222 views

Understanding noConfusion

Data.List.getLast is defined as follows: ...
retonlage's user avatar
0 votes
0 answers
93 views

Is there an algebreic type in lean4?

In lean4 I've seen the Real, Rat, and Int types, but is there an Algebreic type? Loooking at: https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/ which links ...
Erotemic's user avatar
  • 101
4 votes
2 answers
139 views

How to think about writing Lean theorems

In Lean we make definitions and formulate theorems about the things we have defined. Seemingly, to each definition there exists several simple theorems. Let's go to ...
Alex Byard's user avatar
2 votes
1 answer
156 views

Understanding Mathlib/MeasureTheory Notation

I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having ...
Alex Byard's user avatar
0 votes
1 answer
55 views

Automatic nightly Lean update?

I recently answered my own question for how to set up a Lean project with Mathlib dependencies. I realize I don't know everything about this. The route I follow starts by navigating to the correct ...
Alex Byard's user avatar
5 votes
1 answer
184 views

What is the precise meaning of "reducible"?

In Lean 4, I've seen the terms "reducible", "semi-reducible" and "irreducible" mentioned a lot. What is the precise meaning and how are these concepts used in code? When ...
Adomas Baliuka's user avatar
3 votes
1 answer
460 views

Does lean 4 have built-in dictionary types?

Are there builtin dictionary/map types in Lean 4 prover? I'd like to use dictionaries in my program and prove properties about it, but I am not sure if there is a dictionary type in Lean 4. A similar ...
tinlyx's user avatar
  • 1,896
1 vote
1 answer
78 views

Where do I prove that a return type is valid?

I am learning Lean 4 by implementing a fixed-length vector type. Type definition: ...
retonlage's user avatar
4 votes
1 answer
132 views

Why can addition be used in pattern matching Nats but not multiplication

Here's a simple dummy function in Lean 4: def foo : Nat → Nat | (m*2) => m | (m+2) => m | (m+1) => m | (0) => 0 Lean has no trouble ...
Nate Glenn's user avatar