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