Menu
I'm looking for utility similar to one of Hoogle for Haskell. For the sake of example, let's say I need a function of signature forall n m:nat, n <> m -> m <> n.
When my Google searches don't yield any results, I write Definition foo: forall n m:nat, n <> m -> m <> n. and write intros; auto with arith. to prove it. But is there any way to not pollute my workspace with these temporary results and search for them based on their type? I'm sure I've seen this symmetry stated somewhere in standard library.
382
Like most functional programming languages, Coq can often figure out these types for itself when they are not given explicitly -- i.e., it can do type inference -- but we'll generally include them to make reading easier. Having defined a function, we should next check that it works on some examples.
Then, all logical judgments in Coq are typing judgments: the very heart of Coq is in fact a type -checking algorithm. Prop is the sort for propositions, i.e. well-formed propositions are of type Prop. Typical propositions are:
Each notation symbol is also associated with a notation scope. Coq tries to guess what scope is meant from context, so when it sees S (O × O) it guesses nat_scope, but when it sees the product type bool × bool (which we'll see in later chapters) it guesses type_scope.
One point to note is that the argument and return types of this function are explicitly declared. Like most functional programming languages, Coq can often figure out these types for itself when they are not given explicitly -- i.e., it can do type inference -- but we'll generally include them to make reading easier.
There's a Search command that's somewhat similar to Hoogle, but a bit more precise. Here are some searches you might use for symmetry of not. In practice I would use the first and fall back to the second if there were a lot of results.
Search (_ <> _). (* everything related to not equal *)
Search (?a <> ?b -> ?b <> ?a). (* exactly what you want -
note that unlike Hoogle, you need to use ?a for a pattern variable *)
Search (?R ?a ?b -> ?R ?b ?a). (* this searches for any symmetry theorem;
not terribly useful for it's cool that it works *)
Search not "_sym". (* if you know some of the theorem name you can use that, too *)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
