I am trying to understand how to move from theorems that operate on computable functions to theorems that use inductively defined relations to represent computations. Consider this simple development below. Let's start with a standard definition of relations and their properties:
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).
Now I define three properties defined for a relation R and two functions F and 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).
I state a theorem that if R is reflexive and property A holds for R, F and G, then property B also holds R, F and 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.
Finally I state a theorem that if R is reflexive and transitive, and property A holds for R, F and G, then property C holds for R and 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.
Now I would like to move from representing F and G as computations to representing them as relations. So instead of saying F : X -> X I will now just say F : relation X and insist that F is deterministic:
Definition deterministic {X : Type} (F : relation X) :=
forall x y1 y2, F x y1 -> F x y2 -> y1 = y2.
I restate all three properties:
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.
Transformation pattern that I have followed is that expression R a (F b) is turned into F b x -> R a x, meaning "F b evaluates to some x and a is in relation R with that x". Now for the theorems. First one follows quite easily:
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.
But I am stuck with the second one. I start the proof like this:
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.
and end with a following goal to prove (some irrelevant hypotheses omitted):
H : propA' R F G Fdet Gdet
H0 : F a x
H1 : F b y
H2 : R a b
─────────────────────────────────────────────────────
G y b
The problem is that G is now an explicit premise of propA' and I have to prove it if I want to rely on propA'. But I have no assumptions about G in my current proof context and I don't see a way to finish the proof. Previously in aPropC, that used functions, G would only appear in conclusions of aPropA and aPropB. So the shape of the goal matched the shape of my hypotheses and known lemmas, allowing me to use them easily.
Where am I going wrong here? Is my transition from functions to relations incorrect? Is there any technique that I could use here?