如何解决等价于复杂类型的复杂函数
我想证明下引理。
Require Import CoLoR.Util.Vector.VecUtil.
Require Import Coq.Vectors.Vector.
From mathcomp Require Import ssreflect.
Lemma Vcast_func' (A:Type):
forall (n m l:nat)(v:t A (n+0))(eq:n+0=m+0)
(func1:t A (n+0) -> t A l)(func2:t A (m+0) -> t A l)
(foo: forall {n l:nat},(t A (n+0) -> t A l) -> t A (n+0) -> t A (n+0)),Equiv func1 func2 eq -> Vcast (foo func1 v) eq = foo func2 (Vcast v eq).
Proof.
move=> n m l v eq.
Abort.
我要使用根据Equality on complex functions的解决方案。
但是,我无法进行case: m / eq
,因为m
不能照原样推断m+0
。另外,由于假设中使用了n+0=m+0
,所以我无法将n=m
重写为n+0=m+0
。
有什么解决办法吗?
解决方法
假设eq
无法修改,但是您可以制作一个副本,将其用于目标。
move:(eq)=> eq'.
然后,eq
不再用于目标,仅用于副本eq'
。
这是一个解决方案:
Require Import CoLoR.Util.Vector.VecUtil.
Require Import Coq.Vectors.Vector.
From mathcomp Require Import ssreflect.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.Eqdep_dec.
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+0))(eq:n+0=m+0)
(func1:t A (n+0) -> t A l)(func2:t A (m+0) -> t A l)
(foo: forall {n l:nat},(t A (n+0) -> t A l) -> t A (n+0) -> t A (n+0)),Equiv func1 func2 eq -> Vcast (foo func1 v) eq = foo func2 (Vcast v eq).
Proof.
move=> n m l v e.
have e' : n = m by rewrite -{1}(plus_n_O n) -{1}(plus_n_O m) in e.
rewrite -{}e' in e * => func1 func2 foo.
rewrite (UIP_refl_nat _ e) /= => {}e.
suff -> : func1 = func2 by [].
apply: functional_extensionality=> {}v.
exact: e.
Qed.
详细信息:
-
自
n + 0 = m + 0
起,我们知道n = m
。这就是have
策略的工作。 -
因此,我们可以在任何地方将
m
替换为n
。 -
最后,由于
e : n + 0 = n + 0
引理,我们认为eq_refl
必须等于UIP_refl_nat
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。