leanprover / logic_and_proof Goto Github PK

View Code? Open in Web Editor NEW

96.0 15.0 41.0 7.31 MB

CMU Undergrad Course

License: Apache License 2.0

Makefile 0.97% TeX 91.01% Shell 0.29% HTML 0.49% Python 7.24%

logic_and_proof's Introduction

Logic and Proof

Built using Sphinx and restructured text. Also requires convert (https://imagemagick.org) for image conversion.

How to build

The build requires python 3 (install python3-venv on ubuntu).

make install-deps
make images
make html
make latexpdf

The call to make install-deps is only required the first time, and only if you want to use the bundled version of Sphinx and Pygments with improved syntax highlighting for Lean.

The call to make images is also only required the first time, or if you add new latex source to latex_images after that.

How to test the Lean code snippets

make leantest

How to deploy

./deploy.sh leanprover logic_and_proof

How to contribute

Pull requests with corrections are welcome. Please follow our commit conventions <https://github.com/leanprover/lean/blob/master/doc/commit_convention.md>. If you have questions about whether a change will be considered helpful, please contact Jeremy Avigad, [email protected].

logic_and_proof's People

Contributors

Stargazers

Watchers

logic_and_proof's Issues

ND proof section 8.5 is incomplete

The MD+LaTeX code looks right, but the proof tree in section 8.5 is incomplete. Hypothesis 2 does not appear in the derivation tree.

relations: last proof sec 13.1

https://leanprover.github.io/logic_and_proof/relations.html

Theorem. Suppose :math:\leq is a partial order on a domain :math:A. Define :math:a < b to mean that :math:a \leq b and :math:a \neq b. Then :math:< is a strict partial order. Moreover, if :math:\leq is total, so is :math:<.

The second paragraph of the proof of the above theorem says

To show transitivity, suppose :math:a < b and :math:b < c. Then we have :math:a \leq b, :math:b \leq c, :math:a \neq b, and :math:b \neq c. By the transitivity of :math:\leq, we have :math:a \leq c. To show :math:a < c, we only have to show :math:a \neq c. So suppose :math:a = c. then, from the hypotheses, we have :math:c < b and :math:b < c, violating asymmetry. So :math:a \neq c, as required.

I believe this proof is wrong; we can't use the asymmetry of <. This property was proved using the transitivity of this relation, the one we are trying to prove. A possible alternative would be:

To show transitivity, suppose :math:a < b and :math:b < c. Then we have :math:a \leq b, :math:b \leq c, :math:a \neq b, and :math:b \neq c. By the transitivity of :math:\leq, we have :math:a \leq c. To show :math:a < c, we only have to show :math:a \neq c. So suppose :math:a = c. then, from the hypotheses, we have :math:c < b and :math:b < c, and by the definition :math:< we have :math:c \leq b, :mathb\leq c, :math:c\neq b and :math:b\neq c which violates the antisymmetry of :math:\leq. So :math:a \neq c, as required.

Does it make sense?

question Ex 10 chapter 9

Ex 10 in https://leanprover.github.io/logic_and_proof/first_order_logic_in_lean.html#equality-and-calculational-proofs

Should the first sorry in the code be replaced by a proof or not?

13.1 order relations

second list of examples should be different from the first list, right? Maybe some can be taken from https://en.wikipedia.org/wiki/Partially_ordered_set#Strict_and_non-strict_partial_orders

building the epub

I got many error like

writing output... [100%] venv/lib/python3.7/site-packages/sphinx/ext/autosummary/templates/autosummary/module
/Users/ar/work/logic_and_proof/classical_reasoning.rst:237: WARNING: Could not lex literal_block as "lean". Highlighting skipped.
/Users/ar/work/logic_and_proof/classical_reasoning.rst:378: WARNING: Could not lex literal_block as "lean". Highlighting skipped.
...

Many inline math blocks are not formatted properly... any idea?

Typo

Ch. 14. An alternative is to think of 𝑅 as a function which, when applied to 𝑎 and 𝐵, returns the proposition that 𝑅(𝑎,𝑏) holds.

change B to lower case

enable LaTeX packages

@avigad needs bussproofs.sty, amssymb.sty, and amsfonts.sty.

Exercises cap 5

https://leanprover.github.io/logic_and_proof/classical_reasoning.html#exercises

Exercise 5 is the same as the second example of 9. Maybe 5 is about drawing the ND proof on a paper and 9 is its implementation in Lean? Maybe is better to make it clear?

Minor typographical errors in Chapter 4: Propositional Logic in Lean

Pdf page 25 - missing backslashes in Ascii column of table (these need escaping)
Pdf page 26, 3rd paragraph - "Building proofs is then a matter of writing down expressions of the write type". Was probably intended to say "right type", suggest "correct type" is less ambigious.
Pdf page 30 - "and introduction" and "or introduction" should probably be hyphenated for readability ("and"/"or" in the natural deduction sense of the word, not the natural language sense of the word), and for consistency with chapter 3.

Also see my attempts to address these issues in f8e4d4e and 01335a7.

Missing proof in Section 7.3

The section mentions:

In the following example, we show that if 𝐴(𝑥) always implies ¬𝐵(𝑥), then there cannot be an 𝑥 for which both 𝐴(𝑥) and 𝐵(𝑥) holds.

Then a new paragraph starts with

There is a restriction on the term 𝑡 that appears in the elimination rule for the universal quantifier and the introduction rule for the existential quantifier, namely, that no variable that appears in 𝑡 becomes bound when you plug it in for 𝑥.

So it seems like the proof between the two paragraphs is missing.

make fails

make files in two ways:

make install-deps fails because https://bitbucket.org/gebner/pygments-main/get/default.tar.gz#egg=Pygments does not exist. I replaced this with just pip install pygments.
make html fails for a reason I can't figure out:

Extension error:
Could not import extension lean_sphinx (exception: cannot import name 'CodeBlock' from 'sphinx.directives' (unknown location))