leanprover / theorem_proving_in_lean4 Goto Github PK
View Code? Open in Web Editor NEWTheorem Proving in Lean 4
Home Page: https://leanprover.github.io/theorem_proving_in_lean4/
License: Apache License 2.0
Theorem Proving in Lean 4
Home Page: https://leanprover.github.io/theorem_proving_in_lean4/
License: Apache License 2.0
It seems that there are two different notations for anonymous constructors:
instance : ToString Rules := { toString := fun rs => "TBD" }
and
instance : ToString Rules := ⟨ fun rs => "TBD" ⟩
The former is defined in the the Structures and Records > Objects and the latter somewhere in Quantifiers and Equality > The Existencial Quantifier.
(1) Shouldn't both anonymous constructors be documented together as two different ways to construct structures or inductive types?
(2) Should there be, at least, a link to this anonymous constructor documentation in the inductive types section too?
Users who actually try the examples in VS Code will be confused when a comment disagrees with what they see when they hover. I think the first such example is
#check Nat.add -- Nat → Nat → Nat
A user reading the tutorial will be completely befuddled by the crosses and the superscript. The main problem is that this undermines reader trust, either in the tool or in the comments. (Note that this is different from leaving something unexplained; here you are saying that they will see one thing, and they actually see another.) You can avoid this by just having an explanation, a forward pointer, or some sort of warning in the comment, the hover, or in the text.
There are also examples where the comment should just be changed to match the hover, as in
#check ident -- ?m → ?m
The link for "Programming in Lean 4" is broken in
These aspects of Lean are explored in a companion tutorial to this one, Programming in Lean 4, though computational aspects of the system will make an appearance here.
Unlike other Lean documentation, such as Functional Programming in Lean, theme changes every time I click on the print icon. I have tried to print the document with Microsoft Edge and Opera.
Steps to reproduce it:
1 Set the clear theme. Sometimes I have to choose other themes before setting the clear theme.
2. Click on the print icon. The theme changes to the navy theme.
I would like the website to keep the light theme so I can print the PDF with a white background.
https://leanprover.github.io/theorem_proving_in_lean4/introduction.html has the text:
If you are reading the book online, you will see a button that reads "try it!" Pressing the button opens up a tab with a Lean editor, and copies the example with enough surrounding context to make the code compile correctly. You can type things into the editor and modify the examples, and Lean will check the results and provide feedback continuously as you type. We recommend running the examples and experimenting with the code on your own as you work through the chapters that follow.
There is no "try it" button however, this is old text from TPIL. Not sure whether the text should be edited or the "try it" links should be added, though.
The file induction_and_recursion.md has two sections titled "Local recursive declarations". It looks like it was moved from one place to another on March 3, 2022 and then it was restored to the old location on June 13, 2022.
I have not checked whether the two sections are identical.
theorem_proving_in_lean4/propositions_and_proofs.md
Lines 36 to 38 in ee6aeb4
It has brought some confusion https://stackoverflow.com/questions/69182724/lean-4-unknown-identifier-proof . People may also try the code on their editor.
Thank you for the great book!
The pages are quite long, and I find it difficult to grasp what is written with only the chapter titles. Why don't you provide a table of contents on appropriate pages?
In the chapter induction and recursion, part "dependant pattern matching", I find the explanations quite hard to follow.
First, the goal of the auxiliairy functions is not described explicitely
Worse, it uses "noConfusion". I was not able to find any documentation about this function, and no definition either.
I think it would be more clear to have a dedicated chapter about unreachable patterns explaining:
An example to prove that 0 != 1 would be a nice illustation I think
I hope my feedback will help improve the documentation !
Hi,
Working through the book and loving it. Thanks.
Quick question on https://github.com/leanprover/theorem_proving_in_lean4/blob/master/propositions_and_proofs.md
In the section Propositional Logic we have
So if we have
p q r : Prop
, the expressionp → q → r
reads "ifp
, then ifq
, thenr
." This is just the "curried" form ofp ∧ q → r
.
I'm curious where the conjunction came from? Would it be possible to clarify the idea here?
I'm wondering if p → q → r
is also the curried form of p ∨ q → r
?
David
I have a few questions about the translation.
Where can I see the translations that are already been created?
How do you accept translators' contributions? What should translators do?
In Chapter 6 Interacting with Lean under Using the Library, the link in the second bullet https://github.com/leanprover/lean4/tree/master/src/Std leads to a page that is not available.
From type_classes Output Parameters
By default, Lean only tries to synthesize an instance Inhabited T
when the term T
is known and does not
contain missing parts. The following command produces the error
"failed to create type class instance for Inhabited (Nat × ?m.1499)
" because the type has a missing part (i.e., the _
).
#check_failure (inferInstance : Inhabited (Nat × _))
Instead #check
succeeds printing :
inferInstance : Inhabited (Nat × ?m.5)
And the same for this example from line 368
-- Error "failed to create type class instance for HMul Int ?m.1767 (?m.1797 x)"
#check_failure fun y => xs.map (fun x => hMul x y)
#check says:
fun y => List.map (fun x => hMulx x y) xs : (y : ?m.79) → List (?m.109 y)
See above
Expected behavior: [What you expect to happen]
failure
Actual behavior: [What actually happens]
no failure, see CI failure:
https://github.com/leanprover/theorem_proving_in_lean4/runs/4193469732?check_suite_focus=true
Reproduces how often: [What percentage of the time does it reproduce?]
You can get this information from copy and pasting the output of lean --version
,
please include the OS and what version of the OS you're running.
Any additional information, configuration or data that might be necessary to reproduce the issue.
I recently tried to search for how to introduce a let
expression, but got no results. It would be nice if the search functionality would return hits to lean keywords as an exception to whatever is currently preventing this.
Thanks for the great book!
It would be useful in some cases to add a button to the Lean code block that, when clicked, takes the user to the Lean Web Editor. Just like the jump button on zulip.
If it is OK, I will submit a PR.
Dear all,
In Propositions and Proofs, when the suffices
keyword is introduced, the text reads, "Writing suffices hq : q
leaves us with two goals.". I was expecting, in the style of using Coq, to see those two goals explicitly shown in the context window/infoview. However, the incomplete example does not do so: there is still only one goal, and it appears to be unchanged from the previous line.
variable (p q : Prop)
example (h : p ∧ q) : q ∧ p :=
have hp : p := h.left
suffices hq : q
Expected type
pq: Prop
h: p ∧ q
⊢ q ∧ p
Is there a different infoview that I should be using that the text doesn't explicitly call out? Or, has this behaviour since changed?
#eval Lean.versionString: 4.0.0, commit 96de208a6b1a575b3f07d978965573d5b6fad454
Chapter 3 Propositions and Proofs uses Or.intro_left, Or.intro_right, and Or.elim pretty heavily, but I believe they are no longer supported in Lean4.
Hello,
Several examples in section Propositions and proof
use Or_elim
.
However, this command isn't working in lean-4.0.0-m2.
Could you change the documentation with a working command? I wasn't able to find a good correction for this ... See #20
Thanks !
While running mdbook test
across my local fork so I could create a PR, I noticed there are many errors reported.
Reading the typeclasses section I found myself wondering how double
(or indeed any function) could be rewritten using a type class instance implicit (as it was the initial example).
As a side note, I also found myself wondering how to write variables that are constrained more than once. For a constrived example of this pattern that appears often in real code, here is some Haskell that has two type variables that constrained twice each:
appendFirstToLast :: (Functor t, Foldable t, Monoid a, Ord a) => t a -> a
appendFirstToLast ta =
let maybeFirst = getFirst . fold . fmap (First . Just) $ ta
maybeLast = getLast . fold . fmap (Last . Just) $ ta
in maybe mempty id $ maybeFirst <> maybeLast
Explaining this for lean is (was) beyond my understanding, but we might want to find a simple example where it's useful and add that in as an advanced case, possibly.
Oh, I figured it out. It's what one would expect 😆 Sorry for the noise!
def stringifiedDouble [Add a] [ToString a] (x : a) : String :=
toString (Add.add x x)
The section Auto Bound Implicit Arguments (in chapter 6 Interacting with Lean) says
When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit argument if it is a single lower case or greek letter.
However (at least in the current version 4.5.0) this feature does not seem to be limited to single letters. For example:
def foo (x : abc) := x
#check foo
produces
foo.{u_1} {abc : Sort u_1} (x : abc) : abc
So presumably this documentation needs to be updated (unless this is actually considered to be a bug in Lean).
The tactics chapter states that
In the first example, the left branch succeeds, whereas in the second one, it is the right one that succeeds.
In the next three examples, the same compound tactic succeeds in each case:example (p q r : Prop) (hp : p) : p ∨ q ∨ r := by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption) example (p q r : Prop) (hq : q) : p ∨ q ∨ r := by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption) example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)The tactic tries to solve the left disjunct immediately by assumption;
if that fails, it tries to focus on the right disjunct; and if that
doesn't work, it invokes the assumption tactic.
However, running it locally cannot solve all the subgoals.
Here is the state left unsolved
example (p q r : Prop) (hq : q) : p ∨ q ∨ r :=
/-
case h
p q r : Prop
hq : q
⊢ q ∨ r
-/
by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)
There is a statement "...has nothing to do with the constant b
declared earlier." but there is no such declaration of b
. There is a b1
and a b2
back in Simple Type Theory.
When it is described how Lean automatically inserts variables that are used implicitly, is it worth mentioning anything about the order they are inserted?
It is noted that namespaces can be reopened. Perhaps worth mentioning that any definitions made after the namespace is reopened are added to the collection of definitions associated with the namespace.
The tactics renameI
and admit
are not colour coded like other tactic names.
There is a statement "Here the rewrite
tactic, abbreviated rw
...". If rw
is replaced by rewrite
it is necessary to apply rfl
to complete the proof, so rw
is a little more than a simple abbreviation of rewrite
.
I don't quite get the sentence "One can also specify imports relative to the current directory; for example,
Importing is transitive." How is transitivity of imports an example of import relative to the current directory?
It is stated "The first character |
in an inductive declaration is optional. We can also separate constructors using a comma instead of |
." I am unable to either omit |
or use a comma. However, it does parse if where
is omitted (though where
is not optional for structure declarations).
Using nightly 2021-09-12.
It is stated "Thus both of the following proofs of zero_add
work:". However, after the statement there is only one proof of zero_add
.
The official website is showing an old version of this repo. This is unfortunate because some improvements in the repo aren't on the official website yet. I have 2 questions:
In the dependent cartesian product example, there is:
universe u v
def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
If I rewrite it as:
variable (α : Type u)
variable (β : α → Type v)
def f (a : α)(b: β a) : (a : α) × (b : β a) := ⟨a, b⟩
I got an error on the b type, but I don't understand why and the message is pretty cryptic:
type mismatch
b
has type
β a : Type v
but is expected to have type
β a : Type v
Anyone can help me out here, please?
The below code from the Quantifiers and Equality chapter gives an "ambiguous, possible interpretations" error for this line: x ∣ y := h₁
you can see it if you paste the code into https://live.lean-lang.org/
def divides (x y : Nat) : Prop :=
∃ k, k*x = y
def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z :=
let ⟨k₁, d₁⟩ := h₁
let ⟨k₂, d₂⟩ := h₂
⟨k₁ * k₂, by rw [Nat.mul_comm k₁ k₂, Nat.mul_assoc, d₁, d₂]⟩
def divides_mul (x : Nat) (k : Nat) : divides x (k*x) :=
⟨k, rfl⟩
instance : Trans divides divides divides where
trans := divides_trans
example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
calc
divides x y := h₁
_ = z := h₂
divides _ (2*z) := divides_mul ..
infix:50 " ∣ " => divides
example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
calc
x ∣ y := h₁
_ = z := h₂
_ ∣ 2*z := divides_mul ..
Ch. 6, section "Using the Library" has the following broken link:
https://github.com/leanprover-community/batteries/tree/main/Std
The following from Ch. 7 should be deleted:
The first character | in an inductive declaration is optional. We can also separate constructors using a comma instead of |.
per the discussion here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Basic.20question.20about.20inductive.20types
Dear lean4 maintainers,
Thanks for your work, I love playing with lean4.
Unfortunately I got stuck with proving one of the exercise theorems in Propositions and Proofs ,¬(p ↔ ¬p), and couldn't find a proof in the source code either. Most likely I'm looking at the wrong place or just can't recognize it because.
I'd appreciate any help.
Cheers,
Matteo
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.