139 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Niels	74cd449f7b	Elements of union	2017-05-24 14:52:52 +02:00
Dan Frumin	826b6ba233	Port the FiniteSets library to HitTactics	2017-05-24 13:54:00 +02:00
Dan Frumin	25d1e1c969	Merge hrecursion into master	2017-05-24 13:00:56 +02:00
Niels	6ffbbb440f	More absorbtion	2017-05-24 12:10:39 +02:00
Niels	565fecec30	Changed names, further work on distributive laws	2017-05-24 11:47:30 +02:00
Niels	e63f1b8bf5	One absorption law	2017-05-23 23:24:22 +02:00
Niels	2f7840c494	Associativity of intersection.	2017-05-23 22:58:35 +02:00
Niels	0bdbcdfc6c	Recursion rule is now defined via induction.	2017-05-23 21:50:26 +02:00
Niels	6bb5e8b690	Added idempotency of the intersection	2017-05-23 21:31:45 +02:00
Leon Gondelman	13737556c6	Setup for finite sets library.	2017-05-23 16:30:31 +02:00
Dan Frumin	5abf0acf06	Switch to the DecidablePaths typeclass	2017-05-23 12:12:22 +02:00
Dan Frumin	ebdaab4de0	Merge Leon's changes into hrecursion	2017-05-23 12:02:06 +02:00
Dan Frumin	9d9b7a4713	Prettify FinSets	2017-05-23 11:58:09 +02:00
Leon Gondelman	afdc4a3e6b	intersection_comm	2017-05-23 11:50:52 +02:00
Dan Frumin	2f68e833af	Finish the comprehension_idem proof with functional extensionality	2017-05-23 00:17:33 +02:00
Niels	c024e27338	Further work on associativity of union.	2017-05-22 23:05:43 +02:00
Dan Frumin	f23d4aeacb	Replace the canonical structures mechanism for recursion with type classes ... See changes in HitTactics.v	2017-05-22 21:06:13 +02:00
Niels	6340f4cd77	Work on finite sets	2017-05-22 18:11:47 +02:00
Dan Frumin	5e594d10f0	Some modifications to the finset module	2017-05-22 17:01:19 +02:00
Niels	b85976a96d	Added Agda code for some HITs	2017-05-22 16:46:58 +02:00
Niels	27d78e1e75	Better gitignore	2017-05-22 16:45:51 +02:00
Dan Frumin	399fab467b	Package both the induction and recursion principles in the same record	2017-05-20 14:05:46 +02:00
Dan Frumin	75120ba602	Update the README	2017-05-18 17:46:00 +02:00
Dan Frumin	44da34d72f	Add a general hit recursion tactic. ... The tactic resolves the induction principle for a HIT using Canonical Structures, following the suggestion of @gallais	2017-05-18 17:43:19 +02:00
Dan Frumin	e81986a920	Add .gitignore and remove the makefile	2017-05-18 17:12:42 +02:00
Dan Frumin	f4bfeb98ca	Add a _CoqProject and a makefile	2017-05-01 19:25:27 +02:00
Niels van der Weide	16f1ab86cb	Expressions	2017-05-01 17:27:49 +02:00
leon-gondelman	14cf6c1031	Add files via upload	2017-04-19 17:16:17 +02:00
nmvdw	0cc0ecfd48	added proof that two reps of Z are iso (if everything set)	2017-01-10 23:46:50 +01:00
nmvdw	21120740b9	Delete HITs.pdf	2017-01-02 13:47:45 +01:00
nmvdw	f76992bb19	Update README.md	2017-01-02 13:45:04 +01:00
nmvdw	c6231c65f7	Add files via upload	2017-01-02 13:44:44 +01:00
nmvdw	3cb7d2c84c	Delete Scriptie.pdf	2017-01-02 13:44:29 +01:00
nmvdw	55dd79d144	Update README.md	2017-01-02 13:43:42 +01:00
nmvdw	e46b93cf69	Add files via upload	2017-01-02 13:42:29 +01:00
nmvdw	5608c93b39	Add files via upload	2017-01-02 13:15:17 +01:00
nmvdw	3999bbdd18	Add files via upload	2017-01-02 13:08:36 +01:00
nmvdw	3f16a48ac9	Update README.md	2017-01-02 13:07:50 +01:00
nmvdw	48c6729b04	Initial commit	2017-01-02 13:06:35 +01:00