search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Lemma relating [transport idmap] and [ap] #211

Closed JasonGross closed 11 years ago

JasonGross commented 11 years ago

Does this theorem exist somewhere already? If not, where should it go and what should it be called?

Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)                                                             
: transport P p u = transport idmap (ap P p) u                                                                                        
  := match p with idpath => idpath end.
mikeshulman commented 11 years ago

It's a special case of transport_compose.

JasonGross commented 11 years ago

Thanks!

andrejbauer commented 11 years ago

Welcome to the land of unsearchable theorems. If we're ever to make progress on formalized mathematics then answering such a question by performing a computer search must become a reality.

spitters commented 11 years ago

It turns out that there is an ocaml version of hoogle: http://search.ocaml.jp/

I am wondering whether it can be made to work for Coq.

Also ssreflect has an improved search (Ch 10). http://hal.inria.fr/inria-00258384/ I am not sure how much of this has been ported to vanilla Coq.

On Tue, Sep 17, 2013 at 10:41 AM, Andrej Bauer notifications@github.comwrote:

Welcome to the land of unsearchable theorems. If we're ever to make progress on formalized mathematics then answering such a question by performing a computer search must become a reality.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/211#issuecomment-24572326 .

JasonGross commented 11 years ago

Writing SearchAbout (_ = transport _ (ap _ _) _). gives me transport_compose, as does SearchAbout (transport _ _ _ = transport _ (ap _ _) _).. How I would know that I'm looking for that, rather than SearchAbout transport idmap. (which gives me transport_path_universe and isequiv_path) or SearchAbout transport ap. (which gives me a list of a few dozen lemmas, including transport_compose), I'm not sure.

JasonGross commented 11 years ago

Another possibility would be making a hott_all database, and write Hint Immediate foo : hott_all for all theorems, so that we could do something like Goal foo. intros. auto with hott_all. Show Proof. to see if the theorem we have unifies with one of the given theorems. Perhaps a feature like this would be useful to get in Coq, a "Does this term unify with the conclusion of any theorem currently known to Coq?" (unify, rather than pattern match).

JasonGross commented 11 years ago

I've submitted a feature request for unification-based search: https://coq.inria.fr/bugs/show_bug.cgi?id=3129

mikeshulman commented 11 years ago

It might be worth considering giving a special name to this particular instance of transport_compose, as it seems to come up a lot. If we did that, then it ought to come up under SearchAbout transport idmap.

spitters commented 11 years ago

And there was whelp before of course: http://matita.cs.unibo.it/PAPERS/whelp.pdf

On Tue, Sep 17, 2013 at 12:57 PM, Bas Spitters spitters@cs.ru.nl wrote:

It turns out that there is an ocaml version of hoogle: http://search.ocaml.jp/

I am wondering whether it can be made to work for Coq.

Also ssreflect has an improved search (Ch 10). http://hal.inria.fr/inria-00258384/ I am not sure how much of this has been ported to vanilla Coq.

On Tue, Sep 17, 2013 at 10:41 AM, Andrej Bauer notifications@github.comwrote:

Welcome to the land of unsearchable theorems. If we're ever to make progress on formalized mathematics then answering such a question by performing a computer search must become a reality.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/211#issuecomment-24572326 .