Details

Autor(en) / Beteiligte

• Pollack, Robert
• Harrison, John
• Aagaard, Mark

Titel

Dependently Typed Records for Representing Mathematical Structure

Ist Teil von

• Lecture notes in computer science, 2000, p.462-479

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

2000

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Consider a statement about groups “For G a group, ...”. A naive approach to formalize this is to unfold the meaning of group, so that every statement about groups begins with 1\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ For\,\,G\,\,a\,\,set,\,\, + \,an\,\,operation\,\,on\,\,G,\,\, + \,\,associative,\,\,e\,\, \in \,\,G,\,... $$\end{document} This “unpackaged” approach can be improved by collecting all the parts of the meaning of group into a context, which need not be explicitly mentioned in every statement. A means of discharging some of the context is provided, so that statements made under that context can be instantiated with particular groups. However once that group context is discharged, all the parts of a group must be mentioned when using any general lemma about groups. Variations on this are supported by many proof tools, e.g. Coq’s Section mechanism [Coq99], Lego’s Discharge [LEG99], Automath contexts and Isabelle locales.