1

我正在尝试使用 à la System F 类型的 lambda 演算编码 Coq 逻辑连接词。这是我编写的一堆代码（我认为是标准的东西）

Definition True := forall X: Prop, X -> X.

Lemma I: True.
Proof.
  unfold True. intros. apply H.
Qed.

Section s.
Variables A B: Prop.


(* conjunction *)

Definition and := forall X: Prop, (A -> B -> X) -> X.
Infix "/\" := and.

Lemma and_intro: A -> B -> A/\B.
Proof.
  intros HA HB. split.
  apply HA.
  apply HB.
Qed.

Lemma and_elim_l: A/\B -> A.
Proof.
  intros H. destruct H as [HA HB]. apply HA.
Qed.

Lemma and_elim_r: A/\B -> B.
Proof.
  intros H. destruct H as [HA HB]. apply HB.
Qed.



(* disjunction *)

Definition or := forall X:Prop, (A -> X) -> (B -> X) -> X.
Infix "\/" := or.

Lemma or_intro_l: A -> A\/B.
  intros HA. left. apply HA.
Qed.

Lemma or_elim: forall C:Prop, A \/ B -> (A -> C) -> (B -> C) -> C.
Proof.
  intros C HOR HAC HBC. destruct HOR.
    apply (HAC H).
    apply (HBC H).
Qed.


(* falsity *)

Definition False := forall Y:Prop, Y.

Lemma false_elim: False -> A.
Proof.
  unfold False. intros. apply (H A).
Qed.

End s.

基本上，我写下了合取、析取、真假的排除和引入法则。我不确定是否正确地做事，但我认为事情应该这样工作。现在我想定义存在量化，但我不知道如何进行。有人有建议吗？

4

1 回答 1

2

存在量化只是合取的概括，其中对的第二个分量的类型取决于第一个分量的值。当没有依赖关系时，它们是等价的：

Goal forall P1 P2 : Prop, (exists _ : P1, P2) <-> P1 /\ P2.
Proof. split. intros [H1 H2]. eauto. intros [H1 H2]. eauto. Qed.

Coq'Art从第 130 页开始有一个关于不可解释性的部分。

Definition ex (T1 : Type) (P1 : T1 -> Prop) : Prop :=
  forall P2 : Prop, (forall x1, P1 x1 -> P2) -> P2.

Notation "'exists' x1 .. x2 , P1" :=
  (ex (fun x1 => .. (ex (fun x2 => P1)) ..))
  (at level 200, x1 binder, right associativity,
  format "'[' 'exists' '/ ' x1 .. x2 , '/ ' P1 ']'") : type_scope.

含意定义的问题（除非我弄错了）是没有依赖消除。有可能证明

forall (A : Type) (P : A -> Prop) (Q : Prop),
  (forall x : A, P x -> Q) -> (exists x, P x) -> Q,

但不是

 forall (A : Type) (P : A -> Prop) (Q : (exists x, P x) -> Prop),
   (forall (x : A) (H : P x), Q (ex_intro P x H)) ->
   forall H : exists x, P x, Q H
于 2013-09-30T10:55:42.773 回答