 Dan Frumin
|
eef533e345
|
Get rid of cow induction for the proof of closedUnion Bfin
|
2017-08-24 12:21:46 +02:00 |
|
|
Dan Frumin
|
e1a8220ba0
|
A simpler split fn for B-finite subobjects.
Allows for shortening of some proofs
|
2017-08-23 22:23:28 +02:00 |
|
|
Dan Frumin
|
f4d89f810c
|
Proof that the trunctation is really needed
If there is no 0-truncation then the resulting type is not an h-set.
|
2017-06-21 14:10:59 +02:00 |
|
|
Dan Frumin
|
ab48ab4a75
|
Decidable equality on FSets
|
2017-06-21 11:22:56 +02:00 |
|
|
Dan Frumin
|
1a3bb2cb5a
|
Use the [Functorish] instance from the HoTT library
|
2017-06-21 11:07:22 +02:00 |
|
|
Dan Frumin
|
a95ddea6ca
|
FSet is a strong powerset monad
|
2017-06-20 11:34:09 +02:00 |
|
|
Dan Frumin
|
47a38b3568
|
Separate the lattice properties proofs, get rid of the admits and general cleanup
|
2017-06-19 21:32:55 +02:00 |
|
|
Dan Frumin
|
8e6ab4c340
|
Separate the extensionality proof
and fix some tactics
|
2017-06-19 21:06:17 +02:00 |
|
|
Dan Frumin
|
490980db0f
|
Some cleanup for the extensionality proof
|
2017-06-19 12:24:57 +02:00 |
|
|
Dan Frumin
|
dce70f517f
|
Minor cleanup of some proofs
|
2017-06-16 13:24:54 +02:00 |
|
|
Dan Frumin
|
6971697c09
|
Add the difference operation
|
2017-06-14 18:06:16 +02:00 |
|
|
Dan Frumin
|
036d1599b2
|
Merge branch 'bloop'
|
2017-06-14 13:09:52 +02:00 |
|
|
Dan Frumin
|
abec9ecd00
|
Comment out the long min fn
|
2017-06-14 13:08:41 +02:00 |
|
|
Dan Frumin
|
a1a6912cb2
|
Use equiv_iff_hprop_curried from HoTT
|
2017-06-14 13:00:20 +02:00 |
|
|
Dan Frumin
|
06dc8a0acd
|
A proof of subset_isIn
|
2017-05-25 18:59:18 +02:00 |
|
|
Dan Frumin
|
294f818b07
|
Add [eq_subset] equivalence
X = Y <~> X ⊂ Y /\ Y ⊂ X
|
2017-05-25 16:28:09 +02:00 |
|
|
Dan Frumin
|
9202c6489d
|
Speed up the compilation of properties.v a little bit
|
2017-05-25 15:11:41 +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 |
|
|
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 |
|
|
Dan Frumin
|
2f68e833af
|
Finish the comprehension_idem proof with functional extensionality
|
2017-05-23 00:17:33 +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 |
|
|
Dan Frumin
|
5e594d10f0
|
Some modifications to the finset module
|
2017-05-22 17:01:19 +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 |
|