Code

Universes clause check#704

Code

Draft

mattam82 wants to merge 33 commits intocoq-8.14MetaCoq/metacoq:coq-8.14from universes-clause-checkMetaCoq/metacoq:universes-clause-checkCopy head branch name to clipboard

+4,387-89

Commits

Commits on Apr 27, 2022

• A try at modeling the algorithm by Bezem et al

  mattam82

  committed
  c1b4d08

  Copy full SHA for c1b4d08

• Terminating but incorrect loop check

  mattam82

  committed
  3b59d47

  Copy full SHA for 3b59d47

Commits on Apr 28, 2022

• Improved version, whose termination relies on the correctness of check_model

  mattam82

  committed
  15d240f

  Copy full SHA for 15d240f

• Move back to template-coq folder

  mattam82

  committed
  a0373f3

  Copy full SHA for a0373f3

Commits on Apr 29, 2022

• Improve the algorithm after discussion with Marc Bezem

  mattam82

  committed
  ba2b446

  Copy full SHA for ba2b446

• Comment a bit

  mattam82

  committed
  eeb372a

  Copy full SHA for eeb372a

Commits on Apr 30, 2022

• Try enforcing new constraints

  mattam82

  committed
  9e39fce

  Copy full SHA for 9e39fce

Commits on May 3, 2022

• Reorganize inner loop

  mattam82

  committed
  736e5f7

  Copy full SHA for 736e5f7

• Cleaner inner_loop

  mattam82

  committed
  7b6d289

  Copy full SHA for 7b6d289

• Finished inner loop

  mattam82

  committed
  0705f9a

  Copy full SHA for 0705f9a

• Inner loop termination proven

  mattam82

  committed
  29cbf61

  Copy full SHA for 29cbf61

• Before change of v_minus_w_bound

  mattam82

  committed
  6ccf15a

  Copy full SHA for 6ccf15a

Commits on May 4, 2022

• Prove the well-foundedness of loop

  mattam82

  committed
  c13abdf

  Copy full SHA for c13abdf

Commits on May 5, 2022

• Inner loop termination proof finished

  mattam82

  committed
  d760af6

  Copy full SHA for d760af6

Commits on May 6, 2022

• Finished all proofs

  mattam82

  committed
  661d8b7

  Copy full SHA for 661d8b7

• Finish proofs of auxilliary lemmas

  mattam82

  committed
  2f3d9e7

  Copy full SHA for 2f3d9e7

• Finished all proofs with new invariants

  mattam82

  committed
  ba17eb0

  Copy full SHA for ba17eb0

Commits on May 9, 2022

• Comments and extraction setup

  mattam82

  committed
  ac87ff7

  Copy full SHA for ac87ff7

• Abstract LoopChecking on level / sets / maps implementation

  mattam82

  committed
  c32a432

  Copy full SHA for c32a432

• Move clauses.v to LoopChecking and TemplateLoopChecking

  mattam82

  committed
  8920bf4

  Copy full SHA for 8920bf4

• Functorize the algorithm

  mattam82

  committed
  04d2b78

  Copy full SHA for 04d2b78

Commits on May 10, 2022

• Simplified loops

  mattam82

  committed
  5b63235

  Copy full SHA for 5b63235

• Cleaned up LoopChecking and TemplateLoopChecking

  mattam82

  committed
  7d6c51c

  Copy full SHA for 7d6c51c

• Support correct quoting/unquoting of the universe graph/context.

  Show description for 82ceebf
  mattam82

  committed
  82ceebf

  Copy full SHA for 82ceebf

• Add a new (extracted) plugin to test the loop checking algorithm.

  mattam82

  committed
  14092c3

  Copy full SHA for 14092c3

• Move back to subst_instance_cstr for level constraints

  mattam82

  committed
  0873c0d

  Copy full SHA for 0873c0d

• Move live tests of loop_checking to the test-suite

  mattam82

  committed
  3e93bbc

  Copy full SHA for 3e93bbc

• Revert changes to Universes.v

  mattam82

  committed
  9ce76db

  Copy full SHA for 9ce76db

• Avoid repeateadly folding over clauses in inner loop

  mattam82

  committed
  494abac

  Copy full SHA for 494abac

• Optimize a bit loop checking to avoid partitioning clause repeatedly

  mattam82

  committed
  4b65329

  Copy full SHA for 4b65329

• Fix UnivConstraint -> LevelConstraint change

  mattam82

  committed
  be94c63

  Copy full SHA for be94c63

• Remove useless extraction file in template-coq

  mattam82

  committed
  d9dc4a3

  Copy full SHA for d9dc4a3

• MSetList is no longer needed

  mattam82

  committed
  2549615

  Copy full SHA for 2549615