Stream: Beginner Questions

Topic: Obvious subgoal failed sledgehammer


view this post on Zulip 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

view this post on Zulip Chengsong Tan (Feb 06 2022 at 19:10):

Image-2022-02-06-at-6.51.49-PM.jpeg

view this post on Zulip Maximilian Schaeffeler (Feb 06 2022 at 20:08):

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

view this post on Zulip 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