Zulip Chat Archive

Stream: new members

Topic: Defining a symmetric function


view this post on Zulip Vaibhav Karve (Feb 17 2020 at 01:04):

Suppose I have an enumerated type A (say with 7 different constructors) and I wish to define a symmetric function A -> A -> nat.

The only way I know how to do is to write the definition for all 7 * 7 = 49 variations on the arguments.

However, this is rather inefficient. I know that the function I wish to write is symmetric. Is there a way to give Lean only the 28 different variations and have it fill in the rest automatically by leveraging symmetry?

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:15):

Sure, you can define your relation to be the symmetric closure of a relation R that you define with only 28 inductive constructors

view this post on Zulip Chris Hughes (Feb 17 2020 at 01:15):

It's not a relation.

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:16):

oh, yeah that won't work without a bit of choice if you want to define a nat function

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:16):

I guess a tactic could do it

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:17):

but fundamentally if you have an inductive type with 7 constructors it's difficult to define any binary function without providing 49 pieces of information

view this post on Zulip Vaibhav Karve (Feb 17 2020 at 01:20):

Oh. In that case do you think it is fair to demand that this be a new feature?

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:20):

Like I said, a tactic could do it. It's not a lean feature and doesn't make sense as one

view this post on Zulip Vaibhav Karve (Feb 17 2020 at 01:22):

As in I can define the function with 49 pieces and then add a proof (that's the part that uses the tactic) that it is indeed symmetric? Or is there a way to use the tactic in the definition itself?

view this post on Zulip Vaibhav Karve (Feb 17 2020 at 01:23):

Mario Carneiro said:

Sure, you can define your relation to be the symmetric closure of a relation R that you define with only 28 inductive constructors

Even in the case of the relation, I don't think I understand. Won't lean rejection my definition of R by saying it is a non-exhaustive definition?

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:24):

If it's a relation, you can define it inductively as an inductive rather than a def with a definition by cases

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:24):

in which case it will be false on the cases you omit

view this post on Zulip Mario Carneiro (Feb 17 2020 at 01:42):

Here is a terrible tactic that does the job:

import data.list.defs

namespace tactic

meta def match_goals (ls : list ( × )) : tactic unit := do
  gs  get_goals,
  ls.mmap' $ λ a, b, unify (gs.inth a) (gs.inth b),
  set_goals gs

meta def interactive.cases_symmetric
  (a b : interactive.parse (lean.parser.pexpr std.prec.max)) : tactic unit := do
  a  to_expr a,
  b  to_expr b,
  env  get_env,
  ty  infer_type a,
  let n := (env.constructors_of ty.get_app_fn.const_name).length,
  (() <$ cases_core a []); (() <$ cases_core b []),
  match_goals $ do
    a  list.range n,
    b  list.range n,
    guard (b < a),
    return (n * a + b, n * b + a)
end tactic

inductive weekday
| sun | mon | tue | wed | thu | fri | sat

def foo : weekday  weekday  nat :=
begin
  intros a b,
  cases_symmetric a b,
  -- 28 × |- ℕ

  -- filling with dummy stuff
  (do gs  tactic.get_goals,
    gs.enum.mmap' $ λ n, g, do
      tactic.unify g (reflect n))
end

example : foo weekday.wed weekday.thu = 19 := rfl

theorem foo_symm (m n) : foo m n = foo n m :=
by cases m; cases n; refl

view this post on Zulip Vaibhav Karve (Feb 17 2020 at 02:14):

Thanks for the code! This is beyond my current level of understanding so I will get started on trying to unravel what it does.

view this post on Zulip Mario Carneiro (Feb 17 2020 at 02:36):

The interesting part is this:

#eval do
    a  list.range 7,
    b  list.range 7,
    guard (b < a),
    return (7 * a + b, 7 * b + a)

that just creates a list of goal pairs to merge, and then match_goals goes through and unifies these pairwise

view this post on Zulip Mario Carneiro (Feb 17 2020 at 02:37):

in other words it's just saying "let goal (1,2) be the same as goal (2,1)" and so on

view this post on Zulip Mario Carneiro (Feb 17 2020 at 02:38):

The downside is that you end up with 28 unmarked identical goals and it's up to you to figure out what they correspond to


Last updated: May 13 2021 at 23:16 UTC