## Stream: maths

### Topic: making mynat an add_comm_monoid

#### Kevin Buzzard (Jul 02 2019 at 23:21):

I was trying to prove that a home-rolled nat was an add_comm_monoid in a way which was maximally mathematician-friendly, e.g. no leakage of le or zero: see gist.

My understanding of how Lean works is that I am supposed to come up with a canonical representative for things like mynat.zero -- I choose 0, and similarly I choose 1 for one. That's right, right?

On line 56 I have a zero which is something I never really wanted to see again. Is there a more high-powered tactic which will preserve my choice for 0 as the "canonical representative" of mynat.zero?

Is there a tactic that makes that instance on line 77 by just matching on names?

Finally lines 142 and 146 -- what is the incantation which makes these? I am so bad at making structures. Let's say that you must make an instance of add_semigroup mynat before you make the instance of add_comm_semigroup mynat.

#### Keeley Hoek (Jul 03 2019 at 04:49):

Kevin I think your by common_sense actually is a pretty easily makable tactic

#### Keeley Hoek (Jul 03 2019 at 04:49):

I'll give it a go

#### Keeley Hoek (Jul 03 2019 at 05:07):

...

end mynat

namespace tactic.interactive
open tactic

meta def replace_special_names : name → name
| add := has_add.add
| n := n

