heq question

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

Here's a fairly minimised question

[Kevin Buzzard]

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

[Kevin Buzzard]

Is that example true?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and I want them to be equal

[Kevin Buzzard]

or hequal

[Kevin Buzzard]

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

[Kevin Buzzard]

and I tried some of the suggestions there

[Kevin Buzzard]

(before minimising)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

was the old thread

[Kevin Buzzard]

simp fails to simplify

[Kevin Buzzard]

cc fails

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

fails to simplify

[Kevin Buzzard]

Is what I have written provable?

[Kevin Buzzard]

I don't understand how to use subst

[Kevin Buzzard]

Is there some crazy diamond thing going on?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

sorry -- a group structure

[Kevin Buzzard]

[in real life I have rings]

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

aargh

[Kevin Buzzard]

Am I in real trouble here??

[Kevin Buzzard]

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

[Kevin Buzzard]

Possible progress

[Chris Hughes]

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

[Kevin Buzzard]

aah we're back with subst

[Kevin Buzzard]

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

[Kevin Buzzard]

so I gave up on subst very early

[Kevin Buzzard]

you're suggesting I persevere

[Kevin Buzzard]

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

[Kevin Buzzard]

but it's very close to this

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I perhaps need to learn how to use subst

[Kevin Buzzard]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

That error message is really unhelpful

[Kevin Buzzard]

Does anyone know what it actually means?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

How is that different to what you're doing?

[Chris Hughes]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

I think so.

[Kevin Buzzard]

set_option trace.app_builder true

[Kevin Buzzard]

What was that all about?

[Chris Hughes]

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

[Chris Hughes]

but it does.

[Chris Hughes]

set_option trace.app_builder true

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

[Kevin Buzzard]

yeah that was a bit scary with the =

[Kevin Buzzard]

but if X = Y then F X = F Y

[Kevin Buzzard]

Thanks Chris

[Kevin Buzzard]

Indeed your proof works

[Kevin Buzzard]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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 }

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

because of bad interface

[Mario Carneiro]

oh, there's a bug in congr

[Mario Carneiro]

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'

[Kenny Lau]

say what

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

so I made my own congr instead

[Mario Carneiro]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Kenny suggested a mk_inj solution and that led to the heqs

[Kevin Buzzard]

I remember Chris moaning about heqs before

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

[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]

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

as long as his boss OK's it

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

it helps to think like in category theory here

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and actually this is minorly annoying

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

ah, cap is left assoc?

[Kevin Buzzard]

Is this an oversight

[Kevin Buzzard]

I assume it is

[Kevin Buzzard]

and I already noticed that this was annoying

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

heh

[Kevin Buzzard]

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

[Mario Carneiro]

also lost two chars there

[Kevin Buzzard]

yeah but I only have to do that once

[Kevin Buzzard]

Something else I noticed

[Kevin Buzzard]

was that existsi is kind of dumb

[Mario Carneiro]

I never use it tbh

[Kevin Buzzard]

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

[Mario Carneiro]

lol no

[Kevin Buzzard]

"That doesn't make sense"

[Kevin Buzzard]

"You have to tell me the type"

[Kevin Buzzard]

"because I don't know the type"

[Kevin Buzzard]

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

[Kevin Buzzard]

"

[Mario Carneiro]

just use refine instead

[Kevin Buzzard]

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

[Kevin Buzzard]

I think you once told me to avoid it

[Kevin Buzzard]

but it does exactly what I want sometimes

[Kevin Buzzard]

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

[Mario Carneiro]

For exploratory tactic writing it's fine I guess

[Kevin Buzzard]

what about definitive scheme writing?

[Kevin Buzzard]

:-)

[Kevin Buzzard]

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

[Kevin Buzzard]

OK back to work

[Kevin Buzzard]

Thanks for the comments as ever

[Kevin Buzzard]

rofl

[Kevin Buzzard]

I proved associativity

