It can handle some simplification.Įxact T. You can see those implicits in the expressions by issusing Show Print Implicit., or fiddling with your CoqIDE settings. The expressions might actually be different because they have implicit arguments that differ. Implicits can appear in other ways and cause weird issues, such as when you’re trying to rewrite or do something else to an expression that seems to exactly match one side of the rule you’re rewriting with, but Coq refuses to operate on that expression even though it’s in plain sight. In practice arguments are usually implicit because they’re deducible from the others, so not_eq_sym H is pretty good. Without the you only need to supply (and are only allowed to supply) the one non-implicit argument, H, to not_eq_sym. If you also run About not_eq_sym., you’ll see (among other text): not_eq_sym : forall (A : Type) (x y : A), x y -> y x Here makes all implicit arguments of not_eq_sym explicit. Well, not quite you’d actually write A x y H. So if you supplied these four arguments, just by writing not_eq_sym A x y H where H is a proof of x y, you’d get a proof of y x out. However the literalist programmer view is more like: not_eq_sym is a (fully curried) function that takes in a type A, two things x and y of type A, and finally a proof of the Prop x y, and outputs a proof of the Prop y x. Mathematically, not_eq_sym says: for any type A and any two things x and y of type A, if x y, then y x. ![]() : forall (A : Type) (x y : A), x y -> y x To use that example again: If you run Check not_eq_sym. Similarly SearchRewrite on some expression pattern searches for theorems you could use to rewrite that expression. found the theorem for me (it was called not_eq_sym). For example, I was looking to prove x y given y x.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |