vaibhavkarve / igl2020

Lean project for Fall 2020

igl2020

Lean project for Illinois Geometry Lab @ University of Illinois at Urbana-Champaign. This project started in Fall 2020 and is continuing in Spring 2021.

Aim

We formalize languages, structures, terms, formulae, sentences, first-order logic, Model theory, and O-minimality in the Lean theorem prover.

Participants

1. Tyler Behme
2. Eion Blanchard
3. Scott Harman
4. Philipp Hieronymi
5. Vaibhav Karve
6. Nikil Ravi
7. Joel Schargorodsky
8. Kay Thompson
9. Noble Wulffraat
10. Tianfan Xu
11. Andrew Yin
12. Fenglong Zhao

Installation

Install leanproject from this link following the instructions for your OS.

Navigate to the folder where you would like to clone this project.

Run the following $ leanproject get vaibhavkarve/igl2020 in your terminal or command prompt. This will create a new folder called igl2020 and it will copy mathlib oleans into it.

Updating the project

You do not need to run leanproject get ... after the first time. To get updated versions of all the files in this repository, you can run standard git commands like git pull as often as you want.

Files

All working code can be found in the src/ folder. No changes will be made to files outside the src/ folder.

igl2020's Issues

Add docstrings for instances defined on theories

igl2020/src/model.lean

Line 694 in 7e8efee

instance theory.has_mem : has_mem (sentence L) (theory L) := ⟨set.mem⟩

Make is a simple one-line docstring for each instance.

add definition for `full_theory`

igl2020/src/model.lean

Line 501 in 7e8efee

def full_theory : set (sentence L) := sorry

Define sentences within Lean

We want to be able to define sentences in Lean, which are formulas where every variable occurs bound. The way to do this will be to create var_list which will take in a formula and return a finite subset of the naturals that indexes which variables occur in the formula. This will be a recursive definition and will need to use the vars_in_term_t function. So the goal is to create the var_list function and then create a boolean is_sentence function which will map the var_is_bound function across the list, and then use this to define the subtype sentence analogously to how we have a subtype for admissible terms.

Change some defs to lemmas

The Lean linter is reporting that some of the lemmas have been incorrectly marked as defs. This can be fixed easily.
Full list of defs that need to change:

/- The `def_lemma` linter reports: -/
/- INCORRECT DEF/LEMMA: -/
#print type_is_struc_of_set_lang /- is a lemma/theorem, should be a def -/
#print type_is_struc_of_ordered_set_lang /- is a lemma/theorem, should be a def -/
#print magma_is_struc_of_magma_lang /- is a lemma/theorem, should be a def -/
#print semigroup_is_struc_of_semigroup_lang /- is a lemma/theorem, should be a def -/
#print monoid_is_struc_of_monoid_lang /- is a lemma/theorem, should be a def -/
#print group_is_struc_of_group_lang /- is a lemma/theorem, should be a def -/
#print semiring_is_struc_of_semiring_lang /- is a lemma/theorem, should be a def -/
#print ring_is_struc_of_ring_lang /- is a lemma/theorem, should be a def -/
#print ordered_ring_is_struc_of_ordered_ring_lang /- is a lemma/theorem, should be a def -/

Good challenge for anyone struggling to get more comfortable with git.

Rename terms and aterms

We decided that terms and aterms are not the best names in model.lean :-)

1. Change all occurrences of term to term'.
2. Change all occurrences of aterm to term.

Turn struc into a class

Currently, struc is defined as a structure in model.lean. We can redefine it as a class instead. This will be more in line with the way mathlib defines group and ring.

Note: There will be no need to use M.univ then.

fill in definition for creating a model on theory extended by a singleton sentence

igl2020/src/model.lean

Line 798 in 7e8efee

def model_of_extended {t : theory L} {μ : Model t} {σ : sentence L} (sat_σ: μ.M ⊨ σ) :

Interpret DLO inside of Lean

The theory of DLO (dense linear orders) without endpoints has only a binary relation in its language and has axioms that state precisely the binary relation is a dense linear order. Create the DLO_lang inside Lean and create comments inside Lean for the axioms of DLO in first-order logic.

Define equivalence of formulas

We say that two formulas are equivalent (w.r.t. a given structure) if their interpretations define the same set (there are a few equivalent definitions; I think this one is most straightforward for our purposes). This will give our notion of definable sets more utility once we have that established.

In Lean, we will take the sets defined by two formulas and check whether or not they contain exactly the same elements from the universe.

Prove theory of DLO has quantifier elimination

As a critical step in implementing o-minimality, we need to show that the theory of dense linear orders without endpoints (DLOWE or just DLO) admits quantifier elimination (QE). That is, we will show that any formula in our model (Q; <) is equivalent to a quantifier-free formula.

Prove theorem `term_sub_free`

Prove the theorem :

igl2020/src/model.lean

Line 333 in ecb04fe

