# Zulip Chat Archive

## Stream: new members

### Topic: recursive proof on inductive type

#### fkefjlwejlfk (Jan 29 2023 at 15:19):

hi all,

I have this #mwe

```
inductive room : Type
| Single : room
| Double : room -> room -> room
def process : room -> Prop := sorry
lemma singles_to_double (x y : room) : (process x) ∧ (process y) -> process (room.Double x y) := sorry -- assume we have a proof for this
lemma proof_process_works (r : room) : process r :=
match r with
| room.Single := sorry -- assume we have this proof
| (room.Double x y) :=
begin
apply singles_to_double,
sorry -- what do I do here?
end
end
```

In the `proof_process_works`

lemma, assume we have a proof for `room.Single`

. Now I want to create a proof for `room.Double`

by using the fact that we can kind of split this up with `singles_to_double`

. However, we now get a new goal:

```
process x ∧ process y
```

I can perform `cases`

on `x`

and `y`

, but this process repeats infinitely. Can I make use of the fact that eventually this process will reach base cases of `room.single`

and then use the fact that we already have a proof provided in the first `match`

statement? What do I do here?

Thank you for reading and I wish all of you the best day possible

#### Mario Carneiro (Jan 29 2023 at 15:23):

this is induction

#### Mario Carneiro (Jan 29 2023 at 15:24):

you should do `induction r`

, or alternatively do a recursive proof referencing `proof_process_works`

in the subgoals

#### fkefjlwejlfk (Jan 29 2023 at 15:26):

Mario Carneiro said:

you should do

`induction r`

, or alternatively do a recursive proof referencing`proof_process_works`

in the subgoals

Which tactic do I use to refrence `proof_process_works`

in a subgoal? I tried apply but it gives me an error saying it does not recognize `proof_process_works`

. Sorry for the noob question im kind of new. Im using lean 3

#### fkefjlwejlfk (Jan 29 2023 at 15:28):

Mario Carneiro said:

you should do

`induction r`

, or alternatively do a recursive proof referencing`proof_process_works`

in the subgoals

So instead of pattern matching I start the proof with `induction r`

right?

#### Mario Carneiro (Jan 29 2023 at 15:30):

```
lemma proof_process_works1 : ∀ (r : room), process r
| room.Single := sorry
| (room.Double x y) := singles_to_double _ _ ⟨proof_process_works1 x, proof_process_works1 y⟩
lemma proof_process_works2 (r : room) : process r :=
begin
induction r with x y IH1 IH2,
{ sorry },
{ apply singles_to_double,
split,
{ apply IH1 },
{ apply IH2 } }
end
```

#### fkefjlwejlfk (Jan 29 2023 at 15:35):

Mario Carneiro said:

`lemma proof_process_works1 : ∀ (r : room), process r | room.Single := sorry | (room.Double x y) := singles_to_double _ _ ⟨proof_process_works1 x, proof_process_works1 y⟩`

Thank you!

One question, what does the notatin `_ _ ⟨proof_process_works1 x, proof_process_works1 y⟩`

do exactly? I read it as it filling in the results of the things between the angle brackets in the `_`

placeholders. Is that correct?

#### Reid Barton (Jan 29 2023 at 15:40):

The `_ _`

are placeholders for `x y`

#### Ruben Van de Velde (Jan 29 2023 at 15:40):

Those are three arguments to `singles_to_doubles`

, and the underscores are "lean can figure this out"

#### Reid Barton (Jan 29 2023 at 15:40):

Since you made them explicit arguments to `singles_to_double`

.

#### fkefjlwejlfk (Jan 29 2023 at 15:46):

do these angled brackets have a special meaning? ⟨ and ⟩

#### Kevin Buzzard (Jan 29 2023 at 15:54):

They're a generic constructor notation when there's only one constrictor

#### Kevin Buzzard (Jan 29 2023 at 15:54):

#tpil chapters 7 and 8 is maybe what you want to be reading

Last updated: Dec 20 2023 at 11:08 UTC