Zulip Chat Archive

Stream: general

Topic: heq question


view this post on Zulip Kevin Buzzard (May 20 2018 at 18:53):

I wanted to get affine scheme = scheme finished today, but I have run into a problem whereby restricting to an open subset is not quite the same as restricting to the same not-defeq version of trhe open subset

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:54):

Here's a fairly minimised question

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:54):

import data.set
section oh_heq
parameters (α : Type) (U V W : set α)

lemma HU1 : U  V  W  U := set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)
lemma HV1 : U  V  W  V := set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)
lemma HW1 : U  V  W  W := set.inter_subset_right _ _
lemma HU2 : U  (V  W)  U := set.inter_subset_left _ _
lemma HV2 : U  (V  W)  V := set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_left _ _)
lemma HW2 : U  (V  W)  W := set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_right _ _)

example (F : set α  Type) [ Z : set α, group (F Z)]
(Fres :  X Y : set α, X  Y  F Y  F X)
(i : F U) (j : F V) (k : F W) :
Fres (U  V  W) U HU1 i * Fres (U  V  W) V HV1 j * Fres (U  V  W) W HW1 k
== Fres (U  (V  W)) U HU2 i * Fres (U  (V  W)) V HV2 j * Fres (U  (V  W)) W HW2 k
:= sorry

end oh_heq

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:54):

Is that example true?

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:55):

What's going on is that I am constructing an element of F(U cap V cap W)

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:55):

and I'm constructing "the same" element of F(U cap (V cap W))

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:55):

and I want them to be equal

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:55):

or hequal

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:56):

I feel like I ran into this sort of problem once before

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:56):

and I tried some of the suggestions there

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:56):

(before minimising)

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:56):

congr turns the goal into 29 goals, not all of which are true

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:57):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/dependent.20congr_arg.3F

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:57):

was the old thread

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:58):

simp fails to simplify

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:58):

cc fails

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:59):

hmm maybe I should tell simp that the two intersections are equal

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:59):

 begin
have Hinter : U  V  W = U  (V  W) := by cc,
simp [Hinter],
end

view this post on Zulip Kevin Buzzard (May 20 2018 at 18:59):

fails to simplify

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:00):

Is what I have written provable?

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:00):

I don't understand how to use subst

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

Is there some crazy diamond thing going on?

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

Is the issue that I have put a ring structure on F (U cap V cap W)

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

and a ring structure on F(U cap (V cap W))

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

sorry -- a group structure

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

[in real life I have rings]

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

and a proof that U cap V cap W = U cap (V cap W)

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

but now there's the question as to whether the group structures get identified?

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

aargh

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

Am I in real trouble here??

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

begin
have Hinter : U  V  W = U  (V  W) := by cc,
refine eq.drec_on Hinter _,
congr,
-- now three goals:
-- ⊢ Fres (U ∩ V ∩ W) U HU1 i = Fres (U ∩ V ∩ W) U HU2 i
-- ⊢ Fres (U ∩ V ∩ W) V HV1 j = Fres (U ∩ V ∩ W) V HV2 j
-- ⊢ Fres (U ∩ V ∩ W) W HW1 k = Fres (U ∩ V ∩ W) W HW2 k
sorry,sorry,sorry
end

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

Possible progress

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

import data.set
section oh_heq
parameters (α : Type) (U V W : set α)

lemma HU1 : U  V  W  U := set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)
lemma HV1 : U  V  W  V := set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)
lemma HW1 : U  V  W  W := set.inter_subset_right _ _
lemma HU2 : U  (V  W)  U := set.inter_subset_left _ _
lemma HV2 : U  (V  W)  V := set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_left _ _)
lemma HW2 : U  (V  W)  W := set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_right _ _)

set_option trace.app_builder true

lemma T (F : set α  Type) [ Z : set α, group (F Z)]
(Fres :  X Y : set α, X  Y  F Y  F X)
(i : F U) (j : F V) (k : F W) (s t : set α)
(hst : s = t)
(hsU : s  U) (hsV : s  V) (hsW : s  W)
(htU : t  U) (htV : t  V) (htW : t  W) :
Fres s U hsU i * Fres s V hsV j * Fres s W hsW k
== Fres t U htU i * Fres t V htV j * Fres t W htW k := by subst hst

example (F : set α  Type) [ Z : set α, group (F Z)]
(Fres :  X Y : set α, X  Y  F Y  F X)
(i : F U) (j : F V) (k : F W) :
Fres (U  V  W) U HU1 i * Fres (U  V  W) V HV1 j * Fres (U  V  W) W HW1 k
== Fres (U  (V  W)) U HU2 i * Fres (U  (V  W)) V HV2 j * Fres (U  (V  W)) W HW2 k :=
T _ _ _ _ _ _ _ (set.inter_assoc _ _ _) HU1 HV1 HW1 HU2 HV2 HW2

Trouble is subst doesn't work very well when the expression is more complicated than s = t

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:12):

aah we're back with subst

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:12):

I wrote subst [random_thing] and I get an error I don't understand

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:13):

so I gave up on subst very early

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:13):

you're suggesting I persevere

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:13):

My actual use case has rings and it's addition not multiplication

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:13):

but it's very close to this

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

I used to use eq.drec_on with an explicit motive for things like this. That's really messy.

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:13):

As you saw I tried eq.drec_on and made some progress

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

I perhaps need to learn how to use subst

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

You saw I proved Hinter : U ∩ V ∩ W = U ∩ (V ∩ W)

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

but subst Hinter, which somehow feels like what I want to do, gives me subst tactic failed, hypothesis 'Hinter' is not of the form (x = t) or (t = x)

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

That error message is really unhelpful

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

Does anyone know what it actually means?

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:16):

Hinter looks like both of those forms to me :-)

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:17):

begin
have Hinter : U  V  W = U  (V  W) := by cc,
subst Hinter, -- subst tactic failed, hypothesis 'Hinter' is not of the form (x = t) or (t = x)
sorry
end

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:18):

How is that different to what you're doing?

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

I think it's basically that it has to be a really simple expression. x = t is fine, but anything like f x = t is not. I might be wrong about that.

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

You are telling me that subst won't work unless it literally is (one letter) = (one letter)?

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

Well at the end of the day you apparently proved it and I definitely didn't

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

I think so.

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

set_option trace.app_builder true

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

What was that all about?

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

In this code your goal shouldn't typecheck

begin
have Hinter : U  V  W = U  (V  W) := by cc,
refine eq.drec_on Hinter _,
congr,
-- now three goals:
-- ⊢ Fres (U ∩ V ∩ W) U HU1 i = Fres (U ∩ V ∩ W) U HU2 i
-- ⊢ Fres (U ∩ V ∩ W) V HV1 j = Fres (U ∩ V ∩ W) V HV2 j
-- ⊢ Fres (U ∩ V ∩ W) W HW1 k = Fres (U ∩ V ∩ W) W HW2 k
sorry,sorry,sorry
end

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

but it does.

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

set_option trace.app_builder true

That was because something didn't work and the error message suggested I do that.

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:21):

yeah that was a bit scary with the =

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:21):

but if X = Y then F X = F Y

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:23):

Thanks Chris

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:23):

Indeed your proof works

view this post on Zulip Kevin Buzzard (May 20 2018 at 19:24):

I am currently mulling over having to translate it into the real life situation

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

example (F : set α  Type) [ Z : set α, group (F Z)]
(Fres :  X Y : set α, X  Y  F Y  F X)
(i : F U) (j : F V) (k : F W) :
Fres (U  V  W) U HU1 i * Fres (U  V  W) V HV1 j * Fres (U  V  W) W HW1 k
== Fres (U  (V  W)) U HU2 i * Fres (U  (V  W)) V HV2 j * Fres (U  (V  W)) W HW2 k :=
have Hinter : U  V  W = U  (V  W) := by cc,
@eq.drec_on _ (U  V  W)
(λ s h, Fres (U  V  W) U HU1 i * Fres (U  V  W) V HV1 j * Fres (U  V  W) W HW1 k
== Fres s U (h  HU1) i * Fres s V (h  HV1) j * Fres s W (h  HW1) k) _ Hinter (heq.refl _)

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

Probably the best solution is to get subst to work properly. Might be a good after exams project.

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

Thanks a lot for this Chris! I'll see if this method works in my actual file

view this post on Zulip Mario Carneiro (May 20 2018 at 22:13):

This works, but I'm not very happy with the result

