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