dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

Commit Graph

  • dad6686c4c Make everything work with the new notation Dan Frumin 2017-08-08 17:44:27 +0200
  • 80dabe3162 Get a quotient from an implementation Dan Frumin 2017-08-08 17:06:53 +0200
  • 3cda0d9bf2 Completely fixed notation Niels 2017-08-08 17:00:30 +0200
  • 92bc50d79f Improved notation to unicode Niels 2017-08-08 15:30:12 +0200
  • 2bdec415d9 Improved notatio Niels 2017-08-08 15:29:50 +0200
  • de335c3955 Added join-semilattice Niels 2017-08-08 13:45:27 +0200
  • c1dfef3cc1 Separated lemmas for extensionality for properties, added tactic toHProp Niels 2017-08-08 13:35:28 +0200
  • 4ade6e60cc Clean up the interface.v proofs Dan Frumin 2017-08-08 13:18:45 +0200
  • 4a98d84cbc Added separation Niels 2017-08-08 00:41:27 +0200
  • 76fe6faff2 Small improvements Niels 2017-08-07 23:27:53 +0200
  • 30004e1c8b Added membership of product Niels 2017-08-07 23:15:25 +0200
  • e498b93f16 Added product Niels 2017-08-07 22:13:42 +0200
  • 8c10ab1c0c More cleaning Niels 2017-08-07 16:57:21 +0200
  • 1e373364b2 Some cleaning in notation Niels 2017-08-07 16:49:46 +0200
  • 1bab2206a3 Some cleaning Niels 2017-08-07 16:22:55 +0200
  • a0844f6be4 Some simplifications in proofs, extra proofs for implementation Niels 2017-08-07 15:39:01 +0200
  • d5585f32c6 Added basis for reflection in interface Niels 2017-08-07 14:55:07 +0200
  • d9cde16f5a Added interface of finite stes Niels 2017-08-07 12:20:43 +0200
  • a1e940cc4d Added proof of HSet classes Niels 2017-08-04 20:55:47 +0200
  • 86b4f80aa5 Added proof that Z' is HSet. Niels 2017-08-04 20:54:53 +0200
  • efec2e88f8 Added old proofs in new style (missing: Z' is hset) Niels 2017-08-04 20:42:05 +0200
  • 8cf115c9ab Integers form initial ring. Niels 2017-08-04 17:26:04 +0200
  • 6a3965dfa7 Merge branch 'classes' of https://github.com/nmvdw/HITs-Examples into classes Niels 2017-08-04 14:52:56 +0200
  • 376efbf2e9 Integers form a ring Niels 2017-08-04 14:46:08 +0200
  • 6f016d1b7f Remove a useless vernacular command Dan Frumin 2017-08-03 23:25:25 +0200
  • 90d795b708 Correspondence between enumerated subobjects and k-finite subobjects Dan Frumin 2017-08-03 23:21:43 +0200
  • f106be08de Added merely decidable equality => LEM Niels 2017-08-03 23:01:57 +0200
  • 6d3d0eda9f Construct a mapping from [FSet] to enumerated subobjects Dan Frumin 2017-08-03 18:06:39 +0200
  • 69b4b6d7a5 Fix the implicit arguments for lattice operations Dan Frumin 2017-08-03 17:09:10 +0200
  • 72ce66f833 Make [enumerated A] an hProp & show that Kf => enumerated Dan Frumin 2017-08-03 17:00:02 +0200
  • c7e12d6d25 Enumerated implies Kurarowski-finite Dan Frumin 2017-08-03 15:10:01 +0200
  • 31889d4e48 A short lemma [FSet A = FSetC A] Dan Frumin 2017-08-03 14:43:42 +0200
  • 9cdfc671dc Added structure to k_finite sts Niels 2017-08-03 15:07:53 +0200
  • 0bdf0b79fe Added k_finite in coq project Niels 2017-08-03 13:54:02 +0200
  • efce779b06 Simplify some proofs and barely improve the compilation time Dan Frumin 2017-08-03 12:49:15 +0200
  • 241f5ea377 Added subobjects Niels 2017-08-03 12:27:43 +0200
  • fec00177ad Merge branch 'master' of https://github.com/nmvdw/HITs-Examples Niels 2017-08-03 12:24:39 +0200
  • 7d74b45fc3 Changed lattice Niels 2017-08-03 12:21:34 +0200
  • a61265585b Start proving that Mod2 is a semiring Dan Frumin 2017-08-02 21:58:26 +0200
  • 53e38f0238 Try out HoTTClasses Dan Frumin 2017-08-02 17:08:40 +0200
  • 8a65852d1b Fix compilation Dan Frumin 2017-08-02 15:45:12 +0200
  • 77a449e68b Added lattice constructions Niels 2017-08-02 14:21:12 +0200
  • 4141f9d456 Finalize the definition of K-finite (sub)objects Dan Frumin 2017-08-02 14:14:14 +0200
  • fa076f5f41 k-finiteness Niels 2017-08-02 13:30:25 +0200
  • 2ccece3225 Splitted cons_repr Niels 2017-08-02 11:40:03 +0200
  • 5ee7053631 Removed bad hints Niels 2017-08-01 17:35:23 +0200
  • e6bf0f9d5d Fixed NeutralL and NeutralR Niels 2017-08-01 17:25:57 +0200
  • b3b3e5b6c2 HProp is a lattice Niels 2017-08-01 17:12:32 +0200
  • 0de37d6cea Split the development into different directories Niels 2017-08-01 15:41:53 +0200
  • bae04a6d2b Lowercase enumerated Niels 2017-08-01 15:20:17 +0200
  • 1eec9628ce Lowercase files Niels 2017-08-01 15:13:52 +0200
  • fed9546d11 Some cleanup Niels 2017-08-01 15:12:59 +0200
  • 37e3017cfc Basic properties of enumerated sets Dan Frumin 2017-07-31 17:39:01 +0200
  • b06c59339b Small fix Niels 2017-07-31 14:54:20 +0200
  • 8ff9089d3d Added disjunction. Niels 2017-07-31 14:52:41 +0200
  • f4d89f810c Proof that the trunctation is really needed Dan Frumin 2017-06-21 14:10:59 +0200
  • ab48ab4a75 Decidable equality on FSets Dan Frumin 2017-06-21 11:22:56 +0200
  • 1a3bb2cb5a Use the [Functorish] instance from the HoTT library Dan Frumin 2017-06-21 11:07:22 +0200
  • 3274bed4e0 Lists and finite sets Niels 2017-06-20 17:33:35 +0200
  • c8a84349b1 Further work on lists (simple implementation) Niels 2017-06-20 15:08:52 +0200
  • 8c31e4d382 Lists implement finite sets Niels 2017-06-20 13:54:42 +0200
  • a95ddea6ca FSet is a strong powerset monad Dan Frumin 2017-06-20 11:33:13 +0200
  • 47a38b3568 Separate the lattice properties proofs, get rid of the admits and general cleanup Dan Frumin 2017-06-19 21:32:55 +0200
  • 8e6ab4c340 Separate the extensionality proof Dan Frumin 2017-06-19 21:06:17 +0200
  • 229df7b270 Shortened proofs Niels 2017-06-19 17:54:44 +0200
  • 5f4c834cbe Proofs of the lattice properties (via extensionality) Niels 2017-06-19 17:08:56 +0200
  • 57d8ee9d55 cons representation of finite sets Leon Gondelman 2017-06-19 16:06:04 +0200
  • 490980db0f Some cleanup for the extensionality proof Dan Frumin 2017-06-19 12:24:57 +0200
  • dce70f517f Minor cleanup of some proofs Dan Frumin 2017-06-16 13:24:54 +0200
  • 6971697c09 Add the difference operation Dan Frumin 2017-06-14 18:06:16 +0200
  • 036d1599b2 Merge branch 'bloop' Dan Frumin 2017-06-14 13:09:52 +0200
  • abec9ecd00 Comment out the long min fn Dan Frumin 2017-06-14 13:08:41 +0200
  • a1a6912cb2 Use equiv_iff_hprop_curried from HoTT Dan Frumin 2017-05-26 13:39:30 +0200
  • 2273ecaae0 Merge remote-tracking branch 'origin/leon' into properties Niels 2017-06-06 11:15:13 +0200
  • a98c56d154 changes Niels 2017-06-06 11:15:01 +0200
  • 0d210cae04 first step toward cons-union iso: construction of min function for FSet A, where A is Totally Ordered. To construct min, various lemmas about empty set are needed. This min function is constructed in a very inefficient way w.r.t. proofs of assoc, comm, etc. Leon Gondelman 2017-06-03 00:08:12 +0200
  • f8ed41e5fe trailing white spaces Leon Gondelman 2017-05-26 12:28:07 +0200
  • 2a561d4983 Finished proof of extensionality Niels 2017-05-25 22:21:19 +0200
  • 01e4cb982f Finished proof of extensionality Niels 2017-05-25 22:20:46 +0200
  • 954c273ddf Merge remote-tracking branch 'origin/bloop' into properties Niels 2017-05-25 21:51:27 +0200
  • 06dc8a0acd A proof of subset_isIn Dan Frumin 2017-05-25 18:59:18 +0200
  • 294f818b07 Add [eq_subset] equivalence Dan Frumin 2017-05-25 16:28:09 +0200
  • 9202c6489d Speed up the compilation of properties.v a little bit Dan Frumin 2017-05-25 15:11:41 +0200
  • 140b02e9f4 subset Leon Gondelman 2017-05-24 18:28:24 +0200
  • 74cd449f7b Elements of union Niels 2017-05-24 14:52:52 +0200
  • 826b6ba233 Port the FiniteSets library to HitTactics Dan Frumin 2017-05-24 13:54:00 +0200
  • 25d1e1c969 Merge hrecursion into master Dan Frumin 2017-05-24 13:00:56 +0200
  • 6ffbbb440f More absorbtion Niels 2017-05-24 12:10:39 +0200
  • 565fecec30 Changed names, further work on distributive laws Niels 2017-05-24 11:47:30 +0200
  • e63f1b8bf5 One absorption law Niels 2017-05-23 23:24:22 +0200
  • 2f7840c494 Associativity of intersection. Niels 2017-05-23 22:58:35 +0200
  • 0bdbcdfc6c Recursion rule is now defined via induction. Niels 2017-05-23 21:50:26 +0200
  • 6bb5e8b690 Added idempotency of the intersection Niels 2017-05-23 21:31:45 +0200
  • 13737556c6 Setup for finite sets library. Leon Gondelman 2017-05-23 16:30:31 +0200
  • 5abf0acf06 Switch to the DecidablePaths typeclass Dan Frumin 2017-05-23 12:12:22 +0200
  • ebdaab4de0 Merge Leon's changes into hrecursion Dan Frumin 2017-05-23 12:02:06 +0200
  • 9d9b7a4713 Prettify FinSets Dan Frumin 2017-05-23 11:58:09 +0200
  • afdc4a3e6b intersection_comm Leon Gondelman 2017-05-23 11:50:52 +0200
  • 2f68e833af Finish the comprehension_idem proof with functional extensionality Dan Frumin 2017-05-23 00:17:33 +0200
  • c024e27338 Further work on associativity of union. Niels 2017-05-22 23:05:43 +0200