Defining a symmetric function

Stream: new members

[Vaibhav Karve]

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]

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]

It's not a relation.

[Mario Carneiro]

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

[Mario Carneiro]

I guess a tactic could do it

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Vaibhav Karve]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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