How to fold statements into the calc block?

Stream: new members

[Sean Leather]

Ah, so #new members is a “stream,” and it has multiple “topics.” Now the terminology is coming together in my head.

[Sean Leather]

And I'm too tired to fully comprehend anything else about Zulip right now. I'm sure I'll find lots of messages in the morning. Good night!

[Chris Hughes]

I like the generated profile pictures here.

[Patrick Massot]

You can still use the opportunity to brighten your previous profile picture before uploading

[Mario Carneiro]

usually this is achieved by constructing the set in a way so that it's obvious that it's a finset. How is isCanonicalPartition defined?

[Johan Commelin]

@Huyen Chau Nguyen to format code on this chat (you can still edit your message) use

```lean
put your code here
```

That way it is formatted as a code block with syntax highlighting.

[hpxmd]

Hello, newb in functional languages here! Im stuck on excercise at "2.4. Introducing Definitions"

/- Above, we discussed the process of “currying” a function, that is, taking a function f (a, b) that takes an ordered pair as an argument, and recasting it as a function f' a b that takes two arguments successively. As another exercise, we encourage you to complete the following definitions, which “curry” and “uncurry” a function.
def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := sorry
def uncurry (α β γ : Type) (f : α → β → γ) : α × β → γ := sorry
-/
def curry (α β γ : Type) (f : α × β → γ) : α → β → γ :=

the closest solution i came up with is

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ (a: α) (b: β) (c: γ), c

returns error:

/home/runner/.code.tio:2:56: error: type mismatch, term
  λ (a : α) (b : β) (c : γ), c
has type
  α → β → γ → γ
but is expected to have type
  α → β → γ

i don't understand how i should return this λ itself. As is can't just leave it like "λ (a: α) (b: β) (c: γ)"

[Mario Carneiro]

you need to use f at some point

[hpxmd]

I tried for like whole day and a half. Im no mathematitian also. Should i just continue reading then?

[Marc Huisinga]

the type signature of curry states that given a value of type alpha and a value of type beta, you get a value of type gamma.
the function you defined with your lambda however takes a value of type alpha, a value of type beta and a value of type gamma.
you need to drop the gamma parameter and come up with a way to produce a value of type gamma from values of types alpha and beta, which will involve using f.

[Patrick Massot]

you need to use f at some point

See, the question was under-specified. No wonder the continuum hypothesis is undecidable.

[Patrick Massot]

Seriously, @hpxmd you need to reread the last paragraph of https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#simple-type-theory

[Johan Commelin]

I tried for like whole day and a half. Im no mathematitian also. Should i just continue reading then?

How many mathematicians do you think know what curry means? I bet that 99% think it is something you put on a sausage.

[Patrick Massot]

That's where the specification is explicitly given

[Patrick Massot]

Johan, I think you spend way too much time in Germany

[hpxmd]

Thanks Patrick, ill try that

[hpxmd]

So i had to read wiki to write it:

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ a, λ b, f(a, b)

is this right?

[Kevin Buzzard]

Yup!

[hpxmd]

then i guess i dont understand this lambda calculus thing

[hpxmd]

thank you

[Patrick Massot]

This has not much to do with lambda calculus

[Kevin Buzzard]

This is exactly completely basic lambda calculus, isn't it?

[Patrick Massot]

No, it's about functions of two variable vs function of one variable with values in functions of one variable.

[Patrick Massot]

You could write the answer as $a \mapsto (b \mapsto f (a,b))$ and you woudln't see any $\lambda$

[Patrick Massot]

The point of lambda-calculus is not using a stupid notation instead of a legible one (reading: the one we are used to). It's about the reduction rules

[Marc Huisinga]

this topic made me curious: when getting started with lean (or a similar language), did the function application syntax without parens feel unnatural or even hard to read to any of you, compared to the syntax with parens?
i'm asking because i've heard this complaint quite a lot over the years from people coming from traditional programming languages, and i've been wondering whether this initial feeling is common for everyone, or whether it's just because i've mostly talked to people that had gotten used to the syntax with parens over the years.

[Kevin Buzzard]

I was a mathematician for 25 years before I learnt any functional programming and yes, the lack of brackets looked super-weird to me. I still occasionally put them in by accident.

[Koundinya Vajjha]

Yes but use it long enough and you'll start hating brackets. :-)

[Patrick Massot]

I've caught myself not writing brackets on paper

[Sebastien Gouezel]

In dynamics it is very common to omit the brackets.

