Meaning of " You can use the following intro pattern: destruct ... as [[? ?] | [? ?]]."

[AdamBJ]

Just like the title says. What exactly does "you can use the following intro pattern mean"? Is there some way to combine destruct and intros? Or is it saying that at some point early in the proof we should use destruct ... as [[? ?] | [? ?]].?

[jaewooklee93]

We should use destruct in such way to solve the question simply with proof automation.

[AdamBJ]

Ok, thanks. @jaewooklee93 related to the same question, if I'm trying to prove:

a / st ==>a a

is there a rule like multi_refl I can turn to to solve the goal? It seems like if one is true, then the other should be too.

[AdamBJ]

I get stuck in a similar place for both of the first questions. Eauto, even with the hints, can't seem to solve it though so I guess it's not possible. I'm not sure what else to try though.

[AdamBJ]

I'm still not 100% sure what to make of destruct ... as [[? ?] | [? ?]]. When I destruct a (which as far as I can see is the thing to destruct), I can do something like destruct [a|b|c|d|e], but If I try something of the form [[? ?] | [? ? ] ] it says that the pattern expects 5 objects. How can we use something like destruct ... as [[? ?] | [? ?]] on an aexp?

[Parkdaeyoung]

You can't do that on aexp. aexap is inductively defined and has 5construcors. That's why coq says expects 5 objects. But <destruct ... as [[? ?] | [? ?]]> means there are two cases(or constructors) and both of them have two variable to be named after ?. BTW, Do case analysis step by step and see the contexts to find the pattern. I'm sure you can find it and know what the pattern is supposed to mean. It would be also a great help to admit cases you are uncomfortable with and see next cases.

[AdamBJ]

Ok, thanks for the tip. I've tried working the problem a different way, but now I'm getting stuck here:

5 subgoal
a1 : aexp
a2 : aexp
IHa1 : forall st : state,
       (exists n : nat, a1 = ANum n) \/ (exists a' : aexp, a1 / st ==>a a')
IHa2 : forall st : state,
       (exists n : nat, a2 = ANum n) \/ (exists a' : aexp, a2 / st ==>a a')
st : state
x : nat
H : a1 = ANum x
x0 : nat
H0 : a2 = ANum x0
______________________________________(1/5)
APlus (ANum x) (ANum x0) = ANum (x + x0)

I can't solve the goal though. It's so frustrating, because it seems like it should be true by some constructor or another. But neither I nor eauto/auto can find it. Am I on the right track here? Can I solve the goal?

[AdamBJ]

The final three cases of Plus, Minus and Mult all seem to have the same structure. So I guess if I can solve one of them I'll be able to solve all the others (hence the reason we can automate this proof so well).

[Parkdaeyoung]

Did you do intros. generalize dependent st? Actually, you don't have to do that. If you just do induction on a from the beginning of the proof or specialize IHa1 st. specialize IHa2 st on the current context, you shall use the pattern finally. Then, each of the final 3 cases becomes 4 sub-cases(total 12sub-cases) and you can prove all of them using simple tacticals.

[AdamBJ]

I got it! Thanks so much for the help. I still have a couple question though:

First, I wanted to use an Ltac to solve these goals:

(exists n : nat, APlus a1 a2 = ANum n) \/
(exists a' : aexp, APlus a1 a2 / st ==>a a')
______________________________________(2/3)
(exists n : nat, AMinus a1 a2 = ANum n) \/
(exists a' : aexp, AMinus a1 a2 / st ==>a a')
______________________________________(3/3)
(exists n : nat, AMult a1 a2 = ANum n) \/
(exists a' : aexp, AMult a1 a2 / st ==>a a')

This almost works Ltac rwgoal2 H1:= right; rewrite H; exists(...). eauto. But I'm not sure how to customize the (...) for APlus, AMinus etc.

My second question is about destruct ... as [[? ?] | [? ?]];. I used the pattern to solve the proof but I'm not sure what it does. I've never seen the ? ? pattern before. What's the difference between using the ? ? pattern and simply saying "destruct ..."?

[Parkdaeyoung]

