7

I was trying to go through the famous and wonderful software foundations book but I got to an example where simpl. and reflexivity. just do to much under the covers and are hindering my learning & understanding.

I was going through the following theorem:

Theorem plus_1_neq_0 : forall n : nat,
  beq_nat (n + 1) 0 = false. (* n+1 != 0 *)
Proof.
  intros n.
  destruct n as [| n'].
    -simpl. reflexivity.
    -simpl. reflexivity.
Qed.

what I really want is something that allows me to go through step by step what simpl. and reflexivity. did. Is there something that allows me to do that?

Destruct is suppose to resolve the following issue:

because the first argument to beq_nat (which is just not equal i.e. !=) does a matching but the first input depends on a unknown variable n and the same thing for + so the matching can't do anything, so doing simpl. gets us stuck (for some reason).

which it clearly it must resolve it since Coq later accepts the proof. But if one looks carefully what the second goal is, it seems that the same issue as above is re-introduced:

2 subgoals
______________________________________(1/2)
beq_nat (0 + 1) 0 = false
______________________________________(2/2)
beq_nat (S n' + 1) 0 = false

now we have n' as the first argument for both beq_nat and + again. However, to a novice like me, simpl. miraculously does work this time for some mysterious reason. I obviously read the simpl. documentation but being a novice in this I didn't really know what I was looking for and it was to dense for me to form an understanding of it that was helpful...

Anyway, why does it work here? The reason I am asking is because it would have never occurred to me to use destruct on this example proof, especially cuz of the re ocurrence of n' an unknown variable, and it seems that being able to see what really happened or what was different would be useful. So I thought checking a step-by-step break down of these type of things would be useful (rather than posting a new SO question every other day).

Note I did see this question:

Step by step simplification in coq?

but I couldn't find a way to make it useful for me since it was tailored for that particular example to much. Hopefully my question doesn't become to narrow to my particular example, though it might since the step by step break down might not be possible without knowing how simpl. (or reflexivity.) works already (or at least the above answers to the question above gave me that impression).

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • 1
    In this particular case the key is in here: "now we have n' as the first argument for both beq_nat and + again", this is not quite the case. The first argument of `+` is `S n'`, and looking at the definition of `+` (`plus`) we can see that it is a `Fixpoint` that starts by matching on its first argument, which is sufficient for `simpl` to reduce the expression to `beq_nat (S (n' + 1)) 0`. Now looking at the definition of `beq_nat`, it is also a `Fixpoint` that matches on its first argument, so `simpl` can keep going. – Li-yao Xia Jan 05 '19 at 08:26
  • 1
    As for `reflexivity`, it sees that the goal is `false = false` which is trivially true. – Li-yao Xia Jan 05 '19 at 08:30
  • (I'm not making those comments an answer because I think the more general question of making more explicit what tactics are doing is interesting enough.) – Li-yao Xia Jan 05 '19 at 10:04
  • @Li-yaoXia yea for reflexivity in this case its simple. I should have said that I meant that in other places reflexivity seems to do similar magic to `simpl.` thats why I referenced `reflexivity.` – Charlie Parker Jan 05 '19 at 20:11
  • @Li-yaoXia I don't think your 1st comment is complete enough for me to follow. Perhaps you could still provide an answer, I just won't accept yet. In particular I don't know what " Now looking at the definition of beq_nat, it is also a Fixpoint that matches on its first argument, so simpl can keep going" means. What does it mean to "keep going mean" and how is the `false = false` reached in the second case? – Charlie Parker Jan 05 '19 at 20:15
  • cross posted: https://www.quora.com/unanswered/How-does-one-inspect-what-more-complicated-tactics-do-in-Coq-step-by-step – Charlie Parker Jan 11 '19 at 19:44

2 Answers2

4

One way to break the evaluation down is to give an argument to simpl, as suggested in the question you linked. simpl f allows to simplify only the sub-expressions that appear under calls to f. In this case, simpl Nat.add (or simpl plus or simpl "+") simplifies S n' + 1 into S (n' + 1). Then simpl beq_nat turns beq_nat (S (n' + 1)) 0 into false.

As for reflexivity, it can conclude if the two terms under comparison are equal up to simplification, which means that, if I am not mistaken, you can always replace simpl; reflexivity by just reflexivity.

eponier
  • 3,062
  • 9
  • 20
2

Reducing this step by step:

beq_nat (S n' + 1) 0 = false

  (* Without the `+` notation, which is purely for pretty-printing: *)

beq_nat (plus (S n') 1) 0 = false

  (* by definition of plus:   plus (S n') 1 = S (plus n' 1) *)

beq_nat (S (plus n' 1)) 0 = false

  (* by definition of `beq_nat`,

     beq_nat (S (plus n' 1)) 0 =
     = match S (plus n' 1) with
       | O => ... (* unreachable *)
       | S m => match 0 with
                | O => false
                | S _ => ...
                end
       end
     = match 0 with
       | O => false
       | S _ => ...
       end
     = false
  *)

false = false
Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56