Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Bigop and functional composition.

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Bigop and functional composition.


Chronological Thread 
  • From: (Emilio Jesús Gallego Arias)
  • To: Florent Hivert <>
  • Cc: "ssreflect\@msr-inria.inria.fr" <>
  • Subject: Re: [ssreflect] Bigop and functional composition.
  • Date: Wed, 11 Nov 2015 01:34:22 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
  • Ironport-phdr: 9a23:cPcOXROGLicsW4ZySG0l6mtUPXoX/o7sNwtQ0KIMzox0KPX4rarrMEGX3/hxlliBBdydsKIZzbaI+Pq9EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35nxi775ocCbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskztSQyV630AGkUXjBdSH0CRwhX9RJr3rm3at/RwwjWyOdf3C74uD2eM9aBuHRDhjCMKODkR+3vWzMF2l6dD5hy771xSxo/QYYbdFvdl7LiVUtoeQWdOWY54TS1IGcLvPMM0E+MdMLMA/MHGrFwUoE77XFH0CQ==
  • Organization: CRI ParisTech
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

Archive powered by MHonArc 2.6.18.

Top of Page