recursive definitions

Stream: maths

[Eric Rodriguez]

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]

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]

I would immitate the definition of src#list.mem

[Eric Rodriguez]

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

[Adam Topaz]

I'm confused as to why you need same_arrow

[Eric Rodriguez]

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

[Adam Topaz]

Ah ok

[Adam Topaz]

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]

Obviously the names should be changed :wink:

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Eric Rodriguez]

thanks Mario, that makes sense!