## Stream: Beginner Questions

### Topic: Obvious subgoal failed sledgehammer

#### Chengsong Tan (Feb 06 2022 at 19:06):

Hi all,
I am writing a proof proving two lemmas about derivatives of regular expressions.
I prove them concurrently because they are using each other
during the induction step.
The induction strategy was reverse induction on the structure of string s.
When proving the induction step, I tried to make each rewriting step explicit by using a subgoal for that rewrite.
And since each rewrite step has a lemma with it to go through, sledgehammer will
always find the proof for that rewrite. This method is clumsy but helps me go through without all
the clever erule/frule/etc......
The problem is I got stuck in this middle part where a seemingly obvious rewrite step doesn't
go through with sledgehammer: the fact
`rerase (bders_simp r xs) = rerase (bsimp (bders r xs))`
which appeared in the premise of the subgoal.
I am wondering why is the premise not used? Am I missing
something about quantifier instantiation? (Maybe the xs mean different things in the premise and conclusion?)

``````lemma ders_simp_commute:
shows "s ≠[] ⟹ rerase  (bders_simp r s) = rerase (bsimp (bders r s))"
and "s ≠ [] ⟹ rders_simp (RSEQ r1 r2) s =
rsimp (RALTS  ((RSEQ (rders r1 s) r2) #
(map (rders r2) (orderedSuf s))) )"
apply(induct s arbitrary: r r1 r2 rule: rev_induct)
apply simp
apply simp

apply (simp add: bders_simp_append )
apply(subgoal_tac "rerase (bsimp (bder x (bders_simp r xs))) = (rsimp (rerase (bder x (bders_simp r xs)))) ")
prefer 2
apply (simp add: rerase_bsimp)
apply(subgoal_tac "(rsimp (rerase (bder x (bders_simp r xs)))) = (rsimp (rder x (rerase (bders_simp r xs))))")
prefer 2
apply(subgoal_tac "rerase (bders_simp r xs) = rerase (bsimp (bders r xs))")

prefer 2

sledgehammer
``````

Thanks a lot!
Chengsong

#### Chengsong Tan (Feb 06 2022 at 19:10):

Image-2022-02-06-at-6.51.49-PM.jpeg #### Maximilian Schaeffeler (Feb 06 2022 at 20:08):

Doesn't the premise only apply when xs is nonempty?

#### Chengsong Tan (Feb 06 2022 at 23:11):

Maximilian Schaeffeler said:

Doesn't the premise only apply when xs is nonempty?

Yes you are correct, I need to rethink that to make the induction go through, because for the inductive case
only xs@[x] != [] is guaranteed which says nothing about the non-emptiness of xs.
Probably need to do a case distinction on xs being [] and xs being not [].
Thank you for pointing that out!

Last updated: Jul 15 2022 at 23:21 UTC