[Scott Morrison]

Meh. We should be writing function application as x f anyway. Losing the brackets is partial progress. :-)

[Andrew Ashworth]

Reverse Polish notation was the best thing in calculators. Maybe I ought to implement it in lean 4, hah.

[Andrew Ashworth]

Then you can stare at expressions like 15 7 1 1 + − ÷ 3 × 2 1 1 + + − and truly live the bracket free life

[Robert Solovay]

How do I enter the Greek letter lambda (symbol for functional abstraction) in the Lean javascript window?

[Kevin Buzzard]

\lam

[Kevin Buzzard]

\la apparently works too

[Robert Solovay]

Thanks.

[Kevin Buzzard]

Nice to see you here, by the way!

[Jesse Michael Han]

welcome!

[jachym simon]

Hi!
I am trying to proof completeness theorem for Hilbert style classical propositional system. While working my way through I ran into this lemma below. The lemma is quite important, but i am not able to prove it. I can do that for n and k particular numbers (1,2,3, ..), but not for n and k general. Is there some way to prove it?

def eval := ℕ → bool
def g(n:ℕ)(f:eval): ℕ → bool := (λ m:ℕ, nat.lt_by_cases (λ h:m<n, f m) (λ h, tt) (λ h, tt))

lemma Lemma1(n:ℕ)(f:eval): ∀ k:ℕ, k < n → g n f k = f k :=

Thanks :)

[Kenny Lau]

def eval := ℕ → bool
def g(n:ℕ)(f:eval): ℕ → bool := (λ m:ℕ, nat.lt_by_cases (λ h:m<n, f m) (λ h, tt) (λ h, tt))

lemma Lemma1(n:ℕ)(f:eval): ∀ k:ℕ, k < n → g n f k = f k :=
λ k hk, dif_pos hk

[jachym simon]

def eval := ℕ → bool
def g(n:ℕ)(f:eval): ℕ → bool := (λ m:ℕ, nat.lt_by_cases (λ h:m<n, f m) (λ h, tt) (λ h, tt))

lemma Lemma1(n:ℕ)(f:eval): ∀ k:ℕ, k < n → g n f k = f k :=
λ k hk, dif_pos hk

Thank you :)

[jachym simon]

HI again,
i have got one more connected question. How do i prove the two below? Thought it would be the same, but it does not seem to work.

def eval := ℕ → bool
def g(n:ℕ)(f:eval): ℕ → bool := (λ m:ℕ, nat.lt_by_cases (λ h:m<n, f m) (λ h, tt) (λ h, tt))

lemma Lemma2(n:ℕ)(f:eval): ∀ k:ℕ, k = n → g n f k = tt  :=
lemma Lemma3(n:ℕ)(f:eval): ∀ k:ℕ, k > n → g n f k = tt  :=

[Mario Carneiro]

It might be simpler to not use lt_by_cases

[Mario Carneiro]

and just use if

[Mario Carneiro]

def eval := ℕ → bool
def g (n : ℕ) (f : eval) (m : ℕ) : bool := if m < n then f m else tt

lemma Lemma2 (n : ℕ) (f : eval) (k : ℕ) (h : k = n) : g n f k = tt :=
have ¬ k < n, from λ h', ne_of_lt h' h,
by simp [g, this]

lemma Lemma3 (n : ℕ) (f : eval) (k : ℕ) (h : k > n) : g n f k = tt :=
have ¬ k < n, from not_lt_of_gt h,
by simp [g, this]

[Daniel Donnelly]

Yep, that was it. It was just updating something in the background

[Juho Kupiainen]

How can I browse Lean's mathlib with VS code. Lean works in VS code, but when I open a file in mathlib (I cloned the code) it cannot resolve the imports. I did "leanpkg configure" and "leanpkg build" in the root directory of mathlib

[Bryan Gin-ge Chen]

Are you opening the entire mathlib directory in VS Code? Often these issues occur when you just try to open a random file from mathlib without having opened the directory as a workspace.

[Juho Kupiainen]

Opening the directory helped after I had created a new project according to the instruction on mathlib github page.

[Marko Grdinić]

import data.rat

def mean (l : list rat) : rat := list.sum l / l.length
def E (f : rat -> rat) (l : list rat) := mean $ list.map f l

theorem E.const_left (f : rat -> rat) (c : rat) (l : list rat)
    : E (fun x, c * f x) l = c * E f l  := sorry

