Functions and Propositions

Stream: general

[Olonbayar Temuulen]

Sorry for a noob question, but is there any difference between the have and apply tactics when used on functions and propositions? (The first thought would be that its the same since they are both understood by Lean as types, but my intuition is telling me that maybe it is not exactly the case)?

[Mario Carneiro]

have and apply are actually fairly different, and they do not ever have the same behavior

[Mario Carneiro]

apply changes the goal by applying a lemma and giving you subgoals for the hypotheses ("backward reasoning")

[Mario Carneiro]

have adds a hypothesis to your context given a proof term ("forward reasoning")

[Mario Carneiro]

Rereading your question, perhaps I misread and you meant to compare functions to propositions when used in have and apply. In this case, the answer is that there is no difference: you can use apply to apply a function and get subgoals for the arguments of the function, in just the same way as with lemmas:

def foo : nat :=
begin
  let x : nat,
  { apply nat.succ,
    exact 2 },
  apply nat.add,
  { exact 2 },
  { exact x },
end

#print foo
-- def foo : ℕ :=
-- let x : ℕ := 2.succ in 2.add x

[Olonbayar Temuulen]

Mario Carneiro said:

Rereading your question, perhaps I misread and you meant to compare functions to propositions when used in have and apply. In this case, the answer is that there is no difference: you can use apply to apply a function and get subgoals for the arguments of the function, in just the same way as with lemmas:

def foo : nat :=
begin
  let x : nat,
  { apply nat.succ,
    exact 2 },
  apply nat.add,
  { exact 2 },
  { exact x },
end

#print foo
-- def foo : ℕ :=
-- let x : ℕ := 2.succ in 2.add x

Another noob question -> if A->B is a function, is A->B->C a function as well?

[Arthur Paulino]

I'd say that both A->B and A->B->C are types

[Olonbayar Temuulen]

If I may ask another dumb question -> what is the mathematical difference between functions and types?

[Arthur Paulino]

What do you mean by "mathematical difference"?

[Eric Wieser]

Functions are an example of a type

[Olonbayar Temuulen]

Arthur Paulino said:

What do you mean by "mathematical difference"?

are these same objects?

[Arthur Paulino]

Ah, no. You can have many functions from Nat to Nat, but Nat -> Nat is one type

[Olonbayar Temuulen]

Arthur Paulino said:

Ah, no. You can have many functions from Nat to Nat, but Nat -> Nat is one type

what do you mean by "one type"?

[Arthur Paulino]

I mean that all functions from nat to Nat have that same type

[Arthur Paulino]

What's your background? Computer science, mathematics or some other?

[Olonbayar Temuulen]

Arthur Paulino said:

What's your background? Computer science, mathematics or some other?

Theoretical Economics, Game Theory

[Kevin Buzzard]

A type is what a mathematician calls a set. A term is what they call an element. You can look at the set of all functions from X to Y and that's a type in Lean. Or you can look at one function from X to Y and that's a term

[Jireh Loreaux]

Related to what Kevin is saying, I think this might be part of the confusion: ℕ → ℕ is the type of (all) functions from ℕ to itself. A term f of this type (denoted f : ℕ → ℕ) is a specific function from ℕ to itself.

[Kevin Buzzard]

Yeah, X -> Y is what I'd call Hom(X,Y)

[Olonbayar Temuulen]

thank you, everybody, I'm looking forward to asking more dumb questions, but hopefully each time a bit more meaningful than the last one.

[Olonbayar Temuulen]

Why does the "cc" tactic work on "and" logical operations (and many others) but not for "OR"?

[Mario Carneiro]

cc is for congruence closure, which is to say it proves that some number of equalities implies another equality. It can do some basic preprocessing of the hypotheses which includes breaking up ANDs in the hypotheses and conclusion, but it is not a generic propositional or SMT solver and you should generally use other tactics to perform this kind of preprocessing