给定一个使用“;”策略的有效Coq证明,是否存在一般公式可以将其转换为使用“.”替代“;”的有效等价证明?
许多Coq证明使用“;”或策略序列策略。作为初学者,我想观察每个步骤的执行情况,因此我想用“.”替换“;”,但令我惊讶的是,这可能会破坏证明。
关于“;”的文档很少,我没有在任何地方找到关于“.”的明确讨论。我看到了一篇paper,其中说“t1; t2”的非正式含义是
应用“t2”到当前证明上下文中由“t1”执行产生的每个子目标,
我想知道“.”是否只对当前子目标起作用,这解释了不同的行为方式?但我特别想知道是否有一般解决方案来修复由于将“.”替换为“;”而导致的破坏。
许多Coq证明使用“;”或策略序列策略。作为初学者,我想观察每个步骤的执行情况,因此我想用“.”替换“;”,但令我惊讶的是,这可能会破坏证明。
关于“;”的文档很少,我没有在任何地方找到关于“.”的明确讨论。我看到了一篇paper,其中说“t1; t2”的非正式含义是
应用“t2”到当前证明上下文中由“t1”执行产生的每个子目标,
我想知道“.”是否只对当前子目标起作用,这解释了不同的行为方式?但我特别想知道是否有一般解决方案来修复由于将“.”替换为“;”而导致的破坏。
tac1
只生成一个目标,如果有多种方法可以实现它(一个重要的例子是constructor
),那么tac1.tac2
将承诺第一个成功并在其上运行tac2
。tac1; tac2
将使tac1
尝试一件事情,然后在此之后尝试tac2
,如果失败,则尝试以另一种方式尝试tac1
,然后在此之后尝试tac2
,如果失败,则尝试以另一种方式尝试tac1
,依此类推。 - HTNW