Floris van Doorn
11b1f416f6
feat(nat): add unfold attributes to add, mul, sub and of_num in namespace nat_esimp in both libraries
2015-08-04 13:23:20 +02:00
Floris van Doorn
747d12a385
feat(hott): prove characterization of a pathover in a pathover-type
2015-08-04 13:01:12 +02:00
Floris van Doorn
e198be318f
feat(circle): show that x = x in the circle is always Z
2015-08-04 13:01:11 +02:00
Floris van Doorn
7a780b1b60
feat(hott): various minor changes in the HoTT library
2015-08-04 13:01:11 +02:00
Leonardo de Moura
b3cd3efbb4
refactor(hott): fix "sorry"s at int/basic.hlean, and comment the remaining "sorry"s
2015-07-27 08:34:11 -07:00
Leonardo de Moura
e969c7a8d6
refactor(library): remove 'simp' hack
2015-07-22 10:13:19 -07:00
Leonardo de Moura
267545ca0c
feat(frontends/lean): parse 'with_options' tactical
...
see issue #492
2015-07-13 19:13:41 -04:00
Leonardo de Moura
6ab5cf214c
feat(library,hott): add simp tactic reference
2015-07-13 18:01:40 -04:00
Leonardo de Moura
38d5c361df
refactor(hott/types/trunc): remove unnecessary fold
...
The new unfold tactic performs the fold automatically for us.
see issue #692
2015-07-12 13:07:18 -04:00
Leonardo de Moura
584f9e3f49
fix(library/tactic/unfold_rec): support indexed families at unfold_rec
...
This commit also removes many (now unnecessary) folds from the HoTT
library.
See issue #692
We still have to implement support for recursive definitions based on
brec_on that recurse over inductive families.
2015-07-12 12:32:58 -04:00
Leonardo de Moura
a9515ac7a4
feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function
...
See issue #692 .
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.
2015-07-08 21:19:18 -04:00
Leonardo de Moura
4b1b3e277f
feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'
...
see issue #693
2015-07-07 16:37:06 -07:00
Leonardo de Moura
68785b8bed
fix(library/tactic/generalize_tactic): fixes #711
2015-06-26 19:35:30 -07:00
Leonardo de Moura
de90926eed
refactor(hott): adjust HoTT library to new support for projections
2015-06-26 17:18:30 -07:00
Floris van Doorn
69f91bfd86
fix(types/nat/hott): workaround failed inductions
2015-06-25 23:13:47 -04:00
Floris van Doorn
24762fe843
feat(hit): add hits with 2-path constructors
...
In hit.two_quotient we define a general construction to define hits with 2-dimensional path constructors, similar to quotients.
We can add 2-paths between any two 'words', where a word consists of 1-path constructors, concatenation and inverses.
We use this to define the torus, reflexive quotients and the reduced suspension.
There is still one 'sorry' in the construction
2015-06-25 22:31:41 -04:00
Floris van Doorn
df3ce2b00b
feat(types/eq2): add theorem about eq_of_con_inv_eq_idp
2015-06-25 22:31:41 -04:00
Floris van Doorn
c8eee66c5b
feat(hott/relation): add equivalence closure of a relation
2015-06-25 22:31:41 -04:00
Floris van Doorn
b94b66243e
feat(hott/types): add some theorems about operations of 2-paths
2015-06-25 22:31:41 -04:00
Floris van Doorn
ea0f57aef5
feat(hott): various clean-up and small additions
2015-06-25 22:31:40 -04:00
Floris van Doorn
2748525c21
feat(hit/susp): finish the proof that loop space is adjoint to the suspension
2015-06-25 22:31:40 -04:00
Floris van Doorn
124c9d3d8a
feat(hott): various cleanup and fixes, rename \~ to ~, expand types.pointed
2015-06-25 22:31:40 -04:00
Floris van Doorn
ac03bf7a4a
feat(hott/nat): prove computation rule for cases by inequality
2015-06-25 22:31:40 -04:00
Floris van Doorn
0b9c8e14a4
fix(*/init/nat): fix occurrences where both theorem and [unfold-c] were used
2015-06-25 22:31:40 -04:00
Floris van Doorn
fa1979c128
feat(datatypes): let the type of unit be the lowest non-Prop universe
...
The definitional package (brec_on and cases_on) now use poly_unit instead of unit
closes #698
2015-06-25 17:33:46 -07:00
Leonardo de Moura
cfafc90cc0
refactor(hott,library): make sure files compile even without using "projection macros"
2015-06-22 12:22:11 -07:00
Leonardo de Moura
e382f7c2f9
refactor(hott/algebra/field): cleanup
...
use same definition used in the standard library.
2015-06-21 15:58:54 -07:00
Leonardo de Moura
5830d7d037
refactor(hott/algebra/category/yoneda): reduce compilation time using 'rewrite' tactic
2015-06-18 15:52:08 -07:00
Leonardo de Moura
a4c0699e81
feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic
...
See issue #676
Add new test demonstrating why it is useful to have the old semantics
for 'constructor'
2015-06-17 23:48:54 -07:00
Jeremy Avigad
6b36076ab5
feat({library,hott}/init/nat): add sub_le_succ
2015-06-15 22:53:11 +10:00
Jeremy Avigad
3b010b8c92
feat({library,hott}/algebra/group): add abbreviations e.g. for mul.cancel_left
2015-06-15 22:53:11 +10:00
Jeremy Avigad
a4a8253f50
refactor(library,hott,tests): rename succ_inj to succ.inj, add abbreviation eq_of_succ_eq_succ
2015-06-15 22:52:38 +10:00
Leonardo de Moura
62e1be897c
test(hott/algebra/category): test new 'abstract ... end' expression in the HoTT library
2015-06-12 17:53:01 -07:00
Leonardo de Moura
8b7dc4e03a
feat(frontends/lean): apply eta-reduction in postprocessing step
...
Perhaps, we should add an option to disable this new feature.
Remark: this commit makes commit 46d418a46d418a
2015-06-10 16:29:30 -07:00
Leonardo de Moura
01127061f5
refactor(hott/arity): cleanup
2015-06-10 15:45:46 -07:00
Leonardo de Moura
4b91cfccff
feat(frontends/lean/builtin_exprs): make notation ( e : T ) builtin
...
In the previous approach, the following (definitionally equal) term was being generated
(fun (A : Type) (a : A), a) T e
2015-06-10 14:52:59 -07:00
Floris van Doorn
f995e5ea48
fix(cubical): remove unused basic file
2015-06-04 20:21:52 -04:00
Floris van Doorn
ff41886a32
feat(nat/bquant): give instances for quantification bounded with le
...
also add theorems c_iff_c to logic/connectives, where c is a connective
2015-06-04 20:14:13 -04:00
Floris van Doorn
7f5caab694
feat(nat): redefine le and lt in the standard library
2015-06-04 20:14:13 -04:00
Floris van Doorn
ff01774fd7
renaming(hit): rename type_quotient to quotient, and quotient to set_quotient
...
This renaming is because type_quotient is a nonstandard name. I've had a discussion with Egbert
Rijke, Steve Awodey and Dan Licata, and the consensus for a better name was 'quotient'. I had to
make changes in src/kernel/hits/hits.cpp, I renamed g_type_quotient* by g_hit_quotient* (to avoid
name clash the standard library quotient, although I don't know whether that name clash would
matter).
2015-06-04 20:14:13 -04:00
Floris van Doorn
06528c4791
refactor(types): create cubical subfolder, update markdown files
2015-06-04 20:14:13 -04:00
Floris van Doorn
33e948d9d1
feat(hit/sphere): Prove that maps from S^n to an (n-1)-type are constant
2015-06-04 20:14:13 -04:00
Floris van Doorn
876aa20ad6
feat(hott): Port remainder of §6.3 and §7.2 from the HoTT book
...
Also prove a theorem similar to Lemma 7.3.1
There are still some sorry's in hit.suspension
2015-06-04 20:14:12 -04:00
Floris van Doorn
883b4fedb9
feat(hott): start with proof to characterize (is_trunc n A) using iterated loop spaces
2015-06-04 20:14:12 -04:00
Floris van Doorn
4117455e97
feat(hott): redefine nat.le and nat.lt
...
also some minor modifications in other files
2015-06-04 20:14:12 -04:00
Floris van Doorn
d4a991ef84
feat(hott): define cubes and cubeovers
2015-06-04 20:13:53 -04:00
Jeremy Avigad
fabdae6d54
refactor(hott/algebra/ring.lean,ordered_ring.lean): rename some theorems
2015-06-01 12:35:44 +10:00
Leonardo de Moura
ca110012d8
feat(library/tactic): automate "generalize-intro-induction/cases" idiom
...
closes #645
2015-05-30 21:57:28 -07:00
Leonardo de Moura
6f6848968d
feat(frontends/lean/coercion_elaborator): "coercion lifting" for backtracking case
...
closes #252
2015-05-30 16:44:26 -07:00
Leonardo de Moura
00232e70d6
feat(hott,library): auxiliary theorems for simplifier
2015-05-27 16:35:56 -07:00