theorem proof_irrel_heq {p q : Prop} (e : p = q) (hp : p) (hq : q) : hp == hq :=
by subst q; congr

example (F : set α → Type) [∀ Z : set α, group (F Z)]
(Fres : ∀ X Y : set α, X ⊆ Y → F Y → F X)
(i : F U) (j : F V) (k : F W) :
Fres (U ∩ V ∩ W) U HU1 i * Fres (U ∩ V ∩ W) V HV1 j * Fres (U ∩ V ∩ W) W HW1 k
== Fres (U ∩ (V ∩ W)) U HU2 i * Fres (U ∩ (V ∩ W)) V HV2 j * Fres (U ∩ (V ∩ W)) W HW2 k
:=
by have := set.inter_assoc U V W;
   congr; try{assumption};
   { apply proof_irrel_heq, congr, assumption }

view this post on Zulip Mario Carneiro (May 20 2018 at 22:17):

Didn't I tell you partial functions give you headaches?

view this post on Zulip Mario Carneiro (May 20 2018 at 22:25):

Why do you have a heq goal in the first place?

view this post on Zulip Kenny Lau (May 20 2018 at 22:34):

because of bad interface

view this post on Zulip Mario Carneiro (May 20 2018 at 22:37):

oh, there's a bug in congr

view this post on Zulip Mario Carneiro (May 20 2018 at 22:40):

meta def congr' : parse small_nat? → tactic unit
| none         := focus1 (assumption <|> (congr_core >>
  all_goals (reflexivity <|> try (congr' none))))
| (some 0)     := failed
| (some (n+1)) := focus1 (assumption <|> (congr_core >>
  all_goals (reflexivity <|> try (congr' (some n)))))

now the following proof works:

by have := set.inter_assoc U V W;
   congr'; apply proof_irrel_heq; congr'

view this post on Zulip Kenny Lau (May 20 2018 at 22:41):

say what

view this post on Zulip Mario Carneiro (May 20 2018 at 22:43):

The congr tactic itself should read:

meta def congr : tactic unit :=
do focus1 (assumption <|> (congr_core >> all_goals (reflexivity <|> try congr)))

instead of

meta def congr : tactic unit :=
do focus1 (try assumption >> congr_core >> all_goals (try reflexivity >> try congr))

view this post on Zulip Mario Carneiro (May 20 2018 at 22:43):

but I don't know if we are still doing bugfixes in 3.4.1

view this post on Zulip Mario Carneiro (May 20 2018 at 22:43):

so I made my own congr instead

view this post on Zulip Mario Carneiro (May 20 2018 at 22:45):

Not sure why those proof irrel goals appear though, they should also be taken care of by congr

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

Why do you have a heq goal in the first place?

I thought of a way around it, in this case.

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:09):

The reason was that I wanted to prove two structures were equal, but one depended on (U cap V cap W) and one on (U cap (V cap W)), because of the way the structures were made (I was trying to prove addition on a quotient type was associative).

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:10):

congr would go insane when presented with the problem (the first time I tried it, it turned my goal into 176 goals, no typo)

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:10):

Kenny suggested a mk_inj solution and that led to the heqs

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:10):

I remember Chris moaning about heqs before

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:11):

But last night, 10 minutes after I switched my laptop off and started doing the dishes

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:11):

I realised I could probably work around it on this occasion, by doing something a mathematican would never understand

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:11):

I should restrict my section on U cap (V cap W) to a section on U cap V cap W :-)

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:12):

This only changes it up to equivalence, which is OK for me

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:13):

[terminology: a sheaf is, amongst other things, a map F : (open sets in a top space) -> (rings) together with restriction maps F(U) -> F(V) whenever V is a subset of U]

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:14):

The concept of restricting to a subset which is non-definitionally-equal to the set you started with is alien to mathematics but it's exactly the crazy idea which will get me out of this hell

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:14):

@Mario Carneiro Is Chris right when he suggests that subst could do with some work? His solution seemed to be "subst hst, where h : s = t, and then apply when s and t are more complicated"

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

as opposed to "subst [the thing we actually want to subst]"

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

I could imagine that Chris might want to learn something about tactics over the summer. He has two months of being paid to work for me and can do anything

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

as long as his boss OK's it

view this post on Zulip Mario Carneiro (May 21 2018 at 07:17):

