Beginner Questions

Stream: general

[Clyde Watson]

I'm really new to LEAN (and anything like it), and I've had some problems that might be considered a little too simple.

[Clyde Watson]

Questions answered so far:

Let's say that I declared a variable a of type int. How do I attribute a value to it (let's say, 3)?

How would I define a function that searches for a given object in a list?

How do I know that I've reached the end of a list? I want to know this in order to compare if two strings have the same characters at the same positions.

Is there a document where I can check all the avaliable commands for Lean?

How would I declare a local variable inside a function?

New Questions:

Do string and list char represent the same type?

That's it, for now. Thank you all for your time and patience :)

[Simon Hudon]

First question: you want a definition. You do it with def my_def : int := 7

[Clyde Watson]

Thank you for that, Simon!

[Simon Hudon]

Second question:

def find (x : nat) : list nat -> option nat
| [] := none
| (y :: ys) :=
if x = y then some 0
         else do r <- find ys
                 return (r + 1)

[Clyde Watson]

Thanks again! :simple_smile: I will try to understand the code.

[Simon Hudon]

Don't hesitate to ask more questions. I tried to put as little mysterious stuff as possible but I think if you're not a Haskell adept, do, <- and return are not obvious.

[Mario Carneiro]

First one: Let's say that I declared a variable a of type int. How do I attribute a value to it (let's say, 3)?

The first thing to understand about lean is that it is a functional programming language. If you are used to a more traditional imperative programming language, like C, Java, Python, etc, then there is a bit of culture shock to be had. The big thing to know is that there are no "variables* in lean in the sense meant by this word in imperative languages. (My professor always said this was a bad name for them and preferred the term "assignable" for C/Java style mutable memory locations.) In lean, variables are things that you can substitute values for, but their values never change from the time they are declared. In an imperative language you would call these immutable variables, but there are no mutable variables in lean.

To declare a variable and give it a value, you can use let:

def f (x : nat) : nat :=
let y := 3 in ...

Here f is a function with an input variable of type nat, and inside the body of the function I've declared a variable y (also of type nat) with value 3.

[Mario Carneiro]

Second one: How would I define a function that searches for a given object in a list?

Third, that's related to the second one: How do I know that I've reached the end of a list? I want to know this in order to compare if two strings have the same characters at the same positions.

Usually, a function which is defined on lists will be done by pattern matching, as in Simon's code. This is done in the first two lines, with | [] := and | (y :: ys) :=. This says what to do if the list is empty, and what to do if it is nonempty with head y and tail ys. Defining the function this way automatically takes care of "knowing when I've reached the end of a list", because you can't even get the value from a list unless you are already in the nonempty case - the nonempty check and value retrieval happen at the same time.

[Mario Carneiro]

Here's a function that compares two strings and returns true iff they are equal:

def is_equal : list char → list char → bool
| []        []        := tt
| (x :: xs) []        := ff
| []        (y :: ys) := ff
| (x :: xs) (y :: ys) := (x = y) && is_equal xs ys

[Mario Carneiro]

Fourth: Is there a document where I can check all the avaliable commands for Lean?

This depends on what you mean by "command". There are relatively few actual keywords recognized by the lean language, and you can find a relatively complete list in chapters 4 and 5 of the lean reference manual.

[Mario Carneiro]

Fifth: How would I declare a local variable inside a function? I tried doing the following:

def example_def (a : int) : int :=
variable k : int

I have a feeling that I might have to use let k := int in ..., but I'm not really sure.

Since as mentioned there is no such thing as a local assignable in lean, the best you can do is to have a let declaration, which also requires that you provide the local variable with a value. This is because unlike most pointer based languages, there is no "universal null" value in all types - the values of a type are all explicitly determined by the type. So if you define a variable of type int, then it must contain an integer value, maybe 0 or 42 or something but "unassigned" is not an option. let k := int actually declares k to be a variable of type Type with value int, which is probably not what you want.

[Clyde Watson]

Don't hesitate to ask more questions. I tried to put as little mysterious stuff as possible but I think if you're not a Haskell adept, do, <- and return are not obvious.

You are right, it isn't that obvious. What does "some 0" mean?
I'm having some trouble understand the "do r <- find ys return (r +1)" part. Isn't find missing one argument, that is, the x that it's searching? Also, for some reason, Lean considers ys to have the type "option nat".

[Clyde Watson]

Thanks a lot for all the explanations, Mario! It really is a shock. It's the first time I'm seeing a functional programming language.

[Clyde Watson]

Here's a function that compares two strings and returns true iff they are equal:

def is_equal : list char → list char → bool
| [] [] := tt
| (x :: xs) [] := ff
| [] (y :: ys) := ff
| (x :: xs) (y :: ys) := (x = y) && is_equal xs ys

So, according to the piece of code you sent, whenever I want to compare two kinds of lists, I only have to "place them" side by side?

[Clyde Watson]

One new quesion: In Lean, are there any differences between string and list char?

[Simon Hudon]

You are right, it isn't that obvious. What does "some 0" mean?

some 0 could also be written return 0. Both are expressions of type option nat. option nat has two kinds of values none or some n where n is a natural number. That means option nat either contains a single natural number or nothing. return 0 comes in handy when you think of option nat as a sequential program that may fail or return a natural number. This leads us to your second question:

I'm having some trouble understand the "do r <- find ys return (r +1)" part. Isn't find missing one argument, that is, the x that it's searching? Also, for some reason, Lean considers ys to have the type "option nat".

I apologize, the expression has a syntax error in it. It should be do r <- find ys, return (r +1) (notice the comma in the middle). You can read it as "call find ys then, if it doesn't fail (i.e. produce the value none) take the result (a natural number), call it r and return from the sequence of two instructions with the value of r+1"

[Sean Leather]

One new quesion: In Lean, are there any differences between string and list char?

This is extracted from the core library (init/data/string/basic.lean):

/- In the VM, strings are implemented using a dynamic array and UTF-8 encoding. -/
structure string_imp := (data : list char)
def string := string_imp

[Mario Carneiro]

So, according to the piece of code you sent, whenever I want to compare two kinds of lists, I only have to "place them" side by side?

That's the way pattern match syntax works. In this case, since the type of the function is is_equal : list char → list char → bool, there are two arguments, both lists of chars, and so each case should include two variables, possibly broken into cases. In my code snippet I broke into all four cases, but you can combine some of them with wildcards _, depending on the function you are defining. You should read the second case | (x :: xs) [] := ff as being shorthand for the partial specification is_equal (x :: xs) [] = ff of the function is_equal.

[Mario Carneiro]

One new quesion: In Lean, are there any differences between string and list char?

Just to unpack Sean's answer a bit: In lean, a string is a wrapper around a list char. The wrapper is there because there is a change of underlying data representation - I believe string is stored as an array of bytes, while list char is a linked list, like all list structures.

In fact, the whole function is_equal already exists in lean so you don't need to define it - it's just a = b where a b : string. Pretty much all data types defined in lean have an equality test implemented, and you can write equality tests for your own data structures easily as well.

[Mario Carneiro]

Here's another way to write Simon's find function using pattern matching instead of monad notation:

def find (x : nat) : list nat -> option nat
| [] := none
| (y :: ys) :=
  if x = y then some 0 else
  match find ys with
  | none := none
  | some r := some (r + 1)
  end

The match acts just like the top level pattern match - it takes the result of find ys, which is an option nat, and breaks into cases depending on if it is none or some r for some r. I mentioned before that lean has no "universal null" value, but when you explicitly want to indicate a "null" value, you do it with the option type. Essentially, this function either returns a result, wrapped in some, or it returns failure to find the value, encoded as none here (you might use "null" for this in other languages).

[Kevin Buzzard]

@Clyde Watson I started with Lean after very little functional programming experience (I knew some python / java but only as a hobbyist; I am a professional mathematician). I found http://learnyouahaskell.com/ extremely helpful. Your questions about basic pattern matching seem to indicate that you might be able to learn a lot from this resource (or from some other Haskell learning resources, if the informality of this one is not to your taste). Basically the rule is that if you're defining functions on, or proving things about, so-called "inductive types" like the natural numbers or lists, then you use induction (or recursion), and a syntax which is a completely basic part of functional programming with these "|"s.

[Mario Carneiro]

terminology note: In Haskell, what we call "inductive types" are called (generalized) algebraic data types or GADTs

[Sean Leather]

I started with Lean after very little functional programming experience (I knew some python / java but only as a hobbyist; I am a professional mathematician). I found http://learnyouahaskell.com/ extremely helpful.

@Kevin Buzzard That's pretty cool that you used Learn You a Haskell for Great Good. Did you learn Haskell first and then move to Lean or use it as a tutorial about the related concepts in Lean?

[Kevin Buzzard]

I am not sure I have learnt Haskell in any real sense. The reason I mentioned it was that the website I mentioned showed me how to define functions on lists by recursion using exactly the notation that the OP was originally asking about. Basically my history was: hobbyist programmer (written simple Android apps in java etc), then in 2016 I attempted to read learnyouahaskell just because (a) I knew the people on our joint maths and computing degree had to learn it in their first term and (b) I'd had an undergraduate doing a maths project with me on elliptic curves and they'd used Haskell to write their code, and then later in 2016 I tried reading it again, and then in 2017 I started trying to code in Lean and then I went back to it for a third time and this time it all made sense. But the concept of defining a function on lists by defining it on the constructors was something which dawned on me on the first reading.

[Reid Barton]

Isn't find missing one argument

This is a syntactic oddity of lean--when referring to the thing currently being defined (here find) inside its own definition, parameters to the left of the colon (here (x : nat)) are fixed, and you don't even write them.

[Reid Barton]

So find ys inside the definition of find means the same as find x ys outside it

[Kevin Buzzard]

What does "some 0" mean?

I'll show you how to figure this out yourself!

One really important thing to learn in Lean is that every question of this form is a question which you can begin to investigate yourself, and the sooner you learn how to do this the sooner you can figure out what you need to learn next; you can ask really targetted questions which in general receive better answers.

Here's how you can use Lean to answer your own question, in VS Code. First open a completely new file called scratch.lean and let's see if we can isolate your question. Make this as the only line:

definition X := some 0

It works!

[technical note: This isn't always the case -- sometimes the thing you're trying to understand might rely on some file being imported or some namespace being open and you'll have to resort to right-clicking -- see later.]

Now we have X we can see what this some command really is -- it's defined in the root namespace and is in core lean, so it's probably important.

Now we can write stuff like

#check X

to see that X is a term of type option ℕ. So it looks like option is a function which eats ℕ. What is the type of ℕ? We just check with

#check ℕ

and we see that ℕ has type Type. So option is a function which eats something of type Type. We can look at what option is with

#check option

and we see it's a function from Type to Type (just ignore the universes, you can worry about these later). So some 0 is a term of type option ℕwhich has type Type. So that's where some 0 lives in the tree of terms, types and universes.

[Pro tip: always be checking there are no red underlines in your code. Sometimes random typos which you don't bother to fix can have weird consequences later on. Learn how to use sorry to fix red errors in half-written code]

We didn't look at any definitions yet, we just looked at the types of everything in sight. Everything has a type, and #check x tells you the type of x. Here is a simple picture of the entire type theory of Lean. There are six kinds of things. There are two universes, Type and Prop. A type is something of type Type, and a term is something of type α for α a type. A proposition is something of type Prop, and a proof is something of type H for H a proposition. That's it. The Type stuff is where computer programs live. Prop is where theorems and proofs live. So some 0 is a computable thing, it's a term of type option ℕ : Type.

Next let's actually unravel the definitions. Right-click on some in VS Code and select Go to definition (or left-click and press F12). A new file will open called core.lean and you'll be taken to about line 279 where you'll see that option α is an inductive type with two constructors: none and some val with val : α. So in abstracta your question is answered -- some is a constructor which takes n : ℕ and returns some n : option ℕ. We can just check that with

#check some

and the answer...looks a bit messy. It's clearly some kind of function, but there are question marks. If you don't like those ?M_1 things, you could use the following trick:

#check @some

which works with functions and which might produce nicer output. Now we see that some is actually a Pi type.

Here's a gist with all those commands in. One of the fiddly little VS Code options on the right is "show the output of all the #checks at once"; that might be the one you want here.

https://gist.github.com/kbuzzard/455709bfd5d8fed57f5e4321481adf5b

If you get stuck at some point, send the entire file as a gist (just google for how to do it) or, if it's got quite big, just a minimal working example of your question. It's much easier for experts to answer questions with the full file in front of them. Even experts make silly mistakes sometimes, which others can spot instantly. Actually, sometimes I find my own silly mistakes when I am making the minimal working example. And did I mention to make sure there are no errors in your file?

So that's option, and how to ask if you get stuck along the way. But if you want some more insight as to what the point of this type is, or perhaps want to know more about what an inductive type is or a Pi type, or what the different kinds of brackets all mean (round, squiggly, square), now is the time to go to the docs -- Theorem Proving In Lean is a really good place to look for basic stuff. It's here:

https://leanprover.github.io/theorem_proving_in_lean/

I find the web search functionality really hard to use though; there's a pdf download and I usually search with my pdf viewer and then maybe switch to the html manual later because it looks nicer, if I want to know more. If you want to know more about option then the fourth occurrence of " option " in the pdf is the one you want; it's on p101. There you can see a brief description of the point of option and examples of other inductive types which have similar structures. I wish I had learnt this method earlier -- it took a while to dawn on me that you could just work everything out by right clicking and figuring out if you were a term or a type, a proof or a proposition.

You also need to learn a kind of filter -- stuff you can just ignore for the time being. Stuff like typeclasses, opt_param/out_param, [stuff in brackets] and universes, you can start to worry about them later. Universes are to do with subtle set-theoretic issues like avoiding Russell's Paradox, and the other stuff is technical computer science stuff which you can just treat as magic for the time being. [Typeclasses are some crazy computer science generalisation of notation overloading]

[Amin Bandali]

Another beginner question here: Is it possible to "overload" an instance?

format has an instance for list α:
https://github.com/leanprover/lean/blob/e53f8021ec3bd8b6c7c2eb998932ec79cb941b18/library/init/meta/format.lean#L87-L92
And I'd like to customize that in various places. For instance, say, I'd want to drop the outer square brackets, or another time make the items semicolon-separated rather than comma-separated

[Simon Hudon]

It is possible but I wouldn't advise using it that way. Instead, you should explicitly invoke the formatting code that you're interested in. Just to be sure, can you show an example where that would be handy?

[Amin Bandali]

I see. The example I was aiming to use that for was a structure with a (exts : list string) field, which I wanted format using format!"EXTENDS {my_struct.exts}"

[Simon Hudon]

Yes, that's what I thought. If you replace format!"EXTENDS {my_struct.exts}" with `format!"EXTENDS {my_to_fmt my_struct.exts}" you should get the same result. Unlike in Haskell, Lean doesn't guarantee global uniqueness of instances so you have to be vigilant not to make the instance search more difficult

[Amin Bandali]

Thanks for the explanations :simple_smile: makes sense

[Guy Leroy]

Hi, I'm following a simple tutorial for Lean and an exercice is to define a curry function and an uncurry function.
Could anyone help me with this please?

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := sorry
def uncurry (α β γ : Type) (f : α → β → γ) : α × β → γ := sorry

[Chris Hughes]

If you have a : α and b : β then I can make an element of type α × β by writing ⟨a, b⟩. The pointy bracket is written with \<. If I have x : α × β, then x.1 is the first element of the pair and x.2 is the second element.

[Guy Leroy]

Oh thank you. I am still struggling though, the best I came up with is:

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ f x, f x.1 x.2
def uncurry (α β γ : Type) (f : α → β → γ) : α × β → γ := λ f a b, f ⟨a, b⟩

which is obvisouly wrong as the types don't match but I can't figure out how to make it work

[Guy Leroy]

Any other hint?

[Mario Carneiro]

Your answers are perfect, except they are swapped

[Sean Leather]

To add to Chris's answer, there are a couple of things you can do to learn what you need to do.

• × is notation for prod. How would you know this? You can do #print × in a file and see _ ×:35 _:34 := prod #1 #0.
• Want to find out more about prod, use #print prod.

@[derive list.cons.{0} pexpr ``(has_reflect) (list.nil.{0} pexpr)]
structure prod : Type u → Type v → Type (max u v)
fields:
prod.fst : Π {α : Type u} {β : Type v}, α × β → α
prod.snd : Π {α : Type u} {β : Type v}, α × β → β

• structures have a default constructor mk. Try #print prod.mk.
• Lastly, ⟨a, ..., z⟩ is the anonymous constructor that works for many structures and types.

[Chris Hughes]

They're not quite perfect. You need to get rid of the fs in the lambdas. In lean syntax anything before the colon doesn't need to be introduced with a lambda.

[Chris Hughes]

This is correct.

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ a b, f ⟨a, b⟩
def uncurry (α β γ : Type) (f : α → β → γ) : α × β → γ := λ x, f x.1 x.2

[Sean Leather]

Just to help you see, these are also possible:

def curry (α β γ : Type) : (α × β → γ) → α → β → γ := λ f a b, f ⟨a, b⟩
def uncurry (α β γ : Type) : (α → β → γ) → α × β → γ := λ f x, f x.1 x.2

[Guy Leroy]

Thank you all for the detailed answers! Greatly appreciate it

[Kevin Buzzard]

@Guy Leroy Everything is completely logical and you have a logical brain; I remember being confused about all of this a year ago. You came to my talk yesterday, right? alpha -> beta -> gamma is a type, and you make terms of that type using lambda. After the lambda you'd better take a term of type alpha and then a term of type beta, and then you need to return a term of type gamma. So now hopefully you can get your terms sorted out. For products however, you need to learn the notation. The type is \alpha \times \beta so now you need to know the constructor and the eliminators, which is a fancy way of saying that you need to know how to get something of type alpha x beta from a : alpha and b : beta (that's the constructor for the product) and then you also need to know how to get the things of type alpha and beta from the thing of type alpha x beta -- those are the eliminators. So that's three different pieces of notation -- one for making the product type (that's \times), one for the constructor (that's pointy brackets) and one for the elminators (that's the .1 and .2 notation). A year ago all of these were floating around in my head and I'd just try any of them until something worked. But now I realise that if you keep everything straight then it all starts fitting into place. The pointy brackets are often used for constructors, the dots are often used for eliminators (I hope they are called eliminators, I'm no expert) and the notation for the types depends on the type but is something you pick up as you go along.

[Kevin Buzzard]

As for the stuff before or after the colon, I've realised that this trips mathematicians up. I need to write something about functions. There's so much functiony stuff which CS people do which is very cool but which we don't see in maths at all! Even using functions as maps from props to props is new to mathematicians.

[Mario Carneiro]

Actually .1 is called a projection

[Mario Carneiro]

an eliminator is prod.rec for example

[Guy Leroy]

Thank you for the explanation. Yes I came yesterday. The syntax is slowly starting to make sense, I'm a bit confused at first as we were taught Haskell in first year and it has some similar features.

[Guy Leroy]

But I understand the curry/uncurry functions and their syntax now I think

[Kevin Buzzard]

an eliminator is prod.rec for example

Technical interlude: are the projections defined using prod.rec or are they inbuilt and appear like axioms when the product type is defined? I don't know how to figure this out. I guess they would be easy to define using prod.rec.

[Kevin Buzzard]

But I understand the curry/uncurry functions and their syntax now I think

When I did that exercise last year, the first thing I wanted to prove was that if you curried and then uncurried, you got back to where you started! But at that point in TPIL you don't have enough tools to do that.

[Kevin Buzzard]

"The dot operator is how you access the members of an object" I think I once read in a book on Java. Is this not the appropriate language in Lean? It feels like the same sort of thing.

[Mario Carneiro]

It's a bit hard to tell just by looking at the definition, but projections are defined using the recursor/eliminator

[Sean Leather]

In type theory, what is an eliminator, and what is its opposite?

[Sean Leather]

Conclusion: a projection is an eliminator.

[Mario Carneiro]

In lean, projections are a limited version of the cases_on eliminator

[Mario Carneiro]

They only work when the inductive only has one constructor (which is why they are only generated for structures)

[Mario Carneiro]

and they are obviously nonrecursive (in programming languages with a fixpoint operator this is not as important as it is in lean)

[Mario Carneiro]

The projections are even harder to unfold than I remember... Even #reduce doesn't unfold them, I have to unfold first to the underlying projection macro (printed as [prod.fst c]), and then force that to expand through a change:

#print prod.fst
-- @[reducible]
-- def prod.fst : Π {α : Type u} {β : Type v}, prod α β → α :=
-- λ (α : Type u) (β : Type v) (c : prod α β), [prod.fst c]
example {α β} (a : α × β) : prod.fst.{0 0} a = sorry :=
begin
  delta prod.fst,
  change @prod.cases_on _ _ _ _ _ = _,
  -- prod.cases_on a (λ (fst : α) (snd : β), fst) = sorry
end

[Sean Leather]

I tend to do cases a, dsimp while writing a proof, though I can usually remove the dsimp before I'm done.

[Kevin Buzzard]

Rohan Mitta has just asked me how to formalise an exercise on the topological spaces example sheet: prove that if T1 and T2 are topologies on X (i.e. T1 and T2 are sets of subsets of X) then their intersection is a topology.

[Mario Carneiro]

this is in lean already

[Kevin Buzzard]

That sounds like a question to me, but somehow when you formalise it in Lean it becomes more like a construction. I figured that he needed some predicate is_open_sets and I just glanced through the topological space lean file and didn't spot it

[Kevin Buzzard]

I'm sure it's in Lean already, they form some complete semilattice or whatever

[Mario Carneiro]

it's part of the construction of the complete lattice

[Kevin Buzzard]

I just saw that. But Rohan is trying to learn how to use Lean so I am happy to encourage him to figure this exercise out himself!

[Kevin Buzzard]

It's in Lean but it doesn't look like a proposition, it looks like a construction

[Kevin Buzzard]

Is is_open_sets in Lean? I couldn't find it

[Mario Carneiro]

it is a construction

[Kevin Buzzard]

It looks like an exercise

[Mario Carneiro]

what does is_open_sets mean?

[Kevin Buzzard]

is_open_sets is a map from set (set X) to Prop and it's the conjunction of the axioms saying that the sets are the opens in a topology. Am I not thinking straight?

[Kevin Buzzard]

And he wants to prove is_open_sets A and is_open_sets B implies is_open_sets (A intersect B)

[Kevin Buzzard]

Am I making sense?

[Kevin Buzzard]

definition is_open_sets {α : Type u} (is_open : set α → Prop) :=
  is_open univ ∧ (∀s t, is_open s → is_open t → is_open (s ∩ t)) ∧ (∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))

[Kevin Buzzard]

I think it's that

[Kevin Buzzard]

Now I can make the example sheet question into a proposition.

[Kevin Buzzard]

Is this some equivalent way of formalising the notion of a topological space? Why did we choose the other way?

[Kevin Buzzard]

definition is_to_top {α : Type u} (is_open : set α → Prop) (H : is_open_sets (is_open)) : topological_space α :=
{ is_open := is_open,
  is_open_univ := H.left,
  is_open_inter := H.right.left,
  is_open_sUnion := H.right.right
}

definition top_to_is {α : Type u} (T : topological_space α) : is_open_sets (T.is_open) :=
⟨T.is_open_univ,T.is_open_inter,T.is_open_sUnion⟩

[Kevin Buzzard]

They're kind of the same

[Mario Carneiro]

yes, it is equivalent to unbundling the set (set A) part of topological_space

[Reid Barton]

The difference is just that the mathlib definition does not have the properties split off together into a separate structure/definition

[Kevin Buzzard]

So what I find myself wondering again and again is what the best way is. A year ago there were plenty of things I could formalise in 0 ways; now I find there are plenty of things I can formalise in two ways, and I really struggle to know the right way. What I have now understood is that in some sense it doesn't matter, because if I write a good enough API then probably any one of my choices will be fine. But I am beginning to realise that there's more at stake than this.

[Mario Carneiro]

particularly in view of the complete lattice structure, the intersection theorem is only one part of bigger structure, and using it as such makes sense of the whole finer/coarser thing in a more disciplined way

[Sjoerd de Vries]

I really am a beginner, so forgive me if I sound incredibly stupid.
I'm trying to define a function which can add vectors with entries in ℕ.
I tried something like this:
namespace vectest universe u constant vec : Type u → ℕ → Type u def vec_add (n : ℕ) : vec (list ℕ) n → vec (list ℕ) n → vec (list ℕ) n := sorry end vectest
I don't see how I could specify the desired function like this - of course I intend my input to be a vector of length n with entries in ℕ, but Lean just sees (as far as I can tell) something of Type list ℕ which happens to depend on n. I can't really expect to be able to extract values from the list and add them, then put them back into a new list of length n, if Lean doesn't know that's what I'm talking about, right?

[Kevin Buzzard]

