hello

Stream: new members

[Mario Krenn]

Hi people, let me briefly introduce myself. my name is mario krenn, I am a quantum physicist/AI researcher at university of Toronto (mariokrenn.wordpress.com/).

I learned about Lean by Kevin Buzzard's MO post (https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean), and he introduced me to this channels per email.

I am in particular interested in graph theoretical questions, and hope for suggestions to start learning, in particular i would love seeing the sources of simple graph theory formalized proofs. Thank you!

[Johan Commelin]

@Mario Krenn Hello and welcome! At the moment we have no graph theory in mathlib, the "standard library" for maths in Lean. But there have been several attempts at getting something done. The last attempt is currently WIP on the hedetniemi branch of the repository. (I don't know if you are familiar with git/github.) You can browse the code here: https://github.com/leanprover-community/mathlib/tree/hedetniemi/src/graph_theory

[Jakob Scholbach]

Hello everyone, I just wanted to introduce myself: I am Jakob Scholbach, an algebraic geometer with interests in motives and the Langlands program. I find the recent works on formalization of topics in algebraic geometry very inspiring and I am slowly starting to learn lean. Thanks guys for your help so far, more stupid questions are sure to follow!

[Kevin Buzzard]

Hi Jakob. I think one thing which we are lacking right now but which is probably accessible is a whole bunch of predicates on ring homomorphisms, e.g. being flat, unramified, etale, finite presentation etc, and then transferring all these concepts over to morphisms of schemes. We have the category of schemes but nobody has begun to think about formalising any proofs which involve saying "this morphism is locally X, therefore it is X". There is an art to getting the definitions right in a theorem prover; with the wrong definitions, proving stuff is really slow going and painful. If you get the definition right however then it can be a dream. The problem is that in some sense the art of figuring out the correct definition is a very subtle one, and probably prover-dependent, so it's right now quite an adventure trying to figure out this stuff.

[Jakob Scholbach]

OK, good to know. Speaking about "getting things right" -- in paper mathematics I am very fond of categorical thinking. E.g. I believe a good approach to étale maps is by combining formally étale (a kind of orthogonality relation against simple classes of maps) + finite presentation property, which is a compactness condition, which again is very categorical in flavor. Since I have zero knowledge about formalisation, let me ask very naively: is this kind of thinking useful or not so much?

[Adam Topaz]

@Jakob Scholbach You might be interested in this discussion :smile:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.C3.89tale.20morphisms.20of.20rings/near/219027888

[Adam Topaz]

I think formalizing the equivalence between "categorical" compactness in the category of rings (or algebras over some commutative ring) as being finitely-presented would be a very interesting project as well.

[Riccardo Brasca]

Concerning finite presentation, I recently wrote the definition in terms of quotient of polynomial rings and proved some extremely basic results. (If you are not used to formalized math, "extremely basic" means something like $R$ is a finitely generated $R$-algebra, this is not completely trivial.) I wanted to do more but I switched to the liquid project, if you are interested I have some results still not in mathlib, essentially that the quotient of a finitely presented algebra by a finitely generated ideal is finitely presented.

[Johan Commelin]

@Jakob Scholbach In practice, we often have reasons to write definitions that don't quantify over categories (so no universal properties as definitions), but rather choose something as close as possible to first-order logic.
The categorical characterisations will then be theorems that are part of the API, the interface for using the objects.

[Kevin Buzzard]

All of us mathematicians here have only been using this software for a few years at most. Abstract categorical thinking is super-important, as is trying to find the right abstractions. Maybe you'll find the comments about finding the correct way to think about extending stuff continuously from a dense subset in sections 4 and 5 of the perfectoid paper interesting. Getting definitions right has been very interesting. I was somehow expecting the computer scientists to have all the answers, but actually they have been encouraging us to experiment, because nobody really tried formalising serious maths of this nature before. It took us three goes to get schemes right. You've arrived at a really interesting time. You know about this Scholze challenge? It's really quite active right now.

[Tchsurvives]

cool project! im installing lean right now, just curious how big is lean?

[Notification Bot]

This topic was moved here from #general > hello by Johan Commelin

[Johan Commelin]

@Tchsurvives Welcome! What do you mean by "big"? What measure?

[Tchsurvives]

as in how many megabytes haha

[Tchsurvives]

@Johan Commelin

[Johan Commelin]

The Lean executable is ~16MB it seems.

[Johan Commelin]

The mathlib library is ~50MB after compiling, and ~650.000 lines of code, I think. These numbers change rapidly.

[Anne Baanen]

I count about 6 MB of Lean and C++ code in Lean itself, and another 27 MB of Lean files in Mathlib.

[Anne Baanen]

$ du -b ../lean/library/**/*.lean ../lean/src/**/*.{cpp,h} | awk '{sum += $1} END {print sum}'
6431327
$ du -sb src/**/*.lean | awk '{sum += $1} END {print sum}'
27024149

[Tchsurvives]

i am slightly keen in formalising olympiad euclidean synthetic geometry, as part of the goal towards the IMO grand challenge, where do you recommend i begin?

[Tchsurvives]

i did some searching, but couldnt find much online

[Ruben Van de Velde]

Did you find the #IMO-grand-challenge stream?

[Ruben Van de Velde]

I think Euclidean geometry is still fairly hard at this point

[Johan Commelin]

You can take a look at geometry/euclidean in mathlib, to see what's there already.

[Tchsurvives]

oh i see, ill check it out thanks!

[Johan Commelin]

I wouldn't be surprised if Euclidean geometry actually needs a DSL + a bunch of tactics in order to become doable or even nice.

[Tchsurvives]

what do you mean domain specific language?

[Johan Commelin]

Currently setting up a "geometry problem" in Lean is very roundabout and verbose. It would be nice if we could "switch on" geometry mode, and then be able to talk in very brief terms.

[Johan Commelin]

And not so many people are working on this atm. A lot of effort is being poured into making Lean 4 ready for prime time. After that, I guess people will return to the IMO-GC.

[Johan Commelin]

Other people working on maths/mathlib are (empirical observation) not very interested in Euclidean geometry. It is a somewhat recreational branch of maths these days, which probably explains why.

[Tchsurvives]

i see, ill talk to a few of my friends and see if we can help :) this project is really cool, keep going guys!