theorem E.const_right (c : rat) (l : list rat) : E (fun x, x * c) l = E id l * c :=
    have mult_dist : (fun x, x * c) = (fun x, c * x), from funext $ fun x, mul_comm x c,
    have const_left : E (fun x, c * x) l = c * E id l, from E.const_left id c l,
    calc
        E (fun x, x * c) l = E (fun x, c * x) l : by rw mult_dist
        ... = c * E id l : by rw const_left
        ... = E id l * c : by rw mul_comm

I am trying to rewrite the above so the extraneous names and type annotations are eliminated. Here is what I want to write.

import data.rat

def mean (l : list rat) : rat := list.sum l / l.length
def E (f : rat -> rat) (l : list rat) := mean $ list.map f l

theorem E.const_left (f : rat -> rat) (c : rat) (l : list rat)
    : E (fun x, c * f x) l = c * E f l  := sorry

theorem E.const_right (c : rat) (l : list rat) : E (fun x, x * c) l = E id l * c :=
    calc
        E (fun x, x * c) l = E (fun x, c * x) l : by {rw (funext $ fun x, mul_comm x c)}
        ... = c * E id l : by {rw (E.const_left id c l)}
        ... = E id l * c : by rw mul_comm

It says that the rewrite tactic fails for some reason. At first I thought that it might have been because in the original version some of the arguments were implicit, but that turned out to not be it. I am not sure what to think about this. I am having trouble with similar rewrites in other places. Lean seems to be bad at inferring the right types in the calc block proofs from expressions on the left side.

[Johan Commelin]

In the first one, maybe you can try by { funext, ext, rw mul_comm }?

[Mario Carneiro]

theorem E.const_right (c : rat) (l : list rat) : E (fun x, x * c) l = E id l * c :=
    calc
        E (fun x, x * c) l = E (fun x, c * x) l : by simp only [mul_comm]
        ... = c * E id l : by rw ← E.const_left; refl
        ... = E id l * c : by rw mul_comm

[Mario Carneiro]

If you use ```lean ... ``` then you get syntax highlighting btw

[Mario Carneiro]

also:

theorem E.const_right (c : rat) (l : list rat) : E (fun x, x * c) l = E id l * c :=
by rw [mul_comm, ← E.const_left]; simp only [mul_comm, id]

[Marko Grdinić]

I am surprised by .. = c * E id l : by rw ← E.const_left; refl. Why rewrite to the left? That does not make much sense to me.

[Mario Carneiro]

rw will rewrite any subterm of the entire goal using the given equation from left to right (or right to left if you give the <-). That means that it can be used to rewrite the right side of the equation as well as the left side, at which point both sides become equal and refl closes the goal

[Marko Grdinić]

Ah, I see. I just realized that ... = c * E id l : by rw E.const_left; refl works too. The type error does not indicate what the problem is.

[Mario Carneiro]

Oh, I guess it was able to match f := \lam x, x even if you write from left to right, I wouldn't have expected that

[Mario Carneiro]

The matching problem from right to left is easier, because it doesn't have to do any higher order matching

[Mario Carneiro]

That is, it's easy to match c * E id l against the pattern ?c * E ?f ?l

[Marko Grdinić]

Yeah, I think I understand it now.

rewrite tactic failed, did not find instance of the pattern in the target expression
  E (λ (x : ℚ), c * id x) l
state:
c : ℚ,
l : list ℚ
⊢ E (λ (x : ℚ), c * x) l = c * E id l

I should have looked at the type error more carefully. c * id x and c * x are not quite the same thing here.

Is there a way to make ... = c * E id l : by {rw (E.const_left id c l)} work by getting it to simplify the expression passed to rw namely the E.const_left id c l ?

[Mario Carneiro]

sure, but it would take more than one line to do so

[Mario Carneiro]

        ... = c * E id l : by {
          have := E.const_left id c l,
          dsimp only [id] at this,
          rw this }

[Mario Carneiro]

it's easier in this case to rewrite backwards so you get E (λ (x : ℚ), c * x) l = E (λ (x : ℚ), c * id x) l, which can then be closed by refl

[Mario Carneiro]

because id x is defeq to x

[Marko Grdinić]

Thank you very much. This was definitely instructive for me.

[Reid Barton]

You can also use erw (E.const_left id c l), which unfolds definitions while matching. However, we tend not to use erw much because it can be slow.

[Reid Barton]

In this case you can also just use the term E.const_left id c l directly, without bothering with by rw