Wie wird ein Ziel mithilfe der Funktionsdefinition neu geschrieben?

Question

Ich habe diesen 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. 
    ? 

Und ich möchte den aktuellen subgoal neu zu schreiben, indem die is_eq Definition verwenden. Wie kann ich das machen ?

Answer 1

Ich glaube, dass das Problem ist Ihre Definition von is_eq. Beachten Sie, dass in Ihrem Modul Erklärung Sie den folgenden Typ angegeben haben, für is_eq

is_eq : T -> T -> bool 

aber in Modul NAT verwendet man die propositionaler Gleichheit, deren Typ:

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

ich Ihren Code festgelegt haben, indem eine andere Version von is_eq, basierend auf der Standard-Bibliothek boolesche Gleichheit für natürliche Zahlen und einen einfachen induktiven Beweis für Reflexivität zu tun.

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