[Joseph Myers]

mathlib is designed as an integrated library of mathematics in general and that includes geometry. That means, for example, that setting up geometry at all involved first setting up affine spaces - but the work done on affine spaces in order to be able to say anything about geometry has since been used and extended by people working on lots of other things. It also means that other concepts we need in geometry should be set up in a more generally useful way (providing more generally useful definitions and lemmas is better than providing things very specific to Euclidean geometry). And when something is specific to geometry, it shouldn't be only two-dimensional unless the underlying concept is genuinely limited to two dimensions (for example, we have circumcenter defined for an arbitrary simplex, not just a triangle).

For example, we need to be able to refer to betweenness of points, or points being inside triangles, to even state most IMO geometry problems. Defining that properly means first completing the refactor of convexity to apply to affine spaces, which has been discussed recently, which in turn seems to depend on a refactor of affine spaces so spaces with affine combinations over a semiring underlie a type class asserting those affine combinations agree with those coming from the add_torsor structure. That's also necessary before we can talk cleanly about e.g. the area of a triangle (linking to the measure theory parts of the library).

For example, for oriented angles (which will probably turn out to be much more convenient for formal proofs than the unoriented angles we have, though IMO problems involving angles are stated with unoriented angles) we should first define orientations of vector spaces in general (again, see discussions on Zulip of how that might be done), rather than doing something ad hoc with complex numbers.

I don't think the verbosity of geometry problems (compared to an informal statement) is any more than the verbosity of formal versions of results in other areas, once all the required definitions have been added. It's just that at this point, you probably need to write about 10000 lines more API, in geometry and things it depends on elsewhere in the library, before you can do much in the way of applying it to prove IMO geometry problems.

So "define orientations of vector spaces and prove a load of trivial lemmas about them" is the sort of thing that's more practical at this point towards geometry than actually solving an IMO geometry problem.

[Yaël Dillies]

