recursive proof on inductive type

Stream: new members

[fkefjlwejlfk]

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]

this is induction

[Mario Carneiro]

you should do induction r, or alternatively do a recursive proof referencing proof_process_works in the subgoals

[fkefjlwejlfk]

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]

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]

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]

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]

The _ _ are placeholders for x y

[Ruben Van de Velde]

Those are three arguments to singles_to_doubles, and the underscores are "lean can figure this out"

[Reid Barton]

Since you made them explicit arguments to singles_to_double.

[fkefjlwejlfk]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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