Add modules

[AmosNico]

Add modules to the repository.

Lemmas and definitions are now private by default instead of public in most files (with the exception of Basic.lean, where I decided to make the section public, since most definitions are used in other files). I tried to keep the private/public settings the same as they were before, but it might make sense to make more of them private.

Currently BDD.lean publicly imports Bdd.Basic (via the public imports Bdd.Sim, Bdd.Lift and Bdd.Count), which is probably not wanted. The first two imports are needed for instDecidableSimilar, the last one for the Fintype instance for Vector, which is used in the lemma count_eq_card. The imports for instDecidableSimilar might not be needed in the future, but I am not sure whether we can avoid them now. The Fintype-instance for Vector could be moved to another file, which is then imported publicly (I think eventually this should be added to Mathlib, so I would place it in a separate file Upstream.lean/Preliminaries.lean, though it could probably also be placed in Nary).

This pull request depends on #6.

[AmosNico]

I am struggling to port Sat.lean (and therefore also SatSolver.lean), to the module system. Adding module on top of the file breaks the proof proof of BDD_of_CNF_correct and instDecidableUnsat . The modified proof below seems to be valid Lean 4 code, but still it fails with the following message:

(kernel) application type mismatch
  (Vector.ofFn f)[↑head.1]
argument has type
  (BDD.var ↑head.1).nvars ≤ n
but function has type
  (fun x i ↦ i < n) (Vector.ofFn f) ↑head.1 → Bool

lemma BDD_of_CNF_correct {n} {f : Fin n → Bool} (C : Std.Sat.CNF (Fin n)) :
    Std.Sat.CNF.eval f C = (BDD_of_CNF C).denotation (n := n) (by simp) (Vector.ofFn f) := by
  rcases C with ⟨⟨clauses⟩⟩
  simp only [Std.Sat.CNF.eval, List.size_toArray, List.all_toArray', BDD_of_CNF, List.map_toArray,
    List.length_map, List.foldr_toArray']
  induction clauses with
  | nil => simp only [List.all_nil, List.map_nil, List.foldr_nil, BDD.const_denotation,
    Function.const_apply]
  | cons head tail ih =>
    simp only [List.all_cons, List.map_cons, List.foldr_cons, BDD.and_denotation]
    rw [ih]
    congr 1
    induction head with
    | nil => simp [BDD_of_clause]
    | cons head tail ih =>
      simp only [Std.Sat.CNF.Clause.eval_cons]
      rw [ih]
      simp only [BDD_of_clause, List.map_cons, List.foldr_cons, BDD.or_denotation]
      congr 1
      simp only [BDD_of_literal]
      split
      · simp only [beq_true, *, BDD.var_denotation]  -- BDD.var_denotation seems to cause this
        symm
        apply Vector.getElem_ofFn
      · simp only [beq_false, BDD.not_denotation, BDD.var_denotation, *, Bool.not_inj_iff] 
        symm
        apply Vector.getElem_ofFn

[AmosNico]

The issue mentioned above has been fixed in #4 , by adding an additional argument i < n to the lemma var_denotation.