用更具体的表达式重写假设

Posted 2023-03-28

【中文标题】用更具体的表达式重写假设

【英文标题】：Rewriting hypothesis with a more concrete expression

【发布时间】：2017-04-10 21:08:09

【问题描述】：

假设这些是我目前的前提和目标：

  IHl' : forall l' : list A, In a l'' \/ In a l' -> In a (l'' ++ l')
  l' : list A
  ============================
   ....

现在，我想让假设变成这样：

  IHl' : In a l'' \/ In a l' -> In a (l'' ++ l')
  l' : list A
  ============================
   ....

所以，基本上我用l' 实例化IHl'。有什么策略可以做到这一点吗？应该重写甚至引入一个新的专业假设。

【问题讨论】：

这类问题在这里时不时出现。这是按时间顺序排列的（可能不完整）问题列表，可能会对您有所帮助：1、2、3、4、5、6、7、8 .

@AntonTrunov BTW 这些问题中的一些不应该被标记为其他问题的重复吗？

@Zimmi48 我认为你是对的。我只是想增加连接性（它可能会导致更好的搜索结果）。随意标记您认为合适的问题:)

Best way to perform universal instantiation in Coq的可能重复

【参考方案1】：

只是为将来的参考留下最短的答案：specialize IHl' with l'。

无论如何，我强烈建议你看看@Anton 的评论。