时间戳

首页 > 解决方案 > 在没有完全相同假设的情况下证明两个函数是等价的

coq - 在没有完全相同假设的情况下证明两个函数是等价的

问题描述

第一个问题帖！对于任何不适当的格式，请提前道歉。

试图证明两个版本的函数是等价的，到达这一步后我无法继续。我该如何解决这个问题？

1 subgoal
a' : nat
Ha' : forall b : nat, version1 a' b 0 = version2 a' b 0
b' : nat
Hb' : version1 a' b' b' = version2 a' b' b'
______________________________________(1/1)
version1 a' (S b') (S b') = version2 a' (S b') (S b')

标签： coqcoq-tactic

解决方案

version1正如目前所说，这个目标是不完整的，因为我们不知道什么version2是什么。人们可能会认为该陈述对于 和 的任何选择都应该是正确的version1，version2但是对于这些函数的某些选择，相反的情况是可以证明的：

Definition v1 (a b c : nat) :=
    Nat.leb c 1.

Definition v2 (a b c : nat) :=
    Nat.ltb c 1.

Lemma counterexample :
  ~ (forall (version1 version2 : nat -> nat -> nat -> bool),
     forall a' : nat,
     forall Ha' : (forall b : nat, version1 a' b 0 = version2 a' b 0), 
     forall b' : nat,
     forall Hb': (version1 a' b' b' = version2 a' b' b'),
      version1 a' (S b') (S b') = version2 a' (S b') (S  b')).
Proof.
intros abs.
assert (v1 0 1 1 = v2 0 1 1).
  apply abs.
    auto.
  auto.
discriminate.
Qed.

推荐阅读