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

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

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

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

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

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

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

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

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

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

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

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

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 they ask to complete this ...
  • 193
12 votes
0 answers

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

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

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

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

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

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

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