From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 30 Jan 2006 09:25:36 +0000 (+0000)
Subject: few bits for coq comparison of patterns
X-Git-Tag: make_still_working~7742
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=7099c10f54741e2ecb2f69ef33490ac92b513c4d;hp=30bf48113bb0ea53f5300b3a6a2d129a9f4d73d9;p=helm.git

few bits for coq comparison of patterns
---

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