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