## Stream: general

### Topic: calculate

#### Johan Commelin (May 09 2020 at 05:27):

I've been playing a bit with how to state exercises in Lean. This may also be related to the IMO grand challenge. This is what I've come up with so far.

#### Johan Commelin (May 09 2020 at 05:28):

import data.complex.basic

@[irreducible] def calculate {α : Type*} (a : α) : Prop :=
∃ x, x = a

section bit

variables {α : Type*}

local attribute [reducible] calculate

lemma calculate_zero [has_zero α] :
calculate (0 : α) := ⟨0, rfl⟩

lemma calculate_one [has_one α] :
calculate (1 : α) := ⟨1, rfl⟩

lemma calculate_bit0 [has_add α] {a : α} (h : calculate a) :
calculate (bit0 a) := ⟨bit0 a, rfl⟩

lemma calculate_bit1 [has_one α] [has_add α] {a : α} (h : calculate a) :
calculate (bit1 a) := ⟨bit1 a, rfl⟩

end bit

example : calculate (4 - 2 : ℝ) :=
begin
have : (4 - 2 : ℝ) = 2, norm_num,
rw this,
apply calculate_bit0,
apply calculate_one,
end


#### Johan Commelin (May 09 2020 at 05:29):

My question is: can you modify reducibility settings of definitions while you're inside a tactic proof?

#### Johan Commelin (May 09 2020 at 05:31):

Because inside a game / competition / homework setting I guess you can reasonably enforce that participants / students are only allowed to "hand in" a begin ... end-block. But if they can make calculate reducible inside that tactic block, of course this is all doomed.

#### Johan Commelin (May 09 2020 at 05:33):

I've also been thinking that one might want to add some typeclass that adds some "allowed expressions", for example calculate pi would be an "axiom" for the reals, that could be added by the instructor / kata designer

#### Johan Commelin (May 09 2020 at 05:35):

Maybe in codewars you actually hand in more than just a begin ... end block. So then that's not the intended audience :smile:
But for homework, you could make it a rule.

#### Johan Commelin (May 09 2020 at 05:36):

