Unanswered Questions
30 questions with no upvoted or accepted answers
1
vote
0
answers
29
views
In Lean 4 prover, how to include a constructor into the search scope of a tactic?
I'm translating a soundness proof of system F- from Rocq to Lean 4.
Here is part of the relevant Rocq code:
...
- 131
1
vote
0
answers
19
views
"Pausing updating" Tactic state mid-sentence by a shortcut key or a setting in Lean 4 VSCode extension?
While entering Lean 4 proofs involving mathlib, I noticed that the Lean often get stuck in updating the Tactic state in Infoview while new characters are entered and the current command is not yet ...
- 2,662
3
votes
0
answers
71
views
Manipulating Summations ∑ and telescopic sums in Lean 4
I want to prove the following lemma:
...
1
vote
0
answers
62
views
tactic 'rewrite' failed, pattern is a metavariable
example {p q : Prop} (H: p) : ¬ ¬ p := by
rewrite [←Classical.not_not] at H
Error:
...
- 333
2
votes
0
answers
161
views
Defining Brownian Motion in Lean4
(Disclaimer: I'm worried that this question will appear lazy, but I did spend some time on it and am about to give up.)
In Mathlib, under probability, there are processes, filtrations and martingales. ...
- 101
1
vote
0
answers
66
views
How to enter in Lean 4 the unicode for "LEFT SQUARE BRACKET WITH TICK IN TOP CORNER"
I am using Lean 4 (4.3) and trying to enter some stylized brackets in Unicode: ⦍ .
Per this question, I tried to hover the mouse in VS Code over its definition:
...
- 2,662
4
votes
0
answers
142
views
How do I write a definition/theorem with an arbitrary number $n$ of types?
I am trying to use mathlib to write the definition of a monoidally well-pointed monoidal category. This definition goes like: For all parallel pairs of morphisms $f, g : A_1 \otimes \cdots \otimes A_n ...
- 41
2
votes
0
answers
101
views
Proof Checking for State Machines Similar to TLA+
I'm wanting to find a modern proof assistant that I can use for modeling distributed systems or similar protocols/algorithms.
TLA+ is the most commonly used language in that field, but I recently ...
- 11k
0
votes
0
answers
77
views
Arbitrary sorting of non-comparable elements? (Lean 4)
In Lean I'm working a lot with partial orders, and they have this property that not every element is necessarily comparable (i.e. for a, b in P where P is a partial order, it may not be true that ...
1
vote
0
answers
45
views
Obtaining Elements in Linked Lists in Lean4
I am currently working on a proof involving chains in partially ordered sets in Lean right now, and am facing some issues regarding obtaining an element from a chain of arbitrary length (e.g. given a ...
0
votes
0
answers
73
views
How does one install new dependencies to a Lean 4 programatically e.g., adding aesop by editing lakefile.lean in bash?
I have a github repo at (note it's not a Lean 4 project):
$HOME/learning_lean
with a Lean 4 project at:
...
- 383
0
votes
0
answers
30
views
Inductive assumption in inductive case
likely stupid question here, I'm sure, but I have been trying fruitlessly with little success to figure this problem out. Here is a toy example. Suppose we have this.
...
- 31
0
votes
0
answers
39
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.,
...
- 383
4
votes
0
answers
125
views
Proving "proof methods" as theorems in type-theory based proof systems
For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as
add_assoc : forall (x y : T), x + y + z = x + (y + z).
We can thus prove ...
- 41
1
vote
1
answer
473
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:
...
CommunityBot
- 1