From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pg1-x53f.google.com (mail-pg1-x53f.google.com [IPv6:2607:f8b0:4864:20::53f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c9f79087 for ; Tue, 8 Jan 2019 01:55:02 +0000 (UTC) Received: by mail-pg1-x53f.google.com with SMTP id q62sf1155561pgq.9 for ; Mon, 07 Jan 2019 17:55:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1546912501; cv=pass; d=google.com; s=arc-20160816; b=yZGNcLHQZrpxwObcamWKM4RJBooKE9EZjfphCZ3xzLSusbzd6Bap8RMEkCCAFZdCv5 8i67fTaPjjPfIgdikdKLkIOt9PEXm0txI20YOSo10+dS/9sNHfG92W2hqyQg/nNndn+I JJ37xCva+7BUNAWPdeVrTVHiYW4PAs/clJDXYTFfTOmNM4/EGGYtUupciXk0fHPZanMv tjxk/6Z37W7V8kUPaI9TjWqVuQwUDNzp4g46ObQh/PXA80Wg1sV4xEmx8bGVoWlfQw6O RFnAK0uZuaIi70hndF3lpxcGuuSBBbGxlBtQVgFDrLErICDsavng1zvprSKypwAZPhgG pLOw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=WQiAcGvjcLo1dtrO94x3ToZeRRZLctGkOb6Mnh6mHCo=; b=E7pe1CLW/ssttR/LA+wcjw6jnOQ/GUCdfnoh9vtgtAlR0SNDpBK4Z+2AC6fqKtbpw/ oOuUb9VferSb/bcKiPs4wzyaZiaWmzdNfDeUZlC5qu+I+uXeCg6eZ9BvHGTnGEwun3ks 53YxxlFqpwh39v2LNqML3HqBalMPgkIBBq5TRpEAnMkaS8tFHRBP5tL+pjRigqehFuJm pBa8zNxEAM0VRv69MTWoeTBD8Dy4SN2YPu+CrjESg1Kh0iK2I5PIcwFdKCBbk7Kov6Wx cUCxT8JIO98fg5XB69id0uOhQsvwItSBKJFXLDmuhQxHvcvIbNHqQfrVXn5zHAWqWU1g P75Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=rC1bPRVW; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::132 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=WQiAcGvjcLo1dtrO94x3ToZeRRZLctGkOb6Mnh6mHCo=; b=oSASSs7KM/1y9f7VWJM6BXmlptV6a0pV11YON/1o8PHkIUkG6S8f7YdZm/zeijLZM6 X/lR17w92NBHP0ESSkQbzlOJUJpyH48mR/C/r4ixbvLQui8THM7tmkRW+avtHT//hVfp xX4cLP+l0Pzw9VJJYSitcxLLbHWUmKJ53kankS+N6mu5ETngU87sGeBWizqr1Vv5y0E5 /5ZE7ZfpPFIaYbrjatSWDocKUxJNyk9K0/EyliXHsyS7+qE/kEVfHOytXnWSpJ/Lc6D9 HWxGZq8iq50z/mr2+PwAxk0Ypf0Cqa+riTw+jlNEUNdRG3auXcWg/AztzfbAaCrxSD75 OecA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=WQiAcGvjcLo1dtrO94x3ToZeRRZLctGkOb6Mnh6mHCo=; b=cUdILY/KAY1bGuv4XeNA/h+BoK72TT+nvFdvVSQmtH8IOoioInOQwUYpLtk5m+hG2B UhUlIbLs20YTvEg2Cq3wZpdBjyyJ1BDzmN7B2PiHdIpSIjWBpwmgZxnijioYsSvM0Pv2 kczSNXNkLPDlHQ4Y3ZbNeyJnSCCHAKUkWlY8WY1ygUh0rLqMRBFKJQJ2iI52PUa3Q3Kp ecOLKL0OKS0pfjLpeCH9gBsV++Kw+C2x7Tt+FAU6VrbqDuEDJlX33TnbZTdDdqsZSgDZ 61OFlJz0lYFfCLmiuwaoYPYSV14Q3ISv45UqpA2I3roCNz9d3OZK/KPjNaExygtRu2JW 4bUg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=WQiAcGvjcLo1dtrO94x3ToZeRRZLctGkOb6Mnh6mHCo=; b=PLG6FEI+otHP2duLXmNIVGqY+v8sPF7/hdCAulvq9lwzhqP/1CxZKFG42YmSQqbbBi qtiWXAk5aioBGaynhoeLrhsIQ8FxS4aCyGfoUY2RDIHkCelbn/FrE3MOJz/1AEH+rlNC Hq+oFGc87rmqWeMtM2xYhTNJN1PeFELZYzaxrinppW3bGyQK5INDYwaLV8niyqpUtuPG pXIDP96Ooz4k2KRp3iyc8OPYLmo5hh6rCn7jwDXgQUi7aleRjfF4B7xBQZTXRQGnvbMd OtqVkgSC58xE2K9P+0tepYMlHXw8oozKRiRxWc1CafDK4BAjqD86KZ0QtgFbT9azL3TD nxVw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWaKL+NB6fCRXVswcVc5rUBdeJE/mR+aSvi/3WsB9bxZLt21GOoZ 8feNu8nzJcEys9Xe2n5w3SE= X-Google-Smtp-Source: AFSGD/VLohCbWbu4j5ycrwOHmXX6RcR6ryoFhZx9M5aWGo9eVeJuuCWaUVN6yLl8mClzNMTviXJulg== X-Received: by 2002:a62:c60f:: with SMTP id m15mr269365pfg.6.1546912500939; Mon, 07 Jan 2019 17:55:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:b946:: with SMTP id v6ls709063pgo.9.gmail; Mon, 07 Jan 2019 17:55:00 -0800 (PST) X-Received: by 2002:a63:5b4d:: with SMTP id l13mr28389498pgm.30.1546912500509; Mon, 07 Jan 2019 17:55:00 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1546912500; cv=none; d=google.com; s=arc-20160816; b=gB0/0hsHMn3ocmxn35zjCosmvGl3iYmAYJTSGC1IOyw+QxSz1Py5WJZFbCyL2M7f0S vQJYBLZnzjUIMQk3ZrdRmdw3ldmkvonSjneB2ZHXGyTf5XZeuqpOR2BL7uvPl1ptFzTJ 6vaRGr+DP5+I9ukAJf4H3RVTvZhY9BwPgzwLqFXzyhe1ZPlR49x1RCMZ1Z/51/auIIVa 6kFz8oWNKDxr73Rs1aW8doNcGLt6J/OhcIaeIl6m+sKgPEhrOw83KifUI7J0wTk9Kxc5 640uE0j9wvLfrXcup1cJa8cAIlEdM1HLtK4K4kTcQK9mZMqHq+4/QsUzc8+toGsKDtZb 3SNw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=zM9pwSF0ERc26FPNDAqJBJF3vZa10cMBHRV2Qs9C9i8=; b=AAq6iFc0tNunxcrgsVcI7YND1ixZ5mS6vutqsY/uZ2FAS3aW5uJ0URS8fIfuwmAGar behz9lb8gKx6fywYEVST/4jaK72Ok6XCH2c47/D/cjMm1I1zhBAEcaR7ednrXJviPf97 jHSm97nEMxkTpxhpVAy4kb4LTFN5Xu9G0pkXyc1WKHE0ZNOO9z9Zl23KoYoHAEwAqDBS E+zvTjudKR8m74zT0Nyp2oE6t/BhiNMeCwj+WP72P5BoSmRKLh9HR3/YgtEM1QFJVWLV zphq6pB0JaX1cTVXe0RYYiJYuws8Gj3bZw1uFy2+bV9YFdigk7MceCK8XW1A/OLpjxbL hvyQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=rC1bPRVW; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::132 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x132.google.com (mail-it1-x132.google.com. [2607:f8b0:4864:20::132]) by gmr-mx.google.com with ESMTPS id 23si2915896pgc.4.2019.01.07.17.55.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 07 Jan 2019 17:55:00 -0800 (PST) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::132 as permitted sender) client-ip=2607:f8b0:4864:20::132; Received: by mail-it1-x132.google.com with SMTP id w18so4152541ite.1 for ; Mon, 07 Jan 2019 17:55:00 -0800 (PST) X-Received: by 2002:a02:98bb:: with SMTP id q56mr42433989jaj.24.1546912499820; Mon, 07 Jan 2019 17:54:59 -0800 (PST) MIME-Version: 1.0 References: <9343db17-0282-4a4f-8701-8363317f2f8d@googlegroups.com> In-Reply-To: <9343db17-0282-4a4f-8701-8363317f2f8d@googlegroups.com> From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Mon, 7 Jan 2019 20:54:48 -0500 Message-ID: Subject: Re: [HoTT] The best proof assistant for HoTT from the point of view of automation To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000000cedf5057ee8a215" X-Original-Sender: josephcmac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=rC1bPRVW; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::132 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --0000000000000cedf5057ee8a215 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > Juan wrote: > A trivial example of Hott with Lean... In my case, I learned UniMath just from Voevodsky's video lectures at Oxford (I was not there): Point 9 in this link: https://www.math.ias.edu/vladimir/Lectures I am interested to get back to HoTT, after some time focused in Isabelle/HOL, just for pleasure (my serious job is with Isabelle/HOL). What I love of HoTT is the idea of thinking in a topological way about non-topological problems: this is like a video-game for me, not a project, it is something just for fun. Here is an example of one of my theorems in UniMath (a greedy generalization of Euclidean division). As you can see, automation is almost zero in my program. I guess that it will be shorted in Lean or in Coq (using the HoTT library). [Another motivation is that I have the intuition that HoTT is related to the combinatorics of finite fields via the Weil Conjectures, but I need more experience before to formalize this intuition, e.g., given a type, we can express its topological invariants as the number of points on a variety over a finite field and the correspondence is "natural". This may be non-sense.] Unset Automatic Introduction. (** *** Imports *) Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Foundations.PartA. Definition Increasing :=3D fun (f : nat -> nat) =3D> forall n : nat, f n = =E2=89=A4 f (S n). Lemma powerMonotonic : forall f : nat -> nat, Increasing f -> ( forall n k : nat, f n =E2=89=A4 f (n + k) ). Proof. intros. intros. induction k. rewrite natplusr0. apply (natlehmplusnm 0 (f n) ). change (S k) with (1 + k). rewrite (natpluscomm 1 k). rewrite <- (natplusassoc n k 1). unfold Increasing in X. specialize (X (n + k)). change (S (n + k)) with (1 + (n + k)) in X. rewrite ( natpluscomm 1 (n + k) ) in X. apply (istransnatleh IHk X). Defined. Definition SIncreasing :=3D fun (f : nat -> nat) =3D> forall n : nat, f n <= f (S n). Lemma SpowerMonotonic : forall f : nat -> nat, SIncreasing f -> ( forall n k : nat, f n < f (n + k + 1) ). Proof. intros. intros. induction k. rewrite natplusr0. rewrite -> (natpluscomm n 1). change (1 + n) with (S n). unfold SIncreasing in X. specialize (X n). apply X. change (S k) with (1 + k). rewrite (natpluscomm 1 k). rewrite <- (natplusassoc n k 1). unfold SIncreasing in X. specialize (X (n + k + 1)). rewrite -> (natpluscomm (n + k) 1) in X. change (S (1 + (n + k))) with (1 + (1 + (n + k))) in X. rewrite <-( natplusassoc 1 1 (n + k) ) in X. rewrite -> ( natpluscomm (1 + 1) (n + k) ) in X. rewrite -> ( natplusassoc n k (1 + 1) ) in X. rewrite -> ( natplusassoc (n + k) 1 1 ). rewrite -> ( natpluscomm (n + k) 1 ) in IHk. assert (T :=3D istransnatlth (f n) (f (1 + (n + k))) (f (n + (k + (1 + 1)))) ). rewrite -> ( natplusassoc n k (1 + 1) ). apply T. apply IHk. apply X. Defined. Lemma SpowerLargerThanN : forall f : nat -> nat, SIncreasing f -> ( forall n : nat, (f 0) + n =E2=89=A4 f n ). Proof. induction n. rewrite (natplusr0 (f 0)). apply (natlehmplusnm 0). rewrite <- ( plus_n_Sm (f 0) n). apply (natlehandplusl (f 0 + n) (f n) 1 ) in IHn. change (1 + (f 0 + n)) with (S (f 0 + n)) in IHn. change (1 + f n) with (S (f n)) in IHn. unfold SIncreasing in X. specialize (X n). apply (natlthtolehsn) in X. apply ( istransnatleh IHn X ). Defined. Definition EuclidF :=3D fun (f : nat -> nat) (x : dirprod nat nat) =3D> (f = (pr1 x)) + (pr2 x). Definition GreedyEuclid (f : nat -> nat) (isSIncreasing : SIncreasing f) (n : nat) : dirprod nat nat. Proof. intros. induction n as [ | n x]. - intros. apply (dirprodpair (f 0) 0). - induction (natlthorgeh ((f (pr1 x)) + S (pr2 x)) (f (S (pr1 x)))). + apply ( dirprodpair (pr1 x) (S (pr2 x)) ). + apply ( dirprodpair (S (pr1 x)) (0) ). Defined. Lemma GreedyEuclidLem : forall (f : nat -> nat), SIncreasing f -> forall n : nat, hfiber (fun (x : dirprod nat nat) =3D> EuclidF f x) ((f 0) + n). Proof. intros. unfold hfiber. exists (dirprodpair 0 n). unfold EuclidF. simpl. apply idpath. Defined. --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --0000000000000cedf5057ee8a215 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Juan wrote:
A trivial example of Hott with Lean...
In my case, I = learned UniMath just from Voevodsky's video lectures at Oxford (I was n= ot there): Point 9 in this link:=C2=A0https://www.math.ias.edu/vladimir/Lectures
=
I am interested to get back to HoTT, after some time focused= in Isabelle/HOL, just for pleasure (my serious job is with Isabelle/HOL). = What I love of HoTT is the idea of thinking in a topological way about non-= topological problems: this is like a video-game for me, not a project, it i= s something just for fun. Here is an example of one of my theorems in UniMa= th (a greedy generalization of Euclidean division). As you can see, automat= ion is almost zero in my program. I guess that it will be shorted in Lean o= r in Coq (using the HoTT library).

[Another mo= tivation is that I have the intuition that HoTT is related to the combinato= rics of finite fields via the Weil Conjectures, but I need more experience = before to formalize this intuition, e.g., given a type, we can express its = topological invariants as the number of points on a variety over a finite f= ield and the correspondence is "natural". This may be non-sense.]=

Unset Automatic Introduction.

=
(** *** Imports *)

Require Import UniMa= th.Foundations.NaturalNumbers.

Require Import UniM= ath.Foundations.PartA.

Definition Increasing :=3D = fun (f : nat -> nat) =3D> forall n : nat, f n =E2=89=A4 f (S n).

Lemma powerMonotonic : forall f : nat -> nat, Incre= asing f -> ( forall n k : nat, f n =E2=89=A4 f (n + k) ).
Proo= f.
=C2=A0 intros.
=C2=A0 intros.
=C2=A0 induc= tion k.
=C2=A0 rewrite natplusr0.
=C2=A0 apply (natlehm= plusnm 0 (f n) ).
=C2=A0 change (S k) with (1 + k).
=C2= =A0 rewrite (natpluscomm 1 k).
=C2=A0 rewrite <- (natplusassoc= n k 1).
=C2=A0 unfold Increasing in X.
=C2=A0 speciali= ze (X (n + k)).
=C2=A0 change (S (n + k)) with (1 + (n + k)) in X= .
=C2=A0 rewrite ( natpluscomm 1 (n + k) ) in X.
=C2=A0= apply (istransnatleh IHk X).
Defined.

D= efinition SIncreasing :=3D fun (f : nat -> nat) =3D> forall n : nat, = f n < f (S n).

Lemma SpowerMonotonic : forall f= : nat -> nat, SIncreasing f -> ( forall n k : nat, f n < f (n + k= + 1) ).
Proof.
=C2=A0 intros.
=C2=A0 intros.=
=C2=A0 induction k.
=C2=A0 rewrite natplusr0.
=C2=A0 rewrite -> (natpluscomm n 1).
=C2=A0 change (1 + n) w= ith (S n).
=C2=A0 unfold SIncreasing in X.
=C2=A0 speci= alize (X n).
=C2=A0 apply X.
=C2=A0 change (S k) with (= 1 + k).
=C2=A0 rewrite (natpluscomm 1 k).
=C2=A0 rewrit= e <- (natplusassoc n k 1).
=C2=A0 unfold SIncreasing in X.
=C2=A0 specialize (X (n + k + 1)).
=C2=A0 rewrite -> (n= atpluscomm (n + k) 1) in X.
=C2=A0 change (S (1 + (n + k))) with = (1 + (1 + (n + k)))=C2=A0 in X.
=C2=A0 rewrite <-( natplusasso= c 1 1 (n + k) ) in X.
=C2=A0 rewrite -> ( natpluscomm (1 + 1) = (n + k) ) in X.
=C2=A0 rewrite -> ( natplusassoc n k (1 + 1) )= in X.
=C2=A0 rewrite -> ( natplusassoc (n + k) 1 1 ).
=C2=A0 rewrite -> ( natpluscomm (n + k) 1 ) in IHk.
=C2=A0 = assert (T :=3D=C2=A0 istransnatlth (f n) (f (1 + (n + k))) (f (n + (k + (1 = + 1)))) ).
=C2=A0 rewrite -> ( natplusassoc n k (1 + 1) ).
=C2=A0 apply T.
=C2=A0 apply IHk.
=C2=A0 apply X= .
Defined.

Lemma SpowerLargerThanN : for= all f : nat -> nat, SIncreasing f -> ( forall n : nat, (f 0) + n =E2= =89=A4 f n ).
Proof.
=C2=A0 induction n.
=C2= =A0 rewrite (natplusr0 (f 0)).
=C2=A0 apply (natlehmplusnm 0).
=C2=A0 rewrite <- ( plus_n_Sm (f 0) n).
=C2=A0 apply (= natlehandplusl (f 0 + n) (f n) 1 ) in IHn.
=C2=A0 change (1 + (f = 0 + n)) with (S (f 0 + n)) in IHn.
=C2=A0 change (1 + f n) with (= S (f n)) in IHn.
unfold SIncreasing in X.
specialize (X= n).
apply (natlthtolehsn) in X.
apply ( istransnatleh = IHn X ).
Defined.

Definition EuclidF := =3D fun (f : nat -> nat) (x : dirprod nat nat) =3D> (f (pr1 x)) + (pr= 2 x).

Definition GreedyEuclid (f : nat -> nat) = (isSIncreasing : SIncreasing f) (n : nat) : dirprod nat nat.
Proo= f.
intros.
induction n as [ | n x].
- intros.=
=C2=A0 apply (dirprodpair (f 0) 0).
- induction (natlt= horgeh ((f (pr1 x)) + S (pr2 x)) (f (S (pr1 x)))).
+ apply ( dirp= rodpair (pr1 x) (S (pr2 x)) ).
+ apply ( dirprodpair (S (pr1 x)) = (0) ).
Defined.

Lemma GreedyEuclidLem : = forall (f : nat -> nat), SIncreasing f -> forall n : nat,=C2=A0 hfibe= r (fun (x : dirprod nat nat) =3D> EuclidF f x) ((f 0) + n).
Pr= oof.
=C2=A0 intros.
=C2=A0 unfold hfiber.
=C2= =A0 exists (dirprodpair 0 n).
=C2=A0 unfold EuclidF.
= =C2=A0 simpl.
=C2=A0 apply idpath.
Defined.
=


--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000000cedf5057ee8a215--