Simple tactic using `with`

Stream: new members

[Joey Lupo]

In my code, I have a lemma called bind_skip, and there are numerous instances in my code where I use the pattern

apply bind_skip,
intro x,

and was wondering how to write a basic tactic which could be used like bind_skip_tac with x to execute those exact two lines.

[Mario Carneiro]

I would just use refine bind_skip (\lam x, _)

[Joey Lupo]

hmm, apply seems to be inferring some parameters of bind_skip that refine doesn't get. Is there anyway to make a tactic which is literally a pseudonym for a fixed set of instructions (but also takes a parameter/identifier via with)?

[Joey Lupo]

This was the best MWE I could come up. You can skip everything before the bind_skip. I just needed that there to make it compile.

import data.zmod.basic
import measure_theory.probability_mass_function

variables (G : Type) [fintype G] [group G] [decidable_eq G]

lemma grp_ne_zero : (fintype.elems G).val ≠ 0 :=
begin
  have e : G := (_inst_2.one),
  have h1 : e ∈ (fintype.elems G).val :=  finset.mem_univ e,
  have h2 : 0 < multiset.card (fintype.elems G).val :=
  begin
    apply (multiset.card_pos_iff_exists_mem).mpr,
    exact Exists.intro e h1,
  end,
  exact multiset.card_pos.mp h2,
end

namespace zmod

instance group : Π (n : ℕ) [fact (0 < n)], group (zmod n) :=
  by {intros n h, exact multiplicative.group}

end zmod

noncomputable theory

instance : monad pmf :=
{ pure := @pmf.pure,
  bind := @pmf.bind }

def uniform_grp : pmf G :=
  pmf.of_multiset (fintype.elems G).val (grp_ne_zero G)

def uniform_zmod (n : ℕ) [fact (0 < n)] : pmf (zmod n) := uniform_grp (zmod n)

variables (A B : Type)

lemma bind_skip (p : pmf A) (f g : A → pmf B) :
  (∀ (a : A), f a = g a) → p.bind f = p.bind g :=
begin
  intro ha,
  ext,
  simp,
  simp_rw ha,
end

def p1 : pmf (zmod 5) :=
do
  x ← uniform_zmod 5,
  y ← uniform_zmod 5,
  z ← uniform_zmod 5,
  pure (x + y + z)

def p2 : pmf (zmod 5) :=
do
  x ← uniform_zmod 5,
  y ← uniform_zmod 5,
  z ← uniform_zmod 5,
  pure (x + z + y)

example : p1 = p2 :=
begin
  apply bind_skip,
  intro x,
  apply bind_skip,
  intro y,
  apply bind_skip,
  intro z,
  simp_rw add_right_comm,
end

[Eric Wieser]

Does congr or congr' make progress on that goal?

[Eric Wieser]

Rather that using bind_skip

[Mario Carneiro]

oh, you want refine bind_skip _ _ _ (\lam x, _) since the first three arguments are explicit

[Eric Wieser]

First five, A and B too

[Mario Carneiro]

oh yeah, those should definitely be written variables {A B : Type}

[Joey Lupo]

The reason I ask about a tactic is that one of the hopes of the project is to have some sort of "library" for future proofs relating pmfs (which we can use to model cryptographic protocols, etc., etc.) So it'd be nice to say "use bind_skip_tac with x to eliminate the first line of two pmfs which have the same first line" instead of "write refine .... or "write apply bind_skip and then intro x"

[Mario Carneiro]

It is possible to introduce such tactics on the spot, although it's easier if they don't have arguments; but it is harder for readers to understand a proof using a lot of bespoke tactics, especially if they are just abbreviating a simple combination of simpler tactics

[Mario Carneiro]

I would just suggest writing apply bind_skip, intro x, on one line if you want to make it more like a single tactic

[Joey Lupo]

Yea, that could work I guess.

[Joey Lupo]

