Stream: math-comp users

Topic: ✔ Beta-reduction of finite function

Ricardo (Nov 25 2022 at 14:24):

Hi. How does one beta-reduce an expression of the form f x where f is a finite function in a proof?

Ricardo (Nov 25 2022 at 14:33):

I tried cbn, hnf and simpl and none works.

Ricardo (Nov 25 2022 at 14:38):

I even tried with

  change ([ffun k0 => if fsval k0 \in ks
                      then v
                      else odflt v m.[? fsval k0]]
            (fincl ks_sub [` H]))
    with (if fsval (fincl ks_sub [` H]) \in ks
          then v
          else odflt v m.[? fsval (fincl ks_sub [` H])]).

and didn't work. That's suspicious.

Ricardo (Nov 25 2022 at 15:20):

I found it! rewrite ffunE does the trick.

Notification Bot (Nov 25 2022 at 15:20):

Ricardo has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC