Properly handling sort universe at smt level

[etiennejf]

Properly handling sort universe at smt level

Description

This PR addresses issue #43 and perform the following modifications:

• Optimization:

  • We now explicitly normalize meta variables via normMVar. This function expects that each mvar must be assigned in the Lean4 environment when optimizeExpr is invoked. Otherwise an error is triggered
  • normFVar has been simplified to directly optimize any assigned value (if any). Indeed, any mvar in the assigned value will now be handled by normMVar.
  • normLevel has been updated to only normalize any universe level meta variable present in a given Level.

• Smt Translation

  • A type universe instance is generated at the smt level for each unique sort instance considered as a type universe.
  • Patch isSortOrInhabited to consider existsQuantifier flag to forbid sort type quantifier removal for existential quantifiers

• Blaster tactic

  • Quantifiers are no more reverted before translate.main is invoked (we are only reverting hypotheses). Indeed, we are now explicitly handling mvar instantiation at the preprocessing phase.

• Test suite:

  • Issue31.lean has been added to show that:
    • We are not wrongly unifying sorts with different universes at the smt level.
    • We are properly handling datatype used in expression (e.g., Nat = α, List Nat = α, etc)
  • Issue25.lean has been updated to avoid wrong sort unification
  • Diagnosis in Issue27.lean has been updated to reflect current implementation
  • Issue15.lean has been updated to consider new test cases
  • Issue20.lean has been updated to consider new test cases

Closes #32

Checklist

• All theorems valid for each formalization in CI
• All the specified lean file are properly considered when compiling and verifying the formalization
• Self review of the code has been done.
• Reviewer has been requested.
• Reviewer has performed the following tasks
  • Ensure that all the test cases are still valid
  • Ensure that each specified lean file is properly considered in the tool chain.

[RSoulatIOHK]

Apart from the known limitations currently, this works really well and is really elegant. Way more elegant than any solution I was considering.

[RSoulatIOHK]

The fold accumulates a (counter, hash) pair, right?
Shouldn't the final projection be .2 the accumulated hash rather than .1 (the counter) so that we can differentiate between List Nat and List Int for example?