search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Assignment 10_08 #140

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

I'm trying to follow the guide for this question: (ie
.. P (C n1) t2 ==> (by ST_Plus2) P (C n1) t2' ==> (by ST_Plus2) P (C n1) t2'' ==> (by ST_Plus2) .. P (C n1) (C n2) ==> (by ST_PlusConstConst) C (n1 + n2))

But I'm getting stuck near the end:

3 subgoal
Case := "P" : String.string
t2 : tm
n1 : nat
n2 : nat
H0 : t2 || n2
IHeval2 : t2 ==>* C n2
y : tm
H3 : t2 ==> y
H4 : y ==>* C n2
y0 : tm
H7 : y ==> y0
H8 : y0 ==>* C n2
H : C n1 || n1
IHeval1 : C n1 ==>* C n1
______________________________________(1/3)
y ==> C n2
______________________________________(2/3)
P (C n1) (C n2) ==>* C (n1 + n2)
______________________________________(3/3)
P t1 t2 ==>* C (n1 + n2)

H4 tells us that y mutli-steps to C n2, but I need to show y steps to C n2. Is this goal provable? If so, can someone give me a hint about what to do next?

alkaza commented 9 years ago

Did you try using multistep_congr_1 and multistep_congr_2?

AdamBJ commented 9 years ago

I'm having trouble with syntax. I'd like to apply the congr theorems in IHeval2, something like apply multistep_congr_1 in IHeval2 with (t1:=t1)., but that doesn't seem to be working. Any suggestions?

jaewooklee93 commented 9 years ago

Yeah, it seems impossible. y0 and y looks useless.

alkaza commented 9 years ago

I meant you should have used those theorems before this goal. Right after Case "P".

AdamBJ commented 9 years ago

What's the difference between starting this assignment by doing induction on t: tm vs doing induction on H: t || n? In the first case I know we're breaking t down into its two possible cases, and in the second case we're breaking the "evaluates to" relation down to it constituent cases, but in practice they seem to do the same thing: break down to a constant case and a plus case. However, while I was able to solve this problem by doing induction on t, I couldn't solve it when I started with induction on H. I'm not clear on what the difference is though.

jeehoonkang commented 9 years ago

In this case, I think induction on t and H are equivalent. I am pretty sure you can solve the same problem by induction on H, possibly with more complicated context management.

As you may have experienced, while construct usually clearly reveals the difference between induction on terms and that on derivations (of step, etc). The execution of a while does not depend on the size of the term. So if you want to induct on the execution, rather than the term itself, you have to induction the derivation (H) instead of the term (t).

jeehoonkang commented 9 years ago

137 deals with the same question :-)

AdamBJ commented 9 years ago

@jeehoonkang Ok, thanks. Did you get my email regarding the grading of Assignment 09?