时间戳

首页 > 解决方案 > 复杂函数的平等

coq - 复杂函数的平等

问题描述

我想证明以下引理：

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).是因为Equivfoo 是什么。但我不知道如何证明。

有什么解决办法吗？

标签： coq

解决方案

尽管很直观，但由于缺少功能外延公理，无法在普通 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我们使用外延性。

推荐阅读