calculate

Stream: general

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

/me clearly doesn't know enough about bits

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

Sure

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Or would you still be able to cheat using induction?

[Johan Commelin]

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

[Johan Commelin]

You can probably do something like

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

[Johan Commelin]

And just fool it into checking a trivial exercise

[Mario Carneiro]

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]

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

[Mario Carneiro]

you can't do induction on them

[Mario Carneiro]

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]

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]

Hmm, I like this last idea.

[Johan Commelin]

@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]

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]

what's in the list?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

Unless you get calculate working...

[Kevin Buzzard]

And this is computable

[Johan Commelin]

That doesn't matter. My tactic will reject your answer.

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

The answer is "those ones"

[Mario Carneiro]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

assuming you can define what the required form is

[Johan Commelin]

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

[Johan Commelin]

You still overestimate my skills

[Johan Commelin]

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

[Mario Carneiro]

expr.of_nat does this for numerals

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

"oh and make it computable too please"

[Johan Commelin]

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

[Johan Commelin]

Or would that still require tactics

[Johan Commelin]

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

[Mario Carneiro]

looks good probably requires tactics

[Johan Commelin]

But that's lean's strength

[Johan Commelin]

I'm not opposed to tactics (-;

[Kevin Buzzard]

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

[Mario Carneiro]

then say that

[Kevin Buzzard]

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

[Johan Commelin]

@Kevin Buzzard You have to formalise the "language"

[Kevin Buzzard]

Right

[Johan Commelin]

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]

you can define "disjoint union of intervals" easily enough

[Kevin Buzzard]

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

[Mario Carneiro]

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]

Kevin Buzzard said:

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

But every set is a disjoint union of intervals!

[Kevin Buzzard]

Rofl

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

No?

[Johan Commelin]

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

[Kevin Buzzard]

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]

These systems are by no means perfect

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

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

[Jalex Stark]

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]

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]

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]

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]

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

[Jalex Stark]

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.