英文:
Morphism signature for dependently-typed vectors in coq
问题
I want to be able to rewrite terms inside the predicate P given to Coq.Vectors.Vector.Forall.
The first attempt does not work due to the missing quantification over n.
From Coq Require Import Vector Morphisms Setoid.
Parameter D : Type.
Parameter R : relation D.
Fail Add Parametric Morphism : (@Forall D)
with signature (R ==> iff) ==> Forall2 R ==> iff
as morph1.
(* The term "Forall" has type "(D -> Prop) -> forall n : nat, t D n -> Prop"
while it is expected to have type "(D -> Prop) -> t D ?n -> Prop". *)
I managed to prove the following, with a fixed vector size, but it is useless in practice.
Add Parametric Morphism n : (fun P => @Vector.Forall D P n)
with signature (R ==> iff) ==> Forall2 R ==> iff
as morph2.
Proof.
intros P Q Hpq v1 v2 Hr.
rewrite 2 Forall_nth_order.
rewrite Forall2_nth_order in Hr.
split; intros Hf i Hi; eapply Hpq; eauto.
Unshelve.
all: assumption.
Qed.
What could be a correct signature for morph1?
英文:
I want to be able to rewrite terms inside the predicate P given to Coq.Vectors.Vector.Forall.
The first attempt does not work due to the missing quantification over n.
From Coq Require Import Vector Morphisms Setoid.
Parameter D : Type.
Parameter R : relation D.
Fail Add Parametric Morphism : (@Forall D)
with signature (R ==> iff) ==> Forall2 R ==> iff
as morph1.
(* The term "Forall" has type "(D -> Prop) -> forall n : nat, t D n -> Prop"
while it is expected to have type "(D -> Prop) -> t D ?n -> Prop". *)
I managed to prove the following, with a fixed vector size, but it is useless in practice.
Add Parametric Morphism n : (fun P => @Vector.Forall D P n)
with signature (R ==> iff) ==> Forall2 R ==> iff
as morph2.
Proof.
intros P Q Hpq v1 v2 Hr.
rewrite 2 Forall_nth_order.
rewrite Forall2_nth_order in Hr.
split; intros Hf i Hi; eapply Hpq; eauto.
Unshelve.
all: assumption.
Qed.
What could be a correct signature for morph1?
答案1
得分: 0
这似乎是我在寻找的实例：
Add Parametric Morphism : (@Forall D)
with signature (R ==> iff) ==> forall_relation (fun _ => Forall2 R ==> iff)
as morph1.
然而，它并不太实际，因为在执行重写之前需要在术语中进行显式的 eta 扩展。
英文:
This seems seems to be the instance I was looking for:
Add Parametric Morphism : (@Forall D)
with signature (R ==> iff) ==> forall_relation (fun _ => Forall2 R ==> iff)
as morph1.
It is however not very practical to use, as it requires an explicit eta-expansion in the term before doing the rewrite.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论