Zulip Chat Archive

Stream: general

Topic: Custom Principle Of Induction


view this post on Zulip Henning Dieterichs (Jan 05 2021 at 13:09):

I have a tree and a recursive proposition that no two branches share a leaf (tree_disjoint: tree.disjoint).
I would like to do an inductive proof, say that the list of all leaves of a tree has no duplicates.
Since I'm doing a lot of such inductive proofs, I want a very concise induction scheme.

I don't like the mess that the tree.disjoint hypothesis produces though.
(In my actual scenario, I have more tree cases that represent marked edges and about 40 such inductive proofs.)
A standard inductive proof on tree adds *.disjoint to all induction hypothesis and it does not unfold tree.disjoint,
even though I only need the disjoint prop for the branch case. All other cases just unfold and pass the prop as is.

So I was thinking of a custom induction scheme.

I get this "mess" with induction tr:

case Tree.leaf
    α: Type
    t: α
    tree_disjoint: (Tree.leaf t).disjoint

     C (Tree.leaf t)

case Tree.branch
    α: Type
    t_tr1t_tr2: Tree α
    t_ih_tr1: t_tr1.disjoint  C t_tr1
    t_ih_tr2: t_tr2.disjoint  C t_tr2
    tree_disjoint: (t_tr1.branch t_tr2).disjoint

     C (t_tr1.branch t_tr2)

But I would like to get this with induction tr using (Tree.disjoint_induction tree_disjoint):

case Tree.leaf
    α: Type
    t: α

     C (Tree.leaf t)

case Tree.branch
    α: Type
    t_tr1t_tr2: Tree α
    t_ih_tr1: C t_tr1 -- No disjoint hypothesis here!
    t_ih_tr2: C t_tr2
    -- This is the only thing I need from tr.disjoint:
    tree_disjoint: disjoint t_tr1.leaves t_tr2.leaves

     C (t_tr1.branch t_tr2)

I played around with a custom induction lemma, but failed. The docs don't say much about custom induction lemmas.
It seems like I cannot even add decidable_eq type classes (I non-deterministically get "induction tactic failed, major premise type is ill-formed").
Also, I don't know how to pass the prop tr.tree to the induction lemma.

Do you have an idea? Is this even possible with a custom induction lemma?

This is the context:

import tactic
import data.finset

inductive Tree (α: Type)
| leaf (a: α): Tree
| branch (tr1 tr2: Tree) : Tree

variables { α: Type } [decidable_eq α]

def Tree.leaves_list: Tree α  list α
| (Tree.leaf a) := { a }
| (Tree.branch tr1 tr2) := tr1.leaves_list ++ tr2.leaves_list

def Tree.leaves (a: Tree α): finset α := a.leaves_list.to_finset

def Tree.disjoint : Tree α  Prop
| (Tree.leaf leaf) := true
| (Tree.branch tr1 tr2) := tr1.disjoint  tr2.disjoint  disjoint tr1.leaves tr2.leaves


lemma Tree.rec_on2 {C : Tree α  Sort} (n : Tree α)
  (leaf:  (a : α), C (Tree.leaf a))
  (branch:  (tr1 tr2 : Tree α) (h1: C tr1) (h2: C tr2) (x: disjoint tr1.leaves tr2.leaves), C (tr1.branch tr2)):
  C n :=
begin
  sorry,
end

lemma Tree.leaves_list.nodup { t: Tree α } (tree_disjoint: t.disjoint):
    t.leaves_list.nodup :=
begin
    -- This non-deterministically fails with `induction tactic failed, major premise type is ill-formed` in lean 3.21.0
  induction t using Tree.rec_on2,
  {
    sorry,
  }, {
    sorry,
  }
end

view this post on Zulip Henning Dieterichs (Jan 05 2021 at 13:22):

Why doesn't this work? Tree.rec_on2 should be true.

lemma Tree.rec_on2 { α: Type } [decidable_eq α] {C : Tree α  Sort} (n : Tree α)
  (n_disjoint: n.disjoint)
  (leaf:  (a : α), C (Tree.leaf a))
  (branch:  (tr1 tr2 : Tree α) (h1: C tr1) (h2: C tr2) (x: disjoint tr1.leaves tr2.leaves), C (tr1.branch tr2)):
  C n :=
