Stream: general

Topic: rfl and wildcard pattern

Patrick Massot (Jun 08 2018 at 13:29):

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


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


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

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


Johan Commelin (Jun 08 2018 at 14:34):

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

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

Patrick Massot (Jun 08 2018 at 14:36):

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

Patrick Massot (Jun 08 2018 at 14:36):

Maybe we can add Scott's repo as a dependency

Exactly.

Johan Commelin (Jun 08 2018 at 14:36):

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

Johan Commelin (Jun 08 2018 at 14:36):

So it might not go as smoothly as we hope.

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.

Patrick Massot (Jun 08 2018 at 14:38):

I don't think it's true

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.

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.

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

Patrick Massot (Jun 08 2018 at 14:41):

Simon I don't understand what you wrote

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?

I hope so

Patrick Massot (Jun 08 2018 at 14:43):

Let's see what time is it in Australia.

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.

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?

Patrick Massot (Jun 08 2018 at 14:44):

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

Simon Hudon (Jun 08 2018 at 14:46):

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

True

Patrick Massot (Jun 08 2018 at 14:47):

I don't know what I was thinking

Simon Hudon (Jun 08 2018 at 14:47):

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

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.

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

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

Simon Hudon (Jun 08 2018 at 14:54):

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

Simon Hudon (Jun 08 2018 at 14:55):

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

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.

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?

Simon Hudon (Jun 08 2018 at 15:59):

Is whatever something like semigroup?

yes

Simon Hudon (Jun 08 2018 at 16:00):

Why do you need to strip it away?

Patrick Massot (Jun 08 2018 at 16:01):

because it doesn't work otherwise

Patrick Massot (Jun 08 2018 at 16:01):

see the handcrafted proof above

Simon Hudon (Jun 08 2018 at 16:02):

Do you have an instance of semigroup for α?

Patrick Massot (Jun 08 2018 at 16:03):

linear_ordered_comm_group actually

Patrick Massot (Jun 08 2018 at 16:03):

and the goal is to build linear_ordered_comm_monoid (option α)

Patrick Massot (Jun 08 2018 at 16:04):

but to_string field turns out to be comm_monoid.mul_assoc here

Patrick Massot (Jun 08 2018 at 16:04):

but the proof then needs _root_.mul_assoc

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?

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)

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

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

Simon Hudon (Jun 08 2018 at 16:17):

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

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)

Simon Hudon (Jun 08 2018 at 16:18):

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

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


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