Hi Sjoerd. I would generally discourage the use of constant. Is the idea that you want to model vectors of length n with entries in nat?

[Sjoerd de Vries]

Yes, that's the idea.

[Chris Hughes]

The best way to do that is a function fin n → nat. fin n is a type with n elements.

[Sjoerd de Vries]

So I can think of fin n as being a discrete set with n elements and of vectors as functions. Is there a pre-defined way of adding functions that I can then use to add vectors? And how would I find out if this thing exists without asking any of you?

[Kevin Buzzard]

I think it's not so hard to write these functions yourself and it would probably be a good exercise.

[Chris Hughes]

algebra/pi_instances contains all of these for add, mul etc

[Kevin Buzzard]

Sjoerd -- feel free to send me a private message if you don't want to spam the chat. fin n is a type which has exactly n terms, which you can think of as 0,1,...,n-1.

[Sebastian Ullrich]

Defining vector as a function is quite unusual because of the resulting runtime complexity (which you may not be interested in). The common definitions are as an inductive type (e.g.) or as a subtype of list (data.vector).

[Zak]

Hey, would anyone mind explaining how to prove A ∨ B given two propositions A and B and a proof of A?

[Zak]

I think the question looks a bit like this;

theorem prove_or (A B : Prop) (proof_A : A) : A ∨ B

[Simon Hudon]

You can prove it as:

theorem prove_or (A B : Prop) (proof_A : A) : A ∨ B :=
or.inl proof_A

or

theorem prove_or (A B : Prop) (proof_A : A) : A ∨ B :=
by { left, exact proof_A }

[Zak]

Thank you :D left will be very useful

[Simon Hudon]

Fun fact: left works with any inductive type. It applies the first constructor while right applies the second constructor.

[Patrick Massot]

https://leanprover.github.io/theorem_proving_in_lean/tactics.html#more-tactics

[Kevin Buzzard]

I was mulling over ∨ as a result of this question, thinking how one could explain to a beginner how to work this out, and as a result I ran into something which I myself didn't understand. Is ∨ left associative or right associative? If you can't remember then I figured that one way of finding out was just checking for yourself:

example (P Q R : Prop) : P ∨ Q ∨ R = P ∨ (Q ∨ R) := rfl
example (P Q R : Prop) : P ∨ Q ∨ R = (P ∨ Q) ∨ R := rfl

I was expecting precisely one of these to work. But neither does! The first one (which is the right answer) gives the error

type mismatch, term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  P ∨ Q ∨ R = P ∨ Q ∨ R

[Kevin Buzzard]

Why does rfl not prove that?

[Kenny Lau]

because = is less important than ∨

[Kenny Lau]

think about what a = b or c = d means

[Kenny Lau]

(pp.all would have shown you the problem)

[Kenny Lau]

example (P Q R : Prop) : (P ∨ Q ∨ R) = (P ∨ (Q ∨ R)) := rfl
example (P Q R : Prop) : (P ∨ Q ∨ R) = ((P ∨ Q) ∨ R) := rfl

[Sebastien Gouezel]

Another beginner question: I would like to understand why apply is failing in the following example:

import analysis.real order.filter
open filter

lemma test (a b c : real) : tendsto (λx, a * x) (nhds c) (nhds (a * c)) :=
begin
  apply tendsto_mul,   -- this line fails
  apply_instance,
  exact tendsto_const_nhds,
  exact tendsto_id
end

I know how to work it out with apply tendsto_mul _ _ or refine tendsto_mul _ _ or a direct term proof, but with the above it fails with the error message

invalid apply tactic, failed to unify
  tendsto (λ (x : ℝ), a * x) (nhds c) (nhds (a * c))
with
  tendsto ?m_3 ?m_4 (nhds ?m_6) → tendsto ?m_7 ?m_4 (nhds ?m_8) → tendsto (λ (x : ?m_1), ?m_3 x * ?m_7 x) ?m_4 (nhds (?m_6 * ?m_8))

What I don't get is why this unification problem is hard. Any hint?

[Patrick Massot]

This is higher order unification

[Patrick Massot]

You want Lean to recognize a product of functions

[Kenny Lau]

no that isn't it

[Patrick Massot]

But it could be a product in many ways, in principle

[Kenny Lau]

I suspect it's apply not knowing which term is the last thing

[Patrick Massot]

Hum, it's weird that apply tendsto_mul _ _ works

[Mario Carneiro]

note that tendsto is itself defined as a pi

[Mario Carneiro]

this has been known to confuse apply in the past

[Kevin Buzzard]

because = is less important than ∨

How ironic that the reason the question came up was that the output of #print notation ∨ was what inspired me to ask the question, so I already knew that ∨ was unimportant. Thanks Kenny. It's not the first time I've been done over by binding powers -- I get caught out by ∃ occasionally too.

[Sebastien Gouezel]

note that tendsto is itself defined as a pi

You mean apply unfolds the definition of tendsto all the way up to the filter inclusion, which is indeed a pi? And then I am not surprised it is confused. Is there a way to tell lean that is should never unfold by itself the definition of tendsto, to avoid the problem?

[Mario Carneiro]

these instructions are already in place

[Mario Carneiro]

apply is not supposed to look that deep, but it does

[Mario Carneiro]

it will even look through @[irreducible] definitions, unlike almost anything else

[Sebastien Gouezel]

Yes, I can see that the definition of subset is protected... Do you know if this behavior of applyis by design, and for what reason? This is a real pain for what I would like to do.

[Mario Carneiro]

It's certainly a bug, but we've got to live with it until lean 4 comes around. It only concerns the calculation of how many underscores to insert, and only then in limited circumstances (I'm not sure Patrick was that far off the mark with the note about higher order unification)

[Mario Carneiro]

I think, after you unfold EVERYTHING, the tendsto becomes a bunch of pis applied to a metavariable (the unknown target topology set), which may unfold to still more pis but lean can't be sure

[Sebastien Gouezel]

Thanks for your explanations. Indeed, for proofs written by hand, adding some underscores is not a problem.

I wanted to try my hand at automation, adding @[tendsto_rules] before tendsto lemmas. With the aim that writing applys [tendsto_rules] would try to applysuccessively all the tagged rules, to prove convergence statements. Since apply does not work well in this context, I will have to find another exercise to learn tactics.

For fun, an even "better" example: in my example above, if you try to replace the line exact tendsto_const_nhds with apply tendsto_const_nhds it fails (while the unification looks even easier as there are no premises in tendsto_const_nhds), but it works with apply @tendsto_const_nhds _ _ _ _ _ (I agree, it is only a matter of getting the right number of underscores :)

[Kevin Buzzard]

You could write a tactic which is apply but which works the way you want it to ;-) I have no idea how hard that would be!

