coq - 如何使用具有匹配模式的定理

Question

基本上，我有一个函数，以及关于这个函数的一些属性的定理。

该函数具有以下签名：

Fixpoint compute_solution (s : list nat) : (option list nat) := 
...=> None
...=> Some l

定理是：

Theorem solution_is_correct:
  forall (s : list nat), length s = 9 * 9 ->
       match compute_solution s with
         None => forall s1, length s1 = 9 *9  -> ~ nice_property s1
       | Some s1 => nice_property s1
       end.

现在，当我尝试证明一个附加定理时，我最终会遇到以下情况：

s: list nat
Hs: length s = 9 * 9
prem: list nat
sol: compute_solution s = Some prem
...
================================
nice_property prem

如何利用 solution_is_correct 来证明目标？

感谢您的帮助。

标签： coqtheorem-proving

Answer 1

这应该工作

pose proof (solution_is_correct s Hs) as Tmp.
rewrite sol in Tmp.

但我宁愿修改定理以使其更有用，例如

thm1 : forall s l, ... -> compute_solution s = Some l -> nice_property l
thm2 : forall s, ... -> compute_solution s = None -> ...