Just here to drop that the current state of the convexity refactor is indeed "waiting for the affinity refactor" and the state of the affinity refactor is "thinking about how to do it".

[Tchsurvives]

there's something im unsure about

[Tchsurvives]

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
iff.intro
  (assume ⟨a, (h1 : p a ∨ q a)⟩,
    or.elim h1
      (assume hpa : p a, or.inl ⟨a, hpa⟩)
      (assume hqa : q a, or.inr ⟨a, hqa⟩))
  (assume h : (∃ x, p x) ∨ (∃ x, q x),
    or.elim h
      (assume ⟨a, hpa⟩, ⟨a, (or.inl hpa)⟩)
      (assume ⟨a, hqa⟩, ⟨a, (or.inr hqa)⟩))

[Tchsurvives]

i tend to see long expressions like these in the documentation, but i am wondering how one can come up with it himself

[Tchsurvives]

while using the interactive evaluater in vs code, when i type the first line 'iff.intro' it simply throws an error (waiting for more arguments), and i am left unsure what to write

[Tchsurvives]

is there a systematic way to go about learning how to 'chain' logic like these together? i have played the natural number game and done some simple exercises but i still don't really get the gist of it

[Scott Morrison]

1. Use tactics, rather than term mode.
2. In term mode, if you write _ for missing arguments and hover over the _ you will get a message telling you the expected type of that argument.
3. Read the error message: it's telling you what sort of thing you need to write next.

[Scott Morrison]

Until you understand what is going on though, learn to use tactics first.

[Scott Morrison]

If I were showing someone how to do this proof, I would write

import tactic

example {α : Type*} (p q : α → Prop) : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
begin
  split,
  { intro h,
    rcases h with ⟨x, P|Q⟩,
    { left,
      use x, use P, },
    { right,
      use x, use Q, }, },
  { intro h,
    rcases h with ⟨x, P⟩|⟨x, Q⟩,
    { use x,
      left, use P, },
    { use x,
      right, use Q, }, }
end

[Scott Morrison]

Open this in an editor, and click through it, placing your cursor before and after each tactic, looking how the goal view changes.

[Scott Morrison]

Hopefully you will see that at every step, there is only one possible sensible thing to do, and that's what the next tactic does!

[Scott Morrison]

After you can write tactic proofs like this, a second step is learn how to "golf" them into term mode proofs.

[Tchsurvives]

is there a way to shorten this code

[Tchsurvives]

rcases h with ⟨⟨_,⟨_,⟨_,⟨_,⟨_,_⟩⟩⟩⟩⟩,⟨_,_⟩⟩,

[Kevin Buzzard]

Given that h must be a pretty monstrous term, I'd say that that was a pretty short way of taking it apart!

[Kevin Buzzard]

You can shorten the code by not making such monstrous terms ;-)

[Yaël Dillies]

Tchsurvives said:

rcases h with ⟨⟨_,⟨_,⟨_,⟨_,⟨_,_⟩⟩⟩⟩⟩,⟨_,_⟩⟩,

You can doobtain ⟨⟨_, _, _, _, _, _⟩, _, _⟩ := h,

[Tchsurvives]

h: (∃ (a b c d : pts), α = ∠ b a c ∧ β = ∠ b a d ∧ between c a d) ∧ ang_proper α ∧ ang_proper β

[Tchsurvives]

or perhaps if i put h here, is there a better way to unpack it? (into a b c d and all the $\and$ )

[Yaël Dillies]

I'd put ang_proper α ∧ ang_proper β first.

[Yaël Dillies]

Then obtain ⟨_, _, _, _, _, _, _, _, _⟩ := h will do the job.

[Tchsurvives]

that works great :)

[Tchsurvives]

what will happen when i have two hypotheses of the same name

[Tchsurvives]

like

a: pts
a: pts

[Tchsurvives]

also, what is the difference between a semicolon and a comma in tactic mode

[Yaël Dillies]

Weird stuff. The most common thing is that you get confused yourself and mistake one variable for the other. Second thing that can happen is that Lean picks the wrong variable for you. I'd advise on avoiding homonyms.

[Yaël Dillies]

