Zulip Chat Archive

Stream: new members

Topic: Dependent induction?


Vincent Beffara (Oct 18 2019 at 12:36):

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 (Oct 18 2019 at 12:45):

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 (Oct 18 2019 at 13:07):

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 (Oct 18 2019 at 13:11):

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

Johan Commelin (Oct 18 2019 at 13:13):

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

Johan Commelin (Oct 18 2019 at 13:14):

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

Johan Commelin (Oct 18 2019 at 13:14):

@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 (Oct 18 2019 at 13:17):

@Johan Commelin I am

Vincent Beffara (Oct 18 2019 at 13:20):

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 (Oct 18 2019 at 13:21):

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

Johan Commelin (Oct 18 2019 at 13:21):

@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 (Oct 18 2019 at 13:22):

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

Johan Commelin (Oct 18 2019 at 13:25):

@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 (Oct 18 2019 at 13:26):

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 (Oct 18 2019 at 13:31):

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 (Oct 18 2019 at 13:33):

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 (Oct 18 2019 at 13:35):

(deleted)

Vincent Beffara (Oct 18 2019 at 13:37):

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 (Oct 18 2019 at 13:42):

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 (Oct 18 2019 at 13:42):

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 (Oct 18 2019 at 13:42):

@Tim Baanen you need an auxiliary def

Kenny Lau (Oct 18 2019 at 13:42):

for recursing in a subtype

Kenny Lau (Oct 18 2019 at 13:43):

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

Vincent Beffara (Oct 18 2019 at 14:02):

you need an auxiliary def

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

Kenny Lau (Oct 18 2019 at 14:04):

using library functions like I did :P

Wojciech Nawrocki (Oct 18 2019 at 14:59):

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

Vincent Beffara (Oct 19 2019 at 22:58):

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 (Oct 19 2019 at 23:00):

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 (Oct 19 2019 at 23:45):

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

Kenny Lau (Oct 19 2019 at 23:46):

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

Kenny Lau (Oct 19 2019 at 23:48):

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 (Oct 20 2019 at 06:46):

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

Vincent Beffara (Oct 20 2019 at 06:50):

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 (Oct 20 2019 at 06:52):

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

Mario Carneiro (Oct 20 2019 at 06:53):

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

Vincent Beffara (Oct 20 2019 at 08:26):

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?


Last updated: Dec 20 2023 at 11:08 UTC