在Coq中如何结合两个假设或调整子目标括号完成证明？

解决方法 #

你当前的目标本质是布尔与运算的幂等性，有三种常用策略可以快速完成证明：

• 方案1：直接调用Coq标准库中已有的布尔与运算幂等引理
  输入如下命令即可：

  now apply andb_idempotent.
  

  你的目标(X && X) = X和andb_idempotent的结论完全匹配，调用后会自动完成匹配和验证。
• 方案2：不依赖库引理，直接枚举布尔值的所有可能取值
  输入如下命令：

  destruct (matches_nil r1); destruct (matches_nil r2); simpl; reflexivity.
  

  布尔类型只有true和false两种取值，枚举所有组合后化简，两边等式会自动成立。
• 方案3：直接复用你已有的归纳假设推导
  你可以先把目标里的matches_nil r1 && matches_nil r2匹配为归纳假设的结构，直接复用假设逻辑：

  pattern (matches_nil r1 && matches_nil r2).
  apply IHr1.
  

  执行后也会直接完成证明。

内容的提问来源于stack exchange，提问作者KaisoHHH