A comma is the usual way to separate different tactic invokations. A semicolon means the next tactic invokation applies to all goals.

[Yaël Dillies]

Arf yes

[Tchsurvives]

is there a way of 'intro'-ing a hypothesis in tactic mode

[Tchsurvives]

then having another goal to prove that hypothesis

[Tchsurvives]

intro h := (d ≠ e),

[Tchsurvives]

i hope my question makes sense

[Eric Wieser]

tactic#have

[Tchsurvives]

This code below didnt really work for me though, perhaps theres something im missing?

have h := (d ≠ e),

[Tchsurvives]

Where

d e : pts

[Johan Commelin]

@Tchsurvives you probably want have : instead of have :=

[Tchsurvives]

oh! that works :D thanks

[Yury Yarovikov]

Hi! My name is Yury Yarovikov, I am a research scientist at AIRI. I currently do research on neural theorem proving in Lean, and I would like to join the community, not only for my proffesional research, but also for fun: I primarily view myself as a mathematician, and ITP is an exciting topic that concerns two of my main interests: mathematics and AI. Anyway, I'll be happy to chat about ITP, Lean, automated theorem proving and other stuff

[Tchsurvives]

hi! Screenshot-2022-07-12-at-8.29.55-PM.png sorry what can i use to

1. move the x1 x2 away from injf
   usually if it was in the goal i would use intros x1 x2

2. replace the \exists (g : Y \right X) with g1
   apply exists.intro g1 didnt seem to work, although it worked for another example (see below picture)

[Tchsurvives]

Screenshot-2022-07-12-at-8.33.00-PM.png Screenshot-2022-07-12-at-8.33.05-PM.png

[Tchsurvives]

over here apply exists.intro y seemed to work, but not for functions?

[Henrik Böving]

1. You don't want to "move it away", right now injf says for any x1 x2 this proposition holds. The fact that it's shown in { } means that the parameters will be inferred automatically by Lean. That means if you use this hypothesis somewhere Lean will automatically figure out what x1 and x2 should be based on the first argument (The equality) or the expected result type from where you are using it. So the short answer is if you wish to use it for a concrete x1 x2 just use it, Lean will fill it in on its own in this case. If it was not in { } you would have to explicitly pass them e.g. exact injf myX myOtherX myHypothesis, as it is right now you could write exact injf myHypothesis and Lean will know what x1 and x2 should be.

2. Note that your g is not written g1 but with a unicode index, typable as g\_1 in vscode/emacs if you apply that it will work.

[Violeta Hernández]

Unless you're trying to prove this on your own, you should take a look at docs#function.inv_fun

[Tchsurvives]

2. oh it was my bad i forgot a comma oops haha

[Tchsurvives]

Hey just wondered if there’s any previous work on correctness of graph theory algorithms like dijkstra and prim?

[Kyle Miller]

Mathlib doesn't have these things, but many of them have been formalized before (for example, searching google for "coq dijkstra's algorithm" yielded some github repositories as well as this paper).

One thing about graph theory algorithms is that the way you actually encode a graph is important. In mathlib's graph theory library, we're focusing on encodings useful for theory rather than ones that are useful for efficient algorithms. For example, docs#simple_graph is an adjacency matrix, rather than using adjacency lists.

We would probably want these algorithms for programming purposes, so some of the effort would be to find a good API for that.

[Jeremy Tan]

Is anyone here? My real name is Jeremy Tan Jie Rui and I just installed Lean

[Martin Dvořák]

Yes I am here.

[Jeremy Tan]

image.png I have this thing now, what do I do to get mathlib4 up and running?

[Martin Dvořák]

Did you install the lean4 plugin into VS Code?

[Jeremy Tan]

yes

[Jeremy Tan]

As you can see from the screenshot I already ran lake init ringel to (seemingly) create a new package

[Martin Dvořák]

After installing the plugin, you probably saw Failed to start 'lean' language server with two buttons under.

[Jeremy Tan]

yeah, clicked that button already

[Martin Dvořák]

Did you click on Install Lean using Elan there?

[Jeremy Tan]

yes

[Martin Dvořák]

