Zulip Chat Archive

Stream: general

Topic: rw under a union


view this post on Zulip Kevin Buzzard (May 14 2018 at 19:31):

import data.set
example (α γ : Type)  (F G : γ  set α)
  (H :  (i : γ), F i = G i) : ( (i : γ), F i)  =  (i : γ), G i :=
begin
  refine set.subset.antisymm _ _,
  { apply set.Union_subset_Union,
    intro i,rw (H i),
  },
  { apply set.Union_subset_Union,
    intro i,rw (H i),
  },
end

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:32):

Is there a more sensible method to prove that if F i = G i for all i then the union of the F i equals the union of the G i? I couldn't figure out how to rewrite within the union.

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:32):

Sorry, the Union.

view this post on Zulip Chris Hughes (May 14 2018 at 19:33):

example (α γ : Type)  (F G : γ  set α)
  (H :  (i : γ), F i = G i) : ( (i : γ), F i)  =  (i : γ), G i :=
by rw funext H

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:35):

ha ha that's clever :-)

view this post on Zulip Patrick Massot (May 14 2018 at 19:35):

example (α γ : Type)  (F G : γ  set α)
  (H :  (i : γ), F i = G i) : ( (i : γ), F i)  =  (i : γ), G i :=
by finish

view this post on Zulip Patrick Massot (May 14 2018 at 19:36):

Use automation Luke

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:36):

What does finish do?

view this post on Zulip Patrick Massot (May 14 2018 at 19:36):

It finishes the proof

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:36):

every time??

view this post on Zulip Patrick Massot (May 14 2018 at 19:36):

Yes, nobody told you?

view this post on Zulip Patrick Massot (May 14 2018 at 19:36):

You could also use congr here

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:37):

I've seen congr do rewrites I couldn't do before, I should have tried this

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:37):

I tried conv but I couldn't get that to work either

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:37):

and it was the last line of a 250 line proof :-)

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:37):

so I cheated and asked here.

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:37):

I should be marking Chris' exam script!

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:38):

But I am sick of affine schemes not being schemes

view this post on Zulip Patrick Massot (May 14 2018 at 19:38):

Recently I got to this situation where the goal is a = a (but not if pp.all) and congr alone finished the proof

view this post on Zulip Patrick Massot (May 14 2018 at 19:38):

You should have made that formalization the exam

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:40):

next year

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:40):

What would I do without this chat. Things would go so much more slowly.

view this post on Zulip Patrick Massot (May 14 2018 at 19:47):

I'm always fighting the temptation to post every lemma I need here

view this post on Zulip Patrick Massot (May 14 2018 at 19:48):

I hope to reduce my dependence a bit

view this post on Zulip Patrick Massot (May 14 2018 at 19:49):

But I'm still interested in learning better ways. Here are two lemmas I proved tonight. Usual questions: are there already there? What is the proof from the book?

view this post on Zulip Patrick Massot (May 14 2018 at 19:49):

lemma foldr_ext {α : Type*} {β : Type*} {l : list α} (f f' : α  β  β) (s : β)
  (H :  a  l,  b : β, f a b = f' a b) : foldr f s l = foldr f' s l :=
begin
  induction l with h t IH,
  { simp },
  { have H' := H h (by simp),
    suffices : foldr f s t = foldr f' s t, by simp [H', this],
    apply IH,
    intros a a_t,
    exact H a (by simp[a_t]) }
end

view this post on Zulip Patrick Massot (May 14 2018 at 19:50):

lemma filter_ext {α : Type*} {r: list α} (P P') [decidable_pred P] [decidable_pred P']
  (HP :  i  r, P i = P' i) : filter P r = filter P' r :=
begin
  induction r with h t IH,
  { simp },
  { have HPh : P h = P' h := HP h (by simp),
    have :  (i : α), i  t  P i = P' i,
    { intros i i_t,
      exact (HP i $ by simp [i_t]) },
    by_cases H : P h,
    { have H' : P' h := HPh  H,
      simp [H, H', IH this] },
    { have H' : ¬ P' h := HPh  H,
      simp [H, H', IH this] } }
end

view this post on Zulip Patrick Massot (May 14 2018 at 19:51):

I haven't tried to obfuscate the proofs

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:51):

ha ha can you do the first one with Chris' trick?

view this post on Zulip Patrick Massot (May 14 2018 at 19:52):

But I'm sure two lines are enough

view this post on Zulip Patrick Massot (May 14 2018 at 19:53):

I don't think so, you must not forget we have informations only on elements of the list

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:53):

oh yes

view this post on Zulip Patrick Massot (May 14 2018 at 19:53):

This condition seems a bit too specific

view this post on Zulip Patrick Massot (May 14 2018 at 19:54):

For instance, start with congr and you loose

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:54):

Do I need an import for these? I just this minute upgraded mathlib in my project and I'm re-building it

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:54):

so maybe I just have to wait

view this post on Zulip Kevin Buzzard (May 14 2018 at 19:54):

but I have complaints about foldr currently

view this post on Zulip Patrick Massot (May 14 2018 at 19:54):

import data.list.basic

view this post on Zulip Patrick Massot (May 14 2018 at 19:54):

sorry

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:03):

list.foldr_hom is too strong

view this post on Zulip Patrick Massot (May 14 2018 at 20:04):

Too strong?

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:04):

For your application

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:05):