meta def common_sense : tactic unit :=
do t ← target,
env ← get_env,
match t with
| expr.app (expr.const sn _) e :=
match env.structure_fields sn with
| some l :=
do n :: _ ← tactic.open_namespaces,
let lf := l.map replace_special_names,
v ← lf.mmap resolve_name,
let s : structure_instance_info := {
struct := some sn,
field_names := l,
field_values := v,
},
e ← to_expr $pexpr.mk_structure_instance s, tactic.exact e | none := fail "goal not a structure" end | _ := fail "unsupported goal" end end tactic.interactive namespace mynat instance : add_monoid mynat := by common_sense ...  #### Kevin Buzzard (Jul 03 2019 at 07:00): It works! Thanks! I hate making structures. I will use it forever. #### Kevin Buzzard (Jul 03 2019 at 07:08): Oh this is great. I have no clue how you're supposed to prove that mynat is a comm_semiring. You seem to have to perform the incantations all in exactly the right order in the official way to do it. This way I can just not even care. I went to the end of my multiplication file and typed instance : comm_semiring mynat := by common_sense and it just gave me a list of the fields for which it has failed and what the error messages were for each. I can then just make them at the end of my multiplication file as part of an api. This is brilliant. It's sort-of an idiot-proof structure maker. #### Scott Morrison (Jul 03 2019 at 10:21): Can we have this in mathlib? Maybe called structure_helper? #### Patrick Massot (Jul 03 2019 at 11:34): Kevin, could you post an updated gist using this tactic? It would make this conversation easier to understand #### Kevin Buzzard (Jul 03 2019 at 13:25): Structure tactic add_comm_monoid nat #### Patrick Massot (Jul 03 2019 at 13:49): Nice! I hope mathlib's naming convention won't interfere with merging this useful tactic #### Kevin Buzzard (Jul 03 2019 at 14:26): @Keeley Hoek I can't make preorders because they have this weird lt_iff_not_le field. set_option auto_param.check_exists false class preorder (α : Type u) extends has_le α, has_lt α := (le_refl : ∀ a : α, a ≤ a) (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c) (lt := λ a b, a ≤ b ∧ ¬ b ≤ a) (lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)  I just want to not define lt or lt_iff_le_not_le -- import the tactic inductive mynat : Type namespace mynat def le : mynat → mynat → Prop := sorry instance : has_le mynat := ⟨le⟩ def le_refl : ∀ a : mynat, a ≤ a := sorry -- I think a,b,c should be implicit but Lean doesn't def le_trans : ∀ a b c : mynat, a ≤ b → b ≤ c → a ≤ c := sorry --instance : preorder mynat := by i_checked_all_teh_axioms -- fails -- unknown identifier 'lt' def lt : mynat → mynat → Prop := λ a b, a ≤ b ∧ ¬ b ≤ a -- instance : preorder mynat := by i_checked_all_teh_axioms -- fails /- type mismatch at field 'lt_iff_le_not_le' lt_iff_le_not_le has type ?m_3 < ?m_4 ↔ ?m_3 ≤ ?m_4 ∧ ¬?m_4 ≤ ?m_3 but is expected to have type auto_param (∀ (a b : mynat), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous) -/ end mynat /- class preorder (α : Type u) extends has_le α, has_lt α := (le_refl : ∀ a : α, a ≤ a) (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c) (lt := λ a b, a ≤ b ∧ ¬ b ≤ a) (lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac) -/  #### Scott Morrison (Jul 03 2019 at 14:30): Ah, we'll have to add something that checks if a field is wrapped with auto_param, and then tries running the embedded tactic. #### Mario Carneiro (Jul 03 2019 at 14:31): or opt_param in the case of lt #### Andrew Ashworth (Jul 03 2019 at 14:47): hmm, wasn't there a hole tactic that did this as well that I saw posted awhile back? I may be misremembering #### Patrick Massot (Jul 03 2019 at 14:48): Do you mean https://github.com/leanprover-community/mathlib/blob/d001abfd48d64ac27310590458132009f47c852d/src/tactic/core.lean#L718? It's slightly different #### Andrew Ashworth (Jul 03 2019 at 14:50): ah, I think that is what I was thinking of #### Kevin Buzzard (Jul 03 2019 at 14:59): I just want to not even bother defining lt and lt_iff_le_not_le here #### Scott Morrison (Jul 03 2019 at 15:11): Yes, that's what we're proposing. Keeley's tactic should be able to identify opt_param or auto_param fields, and handle them automatically. #### Keeley Hoek (Jul 03 2019 at 17:05): I'm glad it helped! Yes this should be easy to fix... #### Keeley Hoek (Jul 03 2019 at 17:10): Oh hmm turns out it's a bit yuck... #### Kevin Buzzard (Jul 03 2019 at 17:11): instance : canonically_ordered_comm_semiring mynat := { add := (+), add_assoc := add_assoc, zero := 0, zero_add := zero_add, add_zero := add_zero, add_comm := add_comm, le := (≤), le_refl := le_refl, le_trans := le_trans, le_antisymm := λ a b, le_antisymm, add_le_add_left := add_le_add_left, lt_of_add_lt_add_left := lt_if_add_lt_add_left, bot := _, bot_le := bot_le, le_iff_exists_add := le_iff_exists_add, mul := (*), mul_assoc := mul_assoc, one := 1, one_mul := one_mul, mul_one := mul_one, left_distrib := left_distrib, right_distrib := right_distrib, zero_mul := zero_mul, mul_zero := _, mul_comm := _, zero_ne_one := _, mul_eq_zero_iff := _ }  Also yuck. #### Keeley Hoek (Jul 03 2019 at 17:37): ha! its literally 3am where I am at the moment so I'm going to throw in the towel until morning---but just one last sorried function needs filling in: #### Keeley Hoek (Jul 03 2019 at 17:37): namespace tactic.interactive open tactic meta def replace_special_names : name → name | add := has_add.add | n := n meta def get_type_of_nth_arg_core : ℕ → expr → expr | _ _ := sorry meta def get_type_of_nth_arg (n : name) (k : ℕ) : tactic expr := get_type_of_nth_arg_core k <$> (resolve_name n >>= to_expr >>= infer_type)

meta def run_tac (n : expr) : tactic unit :=
do n ← eval_expr name n,
e ← resolve_name n >>= to_expr,
tac ← eval_expr (tactic unit) e,
tac

meta def resolve_name_or_use_autoparam (sn : name) (n : ℕ × name) : tactic (name × pexpr) :=
do pe ← resolve_name (replace_special_names n.2) <|>
do { t : expr ← get_type_of_nth_arg (sn ++ mk) n.1,
match t with
| (auto_param %%t %%tac) :=
lock_tactic_state $do m ← mk_meta_var t, set_goals [m], run_tac tac, to_pexpr <$> instantiate_mvars m
| _ := failed
end
},
return (n.2, pe)