[Kevin Buzzard]

end of proof looks like this

[Kevin Buzzard]

  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,

[Kevin Buzzard]

restrict to isomorphic set

[Kevin Buzzard]

prove some trivialities

[Kevin Buzzard]

a bit of rewriting

[Kevin Buzzard]

and apply associativity

[Kevin Buzzard]

not sure that proof is mathlib-ready

[Mario Carneiro]

have you tried using simp instead of rw?

[Kevin Buzzard]

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

[Kevin Buzzard]

on exactly one side

[Kevin Buzzard]

so I never got it to do anything useful

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

My goal is too messy for simp

[Kevin Buzzard]

I need comp

[Kevin Buzzard]

lol

[Kevin Buzzard]

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

[Kevin Buzzard]

thanks simp

[Kevin Buzzard]

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)

[Kevin Buzzard]

simp [add_assoc,add_comm],

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

terms are in a comm_ring

[Kevin Buzzard]

obviously-minimised version doesn't exhibit the problem

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

works fine

[Kevin Buzzard]

so it's something in my _s

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

well, I know why

[Kevin Buzzard]

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

[Kevin Buzzard]

I need a better comm_ring constructor I guess

[Chris Hughes]

simp only might help

[Mario Carneiro]

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

[Kevin Buzzard]

existsi (Ua ∩ Ua)

[Kevin Buzzard]

I can't believe I just wrote that

[Kevin Buzzard]

proving add_neg

[Kevin Buzzard]

just restrict everything down to there and it will be fine

[Patrick Massot]

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, },?

[Kevin Buzzard]

yeah, but I like watching the goal slowly decay

[Kevin Buzzard]

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

[Kevin Buzzard]

that surprised me.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

sometimes

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and apply_instance said yes

[Patrick Massot]

Exactly the kind of situation where I'm puzzled

[Patrick Massot]

Why isn't this automatic?

[Kevin Buzzard]

I dunno

[Kevin Buzzard]

I have two choices today

[Patrick Massot]

Is it a bug in the apply tactic?

[Kevin Buzzard]

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

[Patrick Massot]

(Or simp, refine,...)

[Kevin Buzzard]

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

[Kevin Buzzard]

and I am currently at home doing the former

[Kevin Buzzard]

and I'm already on add_comm

[Kevin Buzzard]

but I really should be doing the latter...

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but it takes time

[Kevin Buzzard]

rofl

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

I am much keener on Lean marking their scripts

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

yes and yes

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

In fact I missed Chris' script for Q1

[Kevin Buzzard]

so I don't really know

[Kevin Buzzard]

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"

[Kevin Buzzard]

I could be wrong though

[Kevin Buzzard]

I have no formal proof that it was Kenny's

[Kevin Buzzard]

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

[Kenny Lau]

where did you get my handwriting sample from?

[Kevin Buzzard]

You have sent me lots of handwriting in private zulip chats

[Kevin Buzzard]

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

[Kevin Buzzard]

I am quite good at recognising it

[Kenny Lau]

very interesting

[Kevin Buzzard]

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

[Kevin Buzzard]

which of course is a good thing

[Kenny Lau]

how many questions have you marked?

[Kevin Buzzard]

1.3

[Kenny Lau]

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

[Kevin Buzzard]

doing that one today

[Kevin Buzzard]

or more of it

[Kenny Lau]

I see

[Kevin Buzzard]

Hope to get another 0.3 of it done

[Kevin Buzzard]

indeed I am just off now

[Mario Carneiro]

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

[Mario Carneiro]

using refine instead may help

[Patrick Massot]

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?

[Andrew Ashworth]

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"

[Patrick Massot]

What do you use for automated marking?

[Andrew Ashworth]

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

[Patrick Massot]

Is there anything public?

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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!

[Andrew Ashworth]

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

[Moses Schönfinkel]

Perhaps Kenny uses one of those rainbow pencils.