rocq-provercoq-tactic

How to understand `(elimTF andP top)`?

Section 5.1.3 "Using views in intro patterns" of the book "Mathematical Components" explain how the view intro-pattern works as follows.

First, we have a lemma andP which relates (b1 /\ b1) to b1 && b2.

Lemma andP (b1 b2 : bool) : reflect (b1 /\ b2) (b1 && b2).

We want to prove the following lemma using view intro patterns based on andP.

Lemma example n m k : k <= n ->
  (n <= m) && (m <= k) -> n = k.
Proof.
move=> lekn /andP.

The following paragraphs explain how the view intro-pattern works:

The view intro-pattern /andP has applied the reflection view andP to the top entry of the stack (n <= m) && (m <= k) and transformed it into its equivalent form (n <= m) /\ (m <= k). Note that strictly speaking, lemma andP does not have the shape of an implication, which can be fed with a proof of its premise: it is (isomorphic to) the conjunction of two such implications. The view mechanism implemented in the tactic language has automatically guessed and inserted a term, called hint view, which plays the role of an adapter. More precisely the /andP intro pattern has wrapped the top stack item, called top here, of type ((n <= m) && (m <= k)) into (elimTF andP top) obtaining a term of type ((n <= m) /\ (m <= k)).

Lemma elimTF (P : Prop) (b c : bool) :
  reflect P b -> b = c -> if c then P else ~ P.

Term (elimTF andP top) hence has type

if true then (n <= m) /\ (m <= k) else ~ ((n <= m) /\ (m <= k))

I am confused by the type of (elimTF andP top). Specifically,

Solution

  • Mathcomp uses "implicit arguments" so that one doesn't have to specify arguments (like type variables) that can be deduced automatically from later arguments. In this case, the arguments P , b and c can be deduced from the later argument, so the first argument to elimTF is in fact of type reflect P b .

    If you do Check elimTF _. (i.e. you are providing a wild card argument to elimTF) you will see the type of what is exptected for the rest of the arguments, and the necessary context. It shows that

    elimTF ?Hb
     : ?b = ?c -> if ?c then ?P else ~ ?P
where
?P : [ |- Prop]
?b : [ |- bool]
?c : [ |- bool]
?Hb : [ |- reflect ?P ?b]

    ("elimTF with an argument Hb" has the type of a function that expects one argument, namely a proof of b = c, and it returns either a proof of the proposition P or of ~P depending on whether or not c is true. And for this to type check, the variables P, b , c and Hb in the context must be of the types listed under where.)

    If you want to disable the implicit arguments for elimTF you can do it with

    Arguments elimTF _ _ _ _ _ : clear implicits.

    but there is usually no reason to do so. Implicit arguments, when one manages to get it right, helps you from not having to explicitly enter a lot of type arguments in the terms. This is good since it makes the code more readable. But it can sometimes appear "magic".

    This does not answer all of your questions, so feel free to ask for clarifications.