like Chris' idea

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:05):

Same problem

view this post on Zulip Patrick Massot (May 14 2018 at 20:05):

right

view this post on Zulip Chris Hughes (May 14 2018 at 20:14):

lemma foldr_ext {α : Type*} {β : Type*} {l : list α} (f f' : α  β  β) (s : β)
  (H :  a  l,  b : β, f a b = f' a b) : foldr f s l = foldr f' s l :=
by induction l; simp * {contextual := tt}

view this post on Zulip Patrick Massot (May 14 2018 at 20:14):

:open_mouth:

view this post on Zulip Kenny Lau (May 14 2018 at 20:15):

@Chris Hughes can you derive normal and curvature for r=xi+f(x)j?

view this post on Zulip Patrick Massot (May 14 2018 at 20:15):

@Kenny Lau is this the mechanics exam running joke again?

view this post on Zulip Kenny Lau (May 14 2018 at 20:15):

is it a joke when the exam is tomorrow?

view this post on Zulip Patrick Massot (May 14 2018 at 20:18):

Thank you Chris for not revising mechanics

view this post on Zulip Patrick Massot (May 14 2018 at 20:18):

I disapprove of course

view this post on Zulip Patrick Massot (May 14 2018 at 20:18):

But I still take your proof

view this post on Zulip Chris Hughes (May 14 2018 at 20:19):

I can as of today. @Kenny Lau

view this post on Zulip Kenny Lau (May 14 2018 at 20:19):

ok you win

view this post on Zulip Chris Hughes (May 14 2018 at 20:20):

curvature is dn / ds, where s is arc length I think.

view this post on Zulip Chris Hughes (May 14 2018 at 20:20):

and n is normal

view this post on Zulip Patrick Massot (May 14 2018 at 20:20):

He can golf and compute curvature. What a man!

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:25):

So what is going on with Chris' proof? I feel like I can learn something important here

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:25):

Induction -- sure. Simp does the base case

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:25):

simp doesn't do the inductive step.

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:25):

by itself.

view this post on Zulip Kenny Lau (May 14 2018 at 20:25):

it's a semicolon

view this post on Zulip Kenny Lau (May 14 2018 at 20:26):

simp is simultaneously applied to both goals

view this post on Zulip Kenny Lau (May 14 2018 at 20:26):

the base case and the inductive step

view this post on Zulip Patrick Massot (May 14 2018 at 20:26):

contextual seems to do the magic trick

view this post on Zulip Kenny Lau (May 14 2018 at 20:26):

what does contextual do?

view this post on Zulip Patrick Massot (May 14 2018 at 20:26):

uses context

view this post on Zulip Kenny Lau (May 14 2018 at 20:27):

isn't that simp *?

view this post on Zulip Patrick Massot (May 14 2018 at 20:27):

I hate natural number arithmetic, so I'm cheating for this one. Who could prove me b < a implies b + 1 - a = 0?

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:29):

maybe b < a -> (b + 1) <= a

