Zulip Chat Archive

Stream: general

Topic: rfl and wildcard pattern


view this post on Zulip Patrick Massot (Jun 08 2018 at 13:29):

Have a look at https://github.com/kbuzzard/lean-perfectoid-spaces/blob/b1e6489145be504e64a009226c6811bfd84a5070/src/valuations.lean#L143-L151:

theorem mul_assoc :  (x y z : option α), mul (mul x y) z = mul x (mul y z)
| (some x) (some y) (some z) := congr_arg some $ _root_.mul_assoc x y z
| (some _) (some _) none     := rfl
| (some _) none     (some z) := rfl
| (some _) none     none     := rfl
| none     (some _) (some z) := rfl
| none     (some _) none     := rfl
| none     none     (some z) := rfl
| none none none := rfl

What would be a way to compress this down to three lines? Replacing lines 3 to N by |_ _ _ := rfl doesn' work.

view this post on Zulip Simon Hudon (Jun 08 2018 at 13:32):

I would try something like:

theorem mul_assoc :  (x y z : option α), mul (mul x y) z = mul x (mul y z) :=
by { intros, casesm* option _ ; (apply congr_arg some (_root_.mul_assoc x y z) <|> refl)) }

view this post on Zulip Simon Hudon (Jun 08 2018 at 13:35):

Maybe this would be clearer and faster:

theorem mul_assoc :  (x y z : option α), mul (mul x y) z = mul x (mul y z) :=
by { intros, casesm* option _,
     { exact congr_arg some (_root_.mul_assoc x y z) },
     all_goals { exact rfl } }

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:33):

Thanks. You need to try rfl first or replace names by wildcards since x, y, z are defined only in one case

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:33):

theorem mul_assoc :  (x y z : option α), mul (mul x y) z = mul x (mul y z) :=
by { intros, casesm* option _,
     all_goals { exact congr_arg some (_root_.mul_assoc _ _ _) <|>  exact rfl } }

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:34):

Isn't the correct answer to your initial question obviously?

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:35):

Ok, it's time for some tactic lecture. How to you get Lean to see the name of the theorem we are proving is mul_assoc and there are three variables in order to use this information instead of explicitly writing _root_.mul_assoc _ _ _? Then you can do a bunch of other proofs with the same tactic

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:36):

I don't think we have obviously yet. But indeed it would be the correct answer

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:36):

Maybe we can add Scott's repo as a dependency

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:36):

Exactly.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:36):

But I think it requires adding lots of attribute through mathlib.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:36):

So it might not go as smoothly as we hope.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:37):

His library is not orthogonal to mathlib, so it won't be an easy PR, I guess.

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:38):

I don't think it's true

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:38):

My pull request has not been merged yet but if you want to use my branch the code would end up very similar to your indexed product.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:40):

@Patrick Massot I would love to be proved wrong. But what I've seen so far, is that you need to put a lot of attributes at a lot of definitions. And then afterwards life becomes easy.

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:41):

At least you can add lean-tidy to the project and then import tidy.tidy and get access to obviously. Then it doesn't prove this lemma

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:41):

Simon I don't understand what you wrote

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:42):

At least you can add lean-tidy to the project and then import tidy.tidy and get access to obviously. Then it doesn't prove this lemma

Right... but your point is that it might still prove other lemma's?

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:43):

I hope so

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:43):

Let's see what time is it in Australia.

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:43):

I made a pull request with refine_struct that would be useful here. It hasn't been merged yet but you can still use it.

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:44):

@Scott Morrison We currently have this proof:

theorem mul_assoc :  (x y z : option α), mul (mul x y) z = mul x (mul y z) :=
by { intros, casesm* option _,
      all_goals { exact congr_arg some (_root_.mul_assoc _ _ _) <|>  refl } }

Question: should this be killed by one of your magic tactics?

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:44):

Simon: But the question at hand has no structure to refine

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:46):

Aren't you building up to a monoid or semigroup?

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:47):

