## 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: May 13 2021 at 23:16 UTC