## Stream: math-comp users

### Topic: Equality of dffun

#### Ana de Almeida Borges (Oct 25 2020 at 11:56):

I'd like to prove a lemma that looks vaguely like this:

``````Lemma example (T : finType) (n : nat) (f : {dffun forall k : 'I_n.+1, k.-tuple T}) :
f = [ffun k : 'I_n.+1 => f (id k)].
``````

I expected it would be enough to prove extensional equality, and in fact there is `eq_ffun`:

``````eq_ffun : forall g1 g2 : ?aT -> ?rT,
g1 =1 g2 -> [ffun x => g1 x] = [ffun x => g2 x]
``````

However the `g1` and `g2` are "regular" functions instead of finite functions. I figured it would be alright due to the coercion, but apparently not:

``````Fail rewrite eq_ffun.
(*
Error: The LHS of eq_ffun
[ffun x => _ x]
does not match any subterm of the goal
*)
``````

and:

`````` Fail rewrite (eq_ffun (fun_of_fin f)).
(*
The term "fun_of_fin f" has type
"forall x : ordinal_finType n.+1, x.-tuple T"
while it is expected to have type
"ordinal_finType n.+1 -> ?rT" (cannot instantiate
"?rT" because "x" is not in its scope: available arguments
are "T" "n" "f").
*)
``````

It looks like the coercion is not applicable because `f` has a dependent type. Is there a way around this?

#### Cyril Cohen (Oct 25 2020 at 12:00):

`apply/ffunP`

#### Ana de Almeida Borges (Oct 25 2020 at 12:03):

Thanks Cyril!

Last updated: Jul 25 2024 at 15:02 UTC