[Patrick Massot]

It looks like apply is written in C, not Lean

[Sebastien Gouezel]

I probably speak C++ better than lean, but still I will rather find another exercise, this one is not for me!

[Tomáš Jakl]

I'm sure there's a simple way to use combine values of Prop and if-then-else statements. But I can't find it. What would you put in the place of sorry below? Thanks!

def k : Nat := 5
def uni : Type := Fin k

def em : Nat →  uni := λ n =>
  if n < k then ⟨ n , sorry ⟩
           else ⟨ k-1, by simp ⟩

[Kevin Buzzard]

def em : Nat →  uni := λ n =>
  if h : n < k then ⟨ n , h ⟩
           else ⟨ k-1, by simp ⟩

[Martin Dvořák]

Krásný večer přeji!

[Tomáš Jakl]

Continuing with shockingly trivial questions. I'm trying to define the type of all (directed) graphs. From what I know from type theory, the type should be defined as \sum a : Type, Graph a where Graph a could be defined as follows:

structure Graph (a : Type) where
  edge : a x a -> Prop

why is it that then

def Graphs : Type 1 := \sum a : Type, Graph a

gives me an error "expected token"?

Am I doing something fundamentally wrong or what am I not understanding? Thanks a lot for any pointers!

[Henrik Böving]

Because you either have to use the pure ASCII identifier of the Sigma type or the actual unicode:

structure Graph (a : Type) where
  edge : a × a -> Prop

def Graphs : Type 1 := Σ a : Type, Graph a

or

def Graphs : Type 1 := Sigma fun a => Graph a

also note that there is no need to dive into type theory or anything here, you can also define it as a structure if you wish:

structure Graphs where
  a : Type
  g : Graph a

[Tomáš Jakl]

Thanks for answering. Sorry for being sloppy, I did use unicode in the editor but not here. It turns out that I was using ∑ (i.e. \sum) instead of Σ (i.e. \Sigma) :man_facepalming: No idea how come I missed that there's a distinction between the two in Lean...

(Although, it is a bit weird that sum types are not typeset with \sum...)

[Kevin Buzzard]

As a mathematician I would say the converse -- it would have been a bit weird if mathematical sums of real numbers were not typeset with \sum.

[Sabrina Jewson]

Is it possible to prove that ℕ ≠ ℤ?

[Martin Dvořák]

What do you mean by that?

[Sabrina Jewson]

Is it possible to fill in the sorry in this code?

example : ℕ ≠ ℤ := sorry

[Sabrina Jewson]

This question isn’t for any particular purpose, I just wondered if that’s a thing that can be done in Lean

[Martin Dvořák]

Sabrina Jewson said:

Is it possible to fill in the sorry in this code?

example : ℕ ≠ ℤ := sorry

This is a good question that I, unfortunately, cannot answer.

[Reid Barton]

No, it's not possible.

[Martin Dvořák]

I was thinking about something different. You somehow identify (1 : ℕ) with (1 : ℤ) and (2 : ℕ) with (2 : ℤ) and so on and you want to show that there are elements of ℤ with no corresponding thing on the ℕ side.

[Martin Dvořák]

Which is not a claim about the sizes of the sets, but it speaks about a concrete embedding of natural numbers into integers.

[Martin Dvořák]

I was thinking about taking N : set ℕ := λ n, true and Z : set ℤ := λ z, true and then wanting to reason about N coerced to act like set ℤ instance.

[Sabrina Jewson]

Reid Barton said:

No, it's not possible.

Interesting — more generally, for which types T and U is it impossible to prove that T ≠ U? I discovered that I can easily do it for empty ≠ ℕ using not_nonempty_iff, so is it just possible for the empty/nonempty distinction or are they more ways?

[Martin Dvořák]

I'd be first interested for which types T and U we can prove T = U. The identity relation is defined for all Sort levels, so it should a syntactically valid proposition.

[Reid Barton]

Sabrina Jewson said:

Reid Barton said:

No, it's not possible.

Interesting — more generally, for which types T and U is it impossible to prove that T ≠ U?

The only way is to prove that T and U have different cardinalities

[Sabrina Jewson]

oh okay, that makes sense, let me try it

[Sabrina Jewson]

Okay got it working :D

[Sabrina Jewson]

Thanks for the advice, that’s very interesting

[Martin Dvořák]

Can you please show us what you proved?

[Martin Dvořák]

I want to learn what can be done with types.

[Sabrina Jewson]

I didn’t put effort into making my proof nice though, be warned :V

inductive a
| c1
| c2

inductive b
| c1

example : a ≠ b := begin
  intro h,
  have ha : ∃ x y : a, x ≠ y,
  from ⟨a.c1, a.c2, λ e, begin simp at e, contradiction end⟩,
  rw h at ha,
  cases ha with x ha,
  cases ha with y ha,
  have eq : x = y,
  cases x,
  cases y,
  refl,
  contradiction,
end

[Sabrina Jewson]

I prove first that ∃ x y : a, x ≠ y, then substitute in a for b, then show that this is a contradiction (as all b values are equal)

[Kevin Buzzard]

You could also prove this by showing that the cardinality of a is 2 and the cardinality of b is 1. In general this is the only technique to prove that types are unequal in lean because the cardinality model of Lean's type theory would have all types of a given cardinality being type synonyms for a fixed type; in that model Nat does equal Int, which is why it's not possible to prove that they're unequal in lean

[Martin Dvořák]

So ℕ = ℤ can be proved?

[Kevin Buzzard]

No. It just can't be disproved.

[Martin Dvořák]

Good.

[Martin Dvořák]

Martin Dvořák said:

I'd be first interested for which types T and U we can prove T = U. The identity relation is defined for all Sort levels, so it should a syntactically valid proposition.

..

[Kevin Buzzard]

Trying to prove equality of types is "evil" in a precise sense. It's not the right question in Lean's type theory.

[Martin Dvořák]

Sabrina Jewson said:

I didn’t put effort into making my proof nice though, be warned :V