begin
  sorry,
end

lemma Tree.leaves_list.nodup { t: Tree α } (tree_disjoint: t.disjoint):
    t.leaves_list.nodup :=
begin
  induction t using Tree.rec_on2,
  { sorry, },
  { sorry, },
  { sorry, },
end

view this post on Zulip Yakov Pechersky (Jan 05 2021 at 16:00):

All you need is @[elab_as_eliminator] tagging Tree.rec_on2, and then induction t using Tree.rec_on2 works

view this post on Zulip Mario Carneiro (Jan 05 2021 at 16:06):

I just use refine instead of induction using, it's a lot more reliable

refine Tree.rec_on2 t (λ a, _) (λ tr1 tr2 h1 h2 x, _),

view this post on Zulip Yakov Pechersky (Jan 05 2021 at 16:10):

What would be your proof for Tree.rec_on2? How are you going to show disjoint tr1.leaves tr2.leaves?

view this post on Zulip Eric Wieser (Jan 05 2021 at 16:11):

It seems a shame to have an induction tactic that intros all the hypotheses for you and applies case names, only to not be able to use it

view this post on Zulip Eric Wieser (Jan 05 2021 at 16:13):

I ran into a similar problem with https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.5Brecursor.5D.20doesn't.20understand.20coe_to_sort/near/217396242

view this post on Zulip Mario Carneiro (Jan 05 2021 at 16:13):

are you volunteering to fix induction using in the C++?

view this post on Zulip Eric Wieser (Jan 05 2021 at 16:15):

Perhaps if I had an understanding of the problem. Does lean4 have the same problem with induction using, or is there no using any more?

view this post on Zulip Mario Carneiro (Jan 05 2021 at 16:15):

I think lean 4 has something fancier, but equivalent

view this post on Zulip Mario Carneiro (Jan 05 2021 at 16:15):

I would assume it didn't inherit whatever bug this is

view this post on Zulip Jannis Limperg (Jan 05 2021 at 16:30):

Does with_cases { refine ... } or with_cases { apply ... } do anything useful? I think there's some related functionality there.

view this post on Zulip Mario Carneiro (Jan 05 2021 at 16:31):

It's certainly possible to get equivalent functionality if you use with_cases, but you would have to manually tag the subgoals

view this post on Zulip Mario Carneiro (Jan 05 2021 at 16:32):

I just don't find induction using to be very useful, so I don't really care that it's buggy

view this post on Zulip Jannis Limperg (Jan 05 2021 at 16:40):

with_cases { apply ... } picks up the case names if you give them in the induction principle:

@[elab_as_eliminator]
lemma nat_ind {P :   Prop} (zero : P 0) (successor :  n, P n  P (n + 1)) (n : ) : P n :=
nat.rec zero successor n

example {P :   Prop} (z : P 0) (s :  n, P n  P (n + 1)) (n : ) : P n :=
begin
  with_cases { apply nat_ind },
  case zero { exact z},
  case successor : m ih { exact s m ih }
end

with_cases { refine ... } doesn't...

view this post on Zulip Henning Dieterichs (Jan 05 2021 at 18:35):

I just use refine instead of induction using, it's a lot more reliable

It does not tag the goals though... I like the case ... statement really much!
Thank you very much for the trick with (λ tr1 tr2 h1 h2 x, _). I thought I had to use assume when after refine!

view this post on Zulip Henning Dieterichs (Jan 05 2021 at 18:36):

What would be your proof for Tree.rec_on2? How are you going to show disjoint tr1.leaves tr2.leaves

The first "case" of the induction proof should imply this!

view this post on Zulip Henning Dieterichs (Jan 05 2021 at 18:43):

with_cases is doing something strange here:

lemma Tree.leaves_list.nodup { t: Tree α } (tree_disjoint: t.disjoint):
    t.leaves_list.nodup :=
begin
  with_cases { refine Tree.rec_on2 t (λ a, _) (λ tr1 tr2 h1 h2 x, _),   },
end

Adding (λ a, _) (λ tr1 tr2 h1 h2 x, _), has no effect!


Last updated: May 13 2021 at 05:21 UTC