Bug fix: Properly handling sort universe at smt level

[etiennejf]

Bug fixing Smt translation of sort universe

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. Hence,
    • Flag typeUniverse has been removed from the Translation environment
    • sortCache has been renamed to typeParamCache to avoid any confusion
    • Map indTypeInstCache is used to cache type universe instances that have already been defined at the smt level instance.
    • defineTypeSort is now generic
    • Term typeSymbol and typeSort have been removed
    • sortNamtToSmtSymbol has been renamed to typeParamNameToSmtSymbol to avoid any confusion
    • declareTypeSort has been removed
    • definedSortAndCache has been renamed to defineTypeParamAndCache to avoid any confusion and now also accepts an IndTypeDeclaration instance as argument.
    • generateSortInstDecl has been updated to declare a unique type universe instance at the smt level for each unique sort instance considered as type universe.

• 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.
  • Issue25.lean has been updated to avoid wrong sort unification
  • Diagnosis in Issue27.lean has been updated to reflect current implementation

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]

I don't have specific lines to point this to but I wrote a serie of tests and some of them are showing some difference between the Lean universe types, and the SMT encoding

variable (β : Type u)

theorem universe_given_fixed_test0 :
  (∀ (x : β) (f : β → Nat), f x > 10) →
  (∀ (α : Type u) (x : α) (f : α → Nat), f x > 10) := by
  sorry

#solve [universe_given_fixed_test0]

Caution

Blaster solves this. I don't think it should because the premise is about a particular β from Type u, not all "Type u"

As expected, using an axiom leads to the same result

axiom FixedType : Type u

theorem universe_given_fixed_test (FixedType : Type u) :
  (∀ (x : FixedType) (f : FixedType → Nat), f x > 10) →
  (∀ (α : Type u) (x : α) (f : α → Nat), f x > 10) := by
  intro h a x f
  sorry

#solve [universe_given_fixed_test]

Caution

Same as before

Blaster reaches an error on this example:

theorem exists_must_match_forall :
  ∀ (α : Type u), (∃ (β : Type u), α = β) := by
  intro α
  exact ⟨α, rfl⟩

#solve [exists_must_match_forall]

Caution

genExistsTerm: only one predicate qualifier premise expected but got []

And another error on this one

theorem doesBlasterFindsNat : 
  ∃ (α : Type), α = Nat := by
  exact ⟨Nat, rfl⟩

#solve [doesBlasterFindsNat]

Caution

translateConst: unexpected inductive datatype Lean.Expr.const `Nat []

Which I think is unrelated to this PR, but I just mention it anyway