Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Daniel,

I'm far from expert on the matter, so please take my comments as such.

Daniel Selsam <> writes:

> Definition eval_ffun (f : {ffun unit -> bool}) := if f tt then 1 else 0.
> Goal \sum_(f : {ffun unit -> bool}) eval_ffun f = 1.
> Proof. (* ?? *)

I faced the sample problem, and I'm much afraid that the enum instance
for tuples cannot be unlocked. (Maybe it was causing some divergences?)

Thus, you may be out of luck with that particular statement.

I guess the typical proof would look like:

Definition f1 := finfun [fun x : unit => false].
Definition f2 := finfun [fun x : unit => true].

Lemma enum_ffun : enum {ffun unit -> bool} = [:: f1; f2].
Proof. admit. Qed.

Goal \sum_(f : {ffun unit -> bool}) (f tt) = 1.
Proof. by rewrite /index_enum -enumT enum_ffun !big_cons big_nil !ffunE. Qed.

But the enum_ffun lemma seems hard to prove without being able to unlock
FinTuple.enum.

> Is there a particular solution for the case of bigops with finTypes?

Note that some finTypes do work well, unit, bool, 'I_n, etc...

For the particular case of finitely supported functions, the way I would
workaround this is by defining my own function representation and
working over it with my own, custom enum instance.

An example for your class of functions would be:
[Written in 5 min so excuse the errors/bad notation]

(* Use your own function type *)
Section ubfun.

(* Change this to suit your needs *)
Inductive ubfun := UB of bool.

Definition ubproj u := let: UB b := u in b.

Lemma ubfunK : cancel ubproj UB.
Proof. by case. Qed.

(* To/from fin, etc... *)
Definition from_fin (f : {ffun unit -> bool}) : ubfun := UB (f tt).
Definition to_fin   (f : ubfun) : {ffun unit -> bool} := [ffun=> ubproj f].

Lemma ubfinK : cancel to_fin from_fin.
Proof. by case=> b; rewrite /from_fin ffunE. Qed.

(* Some coercions *)
Definition from_fun (f : simpl_fun unit bool) : ubfun := UB (f tt).
Coercion to_fun (f : ubfun) := let: UB b := f in [fun x : unit => b].

(* Instances *)
Canonical ub_eqType     := Eval hnf in EqType     ubfun (CanEqMixin     
ubfunK).
Canonical ub_choiceType := Eval hnf in ChoiceType ubfun (CanChoiceMixin 
ubfunK).
Canonical ub_countType  := Eval hnf in CountType  ubfun (CanCountMixin  
ubfunK).

(* Replace by your smart-generator. *)
Definition enum_ub : seq ubfun := [:: UB true ; UB false].

Lemma enumP : Finite.axiom enum_ub.
Proof. by do !case. Qed.

Canonical ub_finType  := Eval hnf in FinType ubfun (FinMixin enumP).

(* Convenient to to the unlocking locally *)
Lemma enum_ubP : enum {: ubfun} = [:: UB true; UB false].
Proof. by rewrite enumT unlock. Qed.

End ubfun.

Goal \sum_(f : ubfun) (f tt) = 1.
Proof. by rewrite /index_enum -enumT enum_ubP !big_cons big_nil. Qed.

> I have similar issues all the time with various parts of the
> Mathematical Components library, though I often get lucky by not using
> notations, and alternating between searching for elimination lemmas
> and manually unfolding everything I see. Is there a generic way to
> perform exhaustive computations (e.g. a tactic that unlocks everything
> and computes as much as possible)?

I seem to recall that experts on the library remarked in this mailing
list that the library was not designed to do this kind of computation,
so you are not supposed to do it. (I think that would be "do !(compute;
rewrite ?unlock)").

Best regards,
Emilio