view this post on Zulip Kenny Lau (May 14 2018 at 20:29):

they are equivalent

view this post on Zulip Kenny Lau (May 14 2018 at 20:29):

definitionally

view this post on Zulip Patrick Massot (May 14 2018 at 20:29):

That could be a step yes

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:29):

oh they are defeq right? ;-)

view this post on Zulip Kenny Lau (May 14 2018 at 20:29):

so something like sub_le_zero_of_le?

view this post on Zulip Kenny Lau (May 14 2018 at 20:29):

(deleted)

view this post on Zulip Kenny Lau (May 14 2018 at 20:30):

oh wait nothing

view this post on Zulip Kenny Lau (May 14 2018 at 20:30):

maybe you want nat.eq_zero_of_le_zero if it exists

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:30):

import data.list.basic
open list
lemma foldr_ext {α : Type*} {β : Type*} {l : list α} (f f' : α  β  β) (s : β)
  (H :  a  l,  b : β, f a b = f' a b) : foldr f s l = foldr f' s l :=
begin
  induction l with h t IH,
  { simp },
  simp * {contextual := tt},
end

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:30):

The semicolon isn't important

view this post on Zulip Kenny Lau (May 14 2018 at 20:30):

it is, because it allows you to apply simp to both goals

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:30):

but the contextual is

view this post on Zulip Kenny Lau (May 14 2018 at 20:30):

without the semicolon you need to write it twice

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:30):

sure

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:31):

Oh I see what you're saying -- what I am saying is trivial.

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:31):

I'm just unravelling the semicolon

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:31):

the contextual isn't important for the base case but for the inductive step we have an inductive hypothesis which needs to be used

view this post on Zulip Kenny Lau (May 14 2018 at 20:32):

does simp [*] work?

view this post on Zulip Gabriel Ebner (May 14 2018 at 20:33):

Contextual does not refer to context as in "induction hypothesis" but to the left-hand side of implications: in a = b -> P a, contextual allows simp to use the equation a=b to simplify P a.

view this post on Zulip Kenny Lau (May 14 2018 at 20:33):

oh

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:33):

nat.sub_eq_zero_iff_le

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:35):

example (a b : ℕ) : b < a → b + 1 - a = 0 := nat.sub_eq_zero_of_le

view this post on Zulip Kenny Lau (May 14 2018 at 20:35):

aha

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:35):

using the trick that b < a is by definition b+1 <= a

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:35):

as Kenny pointed out

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:36):

(see #print nat.lt)

view this post on Zulip Patrick Massot (May 14 2018 at 20:36):

Thank you very much

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:38):

This contextual thing is not documented in my simp docs -- I looked through the source or the docs (I don't remember, maybe the source), saw it was there and mentioned it but basically also said I didn't know what it di.

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:38):

d

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:38):

I don't quite understand Gabriel's explanation -- is a = b -> P a supposed to be a hypothesis or a goal?

view this post on Zulip Kenny Lau (May 14 2018 at 20:39):

goal

view this post on Zulip Kenny Lau (May 14 2018 at 20:39):

hmm, but the goal is not an implication

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:39):

does simp [*] work?

no

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:41):

right -- the implications are in the hypotheses

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:41):

Maybe it's just magic

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:41):

"Lean does not do magic" -- K. Lau, a couple of months ago

view this post on Zulip Kevin Buzzard (May 14 2018 at 20:42):

The comment inspired me to start really thinking about how some of the techniques I had picked up actually worked

view this post on Zulip Mario Carneiro (May 14 2018 at 20:47):

