时间戳

首页 > 解决方案 > 具有复杂类型的复杂函数的相等性

coq - 具有复杂类型的复杂函数的相等性

问题描述

我想证明以下引理。

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在假设中使用。

有什么解决办法吗？

标签： coq

解决方案

这是一个解决方案：

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.

更详细地说：

  1. 既然n + 0 = m + 0，我们知道n = m。这就是have策略正在做的事情。

  2. 因此，我们可以到处替换m。n

  3. 最后，由于引理，我们认为e : n + 0 = n + 0必须等于。eq_reflUIP_refl_nat

推荐阅读