# Zulip Chat Archive

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

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

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