lemma filter_congr {p q : α → Prop} [decidable_pred p] [decidable_pred q]
  : ∀ {l : list α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
| [] _     := rfl
| (a::l) h := by simp at h; by_cases pa : p a;
  [simp [pa, h.1.1 pa, filter_congr h.2],
   simp [pa, mt h.1.2 pa, filter_congr h.2]]

Regarding naming: A theorem of the form a = b -> F a = F b is a "congruence" theorem, named with congr at the end. An "extensionality" theorem has the form F a = F b -> a = b where F is some appropriate (collection of) projection-like operations

view this post on Zulip Mario Carneiro (May 14 2018 at 20:47):

map_congr exists in list.basic but not all list theorems have congr theorems stated for them

view this post on Zulip Patrick Massot (May 14 2018 at 20:50):

Thanks!

view this post on Zulip Patrick Massot (May 14 2018 at 20:50):

Is there any difference between my p x = q x and your p x ↔ q x here?

view this post on Zulip Mario Carneiro (May 14 2018 at 20:51):

No, given propext, but mathlib convention is to use iff instead of eq for equivalent propositions

view this post on Zulip Mario Carneiro (May 14 2018 at 20:52):

Otherwise you have to face weird theorems like (a = b) = c = b

view this post on Zulip Chris Hughes (May 14 2018 at 20:53):

It more or less does intros; simp * I think

view this post on Zulip Chris Hughes (May 14 2018 at 20:53):

But I just realise that can't be what it does, because my example didn't have anything to intro.

view this post on Zulip Chris Hughes (May 14 2018 at 20:53):

and simp * doesn't work

view this post on Zulip Patrick Massot (May 14 2018 at 21:06):

Going from = to iff broke a magic finish success

view this post on Zulip Patrick Massot (May 14 2018 at 21:06):

Probably by breaking a magic cc under the hood

view this post on Zulip Patrick Massot (May 14 2018 at 21:08):

This natural number substraction is really a nightmare. Now I want b + k + 1 - (a + k) = b + 1 - a. It's almost the same I had a couple of days ago. But I'm stuck again...

view this post on Zulip Patrick Massot (May 14 2018 at 21:10):

It seems like I really need omega in the end

view this post on Zulip Patrick Massot (May 14 2018 at 21:23):

Is there any hope to use Coq to tell me a proof Lean could understand?

view this post on Zulip Andrew Ashworth (May 14 2018 at 21:27):

No, in general the names of the lemmas used in Coq would be different

view this post on Zulip Patrick Massot (May 14 2018 at 21:28):

But can you get the sequence of Coq lemmas used by omega?

view this post on Zulip Andrew Ashworth (May 14 2018 at 21:28):

I do not have a Coq installation in front of me to look at the output of omega, so I don't know

view this post on Zulip Andrew Ashworth (May 14 2018 at 21:32):

What I did when i had a lot of similar problems was write down a cheat sheet of relevant cancellation lemmas in my notebook... looking them all up was my biggest hurdle

view this post on Zulip Patrick Massot (May 14 2018 at 21:37):

Now I need H : a ≤ b ⊢ 2 * a + (b + 1 - a) - i - 1 = a - i + b. I give up for today

view this post on Zulip Patrick Massot (May 14 2018 at 21:38):

I have four proofs stuck because of such stupid goals

view this post on Zulip Kenny Lau (May 14 2018 at 21:38):

I understand your feeling

view this post on Zulip Kevin Buzzard (May 14 2018 at 22:58):

Going from = to iff broke a magic finish success

You can just deduce your old version from Mario's version of course...

view this post on Zulip Kevin Buzzard (May 14 2018 at 22:59):

This natural number substraction is really a nightmare. Now I want b + k + 1 - (a + k) = b + 1 - a. It's almost the same I had a couple of days ago. But I'm stuck again...

I really like doing these. Patrick -- just type nat.sub and then ctrl-space escape ctrl-space to see what Lean has, you can just browse through stuff.

view this post on Zulip Kevin Buzzard (May 14 2018 at 23:08):

Actually I don't understand how ctrl-space works at all. I just managed to type nat.sub and get it to display nat.add_sub_add_left (which is useful for you) and then after esc ctrl-space I don't see it any more

view this post on Zulip Kevin Buzzard (May 14 2018 at 23:10):

example (a b k : ) : b + k + 1 - (a + k) = b + 1 - a := calc
b + k + 1 - (a + k) = k + (b + 1) - (k + a) : by simp [add_assoc,add_comm]
... = b + 1 - a : by rw nat.add_sub_add_left

view this post on Zulip Kevin Buzzard (May 14 2018 at 23:11):

example (a b k : ) : b + k + 1 - (a + k) = b + 1 - a := calc
b + k + 1 - (a + k) = b + 1 + k - (a + k) : by simp
... = b + 1 - a : by rw nat.add_sub_add_right

view this post on Zulip Kevin Buzzard (May 14 2018 at 23:22):

Now I need H : a ≤ b ⊢ 2 * a + (b + 1 - a) - i - 1 = a - i + b. I give up for today

If i > a but i <= a + b then this one won't be true, because a - i + b is (a - i) + b

view this post on Zulip Kevin Buzzard (May 14 2018 at 23:28):

Here's some true version:

view this post on Zulip Kevin Buzzard (May 14 2018 at 23:28):

example (a b i : ) (H : a  b) : 2 * a + (b + 1 - a) - i - 1 = a + b - i :=
calc 2 * a + (b + 1 - a) - i - 1 = a + (a + (b + 1 - a)) - i - 1 : by simp [two_mul]
... = a + (b + 1) - i - 1 : by rw nat.add_sub_of_le (le_trans H (nat.le_succ _))
... = (a + b) + 1 - (i + 1)  : by simp [add_assoc,nat.sub_sub]
... = a + b - i : by rw nat.add_sub_add_right

view this post on Zulip Andrew Ashworth (May 14 2018 at 23:37):

This natural number substraction is really a nightmare. Now I want b + k + 1 - (a + k) = b + 1 - a. It's almost the same I had a couple of days ago. But I'm stuck again...

I really like doing these. Patrick -- just type nat.sub and then ctrl-space escape ctrl-space to see what Lean has, you can just browse through stuff.

Ctrl-T and typing sub brings up lemmas with sub inside

view this post on Zulip Mario Carneiro (May 15 2018 at 04:35):

By the way patrick, your "stupid goals" are exactly why I wrote range' to take a start and length instead of start and end. Remember, the value of a good modeling decision is not in the beauty of the statements but in the beauty of the proofs. When things are done right, the proof is like everything is given to you just as you need it, but when you write things in a cumbersome way the proofs become orders of magnitude more cumbersome.

view this post on Zulip Mario Carneiro (May 15 2018 at 04:37):

If your desire for clean statements overrides this concern, then just have two versions and write from the "porcelain" version (which looks nice but is hard to work with) to the "plumbing" version (optimized for proofs) before proving anything, and just translate back at the end.

view this post on Zulip Mario Carneiro (May 15 2018 at 04:51):

But cumbersome is as cumbersome does, here's a proof:

example (a b k : ℕ) : b + k + 1 - (a + k) = b + 1 - a :=
by rw [add_comm a, ← nat.sub_sub, add_right_comm, nat.add_sub_cancel]

and a counterexample:

#eval do
  a ← list.range 3,
  b ← list.range 3,
  i ← list.range 3,
  return $ to_bool (∀ (_:a ≤ b), 2 * a + (b + 1 - a) - i - 1 = a - i + b)
 -- [tt, tt, tt, tt, ff, ff, tt, ff, ff, tt, tt, tt, tt, tt, ff, tt, tt, ff, tt, tt, tt, tt, tt, tt, tt, tt, tt]

That's my version of isabelle quickcheck - I just evaluated the theorem at some small numbers and it sometimes fails.

view this post on Zulip Mario Carneiro (May 15 2018 at 04:59):

Assuming you don't want to learn the beautiful theory of monus on the naturals, but just want to pretend it's regular subtraction, I recommend you treat it like a partial function, in the sense that you never state a theorem about - unless the fact that the RHS is less or equal to the LHS is in the context or otherwise deducible. Your second theorem fails this, since it has a variable i being subtracted from stuff even though there is no upper bound on it.

view this post on Zulip Mario Carneiro (May 15 2018 at 05:04):

hm, maybe this is a slightly nicer quickcheck:

#eval do
  a ← list.range 5,
  b ← list.range 5,
  i ← list.range 5,
  guardb (a ≤ b),
  guardb (2 * a + (b + 1 - a) - i - 1 ≠ a - i + b),
  return (a, b, i)

it returns a list of counterexample triples

view this post on Zulip Chris Hughes (May 15 2018 at 07:12):

hmm, but the goal is not an implication

I think it's because some of the hypotheses are an implication

view this post on Zulip Gabriel Ebner (May 15 2018 at 07:15):

Indeed, look at the (condition of the) induction hypothesis.

view this post on Zulip Patrick Massot (May 15 2018 at 07:29):

Sorry I messed up the last statement. What I really need is 2 * a + (b + 1 - a) - i - 1 = a+b-i assuming a ≤ b and i ∈ range' a (b + 1 - a)

view this post on Zulip Patrick Massot (May 15 2018 at 07:30):

I do have all the right bounds, that's what my foldr_congr and filter_ext are made for

view this post on Zulip Patrick Massot (May 15 2018 at 07:32):

But I should probably think about first proving stuff with cumbersome statements and then try to deduce the natural statements from their twisted versions

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:32):