I was thinking of suggesting that myself. I assume you have some composition axioms, so it might be easiest to work with the restriction from (U/\V)/\W to U/\V/\W

view this post on Zulip Mario Carneiro (May 21 2018 at 07:17):

It's not as crazy as it sounds; it's basically using (part of) the fact that (U/\V)/\W and U/\V/\W are "isomorphic but not equal" in the DTT sense

view this post on Zulip Mario Carneiro (May 21 2018 at 07:18):

it helps to think like in category theory here

view this post on Zulip Mario Carneiro (May 21 2018 at 07:18):

subst is a very basic tactic. It does one thing, and does it well

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

you give it a hypothesis of the form term = x or x = term, and it will eliminate x in favor of term everywhere. This is rather restrictive, but the upside is that it never gets tripped up in dependencies like rw and simp can, because it is implemented purely using eq.drec and the variable restriction ensures that the motive is always type correct

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

Oh -- x = t means x = term? ;-)

view this post on Zulip Mario Carneiro (May 21 2018 at 07:22):

(you can also say subst x instead of subst h when you have h : x = term in the context)

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:22):

isomorphic but not equal is something I know well in the context where the underlying sets are different, but I am only just coming to terms with generalising the idea to situations where the DTTist thinks they're isomorphic and the ZFCist is blinded by this because they think they're equal :-)

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:23):

Unrelated -- I see you wrote (U cap V) cap W v U cap V cap W

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:23):

I claim that you mean U cap (V cap W) vs U cap V cap W

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:23):

and actually this is minorly annoying

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:23):

because my proofs that x is in U cap V cap W

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:23):

all look like <<HU,HV>,HW>

view this post on Zulip Mario Carneiro (May 21 2018 at 07:24):

ah, cap is left assoc?

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:24):

Is this an oversight

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:24):

I assume it is

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:24):

and I already noticed that this was annoying

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:24):

but I wasn't confident enough to know whether there are other reasons for this

view this post on Zulip Mario Carneiro (May 21 2018 at 07:24):

I don't have any strong opinions on whether union and intersection are left or right assoc

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:24):

all I knew is that my proofs were two characters longer than I wanted them to be

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:25):

you would do if you had to keep writing <<HU,HV>,HW>

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:25):

heh

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:25):

maybe I should restrict to U cap (V cap W)

view this post on Zulip Mario Carneiro (May 21 2018 at 07:25):

also lost two chars there

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:25):

yeah but I only have to do that once

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:26):

Something else I noticed

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:26):

was that existsi is kind of dumb

view this post on Zulip Mario Carneiro (May 21 2018 at 07:26):

I never use it tbh

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:26):

existsi (<<HU,HV>,HW>)

view this post on Zulip Mario Carneiro (May 21 2018 at 07:26):

lol no

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:26):

"That doesn't make sense"

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:26):

"You have to tell me the type"

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:26):

"because I don't know the type"

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:27):

"even though the goal is "there exists a proof that x is in U cap V cap W"

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:27):

"

view this post on Zulip Mario Carneiro (May 21 2018 at 07:27):

just use refine instead

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:27):

What are your views on "existsi _,tactic.swap"

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:27):

I think you once told me to avoid it

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:27):

but it does exactly what I want sometimes

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:28):

"let's just remove the bloody exists symbol and make it a goal"

view this post on Zulip Mario Carneiro (May 21 2018 at 07:28):

For exploratory tactic writing it's fine I guess

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:28):

what about definitive scheme writing?

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:29):

:-)

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:29):

I guess it's all exploratory as far as I am concerned

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:29):

OK back to work

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:29):

Thanks for the comments as ever

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:38):

rofl

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:38):

I proved associativity

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:38):

end of proof looks like this

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:38):

  existsi (Ua  Ub  Uc), -- brainwave
  existsi (⟨⟨Hxa,Hxb,Hxc : x  Ua  Ub  Uc),
  existsi (Hstandard _ _ (Hstandard _ _ BUa BUb) BUc),
  existsi (set.subset.refl (Ua  Ub  Uc)),
  existsi ((set.inter_assoc Ua Ub Uc  set.subset.refl _) : Ua  Ub  Uc  Ua  (Ub  Uc)),
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,
  rw presheaf_of_types_on_basis.Hcomp',
  rw presheaf_of_types_on_basis.Hcomp',
  rw add_assoc,

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:38):

restrict to isomorphic set

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

prove some trivialities

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

a bit of rewriting

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

and apply associativity

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

not sure that proof is mathlib-ready

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

have you tried using simp instead of rw?

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:43):

simp insists on rewriting a+b+c as c+a+b

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:43):

on exactly one side

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:43):

so I never got it to do anything useful

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:44):

anyway, this is a breakthrough because if I can prove add_assoc I can prove all the ring axioms

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:46):

simp [add_assoc,more stuff] doesn't even do it when we're on the last line

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:46):

My goal is too messy for simp

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:46):

I need comp

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:47):

lol

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:47):

simp [add_assoc,add_comm,(presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add,presheaf_of_types_on_basis.Hcomp'] turns a goal which is closed by rw add_assoc to a goal which is closed by rw add_comm

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:47):

thanks simp

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

goal is (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sa + (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sb + (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sc = (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sa + ((FPRB.to_presheaf_of_types_on_basis).res _ _ _ sb + (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sc)

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

simp [add_assoc,add_comm],

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

goal becomes (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sc + (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sb = (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sb + (FPRB.to_presheaf_of_types_on_basis).res _ _ _ sc

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

Unless my eyes are deceiving me simp just turned add_assoc into add_comm

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:51):

terms are in a comm_ring

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:53):

obviously-minimised version doesn't exhibit the problem

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:54):

sa,sb,sc all in different rings, the FPRB...res is mapping them down all into the same ring

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:55):

example (R : Type) [comm_ring R] (α β γ : Type) (a : α) (b : β) (c : γ)
(f : α  R) (g : β  R) (h : γ  R) : f a + g b + h c = f a + (g b + h c) := begin
simp [add_assoc,add_comm],
end

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:55):

works fine

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:56):

so it's something in my _s

view this post on Zulip Kevin Buzzard (May 21 2018 at 07:58):

but at the end of the day I have a goal which can be cleared (without errors) either with rw add_assoc or simp [add_assoc,add_comm],rw add_comm

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

hey stupid comm_ring, why are you asking me to prove a+0=a and 0+a=a and a+b=b+a?

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

well, I know why

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

but wouldn't it be nice if you didn't

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

I need a better comm_ring constructor I guess

view this post on Zulip Chris Hughes (May 21 2018 at 08:55):

simp only might help

view this post on Zulip Mario Carneiro (May 21 2018 at 09:10):

you can always add -add_comm to your simp set to fix superfluous rewriting

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:13):

existsi (Ua ∩ Ua)

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:13):

I can't believe I just wrote that

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:13):

proving add_neg

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:14):

just restrict everything down to there and it will be fine

view this post on Zulip Patrick Massot (May 21 2018 at 09:17):

Just to be sure: Kevin, do you know you can write repeat { rw (presheaf_of_rings_on_basis.res_is_ring_morphism FPRB _ _ _).map_add, },?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:22):

yeah, but I like watching the goal slowly decay

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:22):

I just had to write rw is_ring_hom.map_neg (FPRB.res _ _ _);try {apply_instance},

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:22):

that surprised me.

view this post on Zulip Patrick Massot (May 21 2018 at 09:22):

I'm still puzzled each time I need to write apply_instance.

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

I don't understand why Lean doesn't do that for me

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

sometimes

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:23):

I applied map_neg (the statement that a morphism of rings satisfies f(-x)=-f(x))

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:23):

and all of a sudden it asked me if f was a ring hom and was the source a ring?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:23):

and apply_instance said yes

view this post on Zulip Patrick Massot (May 21 2018 at 09:25):

Exactly the kind of situation where I'm puzzled

view this post on Zulip Patrick Massot (May 21 2018 at 09:25):

Why isn't this automatic?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:26):

I dunno

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:26):

I have two choices today

view this post on Zulip Patrick Massot (May 21 2018 at 09:26):

Is it a bug in the apply tactic?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:26):

I could spend a pleasant day verifying the axioms of a ring

view this post on Zulip Patrick Massot (May 21 2018 at 09:26):

(Or simp, refine,...)

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:26):

or I could mark 100 proofs of various trivial lemmas about sup of a set of reals

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:26):

and I am currently at home doing the former

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:27):

and I'm already on add_comm

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:27):

but I really should be doing the latter...

