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

I believe that the problem is your definition of is_eq. Notice that in your module declaration, you have specified the following type for is_eq

is_eq : T -> T -> bool

but in module NAT you used the propositional equality, whose type is:

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

I have fixed your code by setting another version of is_eq, based on standard library boolean equality for natural numbers, and doing a simple inductive proof for reflexivity.

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