Stream: Coq users

Topic: software foundations


view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:42):

Hi!
I'm completely new to Coq, started on it a couple of days ago, and am struggling but enjoying myself thoroughly.

The material I'm using is software foundations, and I've recently hit a brick wall with the first "hard" exercise, proving the lower_grade_lowers theorem.

Coq isn't behaving at all the way I would expect, and fails to simplify a pattern match I would expect it to:

  match l with
  | A | _ => Grade l Natural
  end = Grade l Natural

The code is available on the site (and I've written a gist with the minimum amount of code to reproduce) but I'm not sure it's strictly necessary to see my problem: the | A | _ => ... bit seems, to my untrained eye, to be obviously always true, and should simplify to its right hand side. But this does not happen.

Long story short: I'd love both to understand what I'm missing and, if anybody's familiar with the material, maybe a hint at how to solve this problem? I'm kind of stuck at the moment

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:44):

Hi Nicolas, short time no see! You can indeed prove this is true via by using the destruct l tactic.

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:45):

I was trying to avoid destructuring l, since it contains a lot of values and they're all irrelevant to the problem: that pattern match explicitly says whatever the value of l, this simplifies to Grade l Natural - or at least that's how I understand it

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:47):

You understand the meaning correctly, and this is indeed obviously true, but it's not obvious enough that you can skip destruct.

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:47):

But the full proof of this is still one line: destruct l; reflexivity

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:47):

the reason I thought I could was that the exercise specifically tells me I can, but maybe I'm going in the wrong direction altogether...

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:48):

wait, what? do I not need to provide a proof for each possible value of l?

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:49):

just noticed the ;, which I haven't been introduced to yet. Maybe that's the magic trick

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:49):

Yes, but a; b does that by running the tactic b on each goal produced by a.

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:49):

I did not know that!

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:51):

You're probably not expected to at this point, so there might be a better answer with a different proof or with different definitions. But I don't think it's worth getting stuck for now.

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:51):

thank you. That gives me a clear path to proving the theorem, although clearly not quite the one the book expects me to take

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:51):

I understand why solutions are not available, as this material is used in classes, but it does make self-learning much harder

view this post on Zulip Gaëtan Gilbert (Aug 17 2023 at 19:52):

what did you do for the definition of lower_grade?

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:54):

Definition lower_grade (g : grade) : grade :=
  match g with
  | Grade F Minus => Grade F Minus
  | Grade l Minus => Grade (lower_letter l) Plus
  | Grade l m => Grade l (lower_modifier m)
  end.

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:54):

On your original question: since l : Letter is just a simple variant, the rule you're asking for to prove this without destruct is called "eta-equality for sum types". That's "complicated" to implement for plain sum types (without recursion). For inductive types, I think it's undecidable.

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:55):

really? Because I'm reading the pattern match as | _ => foo, and I can't think of a scenario where that would not evaluate to foo, whatever the lhs

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:56):

But that's not just "foo"; it's "do a case distinction on the scrutinee and then always return foo". Those are different.

view this post on Zulip Gaëtan Gilbert (Aug 17 2023 at 19:56):

it is always equal to foo, but that does not mean it reduces to foo inside the type theory

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:57):

I notice you're violating a hint of the exercise: > Hint: To make this a succinct definition that is easy to prove properties about, you will probably want to use nested pattern matching. The outer match should not match on the specific letter component of the grade -- it should consider only the modifier. You should definitely not try to enumerate all of the cases. (Our solution is under 10 lines of code, total.)

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:57):

well, I guess it's good I'm learning this now, because I have no idea why that would be :)

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:58):

@Paolo Giarrusso I don't think I am, here's how I begin my proof:

Theorem lower_grade_lowers :
  forall (g : grade),
    grade_comparison (Grade F Minus) g = Lt ->
    grade_comparison (lower_grade g) g = Lt.
Proof.
  intros [] H. destruct m.

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:58):

this gives me 3 goals to solve, the first two which appear trivial to me because I don't yet understand type theory, but I wasn't able to solve without destructuring l.

view this post on Zulip Gaëtan Gilbert (Aug 17 2023 at 19:59):

when computing lower_grade (Grade l m), if m is Natural or Plus you should not need to look at the value of l
however the way you wrote that match will make it check the value of l, which results in the useless match you got stuck on

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:59):

that hint is about the definition of lower_grade — and | Grade F Minus => Grade F Minus is clearly matching on the letter

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 19:59):

ah, sorry

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 20:00):

I didn't even see that hint!

view this post on Zulip Gaëtan Gilbert (Aug 17 2023 at 20:00):

:ghost:

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 20:00):

and Gaëtan's answer details why that makes a difference

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 20:01):

let me work through that, and then I might have a follow up question on whether that's a general pattern I should try to reproduce (once I'm confident I undestood the pattern)

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 20:01):

thank you so much

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 20:05):

Sounds good — but here's a minimized version of this puzzle since I just typed it. The next question is "why does your lower_grade produce sth like give_B_bad, but that might be for later.

Inductive letter : Type :=
  | A | B | C | D | F.

Definition give_B (l : letter) : letter := B.

Definition give_B_okay (l : letter) : letter :=
  match l with | _ => B end.

Definition give_B_bad (l : letter) : letter :=
  match l with | A | _ => B end.

Goal forall l, give_B l = give_B_okay l.
Proof. reflexivity. Qed.

Goal forall l, give_B l = give_B_bad l.
Proof.
  Fail reflexivity.
  destruct l; reflexivity.
Qed.

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 20:06):

The key thing to realize is that give_B_bad is sugar for a pattern-match with 6 cases, which just happen to have the same body B — if you compiled that, you'd need an actual if or switch (at least without optimizations). That'd be also be true in Scala or Haskell.

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 20:08):

right, so now that I actually read what I'm supposed to do, it basically types itself

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 20:08):

And last: generally, Coq reduction does _NOT_ behave as anything like a "sufficient smart compiler". It follows very specific syntactic rules; proving "obvious" equalities that do not follow from those rules would be a bug.

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 20:09):

Yeah. That's what I have to build an intuition for. I'm still bringing expectations from other languages that don't hold here.

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 20:09):

sounds good — "why" that's the case is probably a question for another day

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 20:12):

and so in general, I should try to reduce on a single component of a product, to help downstream proofs, even it makes my Definition more verbose, right?

view this post on Zulip Nicolas Rinaudo (Aug 17 2023 at 20:12):

this is going to take some getting used to, as I've learned to do the exact opposite :)


Last updated: Jun 23 2024 at 03:02 UTC