Theorem Proving in Lean 4 (Leo)

65 flashcards · Mathematics · by lakesare

1. Visually imagine the case where with let a := t1; t2 is stronger than (fun a => t2) t1

   let a := Nat Notice that the meaning of the expression let a := t1; t2 is very similar to the meaning of (fun a => t2) t1, but the two are not the same. In the first expression, you should think of every instance of a in t2 as a syntactic abbreviation for t1. In the second expression, a is a variable, and the expression fun a => t2 has to make sense independently of the value of a. The let construct is a stronger means of abbreviation, and there are expressions of the form let a := t1; t2 that…

2. Visually imagine what do variables do.

   They get inserted as arguments exactly where they are used. The variable command instructs Lean to insert the declared variables as bound variables in definitions that refer to them by name. Lean is smart enough to figure out which variables are used explicitly or implicitly in a definition.

3. Visually imagine 2 possible scopes for variable.

   to the end of the file A variable stays in scope until the end of the file you are working on.section end Sometimes, however, it is useful to limit the scope of a variable. For that purpose, Lean provides the notion of a section In many respects, however, a namespace ... end block behaves the same as a section ... end block. In particular, if you use the variable command within a namespace, its scope is limited to the namespace. Similarly, if you use an open command within a namespace, its effe…

4. What's the synonym for Sort 0?

   Prop Prop, Type 0, Type 1, Type 2 are nothing but syntax sugar/alternative names for, respectively, Sort 0, Sort 1, Sort 2, Sort 3.

5. Visually imagine universes on this picture.

   When we say "a particular universe" - do we always refer to a particular Sort #n. That is, Sort 0, Sort 1, Sort 2,..., Type 0, Type 1, Type 2,..., Prop are all particular universes (some of them equivalent to each other), and there are no other universes in Lean.

6. What's the synonym for Sort 1?

   Type 0 Prop, Type 0, Type 1, Type 2 are nothing but syntax sugar/alternative names for, respectively, Sort 0, Sort 1, Sort 2, Sort 3.

7. Why is it important to write α : Type u instead of α : Type?

   α : Type only allows a list of α : Type 0! α : Type u allows [Nat, String, Prod] , or, e.g., [Type 3, Type 3, Type 3].α : Type only allows [5, 2, 17]

8. What does this expand into?

   To define polymorphic constants, Lean allows you to declare universe variables explicitly using the universe command. You can avoid the universe command by providing the universe parameters when defining F.

9. Visually imagine how all of these are actually defined: And introduction, ≡ And.introAnd elimination, ≡ And.right; And.leftp ∧ q ≡ And p q

   And is particular type!

10. Visually imagine how you would create a proof of p → q → p with lambdas.

    In the propositions-as-types paradigm, theorems involving only → can be proved using lambda abstraction and application. Compare this proof to the expression fun x : α => fun y : β => x of type α → β → α, where α and β are data types. This describes the function that takes arguments x and y of type α and β, respectively, and returns x.

11. Visually imagine what is show ~ from ~ equivalent to.

    Lean also allows us to specify the type of the final term hp, explicitly, with a show statement.Adding such extra information can improve the clarity of a proof and help detect errors when writing a proof. The show command does nothing more than annotate the type, and, internally, all the presentations of t1 that we have seen produce the same term.

12. Visually imagine what Lean allowed us to do here.

    Lean allows us to flatten nested constructors. It is common to iterate constructions like "And." Lean also allows you to flatten nested constructors that associate to the right, so that these two proofs are equivalent.

13. Visually imagine have in lambdas.

14. What does em stand for?

    Excluded middle The introduction and elimination rules we have seen so far are all constructive, which is to say, they reflect a computational understanding of the logical connectives based on the propositions-as-types correspondence. Ordinary classical logic adds to this the law of the excluded middle, p ∨ ¬p.

15. Visually imagine output.

16. Visually imagine how you would: write a structure using inductive.

    A single constructor - intro. Structure is a special case of inductive datatype. It has only one constructor and is not recursive.

17. Visually imagine a predicate.

    predicate : α → Prop. Notice that if α is any type, we can represent a unary predicate p on α as an object of type α → Prop.Similarly, an object r : α → α → Prop denotes a binary relation on α: given x y : α.

18. How is Prop different from other types?

    No matter what α is, (x : α) → β is again a Prop! Prop is impredicative. It is the typing rule for dependent arrow types, and the universal quantifier in particular, that distinguishes Prop from other types. Suppose we have α : Sort i and β : Sort j, where the expression β may depend on a variable x : α. Then (x : α) → β is an element of Sort (imax i j), where imax i j is the maximum of i and j if j is not 0, and 0 otherwise.

19. What's max a b VS imax a b in Lean?

    max a b - standard max imax a b - b == 0 ? 0 : max a b imax i j is the maximum of i and j if j is not 0, and 0 otherwise

20. Visually imagine a calc proof.

    calc is always based on transitivity! The calc command can be configured for any relation that supports some form of transitivity. It can even combine different relations. You can "teach" calc new transitivity theorems by adding new instances of the Trans type class.

21. Visually imagine what this refers to.

    To the previous anonymous have. To start with, we can use anonymous "have" expressions to introduce an auxiliary goal without having to label it. We can refer to the last expression introduced in this way using the keyword this.

22. [Tactic Combinators] What does a <;> b combinator do?

    a is applied once; b is applied to all resulting subgoals. t₁ is applied to the current goal, and then t₂ is applied to all the resulting subgoals.

23. [Tactic Combinators] What does first | t₁ | t₂ | ... | tₙ combinator do?

    Applies each tᵢ until one succeeds, or else fails. In the first example, the left branch succeeds, whereas in the second one, it is the right one that succeeds. In the next three examples, the same compound tactic succeeds in each case.

24. Visually imagine what this is a shortcut for.

25. Visually imagine what cases d is equivalent to.

    cases d == match d with

26. Give a catchphrase for: separate constructors putting all data into a single constructor

    separate constructors - disjunctive Notice that a type with multiple constructors is disjunctive: an element of Sum α β is either of the form inl aor of the form inl b.single constructor - conjunctive A constructor with multiple arguments introduces conjunctive information: from an element Prod.mk a b of Prod α β we can extract aandb. An arbitrary inductive type can include both features, by having any number of constructors, each of which takes any number of arguments. Inductively defined type…

27. Visually imagine what this is syntax sugar for.

    Keep in mind that the notation ∃ x : α, p is syntactic sugar for Exists (fun x : α => p).

28. Visually imagine the difference between these inductives. logic --- programming False - Empty True -- Unit And --- Prod Or ----- Sum

    logic : Prop programming : Type u Just depends on which universe the resulting type will belong to. The definitions of False, True, And, and Or are perfectly analogous to the definitions of Empty, Unit, Prod, and Sum. The difference is that the first group yields elements of Prop, and the second yields elements of Type u for some u.

