## Stream: Coq users

### Topic: software foundations

#### 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
``````

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

#### 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.

#### 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

#### 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.

#### Paolo Giarrusso (Aug 17 2023 at 19:47):

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

#### 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...

#### Nicolas Rinaudo (Aug 17 2023 at 19:48):

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

#### 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

#### 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.

#### Nicolas Rinaudo (Aug 17 2023 at 19:49):

I did not know that!

#### 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.

#### 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

#### 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

#### Gaëtan Gilbert (Aug 17 2023 at 19:52):

what did you do for the definition of `lower_grade`?

#### Nicolas Rinaudo (Aug 17 2023 at 19:54):

``````Definition lower_grade (g : grade) : grade :=
match g with
end.
``````

#### 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.

#### 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

#### 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.

#### 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

#### 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.)

#### 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 :)

#### 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 :
Proof.
intros [] H. destruct m.
``````

#### 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`.

#### 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

#### 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

ah, sorry

#### Nicolas Rinaudo (Aug 17 2023 at 20:00):

I didn't even see that hint!

:ghost:

#### Paolo Giarrusso (Aug 17 2023 at 20:00):

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

#### 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)

#### Nicolas Rinaudo (Aug 17 2023 at 20:01):

thank you so much

#### 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.
``````

#### 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.

#### 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

#### 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.

#### 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.

#### Paolo Giarrusso (Aug 17 2023 at 20:09):

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

#### 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?

#### 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