Patrick I proved what you wanted, right?

view this post on Zulip Patrick Massot (May 15 2018 at 07:32):

This is all about summing for n from a to b, instead of n from a to a+k

view this post on Zulip Patrick Massot (May 15 2018 at 07:33):

You proved one of the things I wanted, thank you very much to you and Mario, but this is another one

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:33):

The "true version" above

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:33):

I thought I'd done everything for oyu

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:33):

what is missing?

view this post on Zulip Patrick Massot (May 15 2018 at 07:33):

Oh sorry

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:33):

:-)

view this post on Zulip Patrick Massot (May 15 2018 at 07:33):

I missed that one

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:34):

I can believe that these things are not to everyone's tastes. I only did it because I quite like them.

view this post on Zulip Patrick Massot (May 15 2018 at 07:34):

I'm glad you're such a pervert

view this post on Zulip Patrick Massot (May 15 2018 at 07:34):

Thank you very much

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:34):

What I especially like is that Mario's proof is only about 30% shorter :-)

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:35):

[and that I was aware that something like this would probably work after I finished mine...]

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:36):

Indeed, look at the (condition of the) induction hypothesis.

Right -- that's what I'm unclear about. Explicitly -- simp * {contextual := tt} does something different to simp in a situation where there is a _hypothesis_ of the form X -> Y, in which case it does...what?

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:37):

