Automarking exercises with prover

Stream: Lean for teaching

[Thorsten Altenkirch]

Hi,
I am teaching basic logic still using Lean 3 in the moment.

I like to set some exercises where the students have to translate definitions into predicate logic. E.g. something like:

constant People : Type
constants Male Female : People → Prop
constant Parent : People → People → Prop
-- Parent x y means x is a parent of y
constant Married : People → People → Prop
-- Married x y means x is married to y

Define the following relations (People → People → Prop)
using the predicates and relations above:
...
- Uncle x y = x is the uncle of y

Here a possible answer is:

def Sibling (x y : People) : Prop
  := x ≠ y ∧ ∀ z : People , Parent z x ↔ Parent z y

def Uncle (x y : People) :=
  Male x ∧ ∃ z : People, Parent z y ∧ Sibling x z

I would like to automatically mark the submissions using a reasonable tactic for predicate logic. Do people have done this and what are recommendations regarding the tactic and the set up?

I mean I set up one or several possible solution (in case the concept is a bit ambiguous) and then check that their solution is equivalent to at least one of the given ones.

Thanks a lot,
Thorsten

[Damiano Testa]

Speaking for myself, I've been using Lean4 for so long now, that I won't really be able to help with Lean3 questions.

[Malvin Gattinger]

I would guess you actually need a predicate logic theorem prover for auto-grading this?

[Thorsten Altenkirch]

Malvin Gattinger said:

I would guess you actually need a predicate logic theorem prover for auto-grading this?

I thought there must be some tactics which are good at this?

[Thorsten Altenkirch]

Damiano Testa said:

Speaking for myself, I've been using Lean4 for so long now, that I won't really be able to help with Lean3 questions.

Ok so what would be the Lean 4 answer?

[Damiano Testa]

I would probably try to leverage aesop as much as possible.

[Jireh Loreaux]

I think aesop will not be too successful with this. I think duper is likely the answer, but I don't know enough to provide guidance.

[Shreyas Srinivas]

CC: @Henrik Böving

[Shreyas Srinivas]

Shreyas Srinivas said:

CC: Henrik Böving

I was wondering if the cadical integration can do this

[Shreyas Srinivas]

You also mentioned being able to call cvc5

[Henrik Böving]

I can't do that but I know the CVC5 people have some way

[Henrik Böving]

And no LeanSAT doesn't deal with quantifiers right now.

[Henrik Böving]

Jireh Loreaux said:

I think aesop will not be too successful with this. I think duper is likely the answer, but I don't know enough to provide guidance.

Given that it's about quantifier instantiation that is exactly what duper should be good at yes. Superposition solvers such as duper are skillful at taking a bunch of quantified theorems and plugging them together in a clever way :tm:. If that is the kind of automation you are looking for use duper.

[Henrik Böving]

CVC5 would also likely have some success with this see https://github.com/ufmg-smite/lean-smt

[Thorsten Altenkirch]

Ok coming back to Lean 3 : is there no tactic for predicate logic for Lean 3 which could prove some simple equivalences?

[Kevin Buzzard]

I think tauto would do some things? Lean 3 is a dead language though.

[Shreyas Srinivas]

I think we even have difficulties setting up projects without docker images for lean 3

[Shreyas Srinivas]

Something about brew not seeing archived GitHub repositories

[Kevin Buzzard]

Yes, the last time I tried to make a Lean 3 project work I had all sorts of problems :-/ (which I whinged about here and which might have been fixed in the mean time)

[Patrick Massot]

Thorsten Altenkirch said:

Ok coming back to Lean 3

We insist: coming back to Lean 3 is a really really bad idea.

[Arthur Paulino]

Lean 4 can do anything Lean 3 could - and much more.
I would also consider the consequences of imprinting the students' habits with the details of a language that's no longer supported by the developers nor by the community.

[Thorsten Altenkirch]

Patrick Massot said:

Thorsten Altenkirch said:

Ok coming back to Lean 3

We insist: coming back to Lean 3 is a really really bad idea.

I didn't ask for this and I have good reasons to stick to lean 3.

[Thorsten Altenkirch]

My module is an introduction to logic for 400 undergraduates. The main point is that they get the idea of logic using a proof assistants. Wether it is Coq, Lean3 or Lean4 is completely irrelevant!

[Kevin Buzzard]

I'm not so sure that this is a good argument. If it's a language which is becoming harder and harder to actually even install and has no support then this is surely an argument against teaching it.

[Kevin Buzzard]

As I say, the last time I tried to download a Lean 3 project it simply didn't work.

[Shreyas Srinivas]

@Thorsten Altenkirch : This insistence might be annoying. After all, in CS it is not unusual to just pick a tool, however "outdated", that fits a pedagogical purpose.

But we are very keen to avoid the fiasco that python had with python2 vs python3.

[Eric Wieser]

I assume the good reasons are some combination of time invested in:

1. Library code to provide students
2. Written code in handouts / slides
3. Tools for automarking

If the bulk of the friction is in 1, then mathport can still do a large portion of the work for you, though mathport itself will become increasingly hard to run over time.

[Eric Wieser]

Unfortunately mathport can't easily modify / reprint lecture handouts / slides!

[Alexander Bentkamp]

How about super? https://github.com/leanprover/super