In that case, after clicking into the .lean file, an Infoview should appear in the right panel.

[Martin Dvořák]

Can you see Infoview anywhere?

[Jeremy Tan]

image.png ...but I closed the infoview

[Jeremy Tan]

so I reopened VS Code and typed the above commands

[Jeremy Tan]

so there are these .lean files which I understand contain the actual theorems

[Martin Dvořák]

You will need to see the Infoview for pretty much anything.

[Martin Dvořák]

There are probably no theorems in the new project.

[Jeremy Tan]

image.png OK, got the infoview showing

[Jeremy Tan]

(by the way the package is called ringel because I ultimately intend this to contain a formally verified proof of the Ringel–Youngs theorem or Heawood conjecture)

[Jeremy Tan]

Now I have created a new file test.lean and put

import topology.basic

#check topological_space

but it says that topology is an unknown package, how do I get the lean4 version of this package from mathlib?

[Jeremy Tan]

(I know that Lean 4 is the future, so I don't want to rely on Lean 3 things)

[Martin Dvořák]

I am not up to date, but I suggest you first check if the desired part of the topology package has already been ported to Lean 4:
https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Topology

[Jeremy Tan]

but how do I actually get it into my computer so that the code above will work?

[Jeremy Tan]

is there another command for that?

[Jeremy Tan]

wait...

[Matthew Ballard]

You can get up to date info on which files have made it to Lean 4 at: https://leanprover-community.github.io/mathlib-port-status

[Matthew Ballard]

If you want to import mathlib4 files, you need to modify your configuration file, lakefile.lean, to list mathlib4 as a dependency. Alternately, you can delete your current directory and run lake init ringel math which will configure your module to use mathlib4 automatically.

[Jeremy Tan]

I actually did delete my current directory and then ran lake init ringel math

[Jeremy Tan]

Now, however, I am running lake exe cache get and it is not providing any progress updates

[Jeremy Tan]

Attempting to download 1611 file(s)

[Matthew Ballard]

It is not very chatty

[Matthew Ballard]

But it should not take long

[Matthew Ballard]

It depends on your connection speed but usually I don't wait more than a minute for it to finish

[Jeremy Tan]

image.png The command is still not terminating after 5 minutes

[Jeremy Tan]

Ctrl-C or no?

[Matthew Ballard]

Yes

[Matthew Ballard]

Did you copy a lean-toolchain file from another folder?

[Jeremy Tan]

what copying toolchains? I simply followed the instructions on https://github.com/leanprover-community/mathlib4 starting from step 3

[Matthew Ballard]

What are the contents of your lean-toolchain and what is the output of lake update?

[Jeremy Tan]

how do I view the contents of lean-toolchain

[Matthew Ballard]

It is in the root directory of your project. You can view it in VS Code (or another editor or call cat)

[Alex J. Best]

Parcly Taxel said:

Now I have created a new file test.lean and put

import topology.basic

#check topological_space

but it says that topology is an unknown package, how do I get the lean4 version of this package from mathlib?

this is a lean 3 style import btw, files in Lean 4 look like import Mathlib.Topology.Basic

[Jeremy Tan]

Matthew Ballard said:

What are the contents of your lean-toolchain and what is the output of lake update?

lean-toolchain reads leanprover/lean4:nightly-2023-02-24

[Jeremy Tan]

lake update doesn't seem to output anything

[Jeremy Tan]

now I put

import Mathlib.Topology.Basic

#check topological_space

and suddenly it's building everything

[Matthew Ballard]

The purpose of cache is to pull copies of the built files so you don't have to wait. Building everything locally can take a while depending on your machine.

[Jeremy Tan]

I don't know why lake exe cache get didn't work, why it hung

[Matthew Ballard]

I assume you are on Linux? What is the output of curl -V?

[Jeremy Tan]

I am on Ubuntu 22.10

[Jeremy Tan]

curl -V is

curl 7.85.0 (x86_64-pc-linux-gnu) libcurl/7.85.0 OpenSSL/3.0.5 zlib/1.2.11 brotli/1.0.9 zstd/1.5.2 libidn2/2.3.3 libpsl/0.21.0 (+libidn2/2.3.2) libssh/0.9.6/openssl/zlib nghttp2/1.49.0 librtmp/2.3
Release-Date: 2022-08-31
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli GSS-API HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM NTLM_WB PSL SPNEGO SSL threadsafe TLS-SRP UnixSockets zstd

[Jeremy Tan]

As for the topological space check, the building finished but now I get unknown identifier 'topological_space'

[Alex J. Best]

Its called docs4#TopologicalSpace now I think

[Matthew Ballard]

The naming convention has changed as Alex mentioned. You should use TopologicalSpace

[Matthew Ballard]

You can try lake exe cache get! which forces a redownload. (Stepping away for a bit)

[Jeremy Tan]

image.png is the wavy blue line a problem?

[Jeremy Tan]

ok it probably isn't, it just means that the result can be seen by hovering?

[Logan Murphy]

That's right

[Jeremy Tan]

good, that means I can start following https://leanprover.github.io/theorem_proving_in_lean4/title_page.html

[Jeremy Tan]

regarding lake exe cache get it eventually ended with an error:

uncaught exception:
gzip: stdin: unexpected end of file
tar: Unexpected EOF in archive
tar: Unexpected EOF in archive
tar: Error is not recoverable: exiting now

[Anne Baanen]

This means one of your downloaded files is corrupted. Use lake exe cache get! to retry, overwriting all files.

[Jeremy Tan]

I did the command with the ! and I got the same error

[Anne Baanen]

That's weird, it might mean one of the files in the cache is broken. Let me see if it works for me...

[Anne Baanen]

No, it seems everything works for me:

$ lake exe cache get!
Attempting to download 1613 file(s)
Decompressing 1613 file(s)
$ git status
On branch master
Your branch is up to date with 'origin/master'
$ git rev-parse HEAD
5d07683a061300f8b6b528a735af4914570748ef

[Jeremy Tan]

image.png ehh, I did it again and it exited successfully

[Jeremy Tan]

(note the blue circle which indicates success)

[Anne Baanen]

Great! Then you can restart the Lean server in VS Code and import topology

[Jeremy Tan]

Why does this not work for lambda abstraction?

theorem introduce (hp: p) (hq: q): p → q :=
  fun (hp: p) => hq

[Jeremy Tan]

This is trying to prove "if p and q, then (p implies q)"

[Kevin Buzzard]

Works for me. What do you mean by "does not work"?

[Matthew Ballard]

You also only need q to be true for this.

[Jeremy Tan]

unused variable hp

[Matthew Ballard]

That is a warning (yellow) from the linter. Not an error (red)

[Matthew Ballard]

For Lean there are two hp in the context

[Kevin Buzzard]

Right -- your code has both a free variable hp and a bound variable also called hp

[Kevin Buzzard]

and the linter is complaining that in fact your code uses neither :-)

