Dependent induction?

Stream: new members

[Vincent Beffara]

Hi,
I am trying to formalize a few things in graph theory, and for that I am introducing a helper inductive type of non-empty lists, like this :

inductive llist (V : Type) : Type | P : V -> llist | L : V -> llist -> llist

Such lists have a first and last elements,

def first : llist V -> V | (P v) := v | (L v l) := v
def last  : llist V -> V | (P v) := v | (L v l) := last l

and I define a path to be a llist with prescribed endpoints:

def path (V x y) := { l : llist V // first l = x ∧ last l = y }

So far so good, now I want to concatenate paths with compatible endpoints,

def concat {V x y z} (p1 : path V x y) (p2 : path V y z) : path V x z

just concatenating the lists of elements but without repeating the y. For the moment, the only way I manage to do it is to first define it on unconstrained llists, like this,

def concat' {V} (l1 l2 : llist V) (h : last l1 = first l2) : path V (first l1) (last l2)

inductively, and then use that to define concat. When I try to define concat directly by induction on p1.val, it fails because in the inductive step, x is still there while the tail of p1.val obviously doesn't start with x, so the induction hypothesis is not useful.

Am I missing something? What is the right way to use induction for such dependent types?

[Anne Baanen]

Hi! I'm guessing that you're doing induction by pattern-matching on the arguments (as in the tutorial here: https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#pattern-matching). When definining concat, x is fixed (because it's on the left of the colon), but it varies in the recursive call. So you can put it on the right with a Π-type.

[Vincent Beffara]

Hi! I'm guessing that you're doing induction by pattern-matching on the arguments

I am doing it like this, which might be completely misguided:

def concat {V x y z} (p1 : path V x y) (p2 : path V y z) : path V x z :=
begin
    rcases p1 with ⟨l1,hx,hy⟩,
    induction l1 with v v l hr,
    { simp at hx hy, rw [<-hx, hy], exact p2 },
    -- Now the state contains these, which are useless:
    -- hr : first l = x -> last l = y -> path x z
    -- hx : first (L v l) = x
    sorry
end

[Kenny Lau]

don't use tactics for defs unless you know what you're doing

[Johan Commelin]

@Vincent Beffara Kenny's warning is for the following reason: tactics usually leave artifacts that are very annoying to handle later on.

[Johan Commelin]

For proofs this doesn't matter, because of proof irrelevance

[Johan Commelin]

@Kenny Lau It might be helpful to show beginners how to actually do it right, instead of only telling them what not to do.

[Kenny Lau]

@Johan Commelin I am

[Vincent Beffara]

Yes an example would be very helpful, I tried to do it with pattern matching but wasn't able to get anywhere. Using tactics like this does feel wrong but it's the only way I managed to get a working definition :-(

[Vincent Beffara]

(I do get huge lambda terms when using simp later, is that what you mean by "very annoying"? because it is ...)

[Johan Commelin]

@Vincent Beffara I think Tim suggests that you try something like

def concat {V : Type} : Π {x y z : V}, (path V x y) → (path V y z) → path V x z
| x y z p1 p2 := _

[Johan Commelin]

But then... I'm not an expert pattern matcher

[Johan Commelin]

@Vincent Beffara Slightly unrelated. Graph theory seems to be a tricky subject as a first project in Lean. You might get stuck and disappointed rather quickly. Nevertheless I would love to see more graph theory. Hence I suggest you write a bit more about what your goals are. People might be able to suggest a mathematically equivalent approach that makes lots of troubles vanish right away.

[Johan Commelin]

It's something that took me a bit of time to adjust to. Two definitions can be mathematically equal/the same/indistinguishable. But they can behave quite differently in Lean...

[Kenny Lau]

import data.list.basic

universe u

variables {α : Type u}

theorem list.last_append' :
  ∀ {L₁ L₂ : list α} (h₁ h₂), (L₁ ++ L₂).last h₁ = L₂.last h₂
| []     L₂ h₁ h₂ := rfl
| (h::t) L₂ h₁ h₂ := (list.last_cons _ $ list.append_ne_nil_of_ne_nil_right _ _ h₂).trans $
    list.last_append' _ _

def llist (α : Type u) : Type u :=
α × list α

namespace llist

variables (L : llist α)

def first : α :=
L.1

def last : α :=
list.last (L.1 :: L.2) (λ h, list.no_confusion h)

end llist

def path (x y) :=
{ L : llist α // L.first = x ∧ L.last = y }

def concat {x y z : α} (p1 : path x y) (p2 : path y z) : path x z :=
⟨(p1.1.1, p1.1.2 ++ p2.1.1 :: p2.1.2), p1.2.1, begin
  unfold llist.last, dsimp only,
  rw [list.last_cons, list.last_append'],
  { exact p2.2.2 },
  { exact list.append_ne_nil_of_ne_nil_right _ _ (list.cons_ne_nil _ _) }
end⟩

[Anne Baanen]

Here is a pattern-matching based implementation, but unfortunately Lean doesn't recognize that it terminates:

def concat {V y z} : Π {x} (p1 : path V x y) (p2 : path V y z), path V x z
| x ⟨P x', ⟨rfl, rfl⟩⟩ p2 := p2
| x ⟨L x' y', ⟨hx, hy⟩⟩ p2 :=
  let ⟨p1' , ⟨_, hy'⟩⟩ := concat ⟨y', ⟨rfl, hy⟩⟩ p2
  in ⟨L x' p1' , ⟨hx, hy'⟩⟩

(I come from an Agda background, so to me this "should just work" and I can't quickly figure out why not :P)

[Kenny Lau]

(deleted)

[Vincent Beffara]

what are P and L?

P and L are the constructors of my non-empty-list type (P for point and L for link in my head)

[Vincent Beffara]

I tried a few approaches for the non-empty-list type:

• the explicit inductive type
• { l list V // l \neq [] }
• V \times list V
  and also for the concatenation, I thought a bit about just concatenating without looking for compatibility, just dropping a vertex and trusting that it will never be used outside the compatible case, kind of like setting 1/0=0, but then all the lemmas that I want to have, like last (concat l1 l2) = last l2, become conditional ...

[Kenny Lau]

universes u

variables {α : Type u}

inductive llist (α : Type u) : Type u | P : α -> llist | L : α -> llist -> llist

namespace llist

def first : llist α -> α | (P v) := v | (L v l) := v
def last  : llist α -> α | (P v) := v | (L v l) := last l

def path (x y) := { l : llist α // first l = x ∧ last l = y }

def concat_aux {y z} : Π {x} (p11 : llist α) (h : first p11 = x ∧ last p11 = y) (p2 : path y z), path x z
| x (P x') ⟨rfl, rfl⟩ p2 := p2
| x (L x' y') ⟨hx, hy⟩ p2 :=
  let ⟨p1' , ⟨_, hy'⟩⟩ := concat_aux y' ⟨rfl, hy⟩ p2
  in ⟨L x' p1' , ⟨hx, hy'⟩⟩

def concat {x y z : α} (p1 : path x y) (p2 : path y z) : path x z :=
concat_aux p1.1 p1.2 p2

end llist

[Kenny Lau]

@Tim Baanen you need an auxiliary def

[Kenny Lau]

for recursing in a subtype

[Kenny Lau]

@Vincent Beffara my approach above is \a \times list \a

[Vincent Beffara]

you need an auxiliary def

So what would be recommended, having an auxiliary def or using something else than a subtype?

[Kenny Lau]

using library functions like I did :P

[Wojciech Nawrocki]

@Kenny LauBy auxiliary def do you mean one on the underlying type or something else? EDIT: ah, like concat_aux.

[Vincent Beffara]

Hi again, and thanks for all your replies. I'm afraid I am still confused about a few things ... So I have llist which is a non-empty list, path which is a llist with prescribed endpoints, I knew how to concatenate llists, I learned how to concatenate paths and now I want to verify that the llist part coincides. Here is where I am:

import tactic

inductive llist (V : Type) : Type | P : V -> llist | L : V -> llist -> llist
open llist

@[simp] def first {V} : llist V -> V | (P v) := v | (L v l) := v
@[simp] def last  {V} : llist V -> V | (P v) := v | (L v l) := last l

@[simp] def concat_llist {V} : Π (l₁ l₂) (h : last l₁ = first l₂), llist V
    | (P v)   l₂ h := l₂
    | (L v l) l₂ h := L v (concat_llist l l₂ h)

def path (V : Type) (x y : V) := { l : llist V // first l = x ∧ last l = y }

variables {V : Type} {x y z : V} {l : llist V} {l₁ : path V x y} {l₂ : path V y z}

@[simp] def concat_aux : Π {x} (l : llist V) (h : first l = x ∧ last l = y) (p' : path V y z), path V x z
    | x (P v)   h p' := ⟨p'.1, ⟨eq.trans p'.2.1 (eq.trans h.2.symm h.1), p'.2.2⟩⟩
    | x (L v l) h p' := let q := concat_aux l ⟨rfl, h.2⟩ p' in ⟨L x q.1, ⟨rfl, q.2.2⟩⟩

@[simp] def concat (p1 : path V x y) (p2 : path V y z) : path V x z := concat_aux p1.1 p1.2 p2

@[simp] lemma toto' (h1 : last l = y) (h2 : last l = first l₂.1)
    : (concat_aux l ⟨rfl,h1⟩ l₂).1 = concat_llist l l₂.1 h2
    := by { induction l with v v l hr; simp, exact hr h1 h2 }

lemma toto (h : last l₁.1 = first l₂.1) : (concat l₁ l₂).1 = concat_llist l₁.1 l₂.1 h
    := by { simp, have tmp := toto' l₁.2.2 h, assumption }

In the last line, tmp and the goal look identical to me, and yet the tactic fails. What am I doing wrong?

[Vincent Beffara]

My guess would be that the h parameters (which are hidden) do not match, but I thought that for Prop this did not matter?

[Kenny Lau]

if you change assumption to convert tmp then you can see what's wrong

[Kenny Lau]

also since you never used h in concat_llist you shouldn't include it as an input

[Kenny Lau]

import tactic

inductive llist (V : Type) : Type | P : V -> llist | L : V -> llist -> llist
open llist

@[simp] def first {V} : llist V -> V | (P v) := v | (L v l) := v
@[simp] def last  {V} : llist V -> V | (P v) := v | (L v l) := last l

@[simp] def concat_llist {V} : Π (l₁ l₂ : llist V), llist V
    | (P v)   l₂ := l₂
    | (L v l) l₂ := L v (concat_llist l l₂)

def path (V : Type) (x y : V) := { l : llist V // first l = x ∧ last l = y }

variables {V : Type} {x y z : V} {l : llist V} {l₁ : path V x y} {l₂ : path V y z}

@[simp] def concat_aux : Π {x} (l : llist V) (h : first l = x ∧ last l = y) (p' : path V y z), path V x z
    | x (P v)   h p' := ⟨p'.1, ⟨eq.trans p'.2.1 (eq.trans h.2.symm h.1), p'.2.2⟩⟩
    | x (L v l) h p' := let q := concat_aux l ⟨rfl, h.2⟩ p' in ⟨L x q.1, ⟨rfl, q.2.2⟩⟩

@[simp] def concat (p1 : path V x y) (p2 : path V y z) : path V x z := concat_aux p1.1 p1.2 p2

@[simp] lemma toto' (h1 : last l = y) (h2 : last l = first l₂.1)
    : (concat_aux l ⟨rfl,h1⟩ l₂).1 = concat_llist l l₂.1
    := by { induction l with v v l hr; simp, exact hr h1 h2 }

lemma toto (h : last l₁.1 = first l₂.1) : (concat l₁ l₂).1 = concat_llist l₁.1 l₂.1
    := by { simp, have tmp := toto' l₁.2.2 h, convert tmp; rw [l₁.2.1] }

[Vincent Beffara]

Thanks for the hint, I will look at it when I have access to Lean

[Vincent Beffara]

The reason I have h in concat is that I want the simplification lemma that first (concat l1 l2) = first l1 which is wrong without it and I fear having to sprinkle a similar assumption around later. Is your advise to do the opposite then?

[Mario Carneiro]

you can still have that simplification lemma, you just put the side condition in the lemma

[Mario Carneiro]

I don't think concat should be marked @[simp]

[Vincent Beffara]

I realize that I can put the condition in the lemma, but will simp know to look for it hidden in the current state as often as it would just use the lemma without the additional assumption in it?