Andrej Dudenhefner

Avoiding Let ... Qed

1

As pointed out in (https://github.com/coq/coq/issues/10459) and (https://github.com/coq/coq/issues/13584), semantics of `Let ... Qed.` are not coherent / future proof, and also slow down interface file `vos` compilation. Currently, the library contains...

CI cache does not update

6

Currently, after each PR the CI runs `opam upgrade` each time resulting in `upgrade coq 8.12.0 to 8.12.1`. This should be done by the cache (and run only once) which...

Computability: L -> MMA /\ MMA -> TM

6

As previously discussed with @yforster, this PR replaces the laborious, direct `L_computable -> TM_computable` proof by a shorter `L_computable -> MMA_computable`, `MMA_computable -> TM_computable` variant with several benefits. - no...

[stdlib] well-founded list extension

3

Added the following results - well-founded list extension `list_ext` of a well-founded relation (lemma `wf_list_ext`) - infrastructure lemmas `list_ext_inv`, `list_ext_nil_r`, `list_ext_Acc_app`, `Acc_list_ext`, `clos_trans_list_ext_nil_l`, `list_ext_app_l`, `list_ext_app_r`, `clos_refl_trans_list_ext_app_l`, `clos_refl_trans_list_ext_app_r`, `clos_trans_list_ext_app_l`, `clos_trans_list_ext_app_r` -...

- added higher-order matching wrt. beta-equivalence `HOMbeta` - added reduction from `SSTS01` to `HOMbeta` resulting in `undecidable HOMbeta` The reduction is quite different from the known technique by Loader [1]....

faster PCUICSR

3

Replaced slow `firstorder` calls by appropriate `constructor`, `left`, `right` calls. This improves performance from `5m49.68s | 2644580 ko | PCUICSR.vo` to `0m49.37s | 1443968 ko | PCUICSR.vo`, also improving overall...

destruct produces an ill-typed term

3

### Description of the problem The tactic `destruct` constructs an ill-typed term which closes the goal (using `reflexivity`) but fails on `Qed`. Possibly connected to #16900. ### Small Coq file...

Now `Fin.case_L_R'` and `Fin.case_L_R` can be used in computation, similarly to `Fin.caseS'` and `Fin.caseS`. Added lemmas `Fin.case_L_R'_L`, `Fin.case_L_R'_R`, `Fin.case_L_R_L`, `Fin.case_L_R_R`, which are now provable. - [x] Added **changelog**.

Universe inconsistency involving template poly and canonical structure since 8.21

15

### Description of the problem Between `8.20.0` and current `8.21+alpha` for (to me) unclear reasons there are universe inconsistencies in [coq-library-undecidability](https://github.com/uds-psl/coq-library-undecidability/tree/master). ### Small Coq file to reproduce the bug ```coq...

separated L extraction framework

6

Currently, no undecidability and computability result strictly depends on the L extraction framework. In order to improve maintainability of the library, the L extraction framework is moved to a separate...