*[HoTT] The best proof assistant for HoTT from the point of view of automation@ 2019-01-06 16:57 José Manuel Rodriguez Caballero2019-01-07 17:58 ` Langston Barrett 2019-01-08 1:06 ` Juan Ospina 0 siblings, 2 replies; 5+ messages in thread From: José Manuel Rodriguez Caballero @ 2019-01-06 16:57 UTC (permalink / raw) To: HomotopyTypeTheory [-- Attachment #1: Type: text/plain, Size: 1292 bytes --] Hello, After reading the (beautiful) paper Paredes, Belén. "Boson-Lattice Construction for Anyon Models." arXiv preprint arXiv:1804.01605 (2018). https://arxiv.org/pdf/1804.01605.pdf I was rather motivated to explore modular tensor categories: https://ncatlab.org/nlab/show/modular+tensor+category using a proof assistant. My preferred proof assistant is Isabelle/HOL, because of the hight level of automation, but I am not sure that simple type theory is the best formal system to work with modular tensor categories. As far as I know, HoTT has been used in order to formalize category theory in a rather successful way. In my case, I programmed a little bit in UniMath (Coq), but thee automation was almost zero (maybe there is some automation, but I did not know how to use it, everything that I learned in computer sciences was self-taught). So, I wonder in which proof assistant HoTT can be used with a maximum of automation. Kind Regards, José M. -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 1842 bytes --] ^ permalink raw reply [flat|nested] 5+ messages in thread

*Re: [HoTT] The best proof assistant for HoTT from the point of view of automation2019-01-06 16:57 [HoTT] The best proof assistant for HoTT from the point of view of automation José Manuel Rodriguez Caballero@ 2019-01-07 17:58 ` Langston Barrett2019-01-07 20:57 ` Michael Shulman 2019-01-08 1:06 ` Juan Ospina 1 sibling, 1 reply; 5+ messages in thread From: Langston Barrett @ 2019-01-07 17:58 UTC (permalink / raw) To: José Manuel Rodriguez Caballero;+Cc:HomotopyTypeTheory [-- Attachment #1: Type: text/plain, Size: 2361 bytes --] While UniMath doesn't use much automation internally, Coq has very rich facilities for it. Using UniMath as a base for your development doesn't prevent you from using e.g. Ltac for automating proof scripts. Even if you decide to develop without using Coq's automation, I would bet you'll save more time by reusing UniMath's extensive development of category theory than you would by using any sort of proof automation. Here are some resources on automation in Coq: - Tutorial: http://adam.chlipala.net/cpdt/html/Match.html - Reference: https://coq.inria.fr/refman/proof-engine/ltac.html On Sun, Jan 6, 2019 at 8:57 AM José Manuel Rodriguez Caballero < josephcmac@gmail.com> wrote: > Hello, > After reading the (beautiful) paper > > Paredes, Belén. "Boson-Lattice Construction for Anyon Models." arXiv > preprint arXiv:1804.01605 (2018). > https://arxiv.org/pdf/1804.01605.pdf > > I was rather motivated to explore modular tensor categories: > https://ncatlab.org/nlab/show/modular+tensor+category > > using a proof assistant. My preferred proof assistant is Isabelle/HOL, > because of the hight level of automation, but I am not sure that simple > type theory is the best formal system to work with modular tensor > categories. As far as I know, HoTT has been used in order to formalize > category theory in a rather successful way. In my case, I programmed a > little bit in UniMath (Coq), but thee automation was almost zero (maybe > there is some automation, but I did not know how to use it, everything that > I learned in computer sciences was self-taught). > > So, I wonder in which proof assistant HoTT can be used with a maximum of > automation. > > Kind Regards, > José M. > > -- > 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 > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 3598 bytes --] ^ permalink raw reply [flat|nested] 5+ messages in thread

*Re: [HoTT] The best proof assistant for HoTT from the point of view of automation2019-01-07 17:58 ` Langston Barrett@ 2019-01-07 20:57 ` Michael Shulman0 siblings, 0 replies; 5+ messages in thread From: Michael Shulman @ 2019-01-07 20:57 UTC (permalink / raw) To: Langston Barrett;+Cc:José Manuel Rodriguez Caballero, HomotopyTypeTheory The HoTT Coq library (https://github.com/HoTT/HoTT) uses somewhat more automation than UniMath, I believe. In particular, the category theory library that it contains (https://arxiv.org/abs/1401.7694) was developed using many of Chlipala's automation techniques. On Mon, Jan 7, 2019 at 9:58 AM Langston Barrett <langston@galois.com> wrote: > > While UniMath doesn't use much automation internally, Coq has very rich facilities for it. Using UniMath as a base for your development doesn't prevent you from using e.g. Ltac for automating proof scripts. > > Even if you decide to develop without using Coq's automation, I would bet you'll save more time by reusing UniMath's extensive development of category theory than you would by using any sort of proof automation. > > Here are some resources on automation in Coq: > - Tutorial: http://adam.chlipala.net/cpdt/html/Match.html > - Reference: https://coq.inria.fr/refman/proof-engine/ltac.html > > On Sun, Jan 6, 2019 at 8:57 AM José Manuel Rodriguez Caballero <josephcmac@gmail.com> wrote: >> >> Hello, >> After reading the (beautiful) paper >> >> Paredes, Belén. "Boson-Lattice Construction for Anyon Models." arXiv preprint arXiv:1804.01605 (2018). >> https://arxiv.org/pdf/1804.01605.pdf >> >> I was rather motivated to explore modular tensor categories: >> https://ncatlab.org/nlab/show/modular+tensor+category >> >> using a proof assistant. My preferred proof assistant is Isabelle/HOL, because of the hight level of automation, but I am not sure that simple type theory is the best formal system to work with modular tensor categories. As far as I know, HoTT has been used in order to formalize category theory in a rather successful way. In my case, I programmed a little bit in UniMath (Coq), but thee automation was almost zero (maybe there is some automation, but I did not know how to use it, everything that I learned in computer sciences was self-taught). >> >> So, I wonder in which proof assistant HoTT can be used with a maximum of automation. >> >> Kind Regards, >> José M. >> >> -- >> 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 5+ messages in thread

*Re: [HoTT] The best proof assistant for HoTT from the point of view of automation2019-01-06 16:57 [HoTT] The best proof assistant for HoTT from the point of view of automation José Manuel Rodriguez Caballero 2019-01-07 17:58 ` Langston Barrett@ 2019-01-08 1:06 ` Juan Ospina2019-01-08 1:54 ` José Manuel Rodriguez Caballero 1 sibling, 1 reply; 5+ messages in thread From: Juan Ospina @ 2019-01-08 1:06 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1776 bytes --] On Sunday, January 6, 2019 at 11:57:57 AM UTC-5, José Manuel Rodriguez Caballero wrote: > > Hello, > After reading the (beautiful) paper > > Paredes, Belén. "Boson-Lattice Construction for Anyon Models." arXiv > preprint arXiv:1804.01605 (2018). > https://arxiv.org/pdf/1804.01605.pdf > > I was rather motivated to explore modular tensor categories: > https://ncatlab.org/nlab/show/modular+tensor+category > > using a proof assistant. My preferred proof assistant is Isabelle/HOL, > because of the hight level of automation, but I am not sure that simple > type theory is the best formal system to work with modular tensor > categories. As far as I know, HoTT has been used in order to formalize > category theory in a rather successful way. In my case, I programmed a > little bit in UniMath (Coq), but thee automation was almost zero (maybe > there is some automation, but I did not know how to use it, everything that > I learned in computer sciences was self-taught). > > So, I wonder in which proof assistant HoTT can be used with a maximum of > automation. > > Kind Regards, > José M. > A trivial example of Hott with Lean import homotopy.cylinder open cylinder check cylinder_rel check cylinder check base check top check seg constants {A B : Type} (f : A → B) constant {c : A} variables {g : A -> A} example (c : A) : base f (f (g c)) = top f (g c) := begin rewrite seg end -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3411 bytes --] ^ permalink raw reply [flat|nested] 5+ messages in thread

