## Stream: maths

### Topic: recursive definitions

#### Eric Rodriguez (Apr 14 2021 at 16:51):

Hey all, I'm just wondering what sort of ideas there are to help nudge the equation compiler realise that an induction is fair dos. I've read this and none of it was helpful -- apart from the last one, which may well be; I didn't get rel_tac.

For reference, I'm trying to define the membership of an arrow in a path (on quivers); I attach the code below. The issue, I think, is that I need to take a couple generic type arguments before recursing on the path itself, which confuses the compiler and makes it think it needs to check the induction on the typeparams; the path is defined kind of like a list, and so the size is clearly strictly decreasing. There's even a definition path.length, which makes me feel like if I could get that working with rel_tac it would work fine.

#### Eric Rodriguez (Apr 14 2021 at 16:51):

import tactic
import combinatorics.quiver

universes v u

open quiver

inductive same_arrow {V} (q : quiver V) : ∀ {a b c d : V}, (q.arrow a b) → (q.arrow c d) → Prop
| refl {a b : V} (e : q.arrow a b) : same_arrow e e

def mem_path' {V : Type u} (q : quiver.{v} V) : ∀ {a b c d : V}, q.path c d → q.arrow a b → Prop
| _ _ _ _ (path.nil) := λ hom, false
| a b c d (path.cons h t) := λ hom, (same_arrow q hom t) ∨ (mem_path' h hom)

def mem_path {V : Type u} (q : quiver.{v} V) : ∀ {a b : V}, q.path a b → q.total → Prop
| _ _ (path.nil) := λ hom, false
| a b (@path.cons _ _ _ c _ h t) := λ hom, mem_path h hom ∨
(hom = { source := c,
target := b,
arrow := t })


#### Adam Topaz (Apr 14 2021 at 17:00):

I would immitate the definition of src#list.mem

#### Eric Rodriguez (Apr 14 2021 at 17:02):

it's pretty much equal, modulo some workarounds for types not being defeq

#### Adam Topaz (Apr 14 2021 at 17:06):

I'm confused as to why you need same_arrow

#### Eric Rodriguez (Apr 14 2021 at 17:08):

hom is of type q.arrow a b, but t : q.arrow ?m_1 d; equality wouldn't typecheck

Ah ok

#### Adam Topaz (Apr 14 2021 at 17:22):

I think this works?

import tactic
import combinatorics.quiver

universes v u

open quiver

inductive foo {V : Type u} (Q : quiver.{v} V) : Π {a b c d : V}, Q.arrow a b → Q.path c d → Prop
| base {a b} (f : Q.arrow a b) : foo f (quiver.path.cons quiver.path.nil f)
| induct {a b c d x : V} {f : Q.arrow a b} {g : Q.arrow c d} {h : Q.path x c} :
foo f h → foo f (quiver.path.cons h g)


#### Adam Topaz (Apr 14 2021 at 17:27):

Obviously the names should be changed :wink:

#### Mario Carneiro (Apr 14 2021 at 17:49):

In both cases you can fix the errors by moving parameters that don't change left of the colon

def mem_path' {V : Type u} (q : quiver.{v} V) {a b} (hom : q.arrow a b) {c} :
∀ {d : V}, q.path c d → Prop
| _ path.nil := false
| _ (path.cons h t) := same_arrow q hom t ∨ mem_path' h

def mem_path {V : Type u} (q : quiver.{v} V) {a} (hom : q.total) : ∀ {b : V}, q.path a b → Prop
| _ path.nil := false
| _ (path.cons h t) := mem_path h ∨ hom = ⟨_, _, t⟩


#### Mario Carneiro (Apr 14 2021 at 17:50):

I also moved the hom argument left of the colon, which reverses the arguments, but it works even with that one on the other side. The only parameter that really matters is {c} in the first and {a} in the second definition, that is, the first argument of q.path, which is a parameter of the inductive

#### Eric Rodriguez (Apr 14 2021 at 18:02):

Thanks for that idea Adam, I ended up playing with it, and I think you need to make base instead be:
| base {a b c : V} (f : a ⟶ b) : ∀ p : path c a, foo f (p.cons f) but otherwise it seems to work!
(The defn you gave me ends up being essentially p.starts_with, as far as I could tell)

#### Eric Rodriguez (Apr 14 2021 at 18:03):

And thanks too, Mario; I was worried that if I moved them left, I wouldn't be able to induct properly. I know there's a subtle difference between params left of and params right of the colon, but I'm not too sure what it is; do you know where I can read more about them?

#### Adam Topaz (Apr 14 2021 at 18:09):

Yes you're right @Eric Rodriguez ! My definition just says that the arrow is the first thing in the path, but with your change it should work :smile:

#### Mario Carneiro (Apr 14 2021 at 18:09):

the difference is that variables on the left are considered "parameters" and don't change during the recursion. For an inductive type, you generally want the "parameters" of the inductive on the left and the "indices" on the right

#### Mario Carneiro (Apr 14 2021 at 18:10):

this ensures that lean determines that it is recursive in the right way

#### Eric Rodriguez (Apr 14 2021 at 18:18):

thanks Mario, that makes sense!

Last updated: May 14 2021 at 19:21 UTC