Questions tagged [lean]

Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.

Filter by
Sorted by
Tagged with
4 votes
1 answer
116 views

Can we completely erase propositions in the type checker?

Related question on semantic side: How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken? Suppose we have an impredicative universe of ...
  • 4,740
3 votes
1 answer
119 views

Equality type and Propositions

I'm writing a library in the Lean computer proof assistant. Evidently, X : Type x : X y : X #check x = y Produces "Prop" and not "Type"; ...
1 vote
2 answers
54 views

Suppressing notation in Lean

I'm using the Lean computer proof assistant and customizing some notation. Here's the example I'm working with: ...
0 votes
2 answers
107 views

Coproducts in Lean

All, I am using Lean. I am hoping to obtain a coproduct construction which works something like this: ...
1 vote
1 answer
69 views

Inductive types associated to instances of a structure in Lean

I am using the Lean computer proof assistant. I am using the combinatorial structure of a graph with an abelian operation on its edges as a learning example. In it I have a structure Graph. I want to ...
1 vote
1 answer
76 views

Making a finite graph type in Lean - introduction rule

I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a "finite set&...
5 votes
1 answer
97 views

In lean, how do I expand a definition without knowing what it is?

Suppose I have a goal of proving $a \lt b$ But I don't how < is defined. Maybe it's defined as $\exists c \in \mathbb{N}. a + c + 1 = b$ or maybe it's defined ...
1 vote
2 answers
83 views

In lean, how to work around "invalid pattern, 'x' already appeared in this pattern"

I am trying to define what it means for an item to be in a list. I wrote this case breakdown: ...
3 votes
2 answers
332 views

In lean, why is it possible to prove zero_ne_succ (without adding it as an axiom) by using pattern matching?

If I define a custom set of natural numbers: inductive mynat : Type | zero : mynat | succ : mynat → mynat I can prove no successor is equal to 0 by defining a ...
8 votes
2 answers
288 views

Learning Math Proof via Proof Assistants

I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my ...
7 votes
1 answer
195 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: ...
5 votes
1 answer
84 views

What are the differences between theorem, example, def, etc?

What are all the differences between these keywords that allow for defining top level variables? What I have noticed so far is that theorems can't be anonymous — ...
3 votes
0 answers
96 views

Does Lean have a function that reads a file "at compile time"?

Is there some "pure" function that reads a file before the program is type-checked and returns its contents as a string or something, for example if the file ...
4 votes
1 answer
87 views

How to prove a property of a conditional statement without using tactics in Lean?

This doesn't work even though it is the simplest proof of an if statement that I can think of: ...
2 votes
0 answers
86 views

Does Lean 4 have syntax to refer to the current thing being defined?

If I am defining a function (using def for example) then is there some way to refer to the function being defined inside its definition without using the name of ...
  • 21
2 votes
0 answers
86 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 ...
4 votes
3 answers
473 views

Creating a proof assistant for first order logic in Haskell

I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at? Here are some further details. I have a simple proof checker for ...
5 votes
0 answers
191 views

An algorithm for the substitution of formulas for predicates in first order logic

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
6 votes
1 answer
183 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: ...
5 votes
2 answers
496 views

Lean: dubious noncomputability

In Lean, some definitions must be marked as noncomputable, for example if they depend on the law of the excluded middle or other nonconstructive choice principles. Usually, the reason for ...
6 votes
1 answer
158 views

How do I convince the Lean 4 type checker that addition is commutative?

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
7 votes
1 answer
867 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) := ...
13 votes
3 answers
643 views

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

Question Is CiC stronger than CoC, in terms of proof strength? Context To illustrate the kind of confusion I am in, and what I'd like to learn from the answer, here is part of my inner monologue: If I ...
6 votes
2 answers
178 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. ...
  • 508
2 votes
1 answer
176 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
467 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
504 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
16 votes
1 answer
884 views

How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?

This document showed that Lean's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the ...
  • 4,740
3 votes
2 answers
147 views

Like arbitrary, but for nonempty instead of inhabited

I wrote some code that used a [inhabited ι] assumption, and then used arbitrary ι in the proof. The mathlib linter then ...
20 votes
4 answers
965 views

How usable is Lean for constructive mathematics?

In my answer explaining the differences between Lean and Coq, I emphasized that Lean is "essentially classical" mostly due to sociological norms. Nonetheless, even after posting that, I ...
  • 4,690
12 votes
0 answers
279 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
15 votes
1 answer
489 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 ...
  • 673
8 votes
2 answers
286 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
12 votes
2 answers
204 views

Does Lean have a standard ASCII representation?

From Lean 4 tutorial, I learned that In the Lean standard library, you often see Greek letters to denote types, and the Unicode symbol → as a more compact version of -> and you can also type the ...
  • 1,360
30 votes
2 answers
738 views

What exactly is setoid hell?

One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of ...
7 votes
1 answer
108 views

How does Lean choose which decidability instance to use?

Suppose two separate files define decidability instances for a particular predicate in different ways. If I import both of these files, and attempt to run ...
10 votes
1 answer
148 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 ...
  • 203
5 votes
0 answers
146 views

What would a fully classical and fully univalent ITP and library look like?

Consider two developments in dependent type theory: Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
  • 4,690
7 votes
1 answer
120 views

How to quickly look up what constructor/lemma I should use in Lean4?

When writing this answer, I had a hard time finding the lemma I needed to prove 2 ≤ 3. In Agda, when I have a goal, I can press ...
  • 4,740
6 votes
1 answer
63 views

Lean: how to use the refine_struct tactic for commutative ring structures?

Suppose I want to make bool (i.e. the type {ff,tt} of boolean values) into a commutative ring. The following works: ...
6 votes
1 answer
117 views

How to install Lean-4 stable only?

I followed Lean documentation to install Lean 4 on my Ubuntu Linux (20.04 LTS) using the elan option described there, and updated it to Lean4 ...
  • 1,360
12 votes
1 answer
133 views

Lean: problems with visually indistinguishable instances

I will describe a problem which I have in fact solved, but with considerable pain. My question is whether there are better methods for dealing with similar issues. Lean was giving me messages that ...
6 votes
2 answers
102 views

How do we resolve metavariables that appear in hypotheses and targets in Lean?

There are two related questions that I expound on below. It might seem like these aren't quite related, but they are both about how to deal with meta-variables that appear when working through a ...
  • 363
5 votes
1 answer
67 views

Referencing previous fields when constructing new structure

Let's say I have a simple structure structure foo : Type := (a : ℕ) (b : list (fin a)) when defining the field b I can ...
  • 137
19 votes
1 answer
294 views

How hard is computing integrals in Lean?

Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level ...
  • 988
10 votes
2 answers
103 views

Can Lean simp arguments be ordered?

I want to simplify the expression 0 * 1 * 1 * 1 * 0 using simp only [mul_zero, zero_mul]. I would like ...
14 votes
1 answer
146 views

Proof review: Sum of nCk over antidiagonal = Fibonacci

Theorem to prove: The sum of the binomial coefficients over an antidiagonal is a Fibonacci number. More specifically, the $n$th antidiagonal sums to the $n+1$th Fibonacci number, where the ...
  • 664
10 votes
1 answer
85 views

Rewriting with context in nested expressions (congruence rules)

I am trying to prove the following example in Lean 4: ...
7 votes
3 answers
139 views

Preserve equality with match expression

How can I prove that the matched pattern is equal to the original argument? For example, in the following function, what can I write instead of sorry to prove the ...
8 votes
0 answers
101 views

Has there been any work on automated translation of tactic proofs to everyday language?

There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
  • 363