Zulip Chat Archive

Stream: new members

Topic: Use "have" on "or" hypothesis


view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 17:09):

If we had a hypothesis "HX: ∀x : nat, x ^ 2 - 3 * x + 2 = 0" and wanted to prove "false", we could do so by writing "have H3 := HX 3," and then revert and do norm_num.

But "∀x : nat, x ^ 2 - 3 * x + 2 = 0" is just a way of writing "x = 0 ∨ x = 1 ∨ x = 2 ∨ ... → x ^ 2 - 3 * x + 2 = 0". If instead you had "x = 1 ∨ x = 2 ∨ x = 3 → x ^ 2 - 3 * x + 2 = 0", what is the equivalent of the "have" command?

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 17:25):

This works:

example (x : ) : x = 1  x = 2  x = 3  x ^ 2 - 3 * x + 2 = 0  false :=
begin
  intros hx H,
  exact or.elim hx (by { intro h, simp [h] at H, contradiction })
    (by { intro h',
      exact or.elim h' (by { intro h, simp [h] at H, contradiction })
        (by { intro h, simp [h] at H, contradiction }) })
end

There's probably a cleaner way to do it involving pattern-matching / better use of tactics though.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 17:40):

Oh this is weird. If I import tactic.norm_num, the second contradiction above fails because after simp [h] at H we have H : 2 = 0 ∧ 2 ^ 2 - 3 * 2 = 0 instead of H : 2 + (2 ^ 2 - 3 * 2) = 0. That's scary.

And the following gives me no goals by the end, but also a strange error under example:

import tactic.norm_num
example (x : ) : x = 1  x = 2  x = 3  x ^ 2 - 3 * x + 2 = 0  false :=
begin
  intros hx H,
  exact or.elim hx (by { revert H, norm_num })
    (by { intro h',
      exact or.elim h' (by { revert H, norm_num })
        (by { revert H, norm_num }) })
end
/- type mismatch at application
  eq.trans (nat.pow_eq_pow x 2) (norm_num.pow_bit0_helper x x 1 (pow_one x))
term
  norm_num.pow_bit0_helper x x 1 (pow_one x)
has type
  @eq nat (@has_pow.pow nat nat (@monoid.has_pow nat nat.monoid) x 2)
    (@has_mul.mul nat (@semigroup.to_has_mul nat (@monoid.to_semigroup nat nat.monoid)) x x)
but is expected to have type
  @eq nat (@has_pow.pow nat nat nat.has_pow x 2)
    (@has_mul.mul nat (@semigroup.to_has_mul nat (@monoid.to_semigroup nat nat.monoid)) x x) -/

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 17:47):

This works:

example (x : ) : x = 1  x = 2  x = 3  x ^ 2 - 3 * x + 2 = 0  false :=
begin
  intros hx H,
  exact or.elim hx (by { intro h, simp [h] at H, contradiction })
    (by { intro h',
      exact or.elim h' (by { intro h, simp [h] at H, contradiction })
        (by { intro h, simp [h] at H, contradiction }) })
end

There's probably a cleaner way to do it involving pattern-matching / better use of tactics though.

Wait a minute -- that's not the correct goal, though. The order of associativity is wrong.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 17:48):

Oops, you're right! Let me take another look.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 17:48):

I'm actually confused as to how you managed to prove that statement at all -- it's not true that for any x, x^2 - 3x + 2 = 0 is false.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 17:51):

(deleted)

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 17:59):

It's true that the goal (x = 1 ∨ x = 2 ∨ x = 3 → x ^ 2 - 3 * x + 2 = 0) → false can't be proved (I just spent an embarrassingly long time attempting it nonetheless), but as you say, that's quite different from the one I proved above, which is x = 1 ∨ x = 2 ∨ x = 3 → (x ^ 2 - 3 * x + 2 = 0 → false).

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 18:02):

Anyways, returning to your original question, my instinct when I want to use hypotheses of the form H : h1 ∨ h2 is to immediately start writing exact or.elim H (by {}) (by {}) and then start filling in the curly braces. I'd be curious if more experienced members have better advice.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 18:02):

You must've made a typo -- the two statements you've written are identical.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 18:03):

Yes, sorry about that. I've fixed it above.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 18:05):

That can't be right -- (P → Q) → false just means that P → Q is false, which is exactly right, since indeed Q is not always true when P is true. (...I'm letting P: x = 1 ∨ x = 2 ∨ x = 3 and Q : x ^ 2 - 3 * x + 2 = 0)

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 18:06):

On the other hand P → (Q → false) (which you proved, although I have no clue how it worked) can't be right, since that implies Q is always false when P is true. But this isn't right, since you can have x = 1 or x = 2, for which P is true and Q is true.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 18:07):

I must be confused on something basic here, as Lean couldn't possibly accept a proof of a false statement.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 18:09):

I think we should be careful with the quantifiers here. There's a (x : nat) before the statement, which is \forall x in front of everything.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 18:11):

But how does that make a difference?

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 18:14):

You're right. That doesn't. I think I'm getting confused now too. :) Give me a minute.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 18:22):

haha, OK. I see the issue. Remember that subtraction over the nats won't do what you expect, in particular n - m when n < m gives you zero!

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 18:23):

That explains the second part. Let me now put together a proof of the first part.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 18:24):

(deleted)

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 18:25):

Ah, ok, I see. Changing nat to int does break things.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 19:11):

It's still true that 3 ^ 2 - 3 * 3 + 2 = 0 is false in nat, even though subtraction is not the mathematics subtraction on nat.

view this post on Zulip Chris Hughes (Oct 06 2018 at 19:12):

(deleted)

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 19:12):

I guess you should be proving example : ¬ (∀ x, x = 1 ∨ x = 2 ∨ x = 3 → x ^ 2 - 3 * x + 2 = 0) := sorry

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 19:13):

The way to think about it is that if something is directly before the colon, you can move it to the right but you then have to add a universal quantifier. I agree that these things are confusing!

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 20:05):

Consider the following:

example (x : ) : (x = 1  x = 2  x = 3  x ^ 2 - 3 * x + 2 = 0) := sorry
example (x : ) : (x = 1  x = 2  x = 3  x ^ 2 - 3 * x + 2 = 0)  false := sorry

As Kevin says, the stuff to the left of the colon corresponds to a forall quantifier. One thing to keep in mind is that with the forall quantifiers there, these expressions are closely related to certain Prop-valued functions (predicates) over the nats. The first predicate (λ x, x = 1 ∨ x = 2 ∨ x = 3 → x ^ 2 - 3 * x + 2 = 0) happens to be false for every nat, so we have finally:

example : ( x, x = 1  x = 2  x = 3  x ^ 2 - 3 * x + 2 = 0)  false :=
begin
  intro h,
  replace h := h 1 (or.inl rfl),
  contradiction
end

The predicate corresponding to the second one (λ x, (x = 1 ∨ x = 2 ∨ x = 3 → x ^ 2 - 3 * x + 2 = 0) → false) is sometimes true and sometimes false. In particular it's true when x=1, x=2, x=3 but false everywhere else. The Prop version of this (∀x, (x = 1 ∨ x = 2 ∨ x = 3 → x ^ 2 - 3 * x + 2 = 0) → false) then should be false, so

example : ( x, (x = 1  x = 2  x = 3  x ^ 2 - 3 * x + 2 = 0)  false)  false:=
begin
  intro H,
  replace H := H 0,
  simp at H,
  exact H (by { intro h, exact or.elim h (by contradiction) (by contradiction) })
end

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:33):

Thanks -- that makes sense. And although the notation you gave (replace h := h 1 (or.inl rfl),) doesn't seem to be working, I guess just adding the forall x allows one to use the have command normally, i.e. as have h3 := h 3,

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 20:38):

Sorry for all the edits! Thinking about this definitely cleared up a lot of confusion on my end. Hopefully it's all right now.

replace only works in tactic mode, so if you're using term mode, you'll have to do what you did with have.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:47):

Tactic mode just means enclosed by begin and end, right? replace doesn't seem to be working for me in tactic mode either. I'm using the web editor, does that affect things?