view this post on Zulip Patrick Massot (May 21 2018 at 09:27):

Too bad you can't quite hire Kenny or Chris to mark these exams for you...

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:27):

I knew that once I managed add_assoc the rest would be trivial

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:27):

but it takes time

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:27):

rofl

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:27):

I'm not sure if the university would be keen on students marking their own scripts

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

yep, universities tend to have all kind of stupid administrative rules like that

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:28):

I am much keener on Lean marking their scripts

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:28):

When they're done I might well write a blog post about how Lean does the question

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

Do you know which ones are from Kenny and Chris or are there anonymous?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:28):

yes and yes

view this post on Zulip Patrick Massot (May 21 2018 at 09:29):

Do you mean two out of 100 gave answer in Lean written on paper, and you guessed?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:29):

I recognise their handwriting and I know enough about where they were sitting in the room to be able to work it out

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:30):

In fact I missed Chris' script for Q1

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:30):

so I don't really know

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:30):

but I did notice Kenny's, a combination of the handwriting, the way he presented the arguments, and the fact that I did unfortunately know that his script would be "around this point in the pile"

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:31):

I could be wrong though

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:31):

I have no formal proof that it was Kenny's

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:31):

In fact it was the fact that I recognised Kenny's handwriting that I realised I must have missed Chris' script

view this post on Zulip Kenny Lau (May 21 2018 at 09:32):

where did you get my handwriting sample from?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:32):

You have sent me lots of handwriting in private zulip chats

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:32):

and I am sort of a bit weird about handwriting for some reason

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:32):

I am quite good at recognising it

view this post on Zulip Kenny Lau (May 21 2018 at 09:33):

very interesting

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:33):

I guess I should be clear: I have no way of verifying that the script I strongly suspected was Kenny's, was Kenny's

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:34):

which of course is a good thing

view this post on Zulip Kenny Lau (May 21 2018 at 09:34):

how many questions have you marked?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:34):

1.3

view this post on Zulip Kenny Lau (May 21 2018 at 09:34):

did you mark the sup(A+B)=sup(A)+sup(B)?

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:35):

doing that one today

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:35):

or more of it

view this post on Zulip Kenny Lau (May 21 2018 at 09:35):

I see

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:35):

Hope to get another 0.3 of it done

view this post on Zulip Kevin Buzzard (May 21 2018 at 09:35):

indeed I am just off now

view this post on Zulip Mario Carneiro (May 21 2018 at 09:36):

Sometimes you get those apply_instance goals when you use apply with underscores, due to some strange elaboration order stuff. Essentially those goals are unknown at the time when instance resolution normally happens

view this post on Zulip Mario Carneiro (May 21 2018 at 09:36):

using refine instead may help

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

Do you get a student teacher collusion law suit if some other student realize Kenny answered "This function is continuous because it goes from R to R" as a signal to trigger special marking?

view this post on Zulip Andrew Ashworth (May 21 2018 at 10:19):

I always appreciated automated marking, which you can do for programming assignments (and Lean, too!). Instant feedback if the grader is set up correctly, less need to attend office hours in order to discover that "one special trick professors want you to know about"

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

What do you use for automated marking?

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

Our CS department cobbled together a web server and a bunch of Python scripts

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

Is there anything public?

view this post on Zulip Andrew Ashworth (May 21 2018 at 10:23):

hmm, doubt it. shell scripts aren't the sort of thing that people would even think to release

view this post on Zulip Andrew Ashworth (May 21 2018 at 10:30):

they all tend to be custom solutions based on whatever your institution's favorite content management system is... for example, this one links with Canvas: https://github.com/arthuraa/sf-grader

view this post on Zulip Kevin Buzzard (May 25 2018 at 17:40):

Do you know which ones are from Kenny and Chris or are there anonymous?

OK so I asked some question about sups. I got about 80 correct solutions, of which 79 were a proof by contradiction, and one was constructive. And in Kenny's handwriting. And using the kind of pen he uses. But really -- it is anonymous!

view this post on Zulip Andrew Ashworth (May 25 2018 at 17:42):

You can tell the difference between pens? Does he have a fountain pen?

view this post on Zulip Moses Schönfinkel (May 25 2018 at 17:46):

Perhaps Kenny uses one of those rainbow pencils.


Last updated: May 15 2021 at 22:14 UTC