Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] The best proof assistant for HoTT from the point of view of automation
@ 2019-01-06 16:57 José Manuel Rodriguez Caballero
  2019-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 automation
  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
  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 automation
  2019-01-07 17:58 ` Langston Barrett
@ 2019-01-07 20:57   ` Michael Shulman
  0 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 automation
  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-08  1:06 ` Juan Ospina
  2019-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

* Re: [HoTT] The best proof assistant for HoTT from the point of view of automation
  2019-01-08  1:06 ` Juan Ospina
@ 2019-01-08  1:54   ` José Manuel Rodriguez Caballero
  0 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, other threads:[~2019-01-08  1:55 UTC | newest]

Thread 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

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).