I know that nobody asked and nobody cares, but this is my refactor of your proof:

example : a ≠ b :=
begin
  intro h,
  have ha : ∃ x y : a, x ≠ y,
  { use a.c1, use a.c2, },
  rw h at ha,
  rcases ha with ⟨x, y, neq⟩,
  cases x,
  cases y,
  exact neq rfl,
end

[Martin Dvořák]

You taught me a new thing — equality between types can be used in rw.

[Martin Dvořák]

Kevin Buzzard said:

Trying to prove equality of types is "evil" in a precise sense. It's not the right question in Lean's type theory.

Can someone tell us more than "don't do it" please?

[Mario Carneiro]

You can prove equalities of types in roughly three scenarios:

• The types are definitionally equal, i.e. if def foo := nat then foo and nat are provably equal.
• The types are built from the same inductive families applied to equal arguments, for example fin (a + b) and fin (b + a) are equal because a + b = b + a and fin is a function (a type function, but a function nonetheless)
• There is a coincidence of different indices of an inductive family being equal because of cardinality considerations (roughly: cantor's theorem). That is, if you have an inductive family inductive foo : set Type -> Type then it can't be injective because no such function can be.

[Kevin Buzzard]

import tactic

@[derive fintype]
inductive a
| c1
| c2

@[derive fintype]
inductive b
| c1

example : a ≠ b := λ h,
  by obtain ⟨⟩ : fintype.card a = fintype.card b := by simp only [h]

[Kevin Buzzard]

I think this can be golfed, but I can't get rid of the simp only because the rewrite isn't type-correct.

[Kevin Buzzard]

Golfing your proof using mathlib rcases:

import tactic

inductive a
| c1
| c2

inductive b
| c1

example : a ≠ b :=
begin
  intro hab,
  have h : ∃ x y : a, x ≠ y := ⟨a.c1, a.c2, λ m, a.no_confusion m⟩,
  rw hab at h,
  rcases h with ⟨⟨⟩, ⟨⟩, h⟩,
  exact h rfl,
end

[Kevin Buzzard]

Lean 4 has rcases in Std so you don't need to use mathlib to have access to it:

import Std.Tactic.RCases

inductive a
| c1
| c2

inductive b
| c1

example : a ≠ b := by
  intro hab
  have h : ∃ x y : a, x ≠ y := ⟨a.c1, a.c2, λ m => a.noConfusion m⟩
  rw [hab] at h
  rcases h with ⟨⟨⟩, ⟨⟩, h⟩
  exact h rfl

[Henrik Böving]

Kevin Buzzard said:

Trying to prove equality of types is "evil" in a precise sense. It's not the right question in Lean's type theory.

Note that it can be interesting to prove equality of types (or lemmas that let you rewrite one type into the other) When writing functions though. For example when we are operating on length indexed lists and there is two different arithmetic expression in the length index of two lists and we would like to say zip it with a function of type List a n -> List b n -> List (Prod a b) n it can be interesting to prove that the types of the two lists are in fact equal by showing that the two arithmetic expressions in their indices match up.

[Kevin Buzzard]

Precisely this sort of problem, when the two ns aren't definitionally equal, was a genuine issue with category theory in LTE. We have had to develop tools such as eq_to_hom and eq_to_iso to manage the stuck eq.rec terms.

[Kevin Buzzard]

I proved they weren't equal in term mode in Lean 4:

inductive a
| c1
| c2

inductive b
| c1

example : a ≠ b := λ (hab : a = b) =>
  have h : ∃ xₐ yₐ : a, xₐ ≠ yₐ := ⟨a.c1, a.c2, a.noConfusion⟩
  have hb : ∃ x' y' : b, x' ≠ y' := hab ▸ h
  hb.casesOn λ ⟨⟩ ⟨⟨⟩, hxy⟩ => hxy rfl

[Trebor Huang]

The equality in Lean is "underspecified", i.e. we don't determine everything with the current rules and axioms. A few ways to specify that are

• Add the ability to pattern match on types, which gives us a no-confusion thing. This sort of makes the universe an inductive type.
• Univalence.
• Something in the style of observational type theory. This sort of makes the universe a coinductive type.

[Trebor Huang]

A quick way to see if something cannot be proved in Lean, is to look at these three possibilities. If they disagree then the proposition can't be proved or disproved. (For the N=Z thing, the result is "false, true, depends", so you know you can't prove or disprove it)

[Sabrina Jewson]

I would like function of this form:

def finmap.map_keys (α β γ : Type*) [decidable_eq β]
  (m : finmap (λ _ : α, γ)) (f : α → β) (f_inj : function.injective f)
  : finmap (λ _ : β, γ)

I spent a while trying to implement it myself and ended up with around 50 lines of code:

Lots of code…

variables {α β γ : Type*}

def list.map_keys (f : α → β) : list (Σ _ : α, γ) → list (Σ _ : β, γ)
  := @list.map (Σ _ : α, γ) (Σ _ : β, γ) (λ pair, sigma.mk (f pair.fst) pair.snd)

def list.map_keys_cons {f : α → β} {hd : Σ _ : α, γ} {tl : list (Σ _ : α, γ)}
  : list.map_keys f (hd :: tl) = sigma.mk (f hd.fst) hd.snd :: list.map_keys f tl
:= rfl

def finmap.map_keys
  [decidable_eq β]
  (m : finmap (λ _ : α, γ))
  (f : α → β)
  (f_inj : function.injective f)
  : finmap (λ _ : β, γ)
:= m.lift_on
  (λ m, (m.entries.map_keys f).to_finmap)
  (λ a b perm, begin
    cases a with a_entries a_nodupkeys,
    cases b with b_entries b_nodupkeys,
    dsimp,
    dsimp at perm,
    induction perm with
        head l₁ l₂ l₁_perm_l₂ perm_ih
        x y tail
        l₁ l₂ l₃ l₁_perm_l₂ l₂_perm_l₃ perm_ih₁ perm_ih₂
    ,
    { refl, },
    {
      rw [list.map_keys_cons, list.map_keys_cons, finmap.to_finmap_cons, finmap.to_finmap_cons],
      rw perm_ih (list.nodupkeys_cons.mp a_nodupkeys).2 (list.nodupkeys_cons.mp b_nodupkeys).2,
    },
    {
      repeat { rw [list.map_keys_cons, finmap.to_finmap_cons], },
      apply finmap.insert_insert_of_ne,
      simp at a_nodupkeys,
      intro h,
      exact a_nodupkeys.left (or.inl (f_inj h).symm),
    },
    {
      have l₂_nodupkeys, from (list.perm_nodupkeys l₁_perm_l₂).mp a_nodupkeys,
      rw [perm_ih₁ a_nodupkeys l₂_nodupkeys, perm_ih₂ l₂_nodupkeys b_nodupkeys],
    }
  end)

