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...

[edklencl]

import Mathlib.Data.Nat.Notation
example (P : ℕ → Prop)(h:∀ n, P n ↔ ¬(P (n+1)↔P (n+2))):∀ n, P n → P  (n+3):=by
intro n pn
specialize h n

[edklencl]

help

[Timo Carlin-Burns]

(You may be looking for #backticks)

```
your lean code here
```

[edklencl]

(deleted)

[Daniel Weber]

You need to import Mathlib.Data.Nat.Notation for the ℕ notation

[BANGJI HU]

Perhaps you could tell me where to find relevant information?

[BANGJI HU]

@Daniel Weber

[Daniel Weber]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Notation.html#term%E2%84%95

[BANGJI HU]

import Mathlib.Data.Nat.Notation

import Mathlib.Data.Nat.Notation

theorem problem (P : ℕ → Prop) (h : ∀ n, P n ↔ ¬(P (n+1) ↔ P (n+2))) : ∀ n, P n → P (n+3) := by
  intro n hn
  have h1 := h n
  have h2 := h (n+1)
  have h3 := h (n+2)

  apply Classical.byContradiction
  intro hnot

  -- Assume that P(n+1) ↔ P(n+2)
  have h4 : P (n+1) ↔ P (n+2) := by
    apply Iff.intro
    · intro h5
      apply Classical.byContradiction
      intro h6
      have h7 : ¬(P (n+2) ↔ P (n+3)) := h2.mp h5
      have h8 : P (n+2) ↔ P (n+3) := by
        apply Iff.intro
        · intro h9
          apply False.elim
          exact h6 h9
        · intro h9
          exact False.elim (hnot h9)
      exact h7 h8
    · intro h5
      apply Classical.byContradiction
      intro h6
      have h7 : ¬(P (n+1) ↔ P (n+2)) := h1.mp hn
      have h8 : P (n+1) ↔ P (n+2) := by
        apply Iff.intro
        · intro _
          exact h5
        · intro _
          apply False.elim
          exact h6
      exact h7 h8

  -- Now we need to show ¬(P(n+1) ↔ P(n+2)) holds
  have h5 : ¬(P (n+1) ↔ P (n+2)) := h1.mp hn
  exact h5 h4

[BANGJI HU]

type mismatch
h6
has type
¬P (n + 1) : Prop
but is expected to have type
False : Prop

[BANGJI HU]

@Daniel Weber

[BANGJI HU]

import Mathlib.Data.Nat.Notation

import Mathlib.Data.Nat.Notation

theorem problem (P : ℕ → Prop) (h : ∀ n, P n ↔ ¬(P (n+1) ↔ P (n+2))) : ∀ n, P n → P (n+3) := by
  intro n hn
  have h1 := h n
  have h2 := h (n+1)
  have h3 := h (n+2)

  apply Classical.byContradiction
  intro hnot

  -- Assume that P(n+1) ↔ P(n+2)
  have h4 : P (n+1) ↔ P (n+2) := by
    apply Iff.intro
    · intro h5
      apply Classical.byContradiction
      intro h6
      have h7 : ¬(P (n+2) ↔ P (n+3)) := h2.mp h5
      have h8 : P (n+2) ↔ P (n+3) := by
        apply Iff.intro
        · intro h9
          apply False.elim
          exact h6 h9
        · intro h9
          exact False.elim (hnot h9)
      exact h7 h8
    · intro h5
      apply Classical.byContradiction
      intro h6
      have h7 : ¬(P (n+1) ↔ P (n+2)) := h1.mp hn
      have h8 : P (n+1) ↔ P (n+2) := by
        apply Iff.intro
        · intro _
          exact h5
        · intro _
          apply False.elim
          exact h6
      exact h7 h8

  -- Now we need to show ¬(P(n+1) ↔ P(n+2)) holds
  have h5 : ¬(P (n+1) ↔ P (n+2)) := h1.mp hn
  exact h5 h4

[BANGJI HU]

type mismatch
h6
has type
¬P (n + 1) : Prop
but is expected to have type
False : Prop

[BANGJI HU]

@Johan Commelin

[Johan Commelin]

@hand bob Please ask a proper question.

[edklencl]

seem to be some issue at exact h6

[Kevin Buzzard]

Perhaps you could tell me where to find relevant information?

Where did this question come from? Did it also come with links to relevant information?

[Kevin Buzzard]

The error is pretty self-explanatory, right? You've given a proof of the wrong theorem.

[edklencl]

@Johan Commelin

[Yaël Dillies]

Please don't mention people for no reason. Also please don't use several Zulip accounts.

[Andrew Yang]

Also please do not cross-post (c.f. https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/help/near/477210998) this is just splitting up the help you will get.

[Yaël Dillies]

Is this again homework from Heather's course?

[edklencl]

maybe i just want some proposition

[Kevin Buzzard]

Sorry, are you (vvbb) equal to hand bob? Can you please delete one of these accounts? This is adding to the confusion.

[Andrew Yang]

If you can ask a proper question such as where did you get this snippet, what have you tried, what help you need (do you understand the maths and just need lean help?) etc, then people would be in a better position to help you.
If you are not a native english speaker then asking in your native language then google translate would work too.
Kevin in the other thread also gave you some preliminary advices (can someone merge these two threads?) but without more context we can only give these vague hints.

[Notification Bot]

12 messages were moved here from #mathlib4 > induction by Johan Commelin.