rw under a union

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

Sorry, the Union.

[Chris Hughes]

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

[Kevin Buzzard]

ha ha that's clever :-)

[Patrick Massot]

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

[Patrick Massot]

Use automation Luke

[Kevin Buzzard]

What does finish do?

[Patrick Massot]

It finishes the proof

[Kevin Buzzard]

every time??

[Patrick Massot]

Yes, nobody told you?

[Patrick Massot]

You could also use congr here

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

so I cheated and asked here.

[Kevin Buzzard]

I should be marking Chris' exam script!

[Kevin Buzzard]

But I am sick of affine schemes not being schemes

[Patrick Massot]

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

[Patrick Massot]

You should have made that formalization the exam

[Kevin Buzzard]

next year

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

I hope to reduce my dependence a bit

[Patrick Massot]

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?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

I haven't tried to obfuscate the proofs

[Kevin Buzzard]

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

[Patrick Massot]

But I'm sure two lines are enough

[Patrick Massot]

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

[Kevin Buzzard]

oh yes

[Patrick Massot]

This condition seems a bit too specific

[Patrick Massot]

For instance, start with congr and you loose

[Kevin Buzzard]

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

[Kevin Buzzard]

so maybe I just have to wait

[Kevin Buzzard]

but I have complaints about foldr currently

[Patrick Massot]

import data.list.basic

[Patrick Massot]

sorry

[Kevin Buzzard]

list.foldr_hom is too strong

[Patrick Massot]

Too strong?

[Kevin Buzzard]

For your application

[Kevin Buzzard]

like Chris' idea

[Kevin Buzzard]

Same problem

[Patrick Massot]

right

[Chris Hughes]

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}

[Patrick Massot]

:open_mouth:

[Kenny Lau]

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

[Patrick Massot]

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

[Kenny Lau]

is it a joke when the exam is tomorrow?

[Patrick Massot]

Thank you Chris for not revising mechanics

[Patrick Massot]

I disapprove of course

[Patrick Massot]

But I still take your proof

[Chris Hughes]

I can as of today. @Kenny Lau

[Kenny Lau]

ok you win

[Chris Hughes]

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

[Chris Hughes]

and n is normal

[Patrick Massot]

He can golf and compute curvature. What a man!

[Kevin Buzzard]

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

[Kevin Buzzard]

Induction -- sure. Simp does the base case

[Kevin Buzzard]

simp doesn't do the inductive step.

[Kevin Buzzard]

by itself.

[Kenny Lau]

it's a semicolon

[Kenny Lau]

simp is simultaneously applied to both goals

[Kenny Lau]

the base case and the inductive step

[Patrick Massot]

contextual seems to do the magic trick

[Kenny Lau]

what does contextual do?

[Patrick Massot]

uses context

[Kenny Lau]

isn't that simp *?

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kenny Lau]

they are equivalent

[Kenny Lau]

definitionally

[Patrick Massot]

That could be a step yes

[Kevin Buzzard]

oh they are defeq right? ;-)

[Kenny Lau]

so something like sub_le_zero_of_le?

[Kenny Lau]

(deleted)

[Kenny Lau]

oh wait nothing

[Kenny Lau]

maybe you want nat.eq_zero_of_le_zero if it exists

[Kevin Buzzard]

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

[Kevin Buzzard]

The semicolon isn't important

[Kenny Lau]

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

[Kevin Buzzard]

but the contextual is

[Kenny Lau]

without the semicolon you need to write it twice

[Kevin Buzzard]

sure

[Kevin Buzzard]

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

[Kevin Buzzard]

I'm just unravelling the semicolon

[Kevin Buzzard]

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

[Kenny Lau]

does simp [*] work?

[Gabriel Ebner]

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.

[Kenny Lau]

oh

[Kevin Buzzard]

nat.sub_eq_zero_iff_le

[Kevin Buzzard]

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

[Kenny Lau]

aha

[Kevin Buzzard]

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

[Kevin Buzzard]

as Kenny pointed out

[Kevin Buzzard]

(see #print nat.lt)

[Patrick Massot]

Thank you very much

[Kevin Buzzard]

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.

[Kevin Buzzard]

d

[Kevin Buzzard]

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

[Kenny Lau]

goal

[Kenny Lau]

hmm, but the goal is not an implication

[Kevin Buzzard]

does simp [*] work?

no

[Kevin Buzzard]

right -- the implications are in the hypotheses

[Kevin Buzzard]

Maybe it's just magic

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

Thanks!

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

It more or less does intros; simp * I think

[Chris Hughes]

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

[Chris Hughes]

and simp * doesn't work

[Patrick Massot]

Going from = to iff broke a magic finish success

[Patrick Massot]

Probably by breaking a magic cc under the hood

[Patrick Massot]

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

[Patrick Massot]

It seems like I really need omega in the end

[Patrick Massot]

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

[Andrew Ashworth]

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

[Patrick Massot]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Patrick Massot]

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

[Patrick Massot]

I have four proofs stuck because of such stupid goals

[Kenny Lau]

I understand your feeling

[Kevin Buzzard]

Going from = to iff broke a magic finish success

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Here's some true version:

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Mario Carneiro]

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.

[Mario Carneiro]

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.

[Mario Carneiro]

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.

[Mario Carneiro]

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.

[Mario Carneiro]

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

[Chris Hughes]

hmm, but the goal is not an implication

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

[Gabriel Ebner]

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

[Patrick Massot]

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)

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

Patrick I proved what you wanted, right?

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

The "true version" above

[Kevin Buzzard]

I thought I'd done everything for oyu

[Kevin Buzzard]

what is missing?

[Patrick Massot]

Oh sorry

[Kevin Buzzard]

:-)

[Patrick Massot]

I missed that one

[Kevin Buzzard]

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

[Patrick Massot]

I'm glad you're such a pervert

[Patrick Massot]

Thank you very much

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

Oh -- maybe I do understand.

[Chris Hughes]

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

[Kenny Lau]

@Chris Hughes can you derive Kepler's laws?

[Kevin Buzzard]

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

[Mario Carneiro]

Hi there, it's your friendly neighborhood mod

[Patrick Massot]

Are we still rewriting under a union?

[Mario Carneiro]

It's all connected, I'm sure

[Patrick Massot]

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

[Mario Carneiro]

even Kepler's laws get involved in some rewrites

[Patrick Massot]

I need a topic "I hate natural numbers"

[Mario Carneiro]

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

[Patrick Massot]

Of course this is what I'm doing

[Patrick Massot]

I'm working on my big_op project

[Patrick Massot]

And this statement is partly what motivated my nth_le_map question

[Patrick Massot]

I wanted to use ext_le on that one

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

We call that cruft

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I have isolated contextual := tt doing something

[Gabriel Ebner]

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.

[Kevin Buzzard]

darn no I haven't

[Kevin Buzzard]

but Gabriel has. Thanks!

[Kevin Buzzard]

Wait -- there is no contextual here?

[Gabriel Ebner]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

That's what I don't get

[Mario Carneiro]

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

[Kevin Buzzard]

Can I break that last line down into simpler steps?

[Patrick Massot]

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

[Patrick Massot]

I'm only fighting the range' stuff

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Patrick Massot]

Yes sorry

[Kevin Buzzard]

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

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

[Gabriel Ebner]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I think I have it now

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Thanks to all as ever.

[Patrick Massot]

Next year Lean will mark all this for you

[Kevin Buzzard]

That's the plan!

[Patrick Massot]

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}

[Patrick Massot]

And often it works!

[Kevin Buzzard]

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!

[Kevin Buzzard]

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