True

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:47):

I don't know what I was thinking

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:47):

You may be able to have only one proof for the whole instance

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:48):

I was carelessly browsing code in lean-perfectoid and saw this lemma with seven stupid lines and focussed on it. But of course its only use is in an instance later.

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:50):

That's a pretty common mindset for me. That's actually a fun part of doing engineering: some days I don't feel smart so I can do some mindless tasks until I feel inspired again. The downside is that I don't consider much contexts while doing that so I end up improving the minutia of solutions that should just scrapped altogether

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:52):

It's a bit annoying that this PR is not merged because it's content is scattered among several files, so it's not immediate to incorporate it into another project

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:54):

What you can do is link to my repo in your toml file

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:55):

I may have to update that branch first but I can do that right now

view this post on Zulip Patrick Massot (Jun 08 2018 at 14:58):

That may be a good solution if @Mario Carneiro and @Johannes Hölzl need more time to review your PR, because the Perfectoid project will need a lot of instances of algebraic objects.

view this post on Zulip Simon Hudon (Jun 08 2018 at 15:26):

It's ready when you are.

view this post on Zulip Patrick Massot (Jun 08 2018 at 15:57):

After doing field ← get_current_field, how would you replace whatever.something with _root_.something inside field so that I can later use it in the relevant version of derive_field?

view this post on Zulip Simon Hudon (Jun 08 2018 at 15:59):

Is whatever something like semigroup?

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:00):

yes

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:00):

Why do you need to strip it away?

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:01):

because it doesn't work otherwise

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:01):

see the handcrafted proof above

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:02):

Do you have an instance of semigroup for α?

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:03):

linear_ordered_comm_group actually

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:03):

and the goal is to build linear_ordered_comm_monoid (option α)

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:04):

but to_string field turns out to be comm_monoid.mul_assoc here

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:04):

but the proof then needs _root_.mul_assoc

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:09):

I find it odd: the types are very similar. Can you give me the error you get when your proof fails?

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:09):

(It is possible to do what you ask but I think we're better off taking a different approach)

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:16):

I minimized to

import algebra.pi_instances

class linear_ordered_comm_group (α : Type)
    extends comm_group α, linear_order α :=
(mul_le_mul_left :  {a b : α}, a  b   c : α, c * a  c * b)

class linear_ordered_comm_monoid (α : Type)
    extends comm_monoid α, linear_order α :=
(mul_le_mul_left :  {a b : α}, a  b   c : α, c * a  c * b)

variables {α : Type} [linear_ordered_comm_group α]


def mul : option α  option α  option α
| (some x) (some y) := some (x * y)
| _        _        := none

def one : option α := some 1

def le : option α  option α  Prop
| (some x) (some y) := x  y
| (some _) none     := false
| none     _        := true

instance : linear_ordered_comm_monoid (option α) :=
by refine_struct { mul := mul, one := one, le := le, .. }; { tactic.derive_field_option }

The game is to add derive_field_option to algebra.pi_instances (from your branch of course) to make it work

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:17):

Again, this is not crucial, Kenny did it by hand, I'm only trying to slowly learn tactic writing for specialized automation

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:17):

Nice :) I'm going to play a bit :D

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:18):

I should go and take care of my family (I'm not even talking about the work I should have been doing)

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:18):

Ah family! They keep interrupting math, don't they? :D

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:20):

The version which doesn't work is:

meta def derive_field_option : tactic unit :=
do b  target >>= is_prop,
  if b then do
     field  get_current_field,
     trace (to_string field),
     intros,
     `[casesm* option _],
     `[all_goals { exact congr_arg some (field _ _ _) <|> exact rfl }]
  else do skip

view this post on Zulip Scott Morrison (Jun 11 2018 at 08:26):

Just arrived back from underwater. I've starred the proof you asked about, @Patrick, and will try out obviously. I suspect it requires more case bashing (on option) than obviously is by default willing to do.


Last updated: May 12 2021 at 03:23 UTC