feedback on the sixth session and the homework · Teaching [with] Coq

I was quite disturbed by the fact that this year the students are really slower in the Reals part. It was surprising because I thought I had simplified the content. Then I was enlightened by a student asking how to multiply both sides of an hypothesis by a number.

So, what really happened is that I'm now too practiced in writing easy proofs Coq. I think directly with backwards reasoning. So I removed many things related to forward reasoning just because "they're not necessary". I honestly believed it simplified things. It does not. So in the future version, I will have to reintroduce (at a carefully chosen moment) forward reasoning and I'm quite sure the students will prove things more easily in the end.

A problem worth noting, showing that Search Blacklist is not sufficient as the only means of encapsulation: some students wrote Rmul_comm instead of Rmult_comm. It started a new very confusing goal because of... setoid_ring/Ring_theory.v!

Pierre Rousselin (Nov 17 2023 at 16:10):

So the need to have simpler, more predictable tactics for teaching (at least at this basic level) is quite real.
So is the need to hide more carefully the "details".
I think both tasks require a lot of time and a lot of expertise. I have a little bit of time and well, almost no expertise (but I can try to help).

Théo Winterhalter (Nov 17 2023 at 16:14):

Pierre Rousselin (Nov 17 2023 at 16:21):

Probably at some point, yes. But now, they are first year undergraduate students. I'm trying to teach them rigour; not to try random things until some magic happens. The idea was actually to make them prove by induction that Nat.le is reflexive.
As for using rewrite with an inequality, it's not even clear to me what it should do/what it does.

Théo Winterhalter (Nov 17 2023 at 16:23):

I see. Then yes, I agree that ideally we could have some teaching mode where we could deactivate some features. Or better yet, cherry pick the only ones we allow.

Huỳnh Trần Khanh (Nov 17 2023 at 16:35):

that would require a lot of engineering effort. and coq has to serve many use cases, not just teaching

Huỳnh Trần Khanh (Nov 17 2023 at 16:39):

ig there are other proof assistants with such fine grained controls. maybe some HOL based stuff?

djao (Nov 17 2023 at 21:42):

I find that defining things using axioms helps to reduce the amount of "magic" that students might stumble upon by chance. For example you can define a clone of the natural numbers using Peano axioms (but with explicitly written Axioms in Coq) to neuter Coq's ability to compute with numbers or rewrite inequalities.

Karl Palmskog (Nov 17 2023 at 22:00):

one (maybe exotic) option for the case of reasoning about natural numbers could be to define an explicit deeply embedded deduction system for Peano arithmetic inside Coq, and let students use it through a proof mode, like they do in the FOL library. I think every other approach is going to "leak" capabilities

Paolo Giarrusso (Nov 18 2023 at 00:42):

As prior art on "teaching languages", there is the "How To Design Programs" family of curricula (With support in DrRacket, but also outside the Lisp family).

Paolo Giarrusso (Nov 18 2023 at 00:47):

in the short term, it should now be possible to trim the stdlib. But in this case, you might have to drop setoid rewriting entirely?

Paolo Giarrusso (Nov 18 2023 at 00:55):

Require Import Arith.
Lemma trans (a b c : nat) : a <= b -> b <= c -> a <= c.
Proof. now intros ->. Qed.

rewriting by a <= b simply replaces a by b in a goal P a as long as P b -> P a. And yes, "setoid rewriting" is arguably a misnomer.

Huỳnh Trần Khanh (Nov 18 2023 at 01:47):

this means even induction needs to be explicitly defined with axioms too :eyes::eyes:

djao (Nov 18 2023 at 04:14):

Indeed, induction needs to be defined with an axiom, but Coq understands commands such as induction x using Ax. where Ax is a relevant axiom.

Paolo Giarrusso (Nov 18 2023 at 15:07):

you don't even need using if the induction principle for type foo is called foo_ind

Pierre Castéran (Nov 18 2023 at 19:46):

I used also the module facility to prevent the students from using too many lemmas from the libraries, withhout writing new axioms.

Module Exercise.

  Inductive nat : Set := O | S (p:nat).

  Fixpoint add (n p: nat) : nat :=
  match n with
  | O => p
  | S m => add m (S p)
  end.

  Lemma addSn_p n : forall p,  add (S n) p = S (add n p).
  Admitted.

  Lemma add_n_O : forall n, add n O = n.
  Admitted.

End Exercise.

Stream: Teaching [with] Coq

Topic: feedback on the sixth session and the homework

Pierre Rousselin (Nov 17 2023 at 16:03):