meta def i_checked_all_teh_axioms : tactic unit :=
do t ← target,
env ← get_env,
match t with
| expr.app (expr.const sn _) e :=
tactic.trace (env.structure_fields sn) >>
match env.structure_fields sn with
| some l :=
do n :: _ ← tactic.open_namespaces,
let l := (list.range l.length).zip l,
v ← l.mfilter_map $resolve_name_or_use_autoparam sn, tactic.trace v, let s : structure_instance_info := { struct := some sn, field_names := v.map prod.fst, field_values := v.map prod.snd, }, tactic.trace v, e ← to_expr$ pexpr.mk_structure_instance s,
tactic.exact e
| none := fail "goal not a structure"
end
| _ := fail "unsupported goal"
end

end tactic.interactive


#### Keeley Hoek (Jul 03 2019 at 17:38):

haha funnily enough run_tac is equivalent to the ridiculous composite

meta def run_tac' (n : expr) : tactic unit :=
do tac ← eval_expr name n >>= resolve_name >>= to_expr >>= eval_expr (tactic unit),
tac


#### Kevin Buzzard (Jul 03 2019 at 17:50):

instance : canonically_ordered_comm_semiring mynat :=
zero := 0,
le := (≤),
le_refl := le_refl,
le_trans := le_trans,
le_antisymm := λ a b, le_antisymm,
bot := ⊥,
bot_le := bot_le,
mul := (*),
mul_assoc := mul_assoc,
one := 1,
one_mul := one_mul,
mul_one := mul_one,
left_distrib := left_distrib,
right_distrib := right_distrib,
zero_mul := zero_mul,
mul_zero := mul_zero,
mul_comm := mul_comm,
zero_ne_one := zero_ne_one,
mul_eq_zero_iff := mul_eq_zero_iff }


I finished my proof.

#### Kevin Buzzard (Jul 03 2019 at 17:55):

Oh that's not maths, that's not in this game

#### Kevin Buzzard (Jul 03 2019 at 17:55):

That is generated without telling the user

#### Kevin Buzzard (Jul 04 2019 at 07:45):

decidable le uses recursion. I am trying to box off what is done by recursion, because mathematicians put it in a different box to induction.

Example: one could present the natural numbers mynat as having two constants mynat.zero and mynat.succ, two axioms mynat.zero_ne_succ and mynat.succ_inj, and one key fact: you can use the induction n tactic if you have n : mynat. The two axioms are proved by Lean using recursion via nat.rec; succ_inj can be proved easily using the completely artificial function pred which no mathematician has ever seen or uses (because it allows 0 as an input and gives the wrong answer), and zero_ne_succ can be proved by defining a function which sends 0 to tt and succ n to ff, again a function which can be defined by recursion but is of no use to us in practice.

If you present nat this way and present addition similarly (mynat.add is a constant, we will always use the + notation, add_zero and add_succ are axioms, don't worry about how it was defined) then one can "prove" things like the "theorem" add_monoid mynat (because now it is a theorem -- all the data has been given to you and there's only a theorem left) purely within tactic mode, by supplying tactic proofs of each of the fields in whatever order you like.

I am looking at what happens to nat if you try and isolate all the computational content and "proofs and data constructed via recursion" and just give the user an inductive principle which can only be used to construct proofs. One way of looking at it is you could say that I was trying to isolate "the bit which mathematicians like best".

#### Keeley Hoek (Jul 04 2019 at 10:14):

Update: it almost works, but its hard to tell when a structure has optional parameters (the "auto-param" kind is fine). It turns out that the generated constructors don't have the opt_param part...

#### Keeley Hoek (Jul 04 2019 at 10:16):

But otherwise it's a lot more robust than before now

#### Keeley Hoek (Jul 04 2019 at 10:23):

