計算可能関数で動作する定理から、計算を表す誘導的に定義された関係を使用する定理に移行する方法を理解しようとしています。以下にこの簡単な開発を考えてみましょう。関係とそのプロパティの標準的な定義で始まるのをしてみましょう：計算可能関数から誘導関係への移動
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).
は今、私は関係Rとの二つの機能FとG用に定義された3つのプロパティを定義します。
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).
私はR場合は、その定理を述べます反射性であり、プロパティAがR,FおよびGの場合、プロパティBもR,FおよびGを保持する。 Rは反射的推移であり、プロパティAはR、Fと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.
最後に、私は定理を述べ、その後、プロパティCはRと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.
今私は関係として、それらを表現するための計算などFとGを表すから移動したいと思います。だからではなく、F : X -> Xを言って、私は今ちょうどF : relation Xを言うとFが決定的であることを主張します：
Definition deterministic {X : Type} (F : relation X) :=
forall x y1 y2, F x y1 -> F x y2 -> y1 = y2.
私はすべての3つのプロパティ修正再表示：私は続いている
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.
変換パターンを表現R a (F b)が入っていることですF b x -> R a xに「F b」と入力して、xと入力し、aはRとなり、その値はxとなります。今定理について。最初は非常に簡単に従います：
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.
しかし、私は第2のものに固執しています。私はこのような証拠を開始：
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.
をし、証明するために、次の目標は（いくつかの無関係な仮説は省略）で終わる：
H : propA' R F G Fdet Gdet
H0 : F a x
H1 : F b y
H2 : R a b
─────────────────────────────────────────────────────
G y b
問題はGが今propA'の明示的な前提であり、私ということです私がpropA'に頼りにしたいと思ったらそれを証明しなければなりません。しかし、私は現在の証明の文脈でGについての仮定を持っておらず、証明を終わらせる方法は見当たりません。以前のaPropCでは、その使用関数Gは、aPropAとaPropBの結論にのみ現れました。だから、目標の形は私の仮説や既知の補題の形に合っていて、簡単に使うことができました。
ここで私は間違っていますか？関数から関係への移行が間違っていますか？私がここで使うことができる技術はありますか？
私が関係を使用したい理由は、私の関数が合計ではないということです。 –