29. Give a catchphrase for {x : α // p x} in set theory.

    All such x that p x is true. The notation {x : α // p x} is syntactic sugar for Subtype (fun x : α => p x). It is modeled after subset notation in set theory: the idea is that {x : α // p x} denotes the collection of elements of α that have property p.

30. Visually imagine a nested inductive type.

    This is known as a nested inductive type. It falls outside the strict specification of an inductive type given in the last section because Tree does not occur strictly positively among the arguments to mk, but, rather, nested inside the List type constructor. Lean then automatically builds the isomorphism between TreeList α and List (Tree α) in its kernel, and defines the constructors for Tree in terms of the isomorphism.

31. In technical terms - what "open Foo" is doing?

    Creates aliases for Foo contents. Foo.a => Foo.a + aFoo.b => Foo.b + bFoo.c => Foo.c + c In Lean, identifiers are given by hierarchical names like Foo.Bar.baz. We saw in Namespaces that Lean provides mechanisms for working with hierarchical names. The command namespace foo causes foo to be prepended to the name of each definition and theorem until end foo is encountered. The command open foo then creates temporary aliases to definitions and theorems that begin with prefix foo.namespace Foo def…

32. Visually imagine assigning an attribute: before def after def.

    before def after def.

33. Visually imagine how to create a function with no arguments.

34. What does autoImplicit stand for.

    automatically bind as an implicit arguments Lean 4 supports a new feature called auto bound implicit arguments. It makes functions such as compose much more convenient to write. When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit argument. Although we love this feature and use it extensively when implementing Lean, we realize some users may feel uncomfortable with it. Thus, you can disable it using the command set_option autoImplicit fal…

35. [auto implicits] Visually imagine what this expands into.

    #check @compose-- {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ Lean 4 supports a new feature called auto bound implicit arguments. It makes functions such as compose much more convenient to write. When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit argument.

36. Visually imagine what .. stands for.

    You can use .. to provide missing explicit arguments as _.

37. Visually imagine a fancy way of calling hi with arguments in reversed order.

    Use named arguments. Named arguments enable you to specify an argument for a parameter by matching the argument with its name rather than with its position in the parameter list. If you don't remember the order of the parameters but know their names, you can send the arguments in any order. You may also provide the value for an implicit parameter when Lean failed to infer it.

38. [inductive] Visually imagine match functions that get automatically created.

    NB: use set_option pp.notation false.match weekday with is simply syntax sugar for Weekday.casesOn and Weekday.rec.

39. [inductive] What should you provide as your motive?

    What match should result in. The elimination principle, Weekday.rec, is defined along with the type Weekday and its constructors. It is also known as a recursor, and it is what makes the type "inductive": it allows us to define a function on Weekday by assigning values corresponding to each constructor.Note that the match expression is compiled using the recursorWeekday.rec generated when you declare the inductive type. The implicit argument, motive, is the codomain of the function being define…

40. [inductive] Visually imagine what Point compiles into.

    The structure command also generates useful recursors and theorems.

41. [inductive] Visually imagine the generated: eliminator constructor

    eliminator - Point.rec constructor - Point.mk The structure command also generates useful recursors and theorems. Here are some of the constructions generated for the declaration above.

42. [inductive] Visually imagine the type following this template.

    If the constructor name is not provided, then a constructor is named mk by default. You can also avoid the parentheses around field names if you add a line break between each field.

43. When can the ⟨arg1, arg2, ...⟩ notation be used.

    For structures (a single constructor!). We will see in Chapter Structures and Records that certain types in Lean are structures, which is to say, the type is defined with a single canonical constructor which builds an element of the type from a sequence of suitable arguments. For every p q : Prop, p ∧ q is an example: the canonical way to construct an element is to apply And.intro to suitable arguments hp : p and hq : q. Lean allows us to use anonymous constructor notation ⟨arg1, arg2, ...⟩ in…

44. [Notation] Visually imagine what this notation is for:

45. [Notation] Visually imagine what this notation is for:

46. [Notation] Visually imagine what this notation is for:

47. [Notation] Visually imagine what this notation is for:

48. [Notation] Visually imagine what this notation is for:

49. [Notation] Visually imagine what this notation is for:

50. [Curry-Howard Isomorphism] Visually imagine the computational equivalent.

51. [Curry-Howard Isomorphism] Visually imagine the computational equivalent.

    Unit.unit == ()

52. [Curry-Howard Isomorphism] Visually imagine the computational equivalent.

    And a b == a ∧ bProd α β == α × β

53. [Curry-Howard Isomorphism] Visually imagine the computational equivalent.

    Or a b == a ∨ bSum α β == α ⊕ β

54. [Curry-Howard Isomorphism] Visually imagine the computational equivalent.

    Exists (λ x : α => p) == ∃ x : α, pSigma (λ a : α => β a) == Σ a : α, β a == (a : α) × β a

55. What does p stand for.

    predicate.

56. What does Prop stand for.

    Proposition.

57. What inductive is called: pair dependent pair.

    pair - Prod Prod α β == α × βComputational equivalent for And.dependent pair - Sigma Sigma (λ a : α => β a) == Σ a : α, β a == (a : α) × β a

58. Visually imagine what this notation is for: () (2, 3)

    () - Unit.unit (2, 3) - Prod.mk 2 3

59. Visually imagine notation for: Sum α β vs Prod α β.

    Sum α β == α ⊕ β Prod α β == α × β

60. Visually imagine 2 inductives that Subtype is a mix of.

    This is a good place to mention another inductive type, denoted {x : α // p}, which is sort of a hybrid between ∃ x : α, P and Σ x : α, P. The notation {x : α // p x} is syntactic sugar for Subtype (fun x : α => p x). It is modeled after subset notation in set theory: the idea is that {x : α // p x} denotes the collection of elements of α that have property p.

61. [inductive families] Visually imagine parameters VS indices of the inductive.

    We have seen that the constructor to an inductive type takes parameters --- intuitively, the arguments that remain fixed throughout the inductive construction --- and indices, the arguments parameterizing the family of types that is simultaneously under construction. In contrast to an ordinary inductive definition, which constructs an element of some Sort u, the more general version constructs a function ... → Sort u, where "..." denotes a sequence of argument types, also known as indices

62. [inductive families] Visually imagine 2 famous inductives that make use of indices.

63. Give a catchphrase for Eq definition.

    We give it a type : Eq 4 5, but then the only we can actually construct is Eq 4 4! For each fixed α : Sort u and a : α, this definition constructs a family of types Eq a x, indexed by x : α. Notably, however, there is only one constructor, refl, which is an element of Eq a a. Intuitively, the only way to construct a proof of Eq a x is to use reflexivity, in the case where x is a. Note that Eq a a is the only inhabited type in the family of types Eq a x.

64. [inductive families] Visually imagine a family of types Vector String creates.

    Here's an example of a family of types for Vector String.

65. Visually imagine 2 alternatives to focusing.

    . case