Okay I found a tricksy way (not intended, but I don't think there is an API for this...)

#### Keeley Hoek (Jul 04 2019 at 10:48):

Ok its even tricker than I thought, extra idea...

#### Keeley Hoek (Jul 04 2019 at 11:13):

Yeah ok I'm really struggling. There is a lot of code now, and by some tricks I can find out which fields have optional/default values, but I can't find a way to determine what the values actually are. Secretly lean knows, but I think it might not be exposed. Does anyone know of a way to find the default value of a field declared opt_param?

#### Keeley Hoek (Jul 04 2019 at 11:14):

(Sounds like this might be a job for lean 3.5.0, just need to add a function)

#### Keeley Hoek (Jul 04 2019 at 11:17):

Here is the current state: https://gist.github.com/khoek/b820b0b242909a22bfd3b16a046eb9de
It does everything you want Kevin except for the lt problem.

#### Mario Carneiro (Jul 04 2019 at 11:23):

try_apply_opt_auto_param_for_apply might help as a template. It uses

when cfg.opt_param (try apply_opt_param) >>
when cfg.auto_param (try apply_auto_param)


#### Mario Carneiro (Jul 04 2019 at 11:24):

which are themselves implemented in lean in the obvious way

#### Mario Carneiro (Jul 04 2019 at 11:25):

but they are expecting the opt/auto_param to be the main goal, not sure if that's true in your case

#### Keeley Hoek (Jul 04 2019 at 13:54):

I can do the handling of those cases just fine (and that code is in the gist), the problem is that there is no way at all I can find to programmically get the opt_param blah associated to an optional field of a structure.

#### Keeley Hoek (Jul 04 2019 at 13:55):

If you make an example structure which has an optional and auto param for comparison, the autogenerated .mk retains the autoparam but drops the optional

#### Mario Carneiro (Jul 04 2019 at 13:55):

An optional field has the type opt_param type default_value

#### Keeley Hoek (Jul 04 2019 at 13:56):

Sure, but this information is not exposed by lean

#### Mario Carneiro (Jul 04 2019 at 13:56):

it's literally in the expr

#### Keeley Hoek (Jul 04 2019 at 13:56):

The expr for what?

#### Mario Carneiro (Jul 04 2019 at 13:56):

the type of the projection

oooooooh!

Hang on

#### Keeley Hoek (Jul 04 2019 at 13:57):

run_cmd (do
tactic.mk_const preorder.lt >>= tactic.infer_type >>= pp >>= tactic.trace
)


#### Keeley Hoek (Jul 04 2019 at 13:58):

I don't see any reference to the opt_param

#### Keeley Hoek (Jul 04 2019 at 13:58):

The constructor preorder.mk is the same; auto_param fields are replicated, the optional ones are dropped

#### Mario Carneiro (Jul 04 2019 at 14:11):

Oh, that's weird... I found a strange parsing issue while investigating this too

structure preorder1 (α : Type) [has_le α] :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b : α, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, lt a b ↔ (a ≤ b ∧ ¬ b ≤ a) := λ _ _, iff.rfl)

structure preorder2 (α : Type) [has_le α] :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt : α → α → Prop := λ a b : α, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, lt a b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)


The type of lt_iff_le_not_le is different in the two cases. preorder2 is the right one. preorder1.lt_iff_le_not_le is trivial as evidenced by the rfl proof. @Sebastian Ullrich Are you aware of this? It looks like that thing you pointed out a while back where structures could define lets and notation and other crazy things. Somehow lt is treated as a notation for the purposes of lt_iff_le_not_le, but it is also an actual field...?

:0

#### Mario Carneiro (Jul 04 2019 at 14:12):

The other weird thing about this is that lt is already defined in the case of preorder, in has_lt, and it's getting "redefined" with a new defeq type in preorder

#### Mario Carneiro (Jul 04 2019 at 14:13):

I can already predict that the lean C++ code to make sense of all this is a rats nest

#### Sebastian Ullrich (Jul 04 2019 at 14:16):

Looks like a straight bug

#### Patrick Massot (Jul 04 2019 at 14:17):

Now is the time were Sebastian will paste that url to the commit which fixed that bug in Lean 4 months ago

#### Kevin Buzzard (Jul 04 2019 at 14:43):

I can make a preorder by just ignoring the lt and lt_iff_whatever fields completely. It's not possible to emulate that behaviour with a tactic?

#### Keeley Hoek (Jul 04 2019 at 14:55):

It appears that lean does not provide a way for lean to access the pre-set optional values of structures, eg. lt in this case.
I think I make it work but it'll be a little bit less robust than I had hoped

#### Keeley Hoek (Jul 04 2019 at 16:17):

@Kevin Buzzard Here is a link to something that works, at least on the two add_monoid and preorder examples I've seen! https://gist.github.com/khoek/cfb72fe41b0725269a14bf9196bb9c73

#### Keeley Hoek (Jul 04 2019 at 16:29):

Are you able to make a canonically_ordered_comm_semiring using it?

#### Kevin Buzzard (Jul 04 2019 at 16:34):

I'm now seeing all sorts of errors like

type mismatch at field 'lt_of_add_lt_add_left'
has type
?m_3 + ?m_4 < ?m_3 + ?m_5 → ?m_4 < ?m_5
but is expected to have type
∀ (a b c : mynat), a + b < a + c → b < c


but this is not your fault -- I have defined lt_of_add_lt_add_left with the inputs implicit but apparently Lean wants them explicit. Nearly there now, just fixing all of them.

#### Kevin Buzzard (Jul 04 2019 at 16:36):

instance : canonically_ordered_comm_semiring mynat := by structure_helper -- works!


#### Kevin Buzzard (Jul 04 2019 at 16:37):

How do I get a complete list of all the typeclasses X such that type class inference can find a term of type X nat ?

#### Kevin Buzzard (Jul 04 2019 at 16:40):

But it works :-) Many thanks Keeley!

#### Kevin Buzzard (Jul 04 2019 at 16:46):

Ultimately I would rather lt_of_add_lt_add_left : ∀ {a b c : mynat}, a + b < a + c → b < c := ... because I believe that this is the idiomatic way to define this function, with a, b, c implicit. It stops the tactic working through. We can put that down to "further work if someone can be bothered".

#### Kevin Buzzard (Jul 04 2019 at 16:50):

@Mario Carneiro you were talking about a bug in Lean. Can this bug be easily fixed in 3.5.1? Would a consequence be that a whole bunch of _'s would need to be removed from mathlib? I feel like the definition of canonically_ordered_comm_semiring.lt_of_add_lt_add_left is "wrong".

canonically_ordered_comm_semiring.lt_of_add_lt_add_left : ∀ (a b c : ?M_1), a + b < a + c → b < c


I want to write some sort of front end for Lean where the user just has to type in simple proofs in tactic mode and that's all they can do. For this project, I don't care about mathlib and I don't care if I'm running a non-standard Lean. On the other hand if people change the behaviour of core tactics like induction then it will break everything I guess.

#### Mario Carneiro (Jul 04 2019 at 16:51):

You should just be using lt_of_add_lt_add_left

#### Mario Carneiro (Jul 04 2019 at 16:51):

which has the right binders

#### Kevin Buzzard (Jul 04 2019 at 16:52):

ooh. ordered_cancel_comm_monoid

#### Kevin Buzzard (Jul 04 2019 at 16:53):

I love that there are just a gazillion really stupid-in-my-eyes classes which are just out there and I don't know the names of any of them.

#### Kevin Buzzard (Jul 04 2019 at 16:53):

I don't want to use it, I want the user to prove it.

#### Mario Carneiro (Jul 04 2019 at 16:54):

There is a tactic that does the restating automatically

#### Kevin Buzzard (Jul 04 2019 at 16:55):

Yeah but I don't want to restate it, I want the user to prove it.

#### Kevin Buzzard (Jul 04 2019 at 16:55):

We're building nat from scratch.

#### Mario Carneiro (Jul 04 2019 at 16:55):

The binders don't matter if you are proving it

#### Mario Carneiro (Jul 04 2019 at 16:55):

it's lambda regardless

#### Kevin Buzzard (Jul 04 2019 at 16:55):

I know, I just feel like I'm lying to the user.

#### Mario Carneiro (Jul 04 2019 at 16:56):

In fact, it's usually better for the axiom to have all explicit or semi implicit binders when proving it

#### Kevin Buzzard (Jul 04 2019 at 16:58):

