Stream: math-comp users

Topic: Equality of dffun

view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Oct 25 2020 at 12:00):

apply/ffunP

view this post on Zulip Ana de Almeida Borges (Oct 25 2020 at 12:03):

Thanks Cyril!

Last updated: Oct 13 2024 at 01:02 UTC