Questions tagged [lean3]

Lean 3 is the previous version of the Lean theorem prover, and has an active "community" release. If using the final "official" release from 2019 (3.4.2) which is incompatible with [mathlib], make this clear in your question.

Filter by
Sorted by
Tagged with
0 votes
1 answer
60 views

Installing relevant packages for Lean's math lib

I'm using the Lean computer proof assistant on my Mac. I tried to import data.nat.basic from lean's documentation, just like this: import data.nat.basic I get this:...
2 votes
1 answer
68 views

Why does an internal term produced by Lean's equation compiler have holes in it?

Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to ...
  • 35
1 vote
1 answer
56 views

Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?

In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
  • 35
0 votes
1 answer
71 views

Prove in Lean that ∀ i, 0 ≤ X i → ∃ i, X i > 1 → ∑ i, X i > 1

How to prove that if a term in a sum is > 1 then the sum is > 1? ...
7 votes
1 answer
202 views

Cardinality of Type in a given universe

I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities: ...
2 votes
0 answers
97 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 ...
5 votes
1 answer
189 views

Define a new Type in Lean: Tensor power of vector space

I want to define the tensor power of a vector space from the Lean library mathlib. Here's the draft I have so far: ...
7 votes
1 answer
880 views

In Lean, contradiction tactic failed but actually goal accomplished

I've been playing with Lean, trying to prove the next lemma: lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) := ...
6 votes
2 answers
182 views

How to prove in Lean that sums are distributive?

Assume we are given three types in Lean. constants A B C : Type There is a canonical map of the following form. ...
  • 518
2 votes
1 answer
180 views

Lemma about splitting of homogeneous polynomial equations into irreducible equations

Proof assistants, and Lean, are completely new to me. How can I derive the following simple lemma in Lean? How can I let Lean check if the lemma is correctly written? How can I let Lean check if the ...
  • 131
12 votes
1 answer
481 views

Lean "nonempty" vs "inhabited"

In the init/logic.lean file of the Lean 3 standard library, nonempty and inhabited are defined. It seems like these two classes ...
9 votes
1 answer
513 views

How to define curry in Lean

I just started with Lean and with this nice SE. In the official web book/tutorial, when explaining definitions https://leanprover.github.io/theorem_proving_in_lean/index.html they ask to complete this ...
  • 193
12 votes
0 answers
291 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 ...
  • 441
16 votes
1 answer
503 views

What does the "motive is not type correct" error mean in Lean?

Sometimes, trying to use rw in Lean, we get an error saying motive is not type correct What does this mean? Often ...
  • 703
8 votes
2 answers
295 views

Strong induction on ℕ with function α → ℕ

I have the following problem. I have a type $\alpha$, function $f : \alpha \to \mathbb{N}$ and predicate $P : \alpha \to \mathrm{Prop}$ and I want to prove that for all $a : \alpha, P a$. How could ...
  • 137
11 votes
1 answer
168 views

Explicit vs implicit universes in lean

I've seen in mathlib several cases where the universes are explicit, that is Type u instead of Type*. Is there any advantage in ...
  • 213
17 votes
2 answers
234 views

What is the difference between refl and rfl in Lean 3?

I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
15 votes
1 answer
111 views

Extends vs including a typeclass argument

In the Lean mathlib, I see some places where a typeclass argument is included in a class definition, such as locally_finite_order. In other places, I see the "<...
28 votes
1 answer
359 views

In Lean, what do double curly brackets mean?

In Lean, explicit function arguments are enclosed in round brackets and implicit ones in curly brackets, as in this example: ...