@Keeley Hoek I would like an over-ride. I'd like to define mynat.lt_of_add_lt_add_left with semi-implicit or implicit binders, and then define mynat.lt_of_add_le_add_left' to be the thing with the stupid binders and then tell your tactic to use the stupid version with the ' just for that field only.

#### Mario Carneiro (Jul 04 2019 at 16:58):

For instance, you might have an assumption that says ∀ (a b c : A), a + b < a + c → b < c and you want to pass it in; if the assumption is implicit then the arguments will get auto applied and it won't fit

#### Mario Carneiro (Jul 04 2019 at 16:58):

I would assume that for Keeley's tactic you can define the binders however you like

#### Keeley Hoek (Jul 04 2019 at 17:01):

Unfortunately Mario it seems that the structure-builder notation refuses to accept specifying a field with different binders =/

#### Keeley Hoek (Jul 04 2019 at 17:01):

Perhaps another bug?

#### Keeley Hoek (Jul 04 2019 at 17:02):

MWE:

structure thingo :=
(func : Π (a : ℕ), ℕ)

-- works
def foo : thingo := {func := λ {a : ℕ}, a + 1}

def concrete {a : ℕ} : ℕ := a + 1
-- doesn't
def bar : thingo := {func := concrete}


#### Kevin Buzzard (Jul 04 2019 at 17:04):

canonically_ordered_comm_semiring
canonically_ordered_monoid,
ordered_comm_monoid
partial_order
lattice.order_bot
partial_order
comm_semiring
zero_ne_one_class


Generated by hand -- each thing extends the things one level of indentation below it.

#### Kevin Buzzard (Jul 04 2019 at 17:06):

That's funny because you would imagine that lam a, f is syntactically equal to lam {a}, f

#### Kevin Buzzard (Jul 04 2019 at 17:07):

structure thingo :=
(func : Π (a : ℕ), ℕ)

-- works
def foo : thingo := {func := λ {a : ℕ}, a + 1}

-- also works!
def concrete {{a : ℕ}} : ℕ := a + 1

def bar : thingo := {func := concrete}


#### Mario Carneiro (Jul 04 2019 at 17:27):

that's not a bug, that's by design

#### Mario Carneiro (Jul 04 2019 at 17:27):

and that's also why I said semi-implicit is a good choice here

#### Kevin Buzzard (Jul 04 2019 at 17:29):

Is there a "correct" decision for the variables in lt_of_add_le_add_left ? Or do you sometimes need one thing and sometimes another?

#### Mario Carneiro (Jul 04 2019 at 17:35):

It might work to use apply to figure out the right number of arguments

#### Keeley Hoek (Jul 05 2019 at 14:54):

ooh, well my tactic could count the number of expected explicit arguments and then instead of fn := fn not compiling fn := \lambda a b, @fn _ a b would compile. Would that have defeq problems?

no

#### Mario Carneiro (Jul 05 2019 at 14:56):

In principle this is what apply is supposed to do, but it may not work for you

#### Keeley Hoek (Jul 05 2019 at 14:57):

Yes, due to the aforementioned opt_param problems the only way I can get those fields filled is using a structure_instance_info, which needs explicit pexprs to be provided.

#### Keeley Hoek (Jul 05 2019 at 14:58):

Also, is your "no" an answer to my question, or "no that won't work"?

#### Mario Carneiro (Jul 05 2019 at 14:58):

no defeq problems

#### Mario Carneiro (Jul 05 2019 at 14:58):

You can elaborate an expr using apply and then quote it to turn it into a pexpr

#### Keeley Hoek (Jul 05 2019 at 15:26):

Oh ok, I see what you are saying. I tried something like this for a bit but there were problems I think with the inter-dependence of the fields and things like le not being decided when le_refl was being decided using an apply. I guess you could build everything consistently so that all the fields of the structure had metavariables in their type in common when they correspond to the same thing? But this seems like some work

#### Kevin Buzzard (Jul 05 2019 at 15:29):

I am using Mario's approach of {{ }}` when necessary

Last updated: May 12 2021 at 07:17 UTC