coq - How to rewrite a goal using function definition?

Question

I have this code:

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.
    ?

And I want to rewrite the current subgoal by using the is_eq definition. How can I do this ?

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.