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

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

tactic.

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

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

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

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

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

?

just noticed the `;`

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

Yes, but `a; b`

does that by running the tactic b on each goal produced by a.

I did not know that!

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.

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

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

what did you do for the definition of `lower_grade`

?

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

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.

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

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

it is always equal to `foo`

, but that does not mean it reduces to `foo`

inside the type theory

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

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

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

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`

.

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

that hint is about the definition of `lower_grade`

— and `| Grade F Minus => Grade F Minus`

is clearly matching on the letter

ah, sorry

I didn't even see that hint!

:ghost:

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

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)

thank you so much

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

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.

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

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.

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

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

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?

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