Hi, I don't know if this is the right place to ask this question. If note, please tell me and I'll move elsewhere.

So I'm learning coq, using Software foundation. I'm currently at the end of the first chapter of LF, trying to do an exercise, and there is something I don't understand.

I have to prove the following theorem, I've started the following way (I'll explain the function useful to understand my issue) :

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

Here grade is a tuple type defined as :

```
Inductive grade : Type :=
Grade (l:letter) (m:modifier).
```

Where letter are enum and modifier types (A,B,C ... and +, natural and minus)

So, issue is, after `destruct m`

I get the following on the right side of the arrow in my goal :

```
grade_comparison
match l with
| A | _ => Grade l Natural
end (Grade l Plus) = Lt
```

Which means, if I'm right, that `lower_grade l Plus`

gets reduced to ```
match l with
| A | _ => Grade l Natural
end
```

So now onto the definition of `lower_grade`

:

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

So I guess we are in the 2nd case of the `match`

, but I really don't understand how does `A | _`

get introduced, as I don't do this kind of filtering at any point.

It would really help if someone has a clue of what's going on here.

Thanks in advance for the help.

Please give a code that compiles. In this forum almost each person willing to anwser will first need to run your code *and then* start to understand the problem and write back. Moreover `simpl`

unfolds definitions at will, so we need all of them.

Here is the code :

```
Inductive letter : Type :=
| A | B | C | D | F.
Inductive modifier : Type :=
| Plus | Natural | Minus.
Inductive grade : Type :=
Grade (l:letter) (m:modifier).
Inductive comparison : Set :=
| Eq : comparison (* "equal" *)
| Lt : comparison (* "less than" *)
| Gt : comparison. (* "greater than" *)
Definition letter_comparison (l1 l2 : letter) : comparison :=
match l1, l2 with
| A, A => Eq
| A, _ => Gt
| B, A => Lt
| B, B => Eq
| B, _ => Gt
| C, (A | B) => Lt
| C, C => Eq
| C, _ => Gt
| D, (A | B | C) => Lt
| D, D => Eq
| D, _ => Gt
| F, (A | B | C | D) => Lt
| F, F => Eq
end.
Theorem letter_comparison_Eq :
forall l, letter_comparison l l = Eq.
Proof.
intros [].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
Definition modifier_comparison (m1 m2 : modifier) : comparison :=
match m1, m2 with
| Plus, Plus => Eq
| Plus, _ => Gt
| Natural, Plus => Lt
| Natural, Natural => Eq
| Natural, _ => Gt
| Minus, (Plus | Natural) => Lt
| Minus, Minus => Eq
end.
Definition grade_comparison (g1 g2 : grade) : comparison :=
match g1, g2 with
| Grade l1 m1 , Grade l2 m2 =>
match letter_comparison l1 l2 with
| Gt => Gt
| Lt => Lt
| Eq => modifier_comparison m1 m2
end
end.
Definition lower_letter (l : letter) : letter :=
match l with
| A => B
| B => C
| C => D
| D => F
| F => F (* Note that you can't go lower than [F] *)
end.
Definition lower_grade (g : grade) : grade :=
match g with
| Grade l m =>
match l, m with
| F, Minus => Grade F Minus
| _, Plus => Grade l Natural
| _ ,Natural => Grade l Minus
| _, Minus => Grade (lower_letter l) Plus
end
end.
Theorem lower_grade_lowers :
forall (g : grade),
grade_comparison (Grade F Minus) g = Lt ->
grade_comparison (lower_grade g) g = Lt.
Proof.
intros g. destruct g as [l m].
simpl. destruct m.
```

I'm precising that I don't want a proof of the theorem, just to understand why the start of my proof yields

```
grade_comparison
match l with
| A | _ => Grade l Natural
end (Grade l Plus) = Lt
```

for the first subgoal

For some reason, Coq will print a match where all branches are the same as `match <expr> with <C1> | _ => <ret> end`

. In your case, after the inner match on two scrutinees in `lower_grade`

is elaborated as two nested matches, the match on `l`

fits that description since it will always return `Grade l Natural`

Yann Leray said:

For some reason, Coq will print a match where all branches are the same as

`match <expr> with <C1> | _ => <ret> end`

. In your case, after the inner match on two scrutinees in`lower_grade`

is elaborated as two nested matches, the match on`l`

fits that description since it will always return`Grade l Natural`

It indeed does fit that description, but Coq won't do further simplification because of the `A | _`

and I'm stuck in the proof. I wanted to avoid doing too much `destruct l`

because in the first and second case (Minus and Natural) it doesn't look like it's necessary, but now I'm stuck. I guess I have to refactor my function `lower_grade`

in some way to avoid this behaviour ?

You would have to `destruct l`

to go further in this proof, since it is the scrutinee of the match in the current goal. You could also refactor your `lower_grade`

function by making sure that the modifier is scrutinised first

I just refactozied as

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

So I no longer scrutinize on l at all (at least I don't think ?)

For some obscure reason I still have the exact same issue, I'm not even matching on l. I truly don't understand.

Yes you do, since you have a case which only happens when `l`

is `F`

Okay, understood. I just tried this

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

and it does work.

Is there some known reason for this behaviour "For some reason, Coq will print a match where all branches are the same as match <expr> with <C1> | _ => <ret> end" (like for coq introducing A out of nowhere )?

The underlying reason is that the code it prints, if you were to give it back, should result in the same code. However, `match <expr> with _ => <result> end`

is elaborated into `<result>`

since the match is useless (and to make this construction possible at all types, even those which have no pattern)

So the next best thing is to print at least one valid pattern in the match

Right, I think I understand, although it's a bit convoluted. Thanks a lot !

Hei Guilhem,

I've just searched for "Software Foundation" and I am happy to find your question, thank you! I've tried your code.

At the beginning of the file *Basics.v*, I also add the line `From Coq Require Import ssreflect.`

to use the SSReflect tactics. You don't have to do so, bu you may be interested in following the same book but trying also the tactics from SSReflect. The benefit I see for the first 6 chapters is that you can achieve the same with a smaller set of tactics, and sometimes shorter proof scripts.

I get the matches displayed **after the simpl step, not after the destruct m step**.

I guess you also want to say:

`(lower_grade (Grade l Plus))`

instead of `(lower_grade l Plus)`

Then

`(lower_grade (Grade l Plus))`

is simplified to:```
match l with
| A | _ => Grade l Natural
end
```

among other simplifications.

This filtering looks at `l`

, and if it's constructed with the constructor `A`

or in any other case (the wildcard `_`

) (here, cases other than `A`

are: `B`

, `C`

, `D`

, `E`

and `F`

) then it returns `Grade l Natural`

. It can seem a bit strange, but it's the behaviour we want when lowering a grade from a `Plus`

. It always becomes `Natural`

(the value between `Minus`

and `Plus`

).

It is always nice to try to use the `simpl`

tactic (or `rewrite /=.`

in SSReflect) to see what one gets. I tend to do it frenetically at many proof steps just to see what happens (nothing can happen) and I often step back, for instance when the goal gets more messy.

After the simplification, you can see a match performed on `l : letter`

. So destructing `l`

(with `case: l=> [].`

in SSReflect) before the simplification helps.

If you write `simpl`

in several subcases, you may prefer to chain the tactics by writing `destruct l; simpl.`

instead of `destruct l. simpl.`

so that simpl is applied in all subgoals resulting from the destruction.

Last updated: Jun 23 2024 at 05:02 UTC