rfl and wildcard pattern

Stream: general

[Patrick Massot]

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.

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

Maybe we can add Scott's repo as a dependency

[Johan Commelin]

Exactly.

[Johan Commelin]

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

[Johan Commelin]

So it might not go as smoothly as we hope.

[Johan Commelin]

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

[Patrick Massot]

I don't think it's true

[Simon Hudon]

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.

[Johan Commelin]

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

[Patrick Massot]

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

[Patrick Massot]

Simon I don't understand what you wrote

[Johan Commelin]

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?

[Patrick Massot]

I hope so

[Patrick Massot]

Let's see what time is it in Australia.

[Simon Hudon]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

True

[Patrick Massot]

I don't know what I was thinking

[Simon Hudon]

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

[Patrick Massot]

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.

[Simon Hudon]

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

[Patrick Massot]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

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.

[Simon Hudon]

It's ready when you are.

[Patrick Massot]

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?

[Simon Hudon]

Is whatever something like semigroup?

[Patrick Massot]

yes

[Simon Hudon]

Why do you need to strip it away?

[Patrick Massot]

because it doesn't work otherwise

[Patrick Massot]

see the handcrafted proof above

[Simon Hudon]

Do you have an instance of semigroup for α?

[Patrick Massot]

linear_ordered_comm_group actually

[Patrick Massot]

and the goal is to build linear_ordered_comm_monoid (option α)

[Patrick Massot]

but to_string field turns out to be comm_monoid.mul_assoc here

[Patrick Massot]

but the proof then needs _root_.mul_assoc

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Scott Morrison]

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.