Equality on complex functions

user_10622059 0
Viewed 63

I want to prove the following lemma:

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.

I think that Vcast (foo func1 v) eq = foo func2 (Vcast v eq). holds because of Equiv whatever foo is. But I don't know how to prove it.

Are there any solutions?

coq
1 Answers

Though intuitive, the statement cannot be proved in plain Coq, because of the lack of the functional extensionality axiom:

forall T S (f g : T -> S), 
  (forall x, f x = g x) ->
  f = g.

Luckily, this axiom is relatively harmless, and already available in the standard library. Here is how we use it:

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.

Note the case analysis on the equality proof n = m. This makes the casts disappear, reducing the goal to foo func1 v = foo func2 v. At this point, it suffices to argue that func1 = func2, for which we use extensionality.

user_16337700
Related