Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Florent,

Florent Hivert 
<>
 writes:

> Precisely, here is an example of what I'd like to do:
>
> Variable T : eqType.
> Variables a b : seq (T -> T)
>
> I'd like to be able to state and prove the following goal:
>
>       (\bigop[\o, id]_(i <- a) i) \o (\bigop[\o, id]_(i <- b) i) =1
>       (\bigop[\o, id]_(i <- a ++ b) i)
>
> This is indeed nearly Lemma big_cat except that I can't provide [\o, id] 
> with
> a Monoid.law structure because equality is =1 and not =.

I'm not an expert and I'm likely missing something, but I tried your
example out of curiosity and I had no problems:

Variable T : Type.

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.

Variables a b : seq (T -> T).

Local Notation "\c" := (funcomp tt).

Lemma l1 : \big[\c/id]_(i <- a) i \o \big[\c/id]_(i <- b) i =
           \big[\c/id]_(i <- a ++ b) i.
Proof. by rewrite big_cat. Qed.

Lemma l2 : \big[\c/id]_(i <- a) i \o \big[\c/id]_(i <- b) i =1
           \big[\c/id]_(i <- a ++ b) i.
Proof. by move=> i; rewrite big_cat. Qed.

Cheers,
Emilio