4

編集:私はおそらく、現在ここで問題をどのように回避しているかを言うべきです。順列の等価性を示すための原則を定義し、

Lemma permInd : ∀ (U : Type) (A : Ensemble U) (φ ψ : Perm A),
  φ ↓ = ψ ↓ → φ ↑ = ψ ↑ → φ = ψ

次に、以下で私に問題を引き起こしている証明コンテキストで補題を適用し、イータ等価項が等しいことを示しています。したがって、用語がレコード内にネストされている場合、問題は eta-equivalence を示しているようです。でも私はレコードを扱うのが苦手なので、何かが欠けているかもしれません。

オリジナル：

レコード フィールドにネストされた eta に相当する用語の等価性を証明するのに問題があります。参考までに、eta-reduction は再帰性によって独立して証明できます。

Lemma etaEquivalence : ∀ (A B : Type) (f : A → B), (λ x : A, f x) = f.
Proof. reflexivity. Qed.

私の現在の証明コンテキストでは、2 つのレコードがあり、それらの等価性を証明する必要があります。完全に破壊され展開されると、証明コンテキストと現在のサブゴールは次のようになります。

U : Type
A : Ensemble U
perm0 : U → U
pinv0 : U → U
permutes0 : IsPerm A perm0 pinv0
============================
 {|
 perm := λ x : U, perm0 x;
 pinv := λ x : U, pinv0 x;
 permutes := permutationComp permutes0 (permutationId A) |} =
 {| perm := perm0; pinv := pinv0; permutes := permutes0 |}

確立されなければならない平等は、

perm0 = λ x : U, perm0 x
pinv0 = λ x : U, pinv0 x

これらの等式は再帰性によって確立できるため、何が問題なのかわかりません。ただし、置換しようとすると適切なサブゴールが生成されますが、レコード内の用語は置換されないため、何かがλ x : U, perm0 xおかしいperm0と思われます。さらに、eqa_reduction を使用して書き直すと、抽象化に関するエラーが発生し、不適切な型の項やネストされた従属引数が発生します。

コンテキストを可能な限り単純化して、以下に貼り付けました。文体の問題と、私がまだ初心者であるという事実を除けば、現在の開発に問題は見られません。

Require Import Unicode.Utf8 Utf8_core Ensembles Setoid.

Class IsPerm {U : Type} (A : Ensemble U) (φ ψ :  U → U) : Prop := {
  pinvLeft    : ∀ x : U, ψ (φ x) = x;
  pinvRight   : ∀ x : U, φ (ψ x) = x;
  closedPerm  : ∀ x : U, In U A x → In U A (φ x);
  closedPinv  : ∀ x : U, In U A x → In U A (ψ x)
}.

Record Perm {U : Type} (A : Ensemble U) : Type := {
  perm : U → U;
  pinv : U → U;
  permutes :> IsPerm A perm pinv
}.

Notation "f ∘ g"  := (λ x, f (g x)) (at level 45).
Notation "P ↓"    := (@perm _ _ P)  (at level 2, no associativity).
Notation "P ↑"    := (@pinv _ _ P)  (at level 2, no associativity).

Instance permutationComp
  {U : Type} {A : Ensemble U} {f g k h : U → U}
    (P : IsPerm A f k) (Q : IsPerm A g h) : IsPerm A (f ∘ g) (h ∘ k).
Proof.
  constructor; intros.
  setoid_rewrite pinvLeft. apply pinvLeft.
  setoid_rewrite pinvRight. apply pinvRight.
  apply closedPerm. apply closedPerm. auto.
  apply closedPinv. apply closedPinv. auto.
Defined.

Instance permutationId
  {U : Type} (A : Ensemble U) :
    IsPerm A (λ x : U, x) (λ x : U, x).
Proof. constructor; intros; auto. Defined.

Definition permComp
  {U : Type} (A : Ensemble U)
    (φ : Perm A) (ψ : Perm A) : Perm A :=
  Build_Perm U A (φ↓ ∘ ψ↓) (ψ↑ ∘ φ↑)
    (permutationComp (permutes A φ) (permutes A ψ)).

Definition permId {U : Type} (A : Ensemble U) : Perm A :=
  Build_Perm U A (λ x : U, x) (λ x : U, x) (permutationId A).

(* problems occur after the application of the tactic simpl, below: *)

Lemma permCompRightIdentity :
  ∀ {U : Type} (A : Ensemble U) (φ : Perm A), permComp A φ (permId A) = φ.
Proof. intros. unfold permComp. simpl. admit. Qed.

最後に、Coq で私を助けてくれて辛抱強く待ってくれた皆さんに感謝します。

4

1 に答える 1

6

証明無関連性は Coq に組み込まれていません。証明無関連公理を仮定すれば、あなたが望むものを簡単に証明することができます:

Require Import ProofIrrelevance.

Lemma permCompRightIdentity :
  ∀ {U : Type} (A : Ensemble U) (φ : Perm A), permComp A φ (permId A) = φ.
Proof.
  intros. unfold permComp. simpl.
  destruct φ.
  f_equal.
  apply proof_irrelevance.
Qed.
于 2012-01-17T09:13:40.097 に答える