view this post on Zulip Kenny Lau (Oct 06 2018 at 20:48):

you need to import tactic.interactive

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:48):

Yes, tactic mode is anything with in a begin/.../end or by {...}.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:48):

Aah, replace is a mathlib tactic?

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:48):

If you have norm_num imported then these basic tactic imports will come too I guess.

view this post on Zulip Patrick Massot (Oct 06 2018 at 20:49):

Congratulations to both of you: you went through a very important Lean initiatory ritual, where the initiate becomes utterly confused, loses all confidence in his or her most elementary mathematical skills. You met ℕ substraction!

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:49):

you need to import tactic.interactive

Oh, thanks, works.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:49):

@Abhimanyu Pallavi Sudhir the lean web editor is horrible! Are you using Lean on a computer you own, or a computer at Imperial?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:50):

@Abhimanyu Pallavi Sudhir the lean web editor is horrible! Are you using Lean on a computer you own, or a computer at Imperial?

My own computer. It (the web editor) seems to be okay for basic proofs, though.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:50):

What OS?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:51):

Windows.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:51):

Patrick -- that logic stuff is super-confusing, and broken - makes things worse :-)

view this post on Zulip Kenny Lau (Oct 06 2018 at 20:52):

Windows.

install a linux VM

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:52):

I do have a Linux VM (Ubuntu, if that still counts). It's just really slow.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:52):

Win10 or 7?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:52):

Win 10.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:52):

OK I have a cheap way of installing Lean on your PC

view this post on Zulip Kenny Lau (Oct 06 2018 at 20:52):

I do have a Linux VM. It's just really slow.

it was a joke

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:53):

For Sage they used to recommend that peolpe on Windows just ran it in a Linux VM

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:53):

(deleted)

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:53):

wait that won't work for you

view this post on Zulip Chris Hughes (Oct 06 2018 at 20:53):

Scott's new method should work, provided there are no spaces in your username.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:54):

https://xenaproject.wordpress.com/getting-lean-and-mathlib-running-in-the-mlc/

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:54):

That way is super-cheap and needs no git or command line.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:54):

However Scott's method is much better, because it will enable you to upgrade properly.

view this post on Zulip Kenny Lau (Oct 06 2018 at 20:55):

https://gist.github.com/kckennylau/611cc453c67df074ad492b4939ddd356

view this post on Zulip Kenny Lau (Oct 06 2018 at 20:55):

this is the one that I use

view this post on Zulip Kenny Lau (Oct 06 2018 at 20:55):

but they don't really recommend this

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 06 2018 at 20:58):

Oh ok. I'll try the cheap way for now -- I'll just re-install the updated versions manually.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 22:07):

this is the one that I use

Kenny, that involves compiling Lean. What's the point of doing that now? Lean has been stable for ages, you can just take the binary.

view this post on Zulip Kenny Lau (Oct 06 2018 at 22:08):

I see

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 23:33):

@Abhimanyu Pallavi Sudhir the way dependent type theory works is that it prefers functions to be defined everywhere and just give junk values at places mathematicians would not normally evaluate them, and it also wants things like - to go from X×XX\times X to XX, for varying XX (see around 300 lines in in core.lean in the core lean library -- class has_sub (α : Type u) := (sub : α → α → α) and class has_div (α : Type u) := (div : α → α → α) ). This means that subtraction on nat has to take two nats and give back a nat (hence 2 - 3 = 0) and division on, say, the reals, has to take two reals and give back a real, hence 1 / 0 = 0. This isn't a logical problem -- they have just artificially extended these functions to places where mathematicians would not normally use them; I think of - and / as being "computer science versions" of these operators, and in the statements of theorems I care about, if either of them are used then I have to do a little check to make sure that the results imply what I want them to say. Of course it doens't matter in the proofs -- you would not object if a mathematician defined a new function f(x,y) to be x/y if y was non-zero but 0 if y was zero and then used f in proofs; that's all that's happening here. Subtraction is particularly horrible because at least division gives the same weird answer in all cases; the behaviour of subtraction actually changes if you move from nat (where it's weird) to int (where it's normal).