*2019-01-08 1:06 ` Juan OspinaRe: [HoTT] The best proof assistant for HoTT from the point of view of automation@ 2019-01-08 1:54 ` José Manuel Rodriguez Caballero0 siblings, 0 replies; 5+ messages in thread From: José Manuel Rodriguez Caballero @ 2019-01-08 1:54 UTC (permalink / raw) To: HomotopyTypeTheory [-- Attachment #1: Type: text/plain, Size: 4488 bytes --] > > 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 := fun (f : nat -> nat) => forall n : nat, f n ≤ f (S n). Lemma powerMonotonic : forall f : nat -> nat, Increasing f -> ( forall n k : nat, f n ≤ 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 := fun (f : nat -> nat) => 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 := 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 ≤ 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 := fun (f : nat -> nat) (x : dirprod nat nat) => (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) => EuclidF f x) ((f 0) + n). Proof. intros. unfold hfiber. exists (dirprodpair 0 n). unfold EuclidF. simpl. apply idpath. Defined. -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 6178 bytes --] ^ permalink raw reply [flat|nested] 5+ messages in thread

end of thread, back to indexThread overview:5+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2019-01-06 16:57 [HoTT] The best proof assistant for HoTT from the point of view of automation José Manuel Rodriguez Caballero 2019-01-07 17:58 ` Langston Barrett 2019-01-07 20:57 ` Michael Shulman 2019-01-08 1:06 ` Juan Ospina 2019-01-08 1:54 ` José Manuel Rodriguez Caballero

Discussion of Homotopy Type Theory and Univalent Foundations Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.hott AGPL code for this site: git clone https://public-inbox.org/ public-inbox