Chengsong Tan (Feb 06 2022 at 19:06): 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!
Notification Bot (Feb 07 2022 at 08:03):Maximilian Schaeffeler has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC