## Stream: general

### Topic: Custom Principle Of Induction

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


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


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

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


#### 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?

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

#### Mario Carneiro (Jan 05 2021 at 16:13):

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

#### 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?

#### Mario Carneiro (Jan 05 2021 at 16:15):

I think lean 4 has something fancier, but equivalent

#### Mario Carneiro (Jan 05 2021 at 16:15):

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

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

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

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

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

#### 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!

#### 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!

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