Zulip Chat Archive

Stream: maths

Topic: recursive definitions


view this post on Zulip 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.

view this post on Zulip 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 })

view this post on Zulip Adam Topaz (Apr 14 2021 at 17:00):

I would immitate the definition of src#list.mem

view this post on Zulip Eric Rodriguez (Apr 14 2021 at 17:02):

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

view this post on Zulip Adam Topaz (Apr 14 2021 at 17:06):

I'm confused as to why you need same_arrow

view this post on Zulip 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

view this post on Zulip Adam Topaz (Apr 14 2021 at 17:11):

Ah ok

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Apr 14 2021 at 17:27):

Obviously the names should be changed :wink:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 14 2021 at 18:10):

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

view this post on Zulip Eric Rodriguez (Apr 14 2021 at 18:18):

thanks Mario, that makes sense!


Last updated: May 14 2021 at 19:21 UTC