如何使用函数定义重写目标？

Question

我有这个代码：

Module Type tDecType.
  Parameter T: Type.
  Parameter is_eq: T -> T -> bool.
  Axiom is_eq_reflexivity: forall x, is_eq x x = true.
  Axiom is_eq_equality: forall x y, is_eq x y = true -> x = y.
End tDecType.

Module NAT <: tDecType.
  Definition T := nat.
  Definition is_eq (x: T) y := x = y.

  Lemma is_eq_reflexivity:
    forall x,
    is_eq x x = True.
  Proof.
    intro x.
    ?

并且我想使用 is_eq 定义重写当前的子目标。我该怎么做？

Answer 1

我认为问题出在您对 is_eq 的定义上。请注意，在您的模块声明中，您已为 is_eq

指定了以下类型

is_eq : T -> T -> bool

但是在模块NAT中你使用了命题等式，它的类型是：

= : forall T, T -> T -> Prop

我已经通过设置另一个版本的 is_eq 修复了你的代码，基于自然数的标准库布尔相等性，并为自反性做了一个简单的归纳证明。

 ...  same code as before.
 Require Import Nat.

 Definition is_eq (x: T) y := eqb x y.

 Lemma is_eq_reflexivity : forall x, is_eq x x = true.
 Proof.
   induction x ; simpl ; auto.
 Qed.

如何使用函数定义重写目标？

How to rewrite a goal using function definition?

coq

coq-tactic