Ssreflect Users Discussion List

[Assia Mahboubi <>]

Dear Florent,

  indeed, as Emilio points out, none of the structures defined in bigop impose
an eqType structure on their carrier, as opposed to the structures in the 
ssralg
hierarchy.
So the lemma you mention is indeed accessible though the bigop infrastructure,
as detailed by Emilio, as are all the identity that hold by reflexivity only.

Now you might still need to revisit the bigop library (well the tiny part 
about
plain monoids in this case), to use =1 in the hypotheses of the lemmas when 
needed:

- this one comes for free:

Lemma my_eq_bigr (I : Type) r (P : pred I) (F1 F2 : I -> (T -> T)) :
  (forall i, P i -> F1 i = F2 i) ->
  \big[\c /id]_(i <- r | P i) F1 i = \big[\c /id]_(i <- r | P i) F2 i.
Proof. exact: eq_bigr. Qed.

- but you're probably more interested by this one:

Lemma my_eq1_bigr (I : Type) r (P : pred I) (F1 F2 : I -> (T -> T)) :
  (forall i, P i -> F1 i =1 F2 i) ->
  \big[\c /id]_(i <- r | P i) F1 i =1 \big[\c /id]_(i <- r | P i) F2 i.
Proof.
move=> eqF12; elim/big_rec2: _ => // i x y /eqF12 eF12 eyx; exact: eq_comp.
Qed.

Best,

assia

Le 11/11/2015 01:34, Emilio Jesús Gallego Arias a écrit :
> Obviously, I'm using Coq's "intensional" equality here, that since 8.4
> validates:
> 
>  f = [eta f]
> 
> Of course, it may not be strong enough for you in the end.
> 
> 
>  (Emilio Jesús Gallego Arias) writes:
> 
>> Lemma cA : associative (@funcomp T T T tt).
>> Proof. by []. Qed.
>>
>> Lemma cfI : right_id id (@funcomp T T T tt).
>> Proof. by []. Qed.
>>
>> Lemma cIf : left_id id (@funcomp T T T tt).
>> Proof. by []. Qed.
>>
>> Canonical cMonoid := Monoid.Law cA cIf cfI.
> 
> 
> Best,
> Emilio
>