Oh -- maybe I do understand.

view this post on Zulip Chris Hughes (May 15 2018 at 07:38):

It's hard to tell because trace.simplify doesn't show you where the rewrites are happening.

view this post on Zulip Kenny Lau (May 15 2018 at 07:39):

@Chris Hughes can you derive Kepler's laws?

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:39):

Where are the mods? Honestly, this place is going down the pan

view this post on Zulip Mario Carneiro (May 15 2018 at 07:40):

Hi there, it's your friendly neighborhood mod

view this post on Zulip Patrick Massot (May 15 2018 at 07:41):

Are we still rewriting under a union?

view this post on Zulip Mario Carneiro (May 15 2018 at 07:41):

It's all connected, I'm sure

view this post on Zulip Patrick Massot (May 15 2018 at 07:41):

What about this one: lemma reverse_range' (a b : ℕ) : reverse (range' a b) = map (λ i, 2*a+b-i-1) (range' a b) ?

view this post on Zulip Mario Carneiro (May 15 2018 at 07:41):

even Kepler's laws get involved in some rewrites

view this post on Zulip Patrick Massot (May 15 2018 at 07:41):

I need a topic "I hate natural numbers"

view this post on Zulip Mario Carneiro (May 15 2018 at 07:42):

That statement reminds me a lot of Kevin's theorem on reversing sums

view this post on Zulip Patrick Massot (May 15 2018 at 07:42):

Of course this is what I'm doing

view this post on Zulip Patrick Massot (May 15 2018 at 07:43):

I'm working on my big_op project

view this post on Zulip Patrick Massot (May 15 2018 at 07:43):

And this statement is partly what motivated my nth_le_map question

view this post on Zulip Patrick Massot (May 15 2018 at 07:43):

I wanted to use ext_le on that one

view this post on Zulip Mario Carneiro (May 15 2018 at 07:44):

suggestion: don't use 2*a+b-i-1, use a-(b+1-a)-i

view this post on Zulip Mario Carneiro (May 15 2018 at 07:45):

otherwise you will spend the whole proof showing that the first thing rewrites to the second

view this post on Zulip Patrick Massot (May 15 2018 at 07:45):

That's part of the nightmare: each time I change my mind on something like this, I must redo all the natural numbers computations lemmas

view this post on Zulip Patrick Massot (May 15 2018 at 07:46):

With 2*a+b-i-1 I can use what Kevin proved last night down the road. Otherwise I return to having nothing

view this post on Zulip Mario Carneiro (May 15 2018 at 07:46):

We call that cruft

view this post on Zulip Mario Carneiro (May 15 2018 at 07:47):

Here's a suggestion: write the theorem so as to minimize the number of rewrites. That is, as soon as you get something technically the same as what you want (in this case, range' a b = map ... (range' a b)), go with it, even if it's written in a kind of weird way

view this post on Zulip Mario Carneiro (May 15 2018 at 07:47):

if you do that for two or three theorems the idioms will stand out

view this post on Zulip Mario Carneiro (May 15 2018 at 07:48):

like in this case keeping b+1-a together as a unit

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:48):

import data.list.basic
open list
lemma foldr_ext {α : Type*} {β : Type*} {l : list α} (f f' : α  β  β) (s : β)
  (H :  a  l,  b : β, f a b = f' a b) : foldr f s l = foldr f' s l :=
begin induction l with A B C, {simp}, -- base case}
  simp at H {contextual := tt},
  sorry,
end

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:48):

I have isolated contextual := tt doing something

view this post on Zulip Gabriel Ebner (May 15 2018 at 07:48):

Right -- that's what I'm unclear about. Explicitly -- simp * {contextual := tt} does something different to simp in a situation where there is a _hypothesis_ of the form X -> Y, in which case it does...what?

Oh no, there is no difference in how simp treats implications in assumptions. If you have a simp lemma/assumption forall x, p x -> f x=g x, then simp will try to prove p a before rewriting f a to g a. And it proves this condition using simp itself! Small demo:

example {n} {q : Prop} (h1 : n=1) (h2 : n*n=n  q) : q := by simp *

Here simp first proves the condition n*n = n (using simp) before rewriting q to true.

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:49):