It’s unfortunately quite a lot — is there any way to shorten this? Is there a really useful method in mathlib that I’m missing?

[Kyle Miller]

Kevin Buzzard said:

Precisely this sort of problem, when the two ns aren't definitionally equal, was a genuine issue with category theory in LTE. We have had to develop tools such as eq_to_hom and eq_to_iso to manage the stuck eq.rec terms.

In graph theory, we don't have the luxury of identity morphisms, so we instead had to develop tools like docs#simple_graph.walk.copy

This was recently added to category theory as docs#quiver.hom.cast for work on quivers, which can't in general just use docs#category_theory.eq_to_hom

[Kyle Miller]

It seems to be a good dependent types design pattern to write a custom eq.rec that's specifically for rewriting indices in type constructors, to "cast" terms of the type to terms of an equal type in a more controlled way. For example, having a cast function to rewrite the length of a length-indexed list types.

[Tyler Josephson ⚛️]

Informally, I might try to prove that ℕ ≠ ℤ by observing that -1 ∈ ℤ and that -1 ∉ ℕ. Is this not a correct proof / is this not possible in Lean?

[Kevin Buzzard]

That's just a syntax error in lean: for a \mem b to typecjeck b must be a term of type set something

[Yaël Dillies]

You could interpret this as showing set.Ici (0 : ℤ) ≠ set.univ, but that certainly isn't showing ℕ ≠ ℤ.

[Niels Voss]

I spent an embarrassingly long time trying to prove that ℕ ≠ ℤ and I now think that it is unlikely that such a proof is possible in Lean. Here's why I think that:
Natural numbers and integers have the same cardinality, so there is some bijection nat_to_int between them. We choose such a bijection (preferably one where nat_to_int (0 : ℕ) = (0 : ℤ)). We can now define the ℤ equivalent of nat.succ by converting from int to nat, adding 1, then converting back. I call this new function new_succ. It has type ℤ -> ℤ.
An important fact about natural numbers is that every natural number is expressible as nat.succ applied some amount of times to nat.zero. Now with our new function, every integer is expressible as new_succ applied some amount of times to (0 : ℤ). I can prove this by showing that the recursor for natural numbers also holds true for integers:

Lots of code

import set_theory.cardinal.basic

universe u

def cardinality_equal : cardinal.mk ℕ = cardinal.mk ℤ :=
eq.trans cardinal.mk_nat cardinal.mk_int.symm
def nat_to_int_conversion_exists : nonempty (ℕ ≃ ℤ) := quotient.exact cardinality_equal
noncomputable def nat_to_int_conversion : ℕ ≃ ℤ := classical.choice nat_to_int_conversion_exists

noncomputable def nat_to_int : ℕ → ℤ := nat_to_int_conversion.to_fun
noncomputable def int_to_nat : ℤ → ℕ := nat_to_int_conversion.inv_fun
theorem nat_to_int_left_inv : function.left_inverse int_to_nat nat_to_int :=
nat_to_int_conversion.left_inv
theorem nat_to_int_right_inv : function.right_inverse int_to_nat nat_to_int :=
nat_to_int_conversion.right_inv

noncomputable def new_succ (n : ℤ) := nat_to_int ((int_to_nat n) + 1)

noncomputable def int.new_rec : Π {motive : ℤ → Sort u}, motive (nat_to_int 0) →
  (Π (n : ℤ), motive n → motive (new_succ n)) → Π (n : ℤ), motive n :=
begin
  intros motive base_case ind_case n,
  set motive' : ℕ → Sort u := λ x : ℕ, motive (nat_to_int x) with hmot,
  have base_case' : motive' 0 := by { rw hmot, exact base_case },
  have ind_case' : Π (n : ℕ), motive' n → motive' n.succ := begin
    intros k prev_step,
    rw hmot at ⊢ prev_step,
    specialize ind_case (nat_to_int k) prev_step,
    unfold new_succ at ind_case,
    rw nat_to_int_left_inv k at ind_case,
    exact ind_case,
  end,
  have := @nat.rec motive' base_case' ind_case' (int_to_nat n),
  rw hmot at this,
  rw nat_to_int_right_inv n at this,
  exact this,
end

Note how int.new_rec basically has the same type as nat.rec, except we have int instead of nat and new_succ instead of nat.succ. We also have nat_to_int 0 instead of 0 but it would be (0 : ℤ) if I chose a more convenient bijection. Since every proof about natural numbers essentially boils down to a bunch of nat.zero, nat.succ, and nat.rec calls, any proof about the natural numbers can be translated to a proof about the integers simply by replacing all instances of nat.succ with new_succ, etc. (well, at least I think it can, I don't know if it has the same definitional equalities).

Since every proof about natural numbers can be translated to an equivalent proof about integers, there's no way to prove ℕ ≠ ℤ because then that proof could be translated to ℤ ≠ ℤ by doing the substitution described above.

I'm not entirely sure if my argument is sound, but it made sense in my head at least.

[Ruben Van de Velde]

You could have believed Reid :)

Reid Barton said:

No, it's not possible.

[Niels Voss]

I figured as much, I just wanted to see if I could justify why to myself

[Patrick Stevens]

I'm not sure your argument is sound. If your argument is correct, wouldn't it prove that $\mathbb{Z} = \mathbb{N}$, by translating one side of the true statement $\mathbb{N} = \mathbb{N}$?

[Niels Voss]

No, because there's no way in Lean to make a function that takes some arbitrary proof and substitutes all instances of nat.succ with new_succ, etc. The rules of Lean don't really allow it, and the closest would could get is a tactic. My argument is necessarily meta-theoretic. Assuming I didn't make a mistake in my reasoning, it would only prove that equality of types is independent of the axioms, and neither prove nor disprove it.
On the other hand, I'm not entirely sure my argument is watertight either because I don't really have a great understanding of type theory and there might be some detail I missed that would make it impossible to translate all proofs (something like the computation rule not getting translated).