Zulip Chat Archive

Stream: new members

Topic: Defining a symmetric function


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?

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

Chris Hughes (Feb 17 2020 at 01:15):

It's not a relation.

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

Mario Carneiro (Feb 17 2020 at 01:16):

I guess a tactic could do it

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

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?

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

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?

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?

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

Mario Carneiro (Feb 17 2020 at 01:24):

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

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

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.

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

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

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: Dec 20 2023 at 11:08 UTC