Zulip Chat Archive

Stream: general

Topic: calculate


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (May 09 2020 at 05:38):

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

view this post on Zulip Johan Commelin (May 09 2020 at 05:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 09 2020 at 05:44):

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

view this post on Zulip Johan Commelin (May 09 2020 at 05:44):

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

view this post on Zulip Johan Commelin (May 09 2020 at 05:44):

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

view this post on Zulip Johan Commelin (May 09 2020 at 05:45):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 09 2020 at 05:57):

/me clearly doesn't know enough about bits

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 09 2020 at 05:59):

Sure

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 09 2020 at 06:02):

Or would you still be able to cheat using induction?

view this post on Zulip Johan Commelin (May 09 2020 at 06:04):

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

view this post on Zulip 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,
  check_answer

view this post on Zulip Johan Commelin (May 09 2020 at 06:05):

And just fool it into checking a trivial exercise

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 06:10):

you can't do induction on them

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 09 2020 at 06:49):

Hmm, I like this last idea.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 09 2020 at 07:10):

what's in the list?

view this post on Zulip 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?"

view this post on Zulip Johan Commelin (May 09 2020 at 07:11):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:11):

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

view this post on Zulip Johan Commelin (May 09 2020 at 07:11):

Unless you get calculate working...

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:12):

And this is computable

view this post on Zulip Johan Commelin (May 09 2020 at 07:12):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 (-;

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:13):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:14):

The answer is "those ones"

view this post on Zulip Mario Carneiro (May 09 2020 at 07:14):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (May 09 2020 at 07:14):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:15):

assuming you can define what the required form is

view this post on Zulip Johan Commelin (May 09 2020 at 07:15):

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

view this post on Zulip Johan Commelin (May 09 2020 at 07:15):

You still overestimate my skills

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 09 2020 at 07:15):

expr.of_nat does this for numerals

view this post on Zulip Mario Carneiro (May 09 2020 at 07:15):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 09 2020 at 07:17):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:18):

"oh and make it computable too please"

view this post on Zulip Johan Commelin (May 09 2020 at 07:27):

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

view this post on Zulip Johan Commelin (May 09 2020 at 07:27):

Or would that still require tactics

view this post on Zulip Johan Commelin (May 09 2020 at 07:28):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:28):

looks good probably requires tactics

view this post on Zulip Johan Commelin (May 09 2020 at 07:29):

But that's lean's strength

view this post on Zulip Johan Commelin (May 09 2020 at 07:29):

I'm not opposed to tactics (-;

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:29):

then say that

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:29):

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

view this post on Zulip Johan Commelin (May 09 2020 at 07:29):

@Kevin Buzzard You have to formalise the "language"

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:29):

Right

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:29):

you can define "disjoint union of intervals" easily enough

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:30):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:30):

Rofl

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:31):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 09 2020 at 07:32):

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

view this post on Zulip Johan Commelin (May 09 2020 at 07:32):

No?

view this post on Zulip Johan Commelin (May 09 2020 at 07:32):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:33):

These systems are by no means perfect

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:39):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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