swh:1:snp:f54a27e650a8acca38b6d19c9bf2c307c6c07756
Raw File
Tip revision: ebcd89f9c3f3d009e7b6fd5d65f31043d2abfff1 authored by Matthieu Sozeau on 19 January 2021, 14:59:22 UTC
Merge pull request #540 from yforster/coq-8.12-jan18
Tip revision: ebcd89f
TODO.md
# Small stuffs

- `assumption_context` should be a boolean function.

- remove duplication of eq_context / eq_context_upto  and eq_decl / eq_decl_upto

- Rename `mkApps_nested` into `mkApps_app` (et inverser la direction de la
  règle)

- Make `wf Σ` `wf_ext Σ` some typeclasses (as at the begining of PCUICCanonicity)
  et changer les : wf Σ -> en {wfΣ : wf Σ} partout, ce qui éviterait bien des
  conditions de bord triviales

- Make complilation of Checker plugin working again

- Remove PCUIC plugin target? And Extraction file?

- Remove remaining warnings.
  May needs `Set Warnings "-notation-overridden".`

- Replace all `eauto with pcuic` by `pcuic` or somehing like this and make
  this tactic available everywhere.

- Recompile the dpd-graph.

- Remove funext axiom from PCUICConfluence.

- Remove ProofIrrelevance axiom everywhere.

- Clean `Derive`s: always derive `Siganture`, `NoConf`, ... directly after the
  definition of the inductive. (To avoid doing it several times.)
  (Mostly done)
  
- Finish the PCUICSigmaCalculus proofs.

# Medium Projects

- Change Template-PCUIC translations to translate casts to applications of 
  identity functions (vm_cast, default_cast etc) to make the back and forth
  the identity and derive weakening/substitution/etc.. from the PCUIC theorems.
  Is that really better than identity functions?
# Big projects

- Refine the longest-simple-path algorithm on universes with the 
  Bender & al algorithm used in Coq, extended with edges of negative weight.
  Alternatively prove the spec for that algorithm. Refinement might be easier:
  it amounts to show that the new algorithm calculates the longest simple
  path between two universes. 

- Verify parsing and printing of terms / votour

- Primivite projections: we could be more relaxed on the elimination sort of the 
  inductive. If it is e.g. InProp, then all projections to types in Prop should
  be definable. Probably not very useful though because if the elimination is 
  restricted then it means some Type is in the constructor and won't be projectable.
  
- Verify the substitution calculus of P.M Pédrot using skewed lists at
  https://github.com/coq/coq/pull/13537 and try to use it to implement efficient explicit 
  substitutions.

## Website

Put a demo using JS-coq on the webiste


## Eta



## Template <-> PCUIC

- Finish the started proofs

- Prove that:
   Γ |- t : A   iff   [Γ] |- [t] : [A]

This is not obvious because we don't have that [ [t] ]⁻¹ = t. The casts are changed
into β-redexes, hence it is only β-convertible and not a syntactical equality.

- Deduce that we have weakening and substitution lemmas in Template from those of
  PCUIC.
back to top