Mentions légales du service

Skip to content

Native algebraic data types even in the presence of polymorphism

Jacques-Henri Jourdan requested to merge discriminate_alg into master
  • Added support for new metas for the eliminate_algebraic transform, letting control which types are eliminated and which are not.
  • In discriminate, added support for algebraic datatypes : duplicate propositions using algebraic datatypes to specialise algebraic datatypes instances. Then, it produces the new meta for instructing eliminate_algebraic to keep these instantiated datatypes.
  • Discrimination is now performed after eliminate_algebraic
  • Added support for algebraic datatypes in the polymorphism encoding.
  • Fixed sessions in examples
  • Simpify some sessions in examples to show that we are indeed gaining some proof power

There has been a few regressions: some old provers did not appreciate that we remove axioms about Booleans telling essentially that true != false. I fixed the corresponding proofs. Nightly works now fully.

Remaining problem to solve:

  • The CE bench of CI is not working correctly, and I don't really understand what is happening and whether this is a real problem. We need to talk about this.
Edited by Jacques-Henri Jourdan

Merge request reports