함수 정의를 사용하여 목표를 다시 작성하는 방법은 무엇입니까?

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 정의를 사용하여 현재 subgoal를 다시 작성합니다. 어떻게해야합니까?

Answer 1

나는이 문제가 is_eq의 정의라고 생각합니다. 내가 설정하여 코드를 해결 한

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

: 모듈 선언에, 당신은 is_eq

is_eq : T -> T -> bool 

을 위해 다음과 같은 유형을 지정했지만 모듈 NAT 당신이 유형이있는 명제 평등을 사용하는 것을 알 다른 버전의 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.