This should come with a tactic (or custom begin ... end environment, like calculate_done, that will check that the final expression can be "calculated"

#### Mario Carneiro (May 09 2020 at 05:38):

You can unfold irreducible in a tactic proof (indeed you can even just remove the attribute)

#### Johan Commelin (May 09 2020 at 05:41):

So then we would need to do something quite a bit more clever.

#### Mario Carneiro (May 09 2020 at 05:41):

In this case, using only the provided lemmas, you are asking to prove that 4 - 2 is a natural number, but this doesn't require computing the number

#### Mario Carneiro (May 09 2020 at 05:41):

If you really wanted to lock it down to the provided lemmas, you could just have an inductive predicate to that effect

#### Johan Commelin (May 09 2020 at 05:44):

But you can't prove calculate n for (n : nat), right? Unless you remove the irreducibility.

#### Johan Commelin (May 09 2020 at 05:44):

You have to turn it into something sufficiently close to a numeral

#### Johan Commelin (May 09 2020 at 05:44):

(E.g. 2 + 2 is fine.)

#### Johan Commelin (May 09 2020 at 05:45):

Maybe I should cook up an example involving determinants, to make this slightly less trivial.

#### Mario Carneiro (May 09 2020 at 05:52):

Indeed I can, using the Power of Induction:

example (n : ℕ) : calculate (n : ℝ) :=
begin
refine nat.binary_rec _ _ n,
{ simp [calculate_zero] },
{ rintro (_|_) n h; simp [nat.bit, calculate_bit0, calculate_bit1, h] }
end


#### Johan Commelin (May 09 2020 at 05:57):

/me clearly doesn't know enough about bits

#### Johan Commelin (May 09 2020 at 05:57):

But this means that whatever definition of calculate you come up with, you can always prove calculate n, I guess.

#### Mario Carneiro (May 09 2020 at 05:58):

I mean you could simplify this by saying that you only provide calculate (nat.succ n) when calculate n, and then it would more clearly be an instance of induction

#### Mario Carneiro (May 09 2020 at 05:58):

but if you couldn't do this kind of thing it would defeat the purpose of lean as a proof assistant. We want to be able to prove properties by induction

Sure

#### Johan Commelin (May 09 2020 at 05:59):

But I thought maybe we can single out certain properties and make them irreducible and yadda yadda...

#### Mario Carneiro (May 09 2020 at 06:00):

Another way to get what you want is to say that you have an infinite number of axioms, calculate 0, calculate 1, calculate 2, ... without using lean quantifiers to get it

#### Johan Commelin (May 09 2020 at 06:01):

Maybe another option would be to have a tactic check_answer that must be the last line of the tactic block?

#### Johan Commelin (May 09 2020 at 06:01):

And the tactic fails if it doesn't like the (p)expr that has been constructed so far.

#### Johan Commelin (May 09 2020 at 06:02):

Or would you still be able to cheat using induction?

#### Johan Commelin (May 09 2020 at 06:04):

Hmm... I'm afraid this won't be foolproof either...

#### Johan Commelin (May 09 2020 at 06:05):

You can probably do something like

  tactic1,
tactic2,
close_goal_by_induction, -- proof accomplished!
show calculate 1,


#### Johan Commelin (May 09 2020 at 06:05):

And just fool it into checking a trivial exercise

#### Mario Carneiro (May 09 2020 at 06:08):

import tactic.core

constant calculate : ℕ → Prop

namespace tactic
namespace interactive
open interactive.types
meta def calculate : tactic unit :=
do
(_root_.calculate %%e) ← target,
n ← e.to_nat,
let ax := mk_simple_name ("calculate_" ++ to_string n),
try (add_decl (declaration.ax ax [] (_root_.calculate %%(reflect n)))),
exact (expr.const ax [])
end interactive
end tactic

example : calculate 5 := by calculate

example : calculate (4 - 2) := by calculate


#### Mario Carneiro (May 09 2020 at 06:09):

this achieves an infinite family of axioms by having the calculate tactic produce them on the fly

#### Mario Carneiro (May 09 2020 at 06:10):

you can't do induction on them

#### Mario Carneiro (May 09 2020 at 06:14):

The downsides of this method are that you get new axioms for every use of calculate:

def T : calculate 5 ∧ calculate 7 := by split; calculate

#print axioms T
-- calculate
-- calculate_5
-- calculate_7


and also that because theorems can't add axioms to the environment, you have to either mark the theorem as a def or prepare the state beforehand:

theorem T : calculate 5 := by calculate -- fails
def T' : calculate 5 := by calculate -- ok
theorem T'' : calculate 5 := by calculate -- ok because T' already added calculate_5


#### Mario Carneiro (May 09 2020 at 06:18):

Johan Commelin said:

Maybe another option would be to have a tactic check_answer that must be the last line of the tactic block?

Rather than the last line, it should be the first line, with a block surrounding the rest of the proof. That way check_answer gets the state, calls the given user tactic, and then checks that the original goal has been solved appropriately. Or, rather than intercepting the expr before the proof is done, you can just examine the proof later with a run_cmd tactic at the end of the file

#### Johan Commelin (May 09 2020 at 06:49):

Hmm, I like this last idea.

#### Johan Commelin (May 09 2020 at 07:09):

@Mario Carneiro Would something like this be a start?

class allowed_exprs (α : Type*) :=
(good_exprs : list name)

def calculate {α : Type*} [allowed_exprs α] (a : α) : Prop :=
∃ x, x = a


#### Kevin Buzzard (May 09 2020 at 07:10):

When I ran into this sort of issue when formalising problem sheets I just told my students that it was their job to formalise the question.

#### Mario Carneiro (May 09 2020 at 07:10):

what's in the list?

#### Kevin Buzzard (May 09 2020 at 07:11):

I realised that actually some questions we ask the students are hugely ambiguous. For example "for which n is it true that all groups of order n are abelian?"

#### Johan Commelin (May 09 2020 at 07:11):

Things like  [bit0, bit1, has_zero.zero, has_zero.one]

#### Kevin Buzzard (May 09 2020 at 07:11):

The answer is "it's the n for which all groups of order n are abelian"

#### Johan Commelin (May 09 2020 at 07:11):

Unless you get calculate working...

#### Kevin Buzzard (May 09 2020 at 07:12):

And this is computable

#### Johan Commelin (May 09 2020 at 07:13):

If the problem statement includes a list of names that are allowed to occur in the answer, you can make it precise. At least that's my current hope

#### Kevin Buzzard (May 09 2020 at 07:13):

But this is part of a more general question -- what does a mathematician even mean when they ask that sort of a question?

#### Mario Carneiro (May 09 2020 at 07:13):

It's easy to detect if a numeral is given by tactics, you don't need this

#### Johan Commelin (May 09 2020 at 07:13):

Right. They mean: give me an answer that is an expr that only uses names from some L : list name. Only L is an implicit variable (-;

#### Kevin Buzzard (May 09 2020 at 07:13):

"For which real numbers x!=3 is (x+1)/(x-3) positive?"

#### Mario Carneiro (May 09 2020 at 07:14):

but I think the problem is that numerals don't suffice for many problems

#### Johan Commelin (May 09 2020 at 07:14):

Mario Carneiro said:

It's easy to detect if a numeral is given by tactics, you don't need this

But I want to be able to allow real.pi (sometimes)

#### Mario Carneiro (May 09 2020 at 07:14):

you can write a tactic that detects terms of the required form

#### Mario Carneiro (May 09 2020 at 07:15):

assuming you can define what the required form is

#### Johan Commelin (May 09 2020 at 07:15):

You mean "you can write a tactic that detects terms of the required form"

#### Johan Commelin (May 09 2020 at 07:15):

You still overestimate my skills

#### Johan Commelin (May 09 2020 at 07:15):

But this "required form". Do you think I'm on the right path with my list name?

#### Mario Carneiro (May 09 2020 at 07:15):

expr.of_nat does this for numerals

#### Mario Carneiro (May 09 2020 at 07:15):

the list name is probably underconstraining if you want a well formed numeral

#### Mario Carneiro (May 09 2020 at 07:16):

There is also a way to do it without tactics, again using an indutive type to define the required form

#### Johan Commelin (May 09 2020 at 07:17):

But wouldn't I be able to prove by induction that every n satisfies the inductive predicate?

#### Mario Carneiro (May 09 2020 at 07:17):

def foo : { n : nat_term // (n : nat) = 4 - 2 } := sorry

#### Mario Carneiro (May 09 2020 at 07:18):

"oh and make it computable too please"

#### Johan Commelin (May 09 2020 at 07:27):

@Mario Carneiro But can we turn that into something that has a slick UI?

#### Johan Commelin (May 09 2020 at 07:27):

Or would that still require tactics

#### Johan Commelin (May 09 2020 at 07:28):

I would like to create something that is foolproof and looks good.

#### Mario Carneiro (May 09 2020 at 07:28):

looks good probably requires tactics

#### Johan Commelin (May 09 2020 at 07:29):

But that's lean's strength

#### Johan Commelin (May 09 2020 at 07:29):

I'm not opposed to tactics (-;

#### Kevin Buzzard (May 09 2020 at 07:29):

How would you do my real number question? It's somehow "clear" to mathematicians that the answer is expected to be a disjoint union of open/closed/semiopen intervals

then say that

#### Kevin Buzzard (May 09 2020 at 07:29):

But this seems to be as much a convention as anything else

#### Johan Commelin (May 09 2020 at 07:29):

@Kevin Buzzard You have to formalise the "language"

Right

#### Johan Commelin (May 09 2020 at 07:29):

Kevin Buzzard said:

But this seems to be as much a convention as anything else

Sure, so hide it in a type class

#### Mario Carneiro (May 09 2020 at 07:29):

you can define "disjoint union of intervals" easily enough

#### Kevin Buzzard (May 09 2020 at 07:30):

"Express as your answer as a disjoint union of intervals" or something

#### Mario Carneiro (May 09 2020 at 07:30):

of course you are stymied to some extent by various general theorems like "every open set is a disjoint union of intervals" and such

#### Johan Commelin (May 09 2020 at 07:30):

Kevin Buzzard said:

"Express as your answer as a disjoint union of intervals" or something

But every set is a disjoint union of intervals!

Rofl

#### Mario Carneiro (May 09 2020 at 07:31):

not every set is the finite disjoint union of intervals, but if it's a polynomial then the options are pretty limited

#### Kevin Buzzard (May 09 2020 at 07:31):

That's great :-) This question is hard!

#### Johan Commelin (May 09 2020 at 07:31):

I think it's pretty clear that we want to inspect the expr that the user provides.

#### Mario Carneiro (May 09 2020 at 07:32):

Did you know that you can inspect exprs using typeclass inference?

No?

#### Johan Commelin (May 09 2020 at 07:32):

But it sounds like that is maybe not "best practice"

#### Kevin Buzzard (May 09 2020 at 07:33):

My daughter is doing maths online nowadays for school and using various web pages which are supposed to inspect her text input and decide whether she got it right.

#### Kevin Buzzard (May 09 2020 at 07:33):

These systems are by no means perfect

#### Kevin Buzzard (May 09 2020 at 07:33):

But it never occurred to me to just tell her to type the question in as the answer

#### Kevin Buzzard (May 09 2020 at 07:34):

She normally has enough trouble with a correct answer not being accepted because of some grammar issue

#### Mario Carneiro (May 09 2020 at 07:37):

class is_numeral (n : ℕ) := mk

instance zero.is_numeral : is_numeral 0 := ⟨⟩
instance one.is_numeral : is_numeral 1 := ⟨⟩
instance bit0.is_numeral {n} [is_numeral n] : is_numeral (bit0 n) := ⟨⟩
instance bit1.is_numeral {n} [is_numeral n] : is_numeral (bit1 n) := ⟨⟩

def exists_numeral (P : ℕ → Prop) := Exists P
theorem exists_numeral.intro {P : ℕ → Prop}
(n : ℕ) [is_numeral n] (h : P n) : exists_numeral P := exists.intro n h

example : exists_numeral (λ n, 4 - 2 = n) :=
exists_numeral.intro 2 rfl -- ok
example : exists_numeral (λ n, 4 - 2 = n) :=
exists_numeral.intro (4 - 2) rfl -- not ok


#### Mario Carneiro (May 09 2020 at 07:38):

this might satisfy your "looks good" criterion with a bit of notation, and gives helpful error messages, but it is not foolproof against hackers

#### Mario Carneiro (May 09 2020 at 07:39):

so you would have to have a tactic as backup if you want more security

#### Mario Carneiro (May 09 2020 at 07:41):

(you should also add attribute [irreducible] exists_numeral so that you can't accidentally circumvent it using split or existsi)

#### Johan Commelin (May 09 2020 at 07:55):

Mario Carneiro said:

this might satisfy your "looks good" criterion with a bit of notation, and gives helpful error messages, but it is not foolproof against hackers

Right, I can still prove exists_numeral for arbitrary nats, right? Because it is almost the same as my first calculate.

#### Mario Carneiro (May 09 2020 at 08:07):

right, the idea here is that a good faith usage not using lots of @ signs will give errors in the right places

#### Jalex Stark (May 09 2020 at 14:34):

I think this conversation is very interesting, but also that a solution is not important to the project of giving homework in Lean

#### Jalex Stark (May 09 2020 at 14:34):

When I graded for a Haskell course in the CS department, checking that the solution compiled was just the first step in grading. If it didn't compile we sent it back to the student and asked them to fix and resubmit.

Once I have a compiling submission, I read the code and make comments about the parts I think could be cleaner or more understandable or more efficient. This is the same work that I did when grading for theorem-proving classes, just with the added benefit that I didn't have to decide how large of holes I let pass through.

#### Jalex Stark (May 09 2020 at 14:39):

Maybe your grading rubric is such that anyone who submits compiling code gets a passing grade, but to get an A on an assignment you have to comment your proof in such a way that the comments on their own would pass for a proof in a normal math class

#### Jalex Stark (May 09 2020 at 14:41):

and then you've still reduced the burden on the grader, they "only" have to check that

1. the writing sounds like good math prose,
2. the comments mean the same thing as the nearby bits of Lean,
3. the path to the proof was reasonably direct / didn't rely on machinery that's "out of scope" for the class

#### Johan Commelin (May 09 2020 at 14:42):

Why not simply correlate the grade to the number of symbols in the proof script?
Golfing FTW!

#### Jalex Stark (May 09 2020 at 14:43):

where in a normal math class 2 is replaced by the significantly harder "verify that the ideas required to formalize this proof are 'out of scope' in the direction of being 'trivial'", or maybe "verify that the ideas required to formalize this proof are probably known to the author". I did the last one a lot and it leads to an awful bias against non-native english speakers.

Last updated: May 13 2021 at 06:15 UTC