I think it's hard to use Ltac because there are so many distinct cases as you said. I'd prefer subst which works with eauto well , such as ... ; subst ; eauto.. (Personally, I use subst when the goal seems to be rewritten or when it's necessary to clear up the contexts.)

I guess destruct ... and `destruct ... as [[? ?] | [? ?]] do the same thing practically. But It's convenient to name all the variables you are going to use in automation. Otherwise, there might be some repetition of names ,which makes it difficult to use tacticals efficiently.

[jaewooklee93]

I didn't use Ltac and I don't even know how to use it :)

For ?, refer to #102 (They're just wildcards.)

@Parkdaeyoung Without [[? ?] | [? ?]], proof automation doesn't work. That's because we need to extract variables from exists before using eauto. Simple destruct doesn't extract variables.

[AdamBJ]

For the next question, I solved for BTrue and BFalse and expected to see inductive hypotheses show up (since True and False make up the base cases, right?) but instead my context looked disappointingly empty:

4 subgoal
st : state
a : aexp
a0 : aexp
______________________________________(1/4)
(BEq a a0 = BTrue \/ BEq a a0 = BFalse) \/
(exists b' : bexp, BEq a a0 / st ==>b b')
______________________________________(2/4)
(BLe a a0 = BTrue \/ BLe a a0 = BFalse) \/
(exists b' : bexp, BLe a a0 / st ==>b b')
______________________________________(3/4)
(BNot b = BTrue \/ BNot b = BFalse) \/
(exists b' : bexp, BNot b / st ==>b b')
______________________________________(4/4)
(BAnd b1 b2 = BTrue \/ BAnd b1 b2 = BFalse) \/
(exists b' : bexp, BAnd b1 b2 / st ==>b b')

Am I misunderstanding the definition of bexp? Where did the inductive hypotheses go?

[jaewooklee93]

Your goal is provable. BEq a a0 = BTrue and BEq a a0 = BFalse are obviously false, but the third one may work. In the viewpoint of bexp, BEq and BLe are also base cases because they don't contain another bexp inside. You will see your induction hypotheses in the cases of BNot and BAnd.

[AdamBJ]

@jaewooklee93 So the ? tell destruct to instantiate the exists in the hypothesis? Then I guess the middle | is to somehow deal with the \/. In the future then, if there is a hypothesis in the context with an exists ... : that I want to get rid of, then I should use destruct with ?? And that makes more sense about bexp, thanks.

[Parkdaeyoung]

@jaewooklee93 Thank you for the correction! But I think some trick can solve the problem. ... ; destruct A ; inversion B ; ... is equivalent to the pattern-version for this problem.

[AdamBJ]

For proving exists b' : bexp, BEq a a0 / st ==>b b'

I have these three rules:

| BS_Eq : forall st n1 n2,
      (BEq (ANum n1) (ANum n2)) / st ==>b 
      (if (beq_nat n1 n2) then BTrue else BFalse)
  | BS_Eq1 : forall st a1 a1' a2,
      a1 / st ==>a a1' ->
      (BEq a1 a2) / st ==>b (BEq a1' a2)
  | BS_Eq2 : forall st v1 a2 a2',
      aval v1 -> 
      a2 / st ==>a a2' ->
      (BEq v1 a2) / st ==>b (BEq v1 a2')

But how can I use them if I don't have any information about the way a or a0 steps, or whether or not they're constants?

[jaewooklee93]

Basically, destruct H as [? ?] extracts n and P(n) from H: exists n, P(n) and destruct H0 as [?|?] splits two cases Q and R from H0: Q \/ R. But for these single destruct we don't have to specify patterns.

And then, for this case, we have (exists n : nat, APlus a1 a2 = ANum n) \/ (exists a' : aexp, APlus a1 a2 / st ==>a a'), simple destruct performs only splitting (because it only destructs outermost target, as we didn't specify the pattern), but if we specify destructing pattern with [[? ?]|[? ?]], destruct performs both of splitting and extracting.

@Parkdaeyoung I see. Maybe destruct A; destruct B will work well, too. (and inversion is a stronger version of destruct) Specifying [[? ?]|[? ?]] simply means that we have to destruct twice.

[jaewooklee93]

@AdamBJ You should use the previous one, aexp_strong_progress.

[AdamBJ]

Well... now I can't figure out how to get the BS_Eqs working. We only have two aexps in the context, so how can I do something like exists (BEq a a0') that seems neccesary in order to get to a point where I can apply aexp_strong_progress?

[AdamBJ]

Also, is there a way I can introduce aexp_strong_progress into the context?

[Parkdaeyoung]

assert it.

[jaewooklee93]

destruct (aexp_strong_progress st a).

[AdamBJ]

Can an aexp step to itself? I know it can multistep to itself (multi_refl), but how about some like a / st ==>a a?

[jaewooklee93]

No, aexp cannot step to itself

[AdamBJ]

But it could muti step to itself, right? How come it can't step to itself?

[jaewooklee93]

Yes, but multi step is not a real step. By the way, this exercise has nothing to do with multi step.

[rhs0266]

I recommend use assert (P1 := aexp_strong progress a1).

[AdamBJ]

@jaewooklee93 A multistep is a series of steps, right? By multi_refl some term x could step to x1, then x2.... then back to x. What isn't it possible for some term to step to itself as some kind of "identity step"? Is it just because we didn't define the language that way?

[jaewooklee93]

Yes, multi is a series of steps with the length of 0,1,2, ... and so on. However, the thing like x ==> x1 ==> x2 ==> ... ==> x is impossible (at least for astep and bstep) because the step for aexp and bexp always make the expression simpler (the complexity is strictly decreasing) that's the reason of no cycles among steps, and multi_refl is totally not related to this fact.

Maybe the name of multi is misleading, the better name for multi can be reachability. Then multi_refl says the following trivial fact. Every expression x can reach to x itself. Then multi_step simply states that, given x can step to y and y can reach to z, then x can reach to z.

In this context, we can say that x can reach to x using multi_refl, but that doesn't mean that x can step to x itself. Rather, if you make any step from x, you cannot come back to x forever.

[AdamBJ]

Ok, thanks jaewook!