From 7099c10f54741e2ecb2f69ef33490ac92b513c4d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Jan 2006 09:25:36 +0000 Subject: [PATCH] few bits for coq comparison of patterns --- helm/papers/matita/matita2.tex | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 8500cfa2c..5c56eccf3 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1467,20 +1467,24 @@ would have resulted in this sequent: \end{grafite} where $H$ is $\beta$-expanded over the second $n$ -occurrence. This is a trick to make the unification algorithm ignore -the head of the application (since the unification is essentially -first-order) but normally operate on the arguments. -This works for some tactics, like rewrite and replace, -but for example not for change and other tactics that do not relay on -unification. +occurrence. + +At this point, since Coq unification algorithm is essentially +first-order, the application of an elimination principle (of the +form $\forall P.\forall x.(H~x)\to (P~x)$) will unify +$x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}. + +Since rewriting, replacing and several other tactics boils down to +the application of the equality elimination principle, the previous +trick deals the expected behaviour. The idea behind this way of identifying subterms in not really far -from the idea behind patterns, but really fails in extending to +from the idea behind patterns, but fails in extending to complex notation, since it relays on a mono-dimensional sequent representation. Real math notation places arguments upside-down (like in indexed sums or integrations) or even puts them inside a bidimensional matrix. In these cases using the mouse to select the wanted term is probably the -only way to tell the system exactly what you want to do. +more effective way to tell the system what to do. One of the goals of \MATITA{} is to use modern publishing techniques, and adopting a method for restricting tactics application domain that discourages -- 2.39.2