What does hypothesis with operator with question mark mean

0
votes

I've been working with the Coq proof assistant for the past few weeks, but I encountered something special today. I'm working my way through the exercises of the "Types and programming languages" book by Benjamin Pierce. In one of these exercises I have to proof for some self-made programming language (Imp in Pierce's exercises) that a specific hoare triplet is valid. I've almost finished this proof, but I'm stuck at a point where I have to proof that the following is valid st X <= st Y where st is some state, and st X returns a value stored at Id X in the state.

My hypothesis state the following: 

st : state
H : (st X <=? st Y) = true

My question now is what the ? means in (st X <=? st Y) = true and how I can use this theorem to prove the goal (which seems almost the same to as H?)?

1
coq
Don't you mean the "Software Foundations" book? – Arthur Azevedo De Amorim
@ArthurAzevedoDeAmorim Yes indeed. I use both books and was a bit confused for a moment :) – user4424299
Since st X and st Y are natural numbers, you can simplify your question into: What does ? mean in <=? and how do I prove forall m n, (m <=? n) = true -> m <= n. ? – Anton Trunov

1 Answers

3
votes

All you need is apply Nat.leb_le, which states that (n <=? m) = true <-> n <= m (depending on your imports, it might require a different prefix). The natural question is, how do you figure that out?

First, you can normally get information about a definition with Print ident. (which shows the body) or Check ident. (which only shows the type - useful for theorems). However, <=? isn't an identifier, it's notation, so you instead need to Locate its definition:

Locate "<=?".
(* Notation
   "x <=? y" := Nat.leb x y : nat_scope (default interpretation) *)

Then, we can find relevant theorems:

Search Nat.leb.
(* ... (9 other theorems *)
   Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m
   ...
 *)

We can also skip the intermediate step and do a more specific search. Note that you need quotes around the notation.

Search "<=?" true. (* ... (three other theorems) Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m *)