Coqで外延性の公理

外延性の公理から集合の等号に対して同値関係を示します。(Coq で)

外延性の公理とは

A, B を任意の集合とするとき、もし任意の集合 X について「X が A の要素であるならば、そのときに限り X は B の要素である」が成り立つならば、A と B は等しい。

外延性の公理から引用。

∈ と=を定義する

Section Axiom_Of_Extensionality.

  Variable Var : Type.
  Variable In : Var -> Var -> Prop.
  Variable Eq : Var -> Var -> Prop.

  (* ここにコードを書く *)

End Axiom_Of_Extensionality.

∈ を In、=を Eq とした。

同値関係とは

1. 反射律: a = a
2. 対称律: a = b ⇒ b = a
3. 推移律: a = b ∧ b = c ⇒ a = c

同値関係を参考。

証明する

まず、外延公理を入れる。

Axiom Extensionality: forall x y, Eq x y <-> forall z : Var, (In z x <-> In z y).

反射律

Lemma Equal_Reflexive : forall x : Var, Eq x x.
Proof.
  intros.
  specialize (Extensionality x x).
  intros.
  destruct H.
  apply H0.
  intros.
  split.
  intros.
  trivial.
  intros.
  trivial.
Qed.

• specialize.から intros.のパターンで公理を仮定における。
• specialize.から intros.のパターンって Tactic ないのかな。

対称律

Lemma Equal_Symmetric : forall x y : Var, Eq x y -> Eq y x.
Proof.
  intros.
  specialize (Extensionality y x).
  specialize (Extensionality x y).
  intros.
  destruct H0.
  destruct H1.
  apply H3.
  intros.
  specialize (H0 H).
  specialize (H0 z).
  destruct H0.
  split.
  trivial.
  trivial.
Qed.

• <->が対称律を満たすことを示すのと本質的にはあんまり変わらない。
• 先に<->の対称律を示したら置き換えて楽に示せたら良いのに。

推移律

Lemma Equal_Transitive : forall x y z : Var, Eq x y /\ Eq y z -> Eq x z.
Proof.
  intros.
  specialize (Extensionality x y).
  specialize (Extensionality y x).
  specialize (Extensionality y z).
  specialize (Extensionality z y).
  specialize (Extensionality z x).
  specialize (Extensionality x z).
  intros.
  destruct H0.
  destruct H1.
  destruct H2.
  destruct H3.
  destruct H4.
  destruct H5.
  destruct H.
  apply H6.
  intros.
  split.
  intros.
  specialize (H3 H12).
  specialize (H3 z0).
  destruct H3.
  apply H3.
  specialize (H5 H).
  specialize (H5 z0).
  destruct H5.
  apply H5.
  trivial.
  intros.
  specialize (H5 H).
  specialize (H5 z0).
  destruct H5.
  apply H14.
  specialize (H3 H12).
  specialize (H3 z0).
  destruct H3.
  apply H15.
  trivial.
Qed.

• 同じ公理を 6 回 specialize.しないといけないもんなのかな。
• 長すぎてもう見返したくない。

SSReflect

外延性の公理から集合の等号に対して同値関係を示します。(SSReflect で)

From mathcomp
     Require Import ssreflect.

Section Axiom_Of_Extensionality.

  Variable Var : Type.
  Variable In : Var -> Var -> Prop.
  Variable Eq : Var -> Var -> Prop.

  Notation "a ∈ A" := (In A a) (at level 55,no associativity).
  Notation "A ≡ B" := (Eq A B) (at level 57, no associativity).

  Axiom Extensionality: forall x y : Var, x ≡ y <-> forall z : Var, (z ∈ x <-> z ∈ y).

  Lemma Equal_Reflexive : forall x : Var, x ≡ x.
  Proof.
    move => x.
    elim : (Extensionality x x) => H1 H2.
    by apply : H2.
  Qed.

  Lemma Equal_Symmetric : forall x y : Var, x ≡ y -> y ≡ x.
  Proof.
    move => x y.
    elim : (Extensionality x y) => H1 H2.
    elim : (Extensionality y x) => H3 H4 XeqY.
    apply : H4 => z.
    apply iff_sym.
    by apply : (H1 XeqY).
  Qed.

  Lemma Equal_Transitive : forall x y z : Var, x ≡ y /\ y ≡ z -> x ≡ z.
  Proof.
    move => x y z.
    elim : (Extensionality x y) => H1 H2.
    elim : (Extensionality y z) => H3 H4.
    elim : (Extensionality x z) => H5 H6.
    case => XeqY YeqZ.
    apply : H6 => z0.
    move : (H1 XeqY z0) (H3 YeqZ z0).
    by apply iff_trans.
  Qed.

End Axiom_Of_Extensionality.

• すごく短くなった

感想

• SSReflect を使おう!