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