Assignment 7 Question 2

[AdamBJ]

I'm stuck on the final case of an induction using aexp in question 2. When I use simpl on aeval (optimize_1mult (AMult a1 a2)) = aeval (AMult a1 a2) I'm hit with this wall of text:

  match a1 with
  | ANum 0 =>
      match a2 with
      | ANum 0 => AMult (optimize_1mult a1) (optimize_1mult a2)
      | ANum 1 => optimize_1mult a1
      | ANum (S (S _)) => AMult (optimize_1mult a1) (optimize_1mult a2)
      | APlus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMinus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMult _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      end
  | ANum 1 => optimize_1mult a2
  | ANum (S (S _)) =>
      match a2 with
      | ANum 0 => AMult (optimize_1mult a1) (optimize_1mult a2)
      | ANum 1 => optimize_1mult a1
      | ANum (S (S _)) => AMult (optimize_1mult a1) (optimize_1mult a2)
      | APlus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMinus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMult _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      end
  | APlus _ _ =>
      match a2 with
      | ANum 0 => AMult (optimize_1mult a1) (optimize_1mult a2)
      | ANum 1 => optimize_1mult a1
      | ANum (S (S _)) => AMult (optimize_1mult a1) (optimize_1mult a2)
      | APlus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMinus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMult _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      end
  | AMinus _ _ =>
      match a2 with
      | ANum 0 => AMult (optimize_1mult a1) (optimize_1mult a2)
      | ANum 1 => optimize_1mult a1
      | ANum (S (S _)) => AMult (optimize_1mult a1) (optimize_1mult a2)
      | APlus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMinus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMult _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      end
  | AMult _ _ =>
      match a2 with
      | ANum 0 => AMult (optimize_1mult a1) (optimize_1mult a2)
      | ANum 1 => optimize_1mult a1
      | ANum (S (S _)) => AMult (optimize_1mult a1) (optimize_1mult a2)
      | APlus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMinus _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      | AMult _ _ => AMult (optimize_1mult a1) (optimize_1mult a2)
      end
  end = aeval a1 * aeval a2

My first question is: why doesn't the left hand side (ie (optimize_1mult (AMult a1 a2))) simpl to just aeval(AMult (optimize_1mult a1) (optimize_1mult a2))? My second question is what to do when confronted with this kind of situation. How can I sift through all that text to find something useful? I feel like destructing a1 and a2 would just make this more chaotic, and I'm hoping that there's an easier way.

[jeehoonkang]

It would be more readable if you enclose codes inside code blocks. :-) I am now reading your question.

Jeehoon

[jaewooklee93]

Your exceedingly long goal begin with match a1 with, so try destruct a1, then it will be decomposed into small parts.

[AdamBJ]

But if I destruct a1 won't I eventually be stuck with something like AMult (AMult (a1_0 a1_1)) a2? It seems like that would be harder to solve.

[jaewooklee93]

However, at least your a1 (= AMult (a1_0 a1_1)) and a2 are smaller than your original goal a. Then you may be able to use your induction hypotheses.

[AdamBJ]

I haven't been able to get it to work by destructing a1 - after destructing a1 n needs to be destructed, then a2.... it gets mind-boggling quickly. Were you able to solve the problem by destructing a1 or is there an easier way that I'm perhaps missing? (a yes or no answer to that question is all I'm looking for) I guess there isn't any way around this problem though, it seems pretty clear that we must do induction on a and induction on a leads to the wall of text.

[jaewooklee93]

Yes, I also needed destruct a1 to solve it and I should destruct the case even more. Actually I used 6 destruct only for the case aeval (optimize_1mult (AMult a1 a2)) = aeval (AMult a1 a2).

6 times of destruct may result in more than 20 independent cases and, of course, I cannot handle them manually. However, clever uses of ;, try rewrite and try omega will lead you to the solution of only 5 lines as the comment mentioned.

[jaewooklee93]

Oh, I missed your first question. First, (optimize_1mult (AMult a1 a2))) is not the same as (AMult (optimize_1mult a1) (optimize_1mult a2)) The counterexample is, if 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.

Actually, that complicated Wall of codes just specifies all the possible optimization around AMult.

[AdamBJ]

I gave this a try: try destruct a1; try destruct n; try destruct a2; try destruct n; simpl; try rewrite IHa1; try rewrite IHa2; try omega; try reflexivity.

But I was still left with 20 subgoals, as you suggested would happen. This is what my context and the first of the 20 subgoals look like:

20 subgoal
n : nat
IHa1 : aeval (optimize_1mult (ANum 0)) = aeval (ANum 0)
IHa2 : aeval (optimize_1mult (ANum (S n))) = aeval (ANum (S n))
______________________________________(1/20)
aeval match n with
      | 0 => ANum 0
      | S _ => AMult (ANum 0) (ANum (S n))
      end = 0

I can't destruct n anymore, and IHa1 and IHa2 just simpl down to true so I'm not sure where to go from here. More generally, can you give some tips for coming up with a strategy that we think will apply to 20+ subgoals? It feels like an impossible job to come up with a strategy that will allow us to solve all of them. How can we factor the form of each subgoal into our thinking? Do I need to examine each goal one by one?

[jeehoonkang]

Hi @AdamBJ ,

As @jaewooklee93 suggested, concatenated tactics (by ;) help a lot in proving things in small codes. However, before optimising proof size, you have to understand what's going on under the hood. For this, I recommend you to:

• At first, do not use ; for a while and try to solve several, say 3, goals out of 20 goals.
• Find the general and common pattern of proofs for the several goals.
• Try to use the found pattern to solve 20 goals at once by concatenating tactics.
• If there are remaining goals, examine it, and adjust the concatenated tactics.

This is rather hand-waving explanation on how to do proofs in general; please understand that I cannot give you more specific answers. Hope you will find a way.

Jeehoon

[AdamBJ]

OK, that's a good overview. Thanks you both for the help.

[alkaza]

I still have no idea where to go after destructing a1.

[jaewooklee93]

@AdamBJ You are almost done. Why did you think that you couldn't destruct n anymore? Your goal began with match n with and that was the most definite signal for the timing to use destruct n again.

[AdamBJ]

In the past when stuck on a case involving S n destructing n again didn't do anything useful - maybe I'd be able to solve for the case when n=1, but then I'd just be stuck on the S S n case. In the case of this question though, I think I'm getting the n in the goal mixed up with the n I destructed earlier. I should have used destruct as... to make things clearer. I'll try the extra destruct once I get back to my laptop, thanks for pointing it out.

[AdamBJ]

@alkaza You have to systematically destruct variables until you can until you get rid of all the "match _ with" stuff. Only then can you apply the inductive hypotheses to solve the sub goals. You'll definitely need to use automation though as the number of sub goals gets pretty large.