Stack Overflow
Stack Overflow

Questions tagged [lean]

Lean is an open source theorem prover being developed at Microsoft Research, with a monolothic standard library developed collaboratively. The Lean Theorem Prover aims to bridge the gap between interactive and automated theorem proving. There are two main versions available; Lean 3 and Lean 4, with similar designs but different syntax.

Resources:

169 questions
28
votes
2 answers

Why haven't newer dependently typed languages adopted SSReflect's approach?

There are two conventions I've found in Coq's SSReflect extension that seem particularly useful but which I haven't seen widely adopted in newer dependently-typed languages (Lean, Agda, Idris). Firstly, where possible predicates are expressed as…
LogicChains
  • 4,332
  • 2
  • 18
  • 27
23
votes
1 answer

what's the difference between lean, f*, and dafny?

They are from Microsoft and seem like they are proof assistants? Besides syntactical differences are there practical aspects that make them different from one another (say ability to do automation, expressive power, etc)? I am new to formal…
JRR
  • 6,014
  • 6
  • 39
  • 59
14
votes
3 answers

Why do Calculus of Construction based languages use Setoids so much?

One finds that Setoids are widely used in languages such as Agda, Coq, ... Indeed languages such as Lean have argued that they could help avoid "Setoid Hell". What is the reason for using Setoids in the first place? Does the move to extensional type…
Henry Story
  • 2,116
  • 1
  • 17
  • 28
8
votes
1 answer

Proving substitution property of successor over equality

I'm trying to understand inductive types from chapter 7 of "theorem proving in lean". I set myself a task of proving that successor of natural numbers has a substitution property over equality: inductive natural : Type | zero : natural | succ :…
Adam Kurkiewicz
  • 1,526
  • 1
  • 15
  • 34
7
votes
2 answers

How can I apply a rewrite to only one term?

In Lean I occasionally want to apply a rw tactic to exactly one of multiple identical terms. For example I have the goal ⊢ 0 = 0 and I want to rw it to ⊢ a * 0 = 0 I also have mul_zero (a : mynat) : a * 0 = 0 Now I should be able to just…
Wheat Wizard
  • 3,982
  • 14
  • 34
6
votes
2 answers

How enter symbols in VS Code for Lean (macOS)

I'm using Lean in VS Code under macOS Catalina with a U.S. keyboard. How do I enter symbols such as for the implication arrow, union, intersection, subset? Is there some built-in or add-on palette to facilitate this? Or do I have to use Option key…
murray
  • 737
  • 2
  • 10
  • 28
6
votes
4 answers

How to prove a = b → a + 1 = b + 1 in lean?

I'm working my way through the chapter 4 of the lean tutorial. I'd like to be able to prove simple equalities, such as a = b → a + 1 = b + 1 without having to use the calc environment. In other words I'd like to explicitly construct the proof term…
Adam Kurkiewicz
  • 1,526
  • 1
  • 15
  • 34
6
votes
1 answer

How to define mutual inductive propositions in Lean?

I try using the syntax for inductive datatypes but it got an error message "mutually inductive types must compile to basic inductive type with dependent elimination". Below is an example of my attempt to define propositions even and odd on natural…
Phil
  • 5,595
  • 5
  • 35
  • 55
5
votes
1 answer

Cases tactic in Lean does not create hypothesis

When using the cases-tactic on an inductive data type, lean produces multiple cases, but does not create a hypothesis stating the assumption of the current case. For example: inductive color | blue | red theorem exmpl (c : color) : true := begin …
502E532E
  • 431
  • 2
  • 11
5
votes
1 answer

extending or inferring (PID / UFD) in a Lean class definition

Why is mathlib's definition of UFD this: class unique_factorization_domain (α : Type*) [integral_domain α] := (factors : α → multiset α) (factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a) (prime_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, prime…
Kevin Buzzard
  • 537
  • 4
  • 11
4
votes
1 answer

Is Lean 4 lazy or strict?

Lean 4 is a purely functional programming language, but is it lazy (like Haskell) or strict (like Idris) and what are the implications of this? Is there a way to opt-in (or opt-out) of laziness?
eyelash
  • 3,197
  • 25
  • 33
4
votes
1 answer

Define a function inside of a proof in Lean

In Lean, we can define a function like this def f (n : ℕ) : ℕ := n + 1 However, inside a proof this is no longer possible. The following code is invalid: theorem exmpl (x : ℕ) : false := begin def f (n : ℕ) : ℕ := n + 1, end I would assume that…
502E532E
  • 431
  • 2
  • 11
4
votes
1 answer

Is there a prefix notation in Lean?

In Haskell I can use parentheses to convert an infix operator like + into a prefix function so (+) 2 3 is the same as 2 + 3. Is there a similar feature in Lean?
eyelash
  • 3,197
  • 25
  • 33
4
votes
2 answers

Apply function in goal in lean proof

There are a tree data structure and a flip method for it. I want to write a proof that if you apply the flip method to a tree twice you get initial tree. I've got a goal ⊢ flip_mytree (flip_mytree (mytree.branch t_ᾰ t_ᾰ_1 t_ᾰ_2)) = mytree.branch t_ᾰ…
osseum
  • 187
  • 14
3
votes
1 answer

How to do cases on a function between finite types?

I'm just starting out with lean. Say I want to prove something about functions between two finite types. For example example (f : Bool -> Bool) : (∀ x : Bool, f (f (f x)) = f x) := sorry since there are just a few possibilities for f ideally I'd…
acupoftea
  • 181
  • 2
  • 11
1
2 3
…
11 12