Custom Principle Of Induction

Stream: general

[Henning Dieterichs]

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

[Henning Dieterichs]

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

[Yakov Pechersky]

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

[Mario Carneiro]

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, _),

[Yakov Pechersky]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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?

[Mario Carneiro]

I think lean 4 has something fancier, but equivalent

[Mario Carneiro]

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

[Jannis Limperg]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jannis Limperg]

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...

[Henning Dieterichs]

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!

[Henning Dieterichs]

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!

[Henning Dieterichs]

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!