lean2/hott/port.md

We port a lot of algebra and number systems (nat, int, ...) files from the standard library to the HoTT library.

Port instructions:
- use the script port.pl in scripts/ to port the file. e.g. execute the following in the `scripts` folder: `./port.pl ../library/algebra/lattice.lean ../hott/algebra/lattice.hlean`
- remove imports starting with `data.` or `logic.` (sometimes you need to replace a `data.` import by the corresponding `types.` import)
- Open namespaces `eq` and `algebra` if needed
- (optional) add option `set_option class.force_new true`
- fix all remaining errors. Typical errors include
  - Replacing "and" by "prod" in comments
  - and.intro is replaced by prod.intro, which should be prod.mk.
  - the usage of the simp tactic

Currently, the following differences exist between the two libraries, relevant to porting:
- All of the algebraic hierarchy is in the algebra namespace in the HoTT library (on top-level in the standard library).
- The projections "zero" and "one" are reducible in HoTT. This was needed to allow type class inferences to infer
```
H : is_trunc 0 A |- is_trunc (succ (-1)) A
H : is_trunc 1 A |- is_trunc (succ 0) A
```
- Projections of most algebraic structures are definitions instead of theorems in HoTT
- Basic properties of `nat.add` have a simpler proof in HoTT (so that it computes better)
chore(hott): update md files, move port.md 2016-01-21 20:31:41 +00:00			`We port a lot of algebra and number systems (nat, int, ...) files from the standard library to the HoTT library.`
feat(hott/algebra): port abstract structures 2015-12-08 17:57:55 +00:00
feat(hott): port nat and int from the standard library 2015-12-09 05:02:05 +00:00			`Port instructions:`
			- use the script port.pl in scripts/ to port the file. e.g. execute the following in the `scripts` folder: `./port.pl ../library/algebra/lattice.lean ../hott/algebra/lattice.hlean`
			- remove imports starting with `data.` or `logic.` (sometimes you need to replace a `data.` import by the corresponding `types.` import)
			- Open namespaces `eq` and `algebra` if needed
			- (optional) add option `set_option class.force_new true`
chore(hott): cleanup 2015-12-09 20:53:48 +00:00			`- fix all remaining errors. Typical errors include`
			`- Replacing "and" by "prod" in comments`
			`- and.intro is replaced by prod.intro, which should be prod.mk.`
feat(nat/div): port to HoTT library 2016-02-23 21:01:34 +00:00			`- the usage of the simp tactic`
chore(hott): more cleanup. Make zero and one reducible (see algebra/port.md) Change some theorems which need to compute into definitions 2015-12-09 22:20:52 +00:00
			`Currently, the following differences exist between the two libraries, relevant to porting:`
			`- All of the algebraic hierarchy is in the algebra namespace in the HoTT library (on top-level in the standard library).`
			`- The projections "zero" and "one" are reducible in HoTT. This was needed to allow type class inferences to infer`
			```
			`H : is_trunc 0 A \|- is_trunc (succ (-1)) A`
			`H : is_trunc 1 A \|- is_trunc (succ 0) A`
			```
			`- Projections of most algebraic structures are definitions instead of theorems in HoTT`
			- Basic properties of `nat.add` have a simpler proof in HoTT (so that it computes better)