从可计算函数移动到归纳关系

我想了解如何从运算可计算函数的定理转移到使用归纳定义关系来表示计算的定理。考虑下面这个简单的开发。让我们先从关系及其属性的标准定义：从可计算函数移动到归纳关系

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三个属性：

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。

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.

最后，我声明一个定理，如果R是自反和传递，以及财产一种用于R，F和G成立，则性质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.

我重申所有三个属性：

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.

但是我坚持第二个。我开始证明是这样的：

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的结论中。所以目标的形状与我的假设和已知的引理的形状相匹配，使我能够轻松地使用它们。

我在哪里错了？我从功能到关系的转换是否不正确？有什么技术可以在这里使用吗？

来源

2017-10-06 Jan Stolarek

Coq中的函数不仅仅是确定性关系，而且还有总计个。所以，你可能想在抛出：

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

然后被functional的概念是deterministic和total连词：

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

或者，您可以添加假设你有关的领域引理你的关系所代表的部分功能。

来源

2017-10-06 14:22:18 gallais

我想使用关系的原因是我的功能不是全部。 –

从可计算函数移动到归纳关系

回答

相关问题