darn no I haven't

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:49):

but Gabriel has. Thanks!

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:50):

Wait -- there is no contextual here?

view this post on Zulip Gabriel Ebner (May 15 2018 at 07:51):

No, simp can use conditional simp lemmas without contextual:=tt. It uses simp to prove the condition.

view this post on Zulip Patrick Massot (May 15 2018 at 07:51):

Mario, the trouble is I want to prove

lemma big.range_anti_mph {φ : R  R} (P :   Prop) [decidable_pred P] (F :   R) (a b : )
  (Hop :  a b : R, φ (a  b) = φ b  φ a) (Hnil : φ nil = nil) :
  φ (big[()/nil]_(i=a..b | (P i)) F i) = big[()/nil]_(i=a..b | (P (a+b-i))) φ (F (a+b-i))

I don't want the a+b-i in the conclusion to be some weird formula which is the same after a dozen rewrites

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:52):

import data.list.basic
open list
lemma foldr_ext {α : Type*} {β : Type*} {l : list α} (f f' : α  β  β) (s : β)
  (H :  a  l,  b : β, f a b = f' a b) : foldr f s l = foldr f' s l :=
begin induction l with A B C, {simp}, -- base case}
  simp at H,
  simp *,
  -- dammit simp, prove it without using contextual
  simp * {contextual := tt}, -- what just happened?
end

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:52):

That's what I don't get

view this post on Zulip Mario Carneiro (May 15 2018 at 07:52):

I don't either. But I don't see that 2*a+whatever anywhere in the statement either

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:52):

Can I break that last line down into simpler steps?

view this post on Zulip Patrick Massot (May 15 2018 at 07:52):

Knowing of course that I proved

lemma big.anti_mph {φ : R  R}
  (Hop :  a b : R, φ (a  b) = φ b  φ a) (Hnil : φ nil = nil) :
  φ (big[()/nil]_(i  r | (P i)) F i) = big[()/nil]_(i  r.reverse | (P i)) φ (F i)

a long time ago

view this post on Zulip Patrick Massot (May 15 2018 at 07:53):

I'm only fighting the range' stuff

view this post on Zulip Patrick Massot (May 15 2018 at 07:54):

And I have

