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 inlower_grade
is elaborated as two nested matches, the match onl
fits that description since it will always returnGrade 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: Oct 13 2024 at 01:02 UTC