search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Assignment 07_02 #87

Closed alkaza closed 9 years ago

alkaza commented 9 years ago

I'm not sure if it is ok to ask this type of question, but I'm stuck and don't know where to go after reaching the "AMult" Case in this Theorem. Any suggestions on what should be done here?

Case := "AMult" : String.string
a1 : aexp
a2 : aexp
IHa1 : aeval (optimize_1mult a1) = aeval a1
IHa2 : aeval (optimize_1mult a2) = aeval a2
______________________________________(1/1)
aeval (optimize_1mult (AMult a1 a2)) = aeval (AMult a1 a2)

For example, 

induction a1.

leads to nowhere...

jaewooklee93 commented 9 years ago

At that point, your desirable next step might be simpl. And then there are plenty of things to try; destruct, rewrite, eauto, omega,... and so on.

Also, before this exercise, you might have been completely fine even though you only used tactics. However, from now on, we need not only tactics but also tacticals (;, try, or repeat) to solve exercises with codes of reasonable size.

This exercise will be a great chance to cultivate your skill to use tacticals properly.

alkaza commented 9 years ago

As far as I tried further destruct, simpl and omega, nothing helped. I'm completely stuck at this point. To apply tacticals, I tried to figure out the pattern, but I keep going in circles:

destruct a1. destruct n. 
destruct a2. destruct n. 
simpl. reflexivity.
destruct n.
simpl. reflexivity.
simpl. reflexivity.
simpl. reflexivity.
simpl. reflexivity.
simpl. reflexivity.
destruct n. 
simpl. omega. 
destruct n. destruct a2. 
destruct n.
simpl. reflexivity.

Could I get any hint on what am I doing wrong?

jaewooklee93 commented 9 years ago

Your code is not wrong, but it is just not efficient. There are some number of repetition of simpl. reflexivity. followed by destruct n, so just simplify the code with destruct n; try simpl; try reflexivity; (and so on.) Those semicolon perform parallel application of tactics.

alkaza commented 9 years ago

Trying to find the pattern to apply tactics, I tried to solve it manually at first:

+    destruct a1. destruct n. destruct a2.
+    destruct n. 
+    simpl. reflexivity.
+    destruct n.
+    simpl. reflexivity.
+    simpl. reflexivity.
+    simpl. reflexivity.
+    simpl. reflexivity.
+    simpl. reflexivity.
+    destruct n.
+    simpl. omega.
+    destruct a2. destruct n.
+    destruct n0.
+    simpl. reflexivity.
+    destruct n0.
+    simpl. reflexivity.
+    simpl. omega.
+    destruct n. destruct n0.
+    simpl. reflexivity.
+    destruct n0.
+    simpl. reflexivity.
+    simpl. omega.
+    destruct n. destruct n0.
+    simpl. reflexivity.
+    destruct n0.
+    simpl. reflexivity.
+    simpl. omega.
+    destruct n. destruct n0. 
+    simpl. reflexivity.
+    destruct n0.
+    simpl. reflexivity.
+    destruct n0.
+    simpl. reflexivity.
+    destruct n0. 
+    simpl. reflexivity.
+    destruct n0.
+    simpl. reflexivity.

After series of destruct:

    destruct a1; try (destruct n; destruct a2); try (destruct n); 
      try (simpl; reflexivity); try (simpl; omega).
    destruct n; try destruct n0; try (simpl; reflexivity); try (simpl; omega).
    destruct n0; try destruct n; try (simpl; reflexivity); try (simpl; omega).
    destruct n0; try (simpl; reflexivity); try (simpl; omega).
    destruct n0; try destruct n; try (simpl; reflexivity); try (simpl; omega).

I remain left with 9 subgoals;

9 subgoal
Case := "AMult" : String.string
a2_1 : aexp
a2_2 : aexp
IHa1 : aeval (optimize_1mult (ANum 1)) = aeval (ANum 1)
IHa2 : aeval (optimize_1mult (APlus a2_1 a2_2)) = aeval (APlus a2_1 a2_2)
______________________________________(1/9)
aeval (optimize_1mult (AMult (ANum 1) (APlus a2_1 a2_2))) =
aeval (AMult (ANum 1) (APlus a2_1 a2_2))
______________________________________(2/9)
aeval (optimize_1mult (AMult (ANum (S (S n))) (APlus a2_1 a2_2))) =
aeval (AMult (ANum (S (S n))) (APlus a2_1 a2_2))
______________________________________(3/9)
aeval (optimize_1mult (AMult (ANum 1) (AMinus a2_1 a2_2))) =
aeval (AMult (ANum 1) (AMinus a2_1 a2_2))
______________________________________(4/9)
aeval (optimize_1mult (AMult (ANum (S (S n))) (AMinus a2_1 a2_2))) =
aeval (AMult (ANum (S (S n))) (AMinus a2_1 a2_2))
______________________________________(5/9)
aeval (optimize_1mult (AMult (ANum 1) (AMult a2_1 a2_2))) =
aeval (AMult (ANum 1) (AMult a2_1 a2_2))
______________________________________(6/9)
aeval (optimize_1mult (AMult (ANum (S (S n))) (AMult a2_1 a2_2))) =
aeval (AMult (ANum (S (S n))) (AMult a2_1 a2_2))
______________________________________(7/9)
aeval (optimize_1mult (AMult (APlus a1_1 a1_2) a2)) =
aeval (AMult (APlus a1_1 a1_2) a2)
______________________________________(8/9)
aeval (optimize_1mult (AMult (AMinus a1_1 a1_2) a2)) =
aeval (AMult (AMinus a1_1 a1_2) a2)
______________________________________(9/9)
aeval (optimize_1mult (AMult (AMult a1_1 a1_2) a2)) =
aeval (AMult (AMult a1_1 a1_2) a2)

if I use simpl, It doesn't unfold to match n with, but to something like:

______________________________________(1/9)
aeval (optimize_1mult a2_1) + aeval (optimize_1mult a2_2) =
aeval a2_1 + aeval a2_2 + 0

Which cannot be proven.

My question is: how do I get aeval out of context? Or what am I doing wrong here?

jaewooklee93 commented 9 years ago

Until that point, you haven't used your induction hypotheses. Your goal (1/9) can be proven just after performing rewrite IHa2. (You may need simpl in IHa2 as well, I'm not sure, though.)

alkaza commented 9 years ago

I used omega instead of induction hypotheses, since it solved a subgoal whenever it could be solved by rewriting the induction hypothesis. I tried to simplify induction hypothesis but it can't be used on goal (1/9) or, in fact, any other goals, because AMult is standing on it's way... I don't know what to do.

jaewooklee93 commented 9 years ago

I guessed that simpl in IHa2 results in IHa2 : aeval (optimize_1mult a2_1) + aeval (optimize_1mult a2_2) = aeval a2_1 + aeval a2_2 and it just fits your purpose, goal (1/9). But if it doesn't work properly, it's strange to me.

In my opinion, omega is strong but not really perfect, since it sometimes fails to clear the goal even though the goal is evident, so we may have to rewrite manually, simpl or subst before using it.

alkaza commented 9 years ago

Yeah, I know, it just worked on previous goals. But at this point I'm stuck.

alkaza commented 9 years ago

Thanks @jaewooklee93 for your help, I finally figured it out, took me 10 destructs and long compilation time, but better than nothing :D

jaewooklee93 commented 9 years ago

That's great.

I think the minimum number of destruct is 6 and it is achievable with connecting all tactics in one group with semicolons.

alkaza commented 9 years ago

I minimized to 7, can't figure out how to make it 6 hahaha