lemma big.map {J : Type*} (f : I  J) (P : J  Prop) [decidable_pred P] (F : J  R) :
  (big[()/nil]_(j  map f r | (P j)) (F j)) = (big[()/nil]_(i  r | (P (f i))) (F (f i)))

view this post on Zulip Patrick Massot (May 15 2018 at 07:54):

So I wanted to write reverse (range' ...) as a map ... (range' ...)

view this post on Zulip Mario Carneiro (May 15 2018 at 07:55):

What are you going to do with the map once you have it?

view this post on Zulip Gabriel Ebner (May 15 2018 at 07:55):

@Kevin Buzzard Look at the left-hand side of the implication in the induction hypothesis in foldr_ext. Contextual simplification makes a difference here: simp then has the additional assumption a ∈ l, which it can use to apply H.

view this post on Zulip Mario Carneiro (May 15 2018 at 07:56):

Okay I think it is time to split this convo in two

view this post on Zulip Patrick Massot (May 15 2018 at 07:56):

Yes sorry

view this post on Zulip Kevin Buzzard (May 15 2018 at 07:57):

Okay I think it is time to split this convo in two

...given that neither thread is about the topic name ;-)

view this post on Zulip Gabriel Ebner (May 15 2018 at 07:59):

case list.cons
α : Type u_1,
β : Type u_2,
f f' : α  β  β,
s : β,
h : α,
t : list α,
IH : ( (a : α), a  t   (b : β), f a b = f' a b)  foldr f s t = foldr f' s t,
H :  (a : α), a  h :: t   (b : β), f a b = f' a b
 foldr f s (h :: t) = foldr f' s (h :: t)

This is the case for cons. ^^ In order to apply IH, you need to prove its left-hand side using H. And to prove a ∈ h :: t, you need the a ∈ t from IH.

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:07):

I am beginning to understand now. I'm writing out the proof in full, and I have to apply IH and then apply H.

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:08):

So everything is there but somehow it's all in a bit of a tangle

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:13):

I think I have it now

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:13):

lemma got_it (P Q R S : Prop) (IH : (P  R)  S) (H0 : P  Q) (H' : Q  R) : S :=
begin
--simp *, -- fails
simp * {contextual := tt},
end

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:14):

I want to use IH to prove S but the hypothesis of IH isn't immediately true; however simp can prove it using other hypotheses.

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:16):

Thanks Gabriel. To show your time isn't being wasted here I'll add it to the simp docs (once I've done another 8 hours of marking..)

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:20):

All of these conversations (threads about what simp does and doesn't do, threads about how to make type class inference work etc) -- it's in some sense sad that they just appear here and then disappear. The type class inference thread especially contains some really useful tips (in the sense that I was genuinely stuck about three times and then got unstucked by the contents of that thread). I will try to write some notes on that thread too, but I have so much marking at the minute and I have decided that it is time to prove an affine scheme is a scheme so I spend all my spare time on that. I am using the zulip "star" functionality a lot at the minute -- star meaning "get back to this later and write it up properly".

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:20):

Thanks to all as ever.

view this post on Zulip Patrick Massot (May 15 2018 at 08:24):

Next year Lean will mark all this for you

view this post on Zulip Kevin Buzzard (May 15 2018 at 08:24):

That's the plan!

view this post on Zulip Patrick Massot (May 17 2018 at 20:55):

Because this {contextual := true} discussion I'm back to beginner level. Except that, instead of trying simp whatever the goal and hope for the best, I try simp * at * { contextual := true}

view this post on Zulip Patrick Massot (May 17 2018 at 20:56):

And often it works!

view this post on Zulip Kevin Buzzard (Apr 17 2019 at 16:29):

This natural number substraction is really a nightmare. Now I want b + k + 1 - (a + k) = b + 1 - a. It's almost the same I had a couple of days ago. But I'm stuck again...

import tactic.omega
example (k a b : ) : b + k + 1 - (a + k) = b + 1 - a := by omega

It works! It works!

view this post on Zulip Kevin Buzzard (Apr 17 2019 at 16:31):

ha ha it's also referring to a question that was about 100 posts before the answer :D


Last updated: May 14 2021 at 21:11 UTC