search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

How can I unfold some portion of my goal? #88

Closed ik1ne closed 3 years ago

ik1ne commented 9 years ago

While solving 7_2, I managed to simplify my goal into this: AMult (optimize_1mult a1) (optimize_1mult a2) = optimize_1mult (AMult a1 a2) And this must be very simple to proof, since Fixpoint optimize_1mult has match a with | AMult e1 e2 ... so I can simpl(or unfold optimize_1mult) right hand side only and then use reflexivity. But, when I try simpl tactics, it also unfolds optimize_1mult in the left side, making the goal nearly impossible to proof without induction/destruct. Do I have to use induction for this goal?

jeehoonkang commented 9 years ago

Try unfold optimize_1mult at 1, unfold optimize_1mult at 2, etc.

jaewooklee93 commented 9 years ago

(optimize_1mult (AMult a1 a2))) is not the same as (AMult (optimize_1mult a1) (optimize_1mult a2)) The counterexample is the case of a1=ANum 1 and a2=ANum 2.

(optimize 1)×(optimize 2)=1×2 doesn't give you the same formula as optimize (1×2)=2.

jeehoonkang commented 9 years ago

May I ask if there is any progress on this issue?

jaewooklee93 commented 9 years ago

I think it is already ended, since it dealt with the last assignment.

ik1ne commented 9 years ago

Oh, yes, I found that I was proving wrong way, so I haven't used unfolding some portion in assignment 7. However, I used it in assignment 08. Thank you!