view this post on Zulip Andrew Ashworth (Oct 06 2018 at 23:46):

:grinning: Could be worse. With computers, ((0 : uint32_t) - 1) = 4294967295.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 23:47):

so Lean's convention is actually closer in this case ;-)

view this post on Zulip Scott Olson (Oct 07 2018 at 03:15):

I'd argue it's quite natural to define versions of functions like nat.sub or division that restrict their domain (either by type or dependent hypothesis argument) rather than returning "junk" values, but it depends on the use case. For example, it's quite nice that nat.sub precisely matches the structure of list.drop, so you can prove things like list.drop n (list.repeat a m) = list.repeat a (m - n).

But you could look at Idris for example where the total division function has type Nat -> (y : Nat) -> Not (y = Z) -> Nat, or look at List.head : (l : List a) -> {auto ok : NonEmpty l} -> a as opposed to Lean's list.head : Π {α} [inhabited α], list α → α.

On the other hand, both Lean and Idris have a head' : list α → option α alternative which is the preferred API in non-dependent modern programming languages, since you can chain convenient methods on the resulting option to deal with the error case in different ways.

view this post on Zulip Scott Olson (Oct 07 2018 at 03:26):

Though as @Kevin Buzzard pointed out, the interface the operator typeclasses have in Lean would get in the way of doing anything like this for the normal subtraction or division syntax.

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 07:42):

I've long been convinced that Lean's approach is the simplest -- but Abhi is a new student at Imperial and I'd not mentioned this stuff to the students yet, and for a mathematician the convention is quite disconcerting and unexpected. As I pointed out recently, mathematicians expect to divide the integer 1 by the integer 2 and get the rational 1/2 because that's what happens with all the standard maths packages. I recently mentioned a possible typeclass trick which might let us emulate that here but it would need a lot of testing until we got it right.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 07 2018 at 09:12):

@Abhimanyu Pallavi Sudhir the way dependent type theory works is that it prefers functions to be defined everywhere and just give junk values at places mathematicians would not normally evaluate them... the behaviour of subtraction actually changes if you move from nat (where it's weird) to int (where it's normal).

Yeah, I get that -- although I'm not sure why this is better than just defining an object called "undefined" (as javascript does it with 1/0, for instance).

view this post on Zulip Kenny Lau (Oct 07 2018 at 09:16):

then the codomain wouldn't be N anymore

view this post on Zulip Kenny Lau (Oct 07 2018 at 09:16):

I'm not sure if javascript functions care about whether its codomain includes undefined

view this post on Zulip Scott Olson (Oct 07 2018 at 09:19):

In a typed setting, the equivalent of that approach is to return option nat as in one of my examples above. I've seen almost no one ever do this for division, though

view this post on Zulip Mario Carneiro (Oct 07 2018 at 09:27):

This is an option. I think there is actually a function nat.psub that implements this

view this post on Zulip Mario Carneiro (Oct 07 2018 at 09:28):

These sorts of functions often go by the name e.g. "safe division"

view this post on Zulip Scott Olson (Oct 07 2018 at 09:33):

I think part of the argument for just using a junk value is that proofs about division like div_self : a ≠ 0 → a / a = 1 will need to include the precondition a ≠ 0 regardless of which definition for division you choose, and so you might as well pick a simple one.

It would be more controversial to define nat/integer division the Lean way for general purpose programming, but even that has been done

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 09:54):

The point simply seems to be that whilst there are several methods for "fixing the problem" (as mathematicians would interpret it), all the ones I've tried seem to result in the "problem being fixed", the functions now being more of a pain to use in practice, and then the dawning realisation that actually...was this ever really a problem? Or was it just a psychological issue? There is no foundational logical issue -- the computer scientists are just using a different function from mathematician's division, and calling it the same name. Mathematicians just need to be aware that these are not the functions they're used to, that the function they're used to can easily be constructed, but do they really need the functions they're used to? I'm not convinced they do.

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 09:55):

What they need instead is to be educated that the CS functions are different and to be aware of this.


Last updated: May 16 2021 at 22:14 UTC