如何解决矛盾陈述的使用
我有两个自然数 a & b。这些数字之间的关系以假设的形式存在(H1 H2 H3)。我想从这些假设中提取矛盾,在此基础上我可以关闭任何子目标。
H1: a<=b
H2: a>=b
H3: a=b.
解决方法
您的假设并不矛盾:a=b
是一个显而易见的解决方案。假设您的假设自相矛盾,lia
策略可以完成这项工作。它可以解决 Z 和 nat 中线性整数算法的任何目标。如果您的假设与线性整数算术相矛盾,lia
将解决任何目标,如:
Require Import Lia.
Goal forall a b : nat,a<=b -> a>=b -> a<>b -> False.
lia.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。