[Jeremy Tan]

I remember learning Coq in one of my university modules but I can't remember much about that language itself

[Jeremy Tan]

theorem introduce (p) (hq: q): p → q :=
  fun (p) => hq

still complains that p is unused

[Matthew Ballard]

Replace the bound variable by _

[Jeremy Tan]

theorem introduce (hq: q): p → q :=
  fun _ => hq

so this produces no errors or warnings. I suppose this is the very essence of introducing an implication, right?

[Logan Murphy]

In your first example, there is a name capture of the type p (defined in the first line) by the lambda-abstracted variable also named p (in the second line).

[Logan Murphy]

In your second example, Lean figures that p is some type, and so it knows the type of the abstracted value _ needs to be p.

[Logan Murphy]

You could keep the explicit type annotation for the abstracted variable even with the wildcard _ (here I use Prop, but any types would work)

theorem introduce (p  q: Prop) (hq: q): p → q :=
  fun (_ : p) => hq

[Jeremy Tan]

I just made this proof by myself; could this be made terser without sacrificing readability?

example: (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  ⟨fun lhs => show p ∨ (q ∨ r) from lhs.elim
    (fun pq => pq.elim (fun pp => Or.inl pp) (fun qq => Or.inr (Or.inl qq)))
    (fun rr => Or.inr (Or.inr rr)),
  fun rhs => show (p ∨ q) ∨ r from rhs.elim
    (fun pp => Or.inl (Or.inl pp))
    (fun qr => qr.elim (fun qq => Or.inl (Or.inr qq)) (fun rr => Or.inr rr))⟩

[Logan Murphy]

Not sure if everyone would consider this more readable, but some of these lambda-abstracted nested propositional rule applications can be shorted to compositions of the rules . I guess it's only readable assuming you know how Or.elim works

example: (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  ⟨fun lhs : (p ∨ q) ∨ r => show p ∨ (q ∨ r) from
  lhs.elim
    (fun pq => pq.elim (Or.inl) (Or.inr ∘ Or.inl))
    (Or.inr ∘ Or.inr),
  fun rhs : p ∨ q ∨ r => show (p ∨ q) ∨ r from
  rhs.elim
    (Or.inl ∘ Or.inl)
    (fun qr => qr.elim (Or.inl ∘ Or.inr) (Or.inr))⟩

[Jeremy Tan]

Well I think I'm getting the hang of this. In a valid proof an expression is at once a function and a proof, and the result of applying functions to each other constructs (parts of a) proof

[Jeremy Tan]

But the proof that sqrt(2) is irrational doesn't seem to be in mathlib4

[Kevin Buzzard]

Here's some other proofs of or_assoc:

import Mathlib

example: (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by tauto

example: (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
⟨ by rintro ((hp | hq) | hr)
     { left; assumption }
     { right; left; assumption }
     { right; right; assumption },
  by rintro (hp | hq | hr)
     { left; left; assumption }
     { left; right; assumption }
     { right; assumption }⟩

example: (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
⟨ λ hpqr => hpqr.elim (λ hpq => hpq.elim Or.inl $ λ hq => Or.inr $ Or.inl hq) λ hr => Or.inr $ Or.inr hr,
  λ hpqr => hpqr.elim (λ hp => Or.inl $ Or.inl hp) $ λ hqr => hqr.elim (λ hq => Or.inl $ Or.inr hq) Or.inr⟩

Irrationality of sqrt(2) is in mathlib3, it's docs#irrational_sqrt_two . But you're right, the file it's in hasn't been ported to mathlib4 yet. You can see how far we are from porting it at this link.

[Kevin Buzzard]

You don't need the shows in your proof:

example: (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  ⟨fun lhs : (p ∨ q) ∨ r => lhs.elim
    (fun pq => pq.elim (Or.inl) (Or.inr ∘ Or.inl))
    (Or.inr ∘ Or.inr),
  fun rhs : p ∨ q ∨ r => rhs.elim
    (Or.inl ∘ Or.inl)
    (fun qr => qr.elim (Or.inl ∘ Or.inr) (Or.inr))⟩

[Jeremy Tan]

how do I get the rewrite to work on the last line here?

example (x y: Nat): (x + y) * (x + y) = x * x + 2 * x * y + y * y :=
  calc
    (x + y) * (x + y) = (x + y) * x + (x + y) * y  := by rw [Nat.mul_add]
    _ = x * x + y * x + (x + y) * y                := by rw [Nat.add_mul]
    _ = x * x + y * x + (x * y + y * y)            := by rw [Nat.add_mul]
    _ = x * x + y * x + x * y + y * y              := by rw [←Nat.add_assoc]
    _ = x * x + x * y + x * y + y * y              := by simp [Nat.mul_comm]
    _ = x * x + 2 * x * y + y * y  := by rw [←Nat.two_mul] -- ???

[Jeremy Tan]

oh right, the one-liner example (x y: Nat): (x + y) * (x + y) = x * x + 2 * x * y + y * y := by linarith works

[Jireh Loreaux]

Note that you can solve the whole thing with ring:

example (x y: Nat): (x + y) * (x + y) = x * x + 2 * x * y + y * y := by ring

[Kevin Buzzard]

Parcly Taxel said:

how do I get the rewrite to work on the last line here?

example (x y: Nat): (x + y) * (x + y) = x * x + 2 * x * y + y * y :=
  calc
    (x + y) * (x + y) = (x + y) * x + (x + y) * y  := by rw [Nat.mul_add]
    _ = x * x + y * x + (x + y) * y                := by rw [Nat.add_mul]
    _ = x * x + y * x + (x * y + y * y)            := by rw [Nat.add_mul]
    _ = x * x + y * x + x * y + y * y              := by rw [←Nat.add_assoc]
    _ = x * x + x * y + x * y + y * y              := by simp [Nat.mul_comm]
    _ = x * x + 2 * x * y + y * y  := by rw [←Nat.two_mul] -- ???

The issue is that x * x + x * y + x * y + y * y is actually ((x * x + x * y) + x * y) + y * y so x * y + x * y is not actually a subterm. You'll have to do a targetted rewrite of add_assoc to make this approach work. This is exactly why ring exists, to save us from having to go through this sort of stuff (sure it's fun to start with, but the novelty wears off after a while when you start actually making a gigantic mathematical library).

[Tchsurvives]

How does nat.lean define an alias from nat.zero.succ to the symbol 1? Or is it done in the lean kernel

[Ruben Van de Velde]

In lean 3, this would be an instance of the has_one typeclass

[Matthew Pocock]

Hi - I'm just taking a look at lean. Got as far as installing it and starting on the theorem proving book. I tried this to see what would happen:

#eval Nat.add 3

It barfed. I was expecting it to display some kind of function value or expression tree. Is this my fat fingers or are there constraints on what we can eval?

[Adam Topaz]

Nat.add 3 is a function. What does it mean to evaluate it? Maybe you should try Nat.add 3 5

[Adam Topaz]

You can, in fact, obtain the underlying docs#Lean.Expr and you can do this using theQq library:

import Qq

open Qq

#eval q(Nat.add 3)

[Matthew Pocock]

Adam Topaz said:

Nat.add 3 is a function. What does it mean to evaluate it? Maybe you should try Nat.add 3 5

Thanks. I wasn't sure if functions were values, in this sense.

[Mario Carneiro]

Functions are values, but they don't have an implementation of Repr which is presumably the error you saw

[Mario Carneiro]

The implementation of #eval isn't compiler magic, it just runs Repr T where T is the type of the value you give it in order to produce the text that is displayed

[Mario Carneiro]

(actually it looks for MetaEval but in most cases this will just be a Repr instance)

[Matthew Pocock]

Ah! That makes sense. Thanks. I'll continue on through the tutorial :D

[Matthew Pocock]

Is there a way to report possible bugs in the tutorials? I'm looking at this from Theorem Proving in Lean 4, Chapter 4: Propositions and Proofs:

variable (p q r s : Prop)

theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=
  fun h₃ : p =>
  show r from h₁ (h₂ h₃)

This introduces a variable s which I can't see used.

[Kevin Buzzard]

Is it used later?

[Matthew Pocock]

Kevin Buzzard said:

Is it used later?

Not as far as I can see

[Matthew Pocock]

I'm seeing that there's lots of unicode used, but so far in the tutorial => is spelled out in ascii, rather than using the unicode ⇒ -- is this me being daft? I don't see a shortcut for this symbol in the vscode mode.

[Ruben Van de Velde]

No, seems like this particular character is only used for https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Relator.html#Relator.%C2%ABterm_%E2%87%92_%C2%BB

[Mario Carneiro]

note that the unicode equivalent for the => in fun x => e is ↦ (shortcut \mapsto or \r-|), not ⇒ (shortcut \=>)

[Matthew Pocock]

Mario Carneiro said:

note that the unicode equivalent for the => in fun x => e is ↦ (shortcut \mapsto or \r-|), not ⇒ (shortcut \=>)

Thanks! I don't think that I would have realised that by myself.

[Mario Carneiro]

vscode says the shortcuts in hover messages

[Matthew Pocock]

Mario Carneiro said:

vscode says the shortcuts in hover messages

Cheers :D Found it. I'm working through the chapter 3 exercise, and finding them really fun. I've been trying out different proof assistants the past month, and so far this is the first one where I've actually been enjoying constructing proofs. Finding working with negations more challenging though.