2017-10-06 6 views
2

J'essaie de comprendre comment passer de théor'emes fonctionnant sur des fonctions calculables'a des théor'emes utilisant des relations inductives pour représenter des calculs. Considérez ce développement simple ci-dessous. Commençons par une définition standard des relations et de leurs propriétés:Passage de fonctions calculables à des relations inductives

Definition relation (X : Type) := X -> X -> Prop. 

Definition reflexive {X : Type} (R : relation X) := 
    forall a, R a a. 

Definition transitive {X : Type} (R : relation X) := 
    forall a b c : X, (R a b) -> (R b c) -> (R a c). 

Maintenant, je définir trois propriétés définies pour une relation R et deux fonctions F et G:

Definition propA {X : Type} (R : relation X) (F G : X -> X) := 
    forall p q, R (F p) q <-> R p (G q). 

Definition propB {X : Type} (R : relation X) (F G : X -> X) := 
    forall x, R x (G (F x)). 

Definition propC {X : Type} (R : relation X) (F : X -> X) := 
    forall a b : X, R a b -> R (F a) (F b). 

je déclare un théorème que si R est réflexif et la propriété A est valable pour R, F et G, alors la propriété B est également R, F et G.

Lemma aPropB {X : Type} {R : relation X} {F G : X -> X} (Rrefl : reflexive R) 
     (H : propA R F G) : 
    propB R F G. 
Proof. 
    unfold propB in *. 
    intros. 
    apply H. apply Rrefl. 
Qed. 

Enfin je déclare un théorème que si R est réflexive et transitive, et la propriété A détient pour R, F et G, alors la propriété C détient pour R et F.

Lemma aPropC {X : Type} {R : relation X} {F G : X -> X} 
     (Rrefl : reflexive R) (Rtrans : transitive R) (H : propA R F G) : 
    propC R F. 
Proof. 
    unfold propC in *. 
    intros. 
    apply H. 
    eapply Rtrans. eassumption. 
    apply aPropB; assumption. 
Qed. 

Maintenant, je voudrais passer de représenter F et G que les calculs pour les représenter comme des relations. Ainsi, au lieu de dire F : X -> X Je vais maintenant simplement dire F : relation X et insister pour que F est déterministe:

Definition deterministic {X : Type} (F : relation X) := 
    forall x y1 y2, F x y1 -> F x y2 -> y1 = y2. 

Je retraiter les trois propriétés:

Definition propA' {X : Type} (R : relation X) (F G : relation X) 
      (Fdet : deterministic F) (Gdet : deterministic G) := 
    forall p q x y, F p x -> G q y -> R x q <-> R p y. 

Definition propB' {X : Type} (R : relation X) (F G : relation X) 
      (Fdet : deterministic F) (Gdet : deterministic G) := 
    forall x y z, F x y -> G y z -> R x z. 

Definition propC' {X : Type} (R : relation X) (F : relation X) 
      (Fdet : deterministic F) := 
    forall a b x y : X, F a x -> F b y -> R a b -> R x y. 

modèle de transformation que j'ai suivi est que l'expression R a (F b) est activée en F b x -> R a x, ce qui signifie "F b évalue à certains x et a est en relation R avec ce x". Maintenant pour les théorèmes. Le premier suit assez facilement:

Lemma aPropB' {X : Type} {R : relation X} {Rrefl : reflexive R} 
     {F G : relation X} {Fdet : deterministic F} {Gdet : deterministic G} 
     (H : propA' R F G Fdet Gdet) : 
    propB' R F G Fdet Gdet. 
Proof. 
    unfold propA', propB' in *. 
    intros. 
    specialize (H x y y z). 
    apply H; auto. 
Qed. 

Mais je suis coincé avec le second. Je commence la preuve comme ceci:

Lemma aPropC' {X : Type} {R : relation X} {F G : relation X} 
     {Fdet : deterministic F} {Gdet : deterministic G} 
     (Rrefl : reflexive R) (Rtrans : transitive R) 
     (H : propA' R F G Fdet Gdet) : 
    propC' R F Fdet. 
Proof. 
    unfold propC' in *. 
    intros. 
    eapply H; try eassumption. 

et se terminent par un but suivant pour prouver (certaines hypothèses non pertinentes omis):

H : propA' R F G Fdet Gdet 
H0 : F a x 
H1 : F b y 
H2 : R a b 
───────────────────────────────────────────────────── 
G y b 

Le problème est que G est maintenant une prémisse explicite de propA' et je dois le prouver si je veux compter sur propA'. Mais je n'ai aucune supposition sur G dans mon contexte actuel de preuve et je ne vois pas un moyen de terminer la preuve. Précédemment dans aPropC, que les fonctions utilisées, G n'apparaîtraient que dans les conclusions de aPropA et aPropB. La forme du but correspondait donc à la forme de mes hypothèses et des lemmes connus, ce qui me permettait de les utiliser facilement.

Où est-ce que je me trompe ici? Ma transition des fonctions aux relations est-elle incorrecte? Y a-t-il une technique que je pourrais utiliser ici?

Répondre

2

Les fonctions dans Coq ne sont pas seulement des relations déterministes, mais aussi total. Donc, vous voudrez peut-être jeter:

Definition total {X : Type} (R : relation X) : Prop := 
    forall x, exists y, R x y. 

Et puis l'idée d'être functional est la conjonction de deterministic et total:

Definition functional {X : Type} (R : relation X) : Prop := 
    deterministic R /\ total R. 

Vous pouvez également ajouter des hypothèses à vos lemmes concernant les domaines de les fonctions partielles que vos relations représentent.

+0

La raison pour laquelle je veux utiliser les relations est que mes fonctions ne seront pas totales. –