Stream: Coq users

Topic: Difficulties in understanding how simpl works


view this post on Zulip Guilhem (Jun 23 2023 at 21:22):

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.

view this post on Zulip Pierre Courtieu (Jun 23 2023 at 21:30):

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 simplunfolds definitions at will, so we need all of them.

view this post on Zulip Guilhem (Jun 23 2023 at 21:36):

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

view this post on Zulip Yann Leray (Jun 23 2023 at 21:38):

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

view this post on Zulip Guilhem (Jun 23 2023 at 21:42):

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 ?

view this post on Zulip Yann Leray (Jun 23 2023 at 21:47):

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

view this post on Zulip Guilhem (Jun 23 2023 at 21:49):

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.

view this post on Zulip Yann Leray (Jun 23 2023 at 21:53):

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

view this post on Zulip Guilhem (Jun 23 2023 at 21:56):

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

view this post on Zulip Yann Leray (Jun 23 2023 at 22:03):

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)

view this post on Zulip Yann Leray (Jun 23 2023 at 22:03):

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

view this post on Zulip Guilhem (Jun 23 2023 at 22:11):

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

view this post on Zulip grianneau (Jul 14 2023 at 12:05):

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