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?
La raison pour laquelle je veux utiliser les relations est que mes fonctions ne seront pas totales. –