编辑:我应该说我目前是如何解决这个问题的。我定义了一个显示排列相等的原则,
Lemma permInd : ∀ (U : Type) (A : Ensemble U) (φ ψ : Perm A),
φ ↓ = ψ ↓ → φ ↑ = ψ ↑ → φ = ψ
然后在下面给我带来麻烦的证明上下文中应用引理,并表明 eta 等效项是相等的。因此,当术语嵌套在记录中时,问题似乎是显示 eta 等价。但是我不擅长处理记录,所以我可能会遗漏一些东西。
原文:
我无法证明嵌套在记录字段中的 eta 等效项的相等性。作为引用,eta-reduction 可通过自反性独立证明:
Lemma etaEquivalence : ∀ (A B : Type) (f : A → B), (λ x : A, f x) = f.
Proof. reflexivity. Qed.
在我当前的证明上下文中,我必须证明两个记录的相等性。完全破坏和展开,证明上下文和当前子目标如下所示:
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 方面帮助我并耐心等待。
最佳答案
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.
关于functional-programming - 不是由 coq 中的自反性建立的 eta 等价项的相等性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/8227328/