Coq中的区分目标

问题描述 投票:0回答:2

我对nat号有两个条件:

H:  a < b
H1: b < a

如何区分目标?是否存在的任何策略?

coq coq-tactic coqide
2个回答
1
投票

使用lia

From Coq Require Import Lia.

Goal forall a b, a < b -> b < a -> False.
  lia.
Qed.

您可以了解有关lia和其他用于算术here的决策过程的更多信息。


0
投票

作为参考,在这种情况下进行手动校对不是那么困难:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo a b (a_lt_b : a < b) : b < a -> False.
Proof. by rewrite ltnNge (ltnW a_lt_b). Qed.
© www.soinside.com 2019 - 2024. All rights reserved.