But, hypothetically, if one wanted to do it for this exact situation, how would one do it? The only reason I asked in the first place was because I figured someone might know how to write a 2-3 line tactic on the spot that accomplishes it.

[Eric Wieser]

I'm guessing congr didn't work?

[Alex J. Best]

You can make simple tactics like so:

meta def bind_skip_tac : tactic unit := do
`[apply bind_skip, intro x]

[Joey Lupo]

How would I pass in the identifier x?

[Joey Lupo]

So it'd be of the form bind_skip_tac with x

[Joey Lupo]

Eric, not sure about congr. I've been doing lots of proofs relating pmfs to each other over the last few weeks and writing the bind_skip lemma (and another similar lemma) made life infinitely easier. My code is at https://github.com/Loops7/cryptolib

[Joey Lupo]

The elgamal file has the main result.

[Alex J. Best]

Check out https://leanprover-community.github.io/extras/tactic_writing.html, I'm on my phone so I can't do it myself right now sorry!

[Joey Lupo]

Awesome, thank you Alex. Thank you for the simple example and link- I think I should be able to get it from here.

[Yakov Pechersky]

bind_skip should have A and B as implicit args, and likely f and g implicit too.

[Yakov Pechersky]

And it should be called bind_congr

[Yakov Pechersky]

And then you won't need a tactic, or write a more useful and general tactic

[Joey Lupo]

What do you mean by "and then I won't need a tactic?" I'm trying to figure out how to write a tactic that takes a parameter "id" and then executes "apply bind_skip, intro id". That's all. congr doesn't change the goal in the same way that bind_skip does, at least to my eyes.

[Joey Lupo]

btw, thank you @Yakov Pechersky for your tip to not use pattern matching on the left side of the arrow in the do-notation. That made my life a lot easier

[Horatiu Cheval]

I think this is the way to pass an identifier to a tactic, like you want

meta def tactic.interactive.bind_skip_tac (x : interactive.parse lean.parser.ident) :=
`[apply bind_skip, intros x]

(that's about the end of my tactic writing knowledge, so hopefully I am not mistaken here)

[Joey Lupo]

Thank you, that does exactly what I'd like it to!

[Eric Wieser]

Are you sure that works? To me that looks like it always calls the introd variable x

[Horatiu Cheval]

Oh, you're right. How do you do it then?

[Eric Wieser]

Here's the congr proof I was suggesting:

example : p1 = p2 :=
begin
  dunfold p1 p2,
  congr' with x : 1,
  congr' with y : 1,
  congr' with z : 1,
  simp_rw add_right_comm,
end

My claim is that the tactic you're asking for already exists, it's congr' (tactic#congr')

[Joey Lupo]

Hmm, I must have been too sleepy and hopeful when I tried Horatiu's solution! I am still curious how one would pass in a identifier to a tactic like that, though.

[Joey Lupo]

Yes, I agree congr' in that form accomplishes the same task. Is there a similar use of congr or congr' that accomplishes this?

lemma bind_skip_const (pa : pmf A) (pb : pmf B) (f : A → pmf B) :
  (∀ (a : A), f a = pb) → pa.bind f = pb :=
begin
  intro ha,
  ext,
  simp,
  simp_rw ha,
  simp [nnreal.tsum_mul_right],
end

def p3 : pmf (zmod 5) :=
do
  x ← uniform_zmod 5,
  y ← uniform_zmod 5,
  z ← uniform_zmod 5,
  pure z

def p4 : pmf (zmod 5) :=
do
  x ← uniform_zmod 5,
  pure x

example : p3 = p4 :=
begin
  apply bind_skip_const,
  intro x,
  apply bind_skip_const,
  intro y,
  simp,
  congr,
end

[Alex J. Best]

Here is an example of adding an optional with property:

setup_tactic_parser
meta def tactic.interactive.bind_skip_tac  (x : parse (tk "with" *> ident)?) : tactic unit :=
do `[apply bind_skip],
  let a := x.get_or_else `_,
  tactic.interactive.intro a