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