search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Dealing with proofs involving complicated destructs #150

Open AdamBJ opened 9 years ago

AdamBJ commented 9 years ago

I was looking at A08_15 and got stuck:

3 subgoal
a1 : aexp
a2 : aexp
IHa1 : forall st : state, aeval st a1 = aeval st (optimize_0plus_aexp a1)
IHa2 : forall st : state, aeval st a2 = aeval st (optimize_0plus_aexp a2)
st : state
______________________________________(1/3)
aeval st a1 + aeval st a2 =
aeval st
  match a1 with
  | ANum 0 => optimize_0plus_aexp a2
  | ANum (S _) =>
      match a2 with
      | ANum 0 => optimize_0plus_aexp a1
      | ANum (S _) => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AId _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | APlus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMinus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMult _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      end
  | AId _ =>
      match a2 with
      | ANum 0 => optimize_0plus_aexp a1
      | ANum (S _) => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AId _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | APlus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMinus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMult _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      end
  | APlus _ _ =>
      match a2 with
      | ANum 0 => optimize_0plus_aexp a1
      | ANum (S _) => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AId _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | APlus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMinus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMult _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      end
  | AMinus _ _ =>
      match a2 with
      | ANum 0 => optimize_0plus_aexp a1
      | ANum (S _) => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AId _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | APlus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMinus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMult _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      end
  | AMult _ _ =>
      match a2 with
      | ANum 0 => optimize_0plus_aexp a1
      | ANum (S _) => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AId _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | APlus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMinus _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      | AMult _ _ => APlus (optimize_0plus_aexp a1) (optimize_0plus_aexp a2)
      end
  end
______________________________________(2/3)
aeval st a1 - aeval st a2 =
aeval st (optimize_0plus_aexp a1) - aeval st (optimize_0plus_aexp a2)
______________________________________(3/3)
aeval st a1 * aeval st a2 =
aeval st (optimize_0plus_aexp a1) * aeval st (optimize_0plus_aexp a2)

Obviously the Aplus case is the tricky bit. I know it will involve some combination of destruct... destruct.... rewrite.... omega... but I'm not sure the order I should apply these tactics. I seem to get lost no matter what I do and end up with 30 or so subgoals. What strategies can we use to approach goals like this one intelligently?

AdamBJ commented 9 years ago

I got the answer by being as systematic as I could; destructing everything, then simpl, then reflexivity, then omega.... so I'm not looking for the answer. Just general strategies for this kinds of problems.