help

Stream: new members

[Steven]

Can anybody help me with setting up lean?

[Steven]

I run ubuntu, and have everything working, except that I cannot import anything out of the mathlib library

[Kevin Buzzard]

we could start by you giving a more precise description of what you have done so far and what is not working, including perhaps screenshots

[Kevin Buzzard]

but here is some generic advice: make sure you have made a project with leanproject and you are opening the project folder with VS Code's "open folder" functionality. PS if you are getting an error in VS Code which contains a link to a web page, read that web page.

[Steven]

damn, you just gave the solution: I hadn't opened the folder using vscode, but it's parent folder
Thank you!!

[kctron sub]

image.png

[kctron sub]

how to prove C y now?

[kctron sub]

i understand it logically, if a or b has to be true, then c is always true, but how to do it in lean

[Mario Carneiro]

The cases h4 with ha hb tactic will split the goal into two goals, one where ha : A y and one with hb : B y

[Mario Carneiro]

If you are using lean 4 (it is hard to tell from your examples whether this is lean 3 or 4), this is written

cases h4 with
| inl ha => ...
| inr hb => ...

[kctron sub]

so what am i writing (im using lean 4)

[kctron sub]

image.png

[Mario Carneiro]

If that code isn't giving you errors, then that's lean 3 code not lean 4

[kctron sub]

i have the sorry in there so its not complete

[Notification Bot]

This topic was moved here from #lean4 > help by Mario Carneiro.

[kctron sub]

oh yeah thanks

[Mario Carneiro]

If you want to do it using term mode, then it would be or.elim h4 (assume ha : A y, ...) (assume hb : B y, ...)

[kctron sub]

whats the ellipsis

[Mario Carneiro]

you can put _ there and lean will tell you what remains to fill in, or sorry like you've been doing

[Mario Carneiro]

this is not the complete proof

[Mario Carneiro]

but you can use it to replace your sorry and make some progress

[kctron sub]

what is supposed to go there though if im just using or.elim

[Mario Carneiro]

Also you should post code as text not images

[Mario Carneiro]

if you replace sorry with or.elim h4 (assume ha : A y, sorry) (assume hb : B y, sorry) it should still work modulo sorry

[kctron sub]

yeah but what am i supposed to put instead of sorry whenever im done with the proof

[kctron sub]

what does or.elim do is what im asking

[Mario Carneiro]

well, if you put _ there instead of sorry, what is the goal state? Do you see how to deduce the goal from there?

[Mario Carneiro]

When you are done with the proof, there will still be or.elim in the proof

[kctron sub]

and do i need to have two assume or cant i just use A y

[Mario Carneiro]

you need two assume, it is a case analysis and there are two cases so you have to handle both

[Mario Carneiro]

that whole line that I wrote should go in the proof

[Mario Carneiro]

What this proof is saying is: "We know A y \/ B y, so either A y or B y is true. Suppose that A y is true. Then ... . So C y is true. Otherwise, B y is true. Then ... , thus C y is true. Hence C y is true in either case."

[Mario Carneiro]

the ... in this proof correspond to the two sorry

[kctron sub]

and what i put in the sorry spot is how im proving C y in both cases

[kctron sub]

??

[kctron sub]

i tried this but both shows are underlined in red

[kctron sub]

section
variable U : Type
variables A B C : U → Prop

variable h1 : ∀x, A x ∨ B x
variable h2 : ∀x, A x → C x
variable h3 : ∀x, B x → C x

example : ∀x, C x :=
assume y,
have h4 : A y ∨ B y, from h1 y,
have h5 : A y → C y, from h2 y,
have h6 : B y → C y, from h3 y,
or.elim h4 (assume ha : A y, show C y, from or.inl h4)
(assume hb : B y, show C y, from or.inr h4)
end

[Thomas Browning]

#backticks

[Mario Carneiro]

^ that's a link btw

[kctron sub]

section
  variable U : Type
  variables A B C : U → Prop

  variable h1 : ∀x, A x ∨ B x
  variable h2 : ∀x, A x → C x
  variable h3 : ∀x, B x → C x

  example : ∀x, C x :=
  assume y,
  have h4 : A y ∨ B y, from h1 y,
  have h5 : A y → C y, from h2 y,
  have h6 : B y → C y, from h3 y,
  or.elim h4 (assume ha : A y, show C y, from or.inl h4)
  (assume hb : B y, show C y, from or.inr h4)
end

[kctron sub]

there you go is it easier for you to read now

[Mario Carneiro]

If you use

or.elim h4 (assume ha : A y, show C y, from _)
(assume hb : B y, show C y, from _)

then the errors on the show go away, so the issue is not the show but the proof you put in for them

[Mario Carneiro]

you correctly said that you wanted to show C y there, but the proof is not showing that

[kctron sub]

section
  variable U : Type
  variables A B C : U → Prop

  variable h1 : ∀x, A x ∨ B x
  variable h2 : ∀x, A x → C x
  variable h3 : ∀x, B x → C x

  example : ∀x, C x :=
  assume y,
  have h4 : A y ∨ B y, from h1 y,
  have h5 : A y → C y, from h2 y,
  have h6 : B y → C y, from h3 y,
  or.elim h4 (assume ha : A y, show C y, from h5 ha)
  (assume hb : B y, show C y, from h6 hb)
end

[Mario Carneiro]

the error message says as much too

type mismatch at application
  (λ (this : C y), this) (or.inl h4)
term
  or.inl h4
has type
  (A y ∨ B y) ∨ ?m_1
but is expected to have type
  C y

It says that or.inl h4 is proving (A y ∨ B y) ∨ something which is not C y

[kctron sub]

no errors

[kctron sub]

im sorry but i think this damn theorem prover is so annoying but thanks for your help

[Mario Carneiro]

what is your background? What got you interested?

[kctron sub]

we have to learn it for school

[Mario Carneiro]

what level are you at? Math or CS oriented?

[kctron sub]

i am doing comp sci B.S.

[kctron sub]

still only on year 2.5

[kctron sub]

wanna do another one

[Mario Carneiro]

I will stick with my earlier suggestion of #tpil then. Once you have the idea of using types for doing logic then it won't be so bad. It helps if you have or get some functional programming experience too

[Mario Carneiro]

and it's actually pretty game-like once you get into it

[Mario Carneiro]

by the way, another fun thing you can do with completed problems is find ways to write them shorter (aka "proof golf"). Here's a short version of your proof:

example : ∀x, C x := λ y, (h1 y).elim (h2 y) (h3 y)

[kctron sub]

section
  variable A : Type
  variable f : A → A
  variable P : A → Prop
  variable  h : ∀x, P x → P (f x)

  example : ∀y, P y → P (f (f y)) :=
  assume y,
  assume f,
  sorry
end

[kctron sub]

where to go from here

[Mario Carneiro]

Hint: h (f y) is a proof of P (f y) -> P (f (f y))

[chensc]

Is there any walking-through videos for the tutorial?

[Kevin Buzzard]

I don't think so, but there is a 24/7 helpline if you're stuck on something (i.e., here)

[chensc]

So I have just started to dive into the tutorial, and got confused, maybe because lack of knowledge in type thorey . There is the following definition:
def is_max (a : ℝ) (A : set ℝ) := a ∈ A ∧ a ∈ up_bounds A

and above it, explanation "/-- Predicate is_max a A means a is a maximum of A -/"

So basically, in Lean, a logical predicate has a type? we can define predicates?
Maybe there is some more detailed explanation which is supposed to be a prerequisite for the tutorial?

and another question: maybe I'm just used to first order set-theoretic logic, but are there any syntax-semantics distinctions in LEAN? I mean, sure Lean deduction system is supposed to be sound, but is it supposed to be complete, in the sense of Godel's Completeness?

[Kevin Buzzard]

a ∈ A ∧ a ∈ up_bounds A is an example of a type in Lean. And a proof of that assertion is a term of that type. Maybe you want to read my witterings on the matter.

[Kevin Buzzard]

Lean is just supposed to be maths, so within Lean, just like within maths, there are things which are true but not provable and things which are undecidable.

[chensc]

But is there a way to prove that Lean is complete as a deduction system? That every true sentence (true in any model) is provable?

[Kevin Buzzard]

you can't prove these things within Lean, you'd have to be reasoning outside the system to do that, and IANAL(ogician).

[Jakub Kądziołka]

the standard foundations are split into two layers, first order logic and ZFC as a theory in this logic. In Lean, the roles of both of these are fulfilled by the same layer, so I don't see any good way to state something similar to Godel's completeness. I also ANAL though

[Kevin Buzzard]

Well all I know is that they proved independence of CH in Lean so some people around here will be able to answer your questions...