theorem term_sub_free (t' t : term L)

Once done, also add a docstring explaining the theorem.

Add term-style proof of app_vec_partial

There is already a tactic-style proof of app_vec_partial here:

igl2020/src/model.lean

Line 83 in 2711656

def app_vec_partial {α : Type} {n m : ℕ} (h : m ≤ n) (f : Func α (n+1))

Given that this is a definition, it should be turned into a term-style proof. The first step of the proof is induction on m. This will translate into pattern matching on m. To allow pattern matching, the type of the function will have to be changed to

def app_vec_partial' {α : Type} {n : ℕ} : Π {m : ℕ},
  m ≤ n → Func α (n+1) → vector α (m+1) → Func α (n-m)
| 0 := sorry
| (m+1) := sorry

Note also that "induction on m" in the tactic-style proof indicates that this will be a recursive definition when translated to a term-style proof.

Prove lemma `models_formula_all_or_none_sentences`

The lemma currently has a skeleton proof but also has a few sorrys that need to be filled in.

Add definition of substructure

Noble suggested a definition for M1 "is a substructure of" M2, provided they are structures on the same language L.

Recursion in the definition of vars_in_term

I am attempting to define terms in a language L and am facing recursion issues.

I define terms in Line 203 and variables in terms in Line 212.

However, lean does not accept the definition of vars_in_term because it is an "unexpected occurrence of recursive function". My understanding is that lean can handle recursive definition as long as it is decreasing in one of its arguments.

So now my question is twofold --

1. is there an alternate definition of terms that might be easier to implement?
2. or, is there a way to create "graded" terms (graded by ℕ) so that we can show that the function vars_in_term is always decreasing the grading?

References:
Possibly relevant chapter from Theorem Proving in Lean

Define the expanded language

In order to properly interpret sentences inside a model, we need to expand our language. Given a language L and an L-structure M, we create a new language L_M which will contain a constant symbol for every element of the domain of M. A reference for this construction can be found in Lou Van Den Dries' logic notes: https://faculty.math.illinois.edu/~vddries/main2.pdf The relevant information is on page 33.

The sorry must be filled in this code-snippet:

def expanded_lang (L : lang)(M : struc L) : lang :=
  sorry

Define the expanded structure

In order to properly interpret sentences inside a model, we need to expand our language. Given a language L and an L-structure M, we create a new language L_M which will contain a constant symbol for every element of the domain of M. A reference for this construction can be found in Lou Van Den Dries' logic notes: https://faculty.math.illinois.edu/~vddries/main2.pdf The relevant information is on page 33.

Now that we have expanded our language, we must meaningfully interpret the new constants we introduced into the language. They should just be interpreted in the canonical way, that is to say, each element of the domain gave us a constant in the expanded language, and we just interpret it as that same exact element. The structure must satisfy that we have the same domain and all other symbols of the language have the same interpretation. Note that we do not have access to substructures or embeddings since the structures are over different languages.

The following code snippet is to be filled in:

def expanded_struc (L: lang)(M : struc L) : struc (expanded_lang L M) :=
  sorry

Prove lemma `iff_models_formula_relation_of_identical_var_assign`

We have a skeleton proof but some sorrys need to still be filled in.

Prove lemma `le_card_of_embedding`

Prove the lemma.

igl2020/src/model.lean

Line 218 in ecb04fe

lemma le_card_of_embedding {L : lang} (M N : struc L) (η : embedding M N) :

prove that isomorphic structures satisfy the same theory

igl2020/src/model.lean

Line 758 in 7e8efee

theorem isomorphic_struc_satisfy_same_theory (M₁ M₂ : struc L)

add statement and proof of lemma `eq_full_theory_iff_elementary_equivalent`

igl2020/src/model.lean

Line 505 in 7e8efee

lemma eq_full_theory_iff_elementary_equivalent : sorry :=

This depends on issue #75. Solve that first.

First-order logical statements for o-minimality

There are two equivalent definitions for o-minimality: a set-theoretic and model-theoretic one, both of which can be found on Wikipedia (https://en.wikipedia.org/wiki/O-minimal_theory). Try to write down what it means for a structure to be o-minimal in first-order logic, either as a code comment or just with pen and paper (or LaTeX if you prefer).

Add in examples of languages and structures

Several of the branches already have solutions to these "sorry"s. Your task is to create a pull request for (one or more) of these so that the solution can be merged into master.

• monoid_lang
• group_lang
• semiring_lang
• ring_lang
• ordered_ring_lang
• semigroup_is_struc_of_semigroup_lang
• monoid_is_struc_of_monoid_lang
• group_is_struc_of_group_lang
• semiring_is_struc_of_semiring_lang
• ring_is_struc_of_ring_lang
• ordered_ring_is_struc_of_ordered_ring_lang

Note: Do a few but not all of these. That will give others a chance to try these out as well and learn on their own.
Questions? Ask here or on Slack.

Add an inhabited instance for each new type declared in model.lean

Writing an inhabited instance for type A means proving that there is at least one term (a : A), i.e. the type is nonempty.
Inhabited instances are explained in TPIL here: https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#type-classes-and-instances

Currently, the following types are missing inhabited instances.

• substruc
• formula
• sentence
• theory
• complete_theory

Prove that a full theory is isomorphism invariant

igl2020/src/model.lean

Line 512 in 7e8efee

theorem full_theory_is_isomorphism_invariant {M N : struc L}

Depends on #75 and #76 . Solve those first.