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

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

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

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