46b354b | Dominique Larchey-Wendling | 03 April 2020, 12:42:19 UTC | update CeCILL license to 2.1 | 03 April 2020, 12:42:19 UTC |
c74841f | Yannick Forster | 06 March 2020, 10:35:48 UTC | Update README.md | 06 March 2020, 10:35:48 UTC |
0abe97a | Dominique Larchey-Wendling | 05 March 2020, 15:45:27 UTC | Merge pull request #37 from DmxLarchey/lmcs_ups changed name of lemma | 05 March 2020, 15:45:27 UTC |
599cb58 | Dominique Larchey-Wendling | 05 March 2020, 15:15:37 UTC | changed name of lemma | 05 March 2020, 15:15:37 UTC |
6bb9129 | Yannick Forster | 05 March 2020, 14:59:16 UTC | Merge pull request #36 from DmxLarchey/lmcs_ups Updates for the LMCS submission | 05 March 2020, 14:59:16 UTC |
d80d1a8 | Dominique Larchey-Wendling | 05 March 2020, 12:54:14 UTC | Removed dependency on Equations for inverting vec and pos dependent types. Possibly inversion lemma for ra_ca_c should be properly laid out instead of hand hacking inversions on a per-need basis which clogs the code | 05 March 2020, 12:54:14 UTC |
57a48d0 | Dominique Larchey-Wendling | 05 March 2020, 10:30:39 UTC | changed the defs of H10 and H10Z to (pos n,pos 0) instead of (pos n,Empty_set) | 05 March 2020, 10:30:39 UTC |
462c3a4 | Yannick Forster | 04 March 2020, 08:47:33 UTC | Merge pull request #31 from uds-psl/more_dprm new version of the DPRM which shows all availalable equivalences | 04 March 2020, 08:47:33 UTC |
5c66f33 | Yannick Forster | 03 March 2020, 17:18:51 UTC | Merge pull request #33 from lgaeher/master Fix makefile and coqdoc compilation | 03 March 2020, 17:18:51 UTC |
28de3a4 | Yannick Forster | 03 March 2020, 17:18:20 UTC | Merge pull request #34 from DmxLarchey/cleanup_murec_compiler Cleanup murec compiler, faster compile | 03 March 2020, 17:18:20 UTC |
70f6378 | Yannick Forster | 03 March 2020, 17:17:56 UTC | Merge pull request #35 from yforster/remove_admits Remove all admits | 03 March 2020, 17:17:56 UTC |
83f7410 | Yannick Forster | 03 March 2020, 16:18:02 UTC | Remove admits | 03 March 2020, 16:19:37 UTC |
ed1f939 | Yannick Forster | 03 March 2020, 10:40:12 UTC | remove axiom | 03 March 2020, 16:19:37 UTC |
19ba623 | Dominique Larchey-Wendling | 02 March 2020, 09:51:49 UTC | small updates | 02 March 2020, 09:51:49 UTC |
6a8aec1 | Dominique Larchey-Wendling | 01 March 2020, 23:14:18 UTC | changed Let in Local Definition in ra_mm_env. to avoid big environments than hinder the efficiency of the omega tactic | 01 March 2020, 23:14:18 UTC |
ab9b33d | Lennard Gäher | 22 February 2020, 18:52:46 UTC | remove parse-comments flag from coqdoc as this breaks doc generation (seems to be a bug in coqdoc as 'unknown token' stuff should not happen according to its documentation?) | 22 February 2020, 18:52:46 UTC |
d22f6f2 | Lennard Gäher | 22 February 2020, 18:50:55 UTC | fix makefile regression introduced by 6ddce394ca5bc2206f6e0e2bcecc0582e70fb6a3 | 22 February 2020, 18:50:55 UTC |
466d429 | Lennard Gäher | 22 February 2020, 18:03:30 UTC | fix html target in makefile | 22 February 2020, 18:03:30 UTC |
5a7d71a | Dominique Larchey-Wendling | 14 February 2020, 12:06:23 UTC | a prime testing procedure and nxtprime reflection tactic a discussion about the shape of possible and impossible fractran RE predicates | 14 February 2020, 12:06:23 UTC |
f6d4c4b | Dominique Larchey-Wendling | 13 February 2020, 22:54:16 UTC | added DPRM for unary predicates including fractran | 13 February 2020, 22:54:16 UTC |
8a3ceb3 | Dominique Larchey-Wendling | 11 February 2020, 13:54:48 UTC | new version of the DPRM which shows equivalence between the computational models of MM, µrec and the different variants of Diohantineness | 11 February 2020, 13:54:48 UTC |
aec2f58 | Dominique Larchey-Wendling | 07 February 2020, 14:16:36 UTC | Merge pull request #29 from yforster/H10Z Reduction from H10 to H10Z | 07 February 2020, 14:16:36 UTC |
605fa43 | Dominique Larchey-Wendling | 07 February 2020, 13:04:14 UTC | redefined H10Z as P(x1,...,xn) = 0%Z and removed dependency over Equations for depelim the pos lib already has inversion for pos (S n) as the tactic "invert pos p" some cleanup as well | 07 February 2020, 13:04:14 UTC |
e0b41e6 | Yannick Forster | 07 February 2020, 11:38:47 UTC | Reduction from H10 to H10Z | 07 February 2020, 11:38:47 UTC |
d552a7f | Yannick Forster | 06 February 2020, 17:42:03 UTC | Merge pull request #22 from uds-psl/better_bezout_extraction Construction of an H10C-universal µ-recursive function | 06 February 2020, 17:42:03 UTC |
468a538 | Dominique Larchey-Wendling | 06 February 2020, 14:55:18 UTC | Merge branch 'master' into better_bezout_extraction resync with updated master | 06 February 2020, 14:55:18 UTC |
9dddee6 | Yannick Forster | 06 February 2020, 13:25:32 UTC | Merge pull request #28 from yforster/mu_to_lambda Mu to lambda | 06 February 2020, 13:25:32 UTC |
c10a31c | Yannick Forster | 06 February 2020, 09:04:54 UTC | Merge remote-tracking branch 'origin/master' into mu_to_lambda | 06 February 2020, 09:04:54 UTC |
98cecb0 | Yannick Forster | 06 February 2020, 09:03:04 UTC | Merge pull request #26 from DmxLarchey/h10_journal A fork for smoother reduction dio_form -> dio_elem | 06 February 2020, 09:03:04 UTC |
2ef5eeb | Yannick Forster | 05 February 2020, 16:41:58 UTC | Added reduction from mu_halting to lambda calculus | 05 February 2020, 16:41:58 UTC |
91a93c4 | Yannick Forster | 04 February 2020, 11:54:14 UTC | progress | 04 February 2020, 11:54:14 UTC |
d575c85 | Yannick Forster | 04 February 2020, 10:01:36 UTC | first chunk on mu -> L | 04 February 2020, 10:01:36 UTC |
4ae7c7a | Dominique Larchey-Wendling | 31 January 2020, 21:45:56 UTC | some more remarks | 31 January 2020, 21:45:56 UTC |
1094251 | Dominique Larchey-Wendling | 31 January 2020, 21:38:52 UTC | reworked and cleanup of the proof of Lagrange for better explanations | 31 January 2020, 21:38:52 UTC |
9bd5607 | Dominique Larchey-Wendling | 30 January 2020, 17:05:41 UTC | Merge pull request #1 from DmxLarchey/lagrange Added Lagrange's theorem | 30 January 2020, 17:05:41 UTC |
f03e863 | Dominique Larchey-Wendling | 30 January 2020, 16:00:08 UTC | finished the proof of Lagrange's theorem on the sum of 4 squares !!! | 30 January 2020, 16:00:08 UTC |
13d8cc8 | Dominique Larchey-Wendling | 30 January 2020, 12:13:25 UTC | nearly completed Lagrange's theorem ! | 30 January 2020, 12:13:25 UTC |
49fc9fe | Dominique Larchey-Wendling | 29 January 2020, 14:48:26 UTC | added the full statement of Luca's theorem | 29 January 2020, 14:48:26 UTC |
f7e9adc | Dominique Larchey-Wendling | 12 December 2019, 12:13:34 UTC | some cleanup in dio_logic and dio_bounded mostly better comments | 12 December 2019, 12:13:34 UTC |
eba1051 | Dominique Larchey-Wendling | 11 December 2019, 12:32:56 UTC | tracking duplications in encodings | 11 December 2019, 12:32:56 UTC |
8732580 | Dominique Larchey-Wendling | 11 December 2019, 12:18:13 UTC | starting to make optimisation with a less dramatic effect | 11 December 2019, 12:18:13 UTC |
55ee683 | Dominique Larchey-Wendling | 11 December 2019, 12:09:47 UTC | further optimisations of the encoding algo | 11 December 2019, 12:09:47 UTC |
0f138dc | Dominique Larchey-Wendling | 11 December 2019, 11:55:30 UTC | reintroduced x = y for smaller encodings | 11 December 2019, 11:55:30 UTC |
3639c3c | Dominique Larchey-Wendling | 11 December 2019, 08:28:27 UTC | some cleanup | 11 December 2019, 08:28:27 UTC |
46b3729 | Dominique Larchey-Wendling | 11 December 2019, 08:13:30 UTC | improvement in the shapa analysis to produce shorter formulas | 11 December 2019, 08:13:30 UTC |
3594fa3 | Dominique Larchey-Wendling | 10 December 2019, 15:04:50 UTC | better notation for De Bruijn extensions wrt the paper | 10 December 2019, 15:04:50 UTC |
fada11c | Dominique Larchey-Wendling | 10 December 2019, 13:17:10 UTC | a more systematic use of "dio by lemma" | 10 December 2019, 13:17:10 UTC |
b816b09 | Dominique Larchey-Wendling | 10 December 2019, 13:08:59 UTC | some more comments | 10 December 2019, 13:08:59 UTC |
c397f3e | Dominique Larchey-Wendling | 10 December 2019, 12:34:29 UTC | reworked the definitions dio_expr now becomes dio_fun which is much more acurate. It could be possible to rework the shape of the Diophantine characterization of alpha and expo to take dio_fun better into account ... | 10 December 2019, 12:34:29 UTC |
88e60c7 | Dominique Larchey-Wendling | 10 December 2019, 00:39:24 UTC | last cleanup for tonight | 10 December 2019, 00:39:24 UTC |
476e5f5 | Dominique Larchey-Wendling | 10 December 2019, 00:32:56 UTC | much more efficient and cleaner dio auto tactic the only problem is that the size of generate formula is increase at each cleaning changing atoms to elem simplified lost of proofs but got me much bigger encodings in the end ... it does really matter since efficiency is not the objective here | 10 December 2019, 00:32:56 UTC |
42b3c41 | Dominique Larchey-Wendling | 09 December 2019, 21:00:35 UTC | cleanup and replaced with dependent reduction ... maybe it would be good to move the definition of reduction_dependent from FRACTRAN_DIO.v to where is belongs ... somewhere in ILL.Definitions | 09 December 2019, 21:00:35 UTC |
f386a03 | Dominique Larchey-Wendling | 09 December 2019, 15:16:50 UTC | started modifying dio_logic to simplify atoms to something close to dio_elem | 09 December 2019, 15:16:50 UTC |
5c8a306 | Dominique Larchey-Wendling | 05 November 2019, 08:55:04 UTC | completed the missing lemma about the godel_beta encoding of list of triples | 05 November 2019, 08:55:04 UTC |
0961c52 | Dominique Larchey-Wendling | 04 November 2019, 14:40:19 UTC | added a second universal MuRec based on the alternate constraints of Andrej Dudenhefner 1+x+y^2=z it is 1/4 of the size of the previous one thanks to a much lighter use of decomp_r (which a big MuRec) Unfinished is the fact that nat_h10luc_surj the encoding of list h10uc into nat is total not that hard but a bit tricky though because of the flat_map replacing (x,y,z) -> x##y##z##vec_nil | 04 November 2019, 14:40:19 UTC |
d74c601 | Dominique Larchey-Wendling | 30 October 2019, 22:06:46 UTC | removed unneeded messages that were poluting the output of make | 30 October 2019, 22:06:46 UTC |
8c735b3 | Dominique Larchey-Wendling | 30 October 2019, 19:40:20 UTC | Merge branch 'master' into better_bezout_extraction | 30 October 2019, 19:40:20 UTC |
6ddce39 | Dominique Larchey-Wendling | 30 October 2019, 19:25:25 UTC | cleanup of the MM -> FRACTRAN_REG -> MMA2 reduction files remove some unneeded Check and Print Assumptions | 30 October 2019, 19:25:25 UTC |
50e31e6 | Dominique Larchey-Wendling | 30 October 2019, 17:40:18 UTC | removed .d files inherited from the CPP'19 developments | 30 October 2019, 17:40:18 UTC |
7750f3d | Dominique Larchey-Wendling | 29 October 2019, 23:43:21 UTC | Corrected for 8.8.2 and also cleanup of the mess arround FRACTRAN and MMA2 Now the reduction is MM -> FRACTRAN_REG -> MMA2 and FRACTRAN (non reg) halting could be removed but I also added the trivial FRACTRAN_REG -> FRACTRAN | 29 October 2019, 23:43:21 UTC |
fc3ec56 | Dominique Larchey-Wendling | 29 October 2019, 20:18:32 UTC | large cleanup of the construction of the universal recalg | 29 October 2019, 20:18:32 UTC |
ac854d0 | Yannick Forster | 29 October 2019, 11:04:00 UTC | Merge pull request #21 from uds-psl/murec A BIG commit containing the DIO_SINGLE -> µ-REC -> MM reductions | 29 October 2019, 11:04:00 UTC |
934f393 | Yannick Forster | 29 October 2019, 11:01:19 UTC | Merge pull request #18 from dominik-kirst/master Trakhtenbrot's theorem | 29 October 2019, 11:01:19 UTC |
992e9b1 | Dominique Larchey-Wendling | 28 October 2019, 22:07:51 UTC | added a universal µ-recursive algorithm of size 8708 and of arity 1 that can decide any H10C problem, hence its own termination problem must be undecidable | 28 October 2019, 22:07:51 UTC |
f190272 | Dominique Larchey-Wendling | 27 October 2019, 11:27:28 UTC | updated gcd and extension of the CRT for preparation with Godel Beta encoding of lists of nats | 27 October 2019, 11:27:28 UTC |
3dc1281 | Dominique Larchey-Wendling | 25 October 2019, 21:35:48 UTC | A BIG commit containing the DIO_SINGLE -> µ-REC -> MM reductions The details are going to be comment in the PR Notice that to avoid having several definitions of MM, I needed to generalize the definition to an arbitrary type of registers of which we only use the instance nat and pos _ but this implies changing mm_instr n with mm_instr (pos n) at not so many but several places in the code the rest will be commented in the PR description | 25 October 2019, 21:35:48 UTC |
833b141 | Yannick Forster | 25 October 2019, 16:55:45 UTC | Delete .DS_Store | 25 October 2019, 16:55:45 UTC |
0aee30f | Yannick Forster | 25 October 2019, 15:28:32 UTC | Merge pull request #17 from uds-psl/induction_on_PR Fixing the induction-on mess | 25 October 2019, 15:28:32 UTC |
0226fdd | Yannick Forster | 25 October 2019, 15:27:55 UTC | Merge pull request #16 from fakusb/patch-2 Require Program to avoid spurious compilation bug | 25 October 2019, 15:27:55 UTC |
a2d831c | Yannick Forster | 25 October 2019, 15:27:42 UTC | Merge pull request #15 from fakusb/patch-1 Update README.md | 25 October 2019, 15:27:42 UTC |
7e5482b | Yannick Forster | 25 October 2019, 15:18:38 UTC | fix equations import | 25 October 2019, 15:18:38 UTC |
3349e33 | Yannick Forster | 25 October 2019, 14:58:12 UTC | Full qualification for imports | 25 October 2019, 14:58:12 UTC |
f450bf3 | Fabian Kunze | 25 October 2019, 14:18:32 UTC | Update firstorder.v | 25 October 2019, 14:18:32 UTC |
0988442 | Fabian Kunze | 25 October 2019, 14:17:52 UTC | Requiring Program before using measure_wf and MR This hopefully fixes a spurious compilation bug that affects some users. WIP, DO NOT MERGE | 25 October 2019, 14:17:52 UTC |
8c6dd6c | Dominique Larchey-Wendling | 25 October 2019, 14:16:22 UTC | cleanup the induction-on tactic mess. remember induction-on revealed a bug in 8.10.0, hopefully getting fixed in 8.10.1 also remove unnecessary Check and Print Assumptions that were bloating the output of make all The one should compile under 8.9.1 (I tested it) | 25 October 2019, 14:16:22 UTC |
f5f16da | Yannick Forster | 25 October 2019, 14:11:26 UTC | take HOU in again | 25 October 2019, 14:11:26 UTC |
365201b | Dominik Kirst | 25 October 2019, 13:58:58 UTC | trakhtenbrot's theorem | 25 October 2019, 13:58:58 UTC |
3e4a9b8 | Fabian Kunze | 25 October 2019, 13:43:38 UTC | Update README.md Readme now adds opam repo for equations | 25 October 2019, 13:43:38 UTC |
b5c5e7d | Yannick Forster | 25 October 2019, 13:25:24 UTC | disable HOU to make travis work once | 25 October 2019, 13:25:24 UTC |
92e1029 | Yannick Forster | 25 October 2019, 10:57:36 UTC | Update opam | 25 October 2019, 10:57:36 UTC |
81eea1b | Yannick Forster | 24 October 2019, 09:27:22 UTC | Update README.md | 24 October 2019, 09:27:22 UTC |
47c8d17 | Yannick Forster | 23 October 2019, 14:54:12 UTC | travis icon | 23 October 2019, 14:54:12 UTC |
dbf4cf8 | Yannick Forster | 23 October 2019, 14:52:45 UTC | update README | 23 October 2019, 14:52:45 UTC |
34e8d80 | Yannick Forster | 23 October 2019, 14:09:53 UTC | Update README | 23 October 2019, 14:09:53 UTC |
4544d71 | Yannick Forster | 23 October 2019, 14:06:11 UTC | Add metacoq dependency to opam file | 23 October 2019, 14:06:25 UTC |
e406355 | Yannick Forster | 23 October 2019, 11:00:02 UTC | fix L for 8.9.1 | 23 October 2019, 11:00:02 UTC |
b68c48e | Dominique Larchey-Wendling | 16 October 2019, 08:59:50 UTC | some more in the README | 16 October 2019, 08:59:50 UTC |
5b17c1c | Dominique Larchey-Wendling | 16 October 2019, 08:57:16 UTC | added "good seed" tags | 16 October 2019, 08:57:16 UTC |
0346d27 | Dominique Larchey-Wendling | 16 October 2019, 08:51:07 UTC | Merge branch 'extraction' of github.com:uds-psl/coq-library-undecidability into extraction | 16 October 2019, 08:51:07 UTC |
b1b7e14 | Dominique Larchey-Wendling | 16 October 2019, 08:50:50 UTC | updated some links in README | 16 October 2019, 08:50:50 UTC |
f1ae464 | Yannick Forster | 16 October 2019, 07:57:17 UTC | we don't need all of metacoq | 16 October 2019, 07:57:17 UTC |
46ccb2e | Yannick Forster | 16 October 2019, 07:33:12 UTC | Merge pull request #12 from fakusb/mergedTMrepo Merged changes from TM-verification repository | 16 October 2019, 07:33:12 UTC |
fc165f4 | Fabian Kunze | 15 October 2019, 13:41:24 UTC | merged commits after 95967cf up to 31e8023765 verified-turing-machines repo | 15 October 2019, 13:44:17 UTC |
ffb39b7 | Yannick Forster | 10 October 2019, 19:14:10 UTC | Test for both 8.8.2 and 8.9.1 | 10 October 2019, 19:14:10 UTC |
549368f | Yannick Forster | 01 October 2019, 16:03:07 UTC | compilation works locally | 01 October 2019, 16:03:07 UTC |
2377511 | Yannick Forster | 01 October 2019, 10:14:15 UTC | travis typo | 01 October 2019, 10:14:15 UTC |
7ea5ad4 | Yannick Forster | 01 October 2019, 10:07:22 UTC | Use MetaCoq from opam | 01 October 2019, 10:07:22 UTC |
edddc56 | Yannick Forster | 01 October 2019, 08:57:36 UTC | Qualify all MetaCoq imports, reorder Makefile | 01 October 2019, 08:57:36 UTC |
9591c53 | Yannick Forster | 01 October 2019, 08:06:34 UTC | Fix MetaCoq import in _CoqProject | 01 October 2019, 08:06:34 UTC |
7386ea1 | Yannick Forster | 01 October 2019, 07:32:54 UTC | qualify metacoq import | 01 October 2019, 07:32:54 UTC |