了解如何从Software Foundations的正则表达式中证明一些引理

Question

我正在通过Software Foundations工作，目前在IndProp部分。注意：我是一个人在做，这不是功课。

我仍在努力思考如何使用这些归纳类型。

在证明泵送引理的过程中（我在：|失败了，我试图证明一些引理...这些引理最终是不必要的，但仍然觉得它们应该是可证明的。

Lemma start_to_exists: forall (T:Type) (re: @reg_exp T) (s: list T),
  s =~ Star re -> exists (s':list T), s' =~ re.

Lemma star_empty_is_empty: forall (T:Type) (s:list T),
  s =~ Star EmptyStr -> s =~ EmptyStr.

Lemma star_empty: forall (T:Type) (s:list T),
  s =~ Star EmptyStr -> s = [].

它们的确非常相似，真的是：试图利用恒星的性质来告诉我们有关s的性质。反转似乎并没有带我到任何地方，因为“星”的定义只会解开更多的星。

虽然我最终找到了激进引理的答案并继续前进，但我想了解上述证明在哪里出了问题，将有助于我更好地使用这些类型。

Answer 1

SF中弱抽引引理的解的存根表明，需要归纳法来解决它。如您所指出的，如果仅使用反演，您将最终得到Star的更多假设，这不会使您走得太远。