如何解决复杂功能平等
我想证明以下引理:
Require Import CoLoR.Util.Vector.VecUtil.
Require Import Coq.Vectors.Vector.
From mathcomp Require Import ssreflect.
Definition Equiv {A n m l}(I:t A n -> t A l)(J:t A m -> t A l)(eq:n=m):Prop:=
forall (a : t A n),I a = J (Vcast a eq) .
Lemma Vcast_func (A:Type):
forall (n m l:nat)(v:t A n)(eq:n=m)
(func1:t A n -> t A l)(func2:t A m -> t A l)
(foo: forall {n l:nat},(t A n -> t A l) -> t A n -> t A n),Equiv func1 func2 eq -> Vcast (foo func1 v) eq = foo func2 (Vcast v eq).
Proof.
induction n;rewrite /Equiv. destruct m => //.
intros.
rewrite !Vcast_refl.
Abort.
我认为Vcast (foo func1 v) eq = foo func2 (Vcast v eq).
之所以成立是因为Equiv
不管是什么foo。但是我不知道如何证明。
有什么解决办法吗?
解决方法
尽管直观,但由于缺少功能可扩展性公理,因此无法用简单的Coq证明该语句:
forall T S (f g : T -> S),(forall x,f x = g x) ->
f = g.
幸运的是,该公理相对无害,并且已经在标准库中提供。这是我们的用法:
Require Import CoLoR.Util.Vector.VecUtil.
Require Import Coq.Vectors.Vector.
From mathcomp Require Import ssreflect.
Require Import Coq.Logic.FunctionalExtensionality.
Definition Equiv {A n m l}(I:t A n -> t A l)(J:t A m -> t A l)(eq:n=m):Prop:=
forall (a : t A n),I a = J (Vcast a eq) .
Lemma Vcast_func (A:Type):
forall (n m l:nat)(v:t A n)(eq:n=m)
(func1:t A n -> t A l)(func2:t A m -> t A l)
(foo: forall {n l:nat},(t A n -> t A l) -> t A n -> t A n),Equiv func1 func2 eq -> Vcast (foo func1 v) eq = foo func2 (Vcast v eq).
Proof.
move=> n m l v e.
case: m / e => /= func1 func2 foo e.
suff -> : func1 = func2 by [].
apply: functional_extensionality=> {}v.
exact: e.
Qed.
请注意对等式证明n = m
的案例分析。这使得强制转换消失,目标降低到foo func1 v = foo func2 v
。在这一点上,只需论证我们使用扩展性的func1 = func2
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。