From d6db84901876935c7bb55c3a7393684c69bc5a8f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 1 Jul 2005 13:10:27 +0000 Subject: [PATCH] An interesting test for replace. --- helm/matita/tests/replace.ma | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 helm/matita/tests/replace.ma diff --git a/helm/matita/tests/replace.ma b/helm/matita/tests/replace.ma new file mode 100644 index 000000000..776750de2 --- /dev/null +++ b/helm/matita/tests/replace.ma @@ -0,0 +1,19 @@ +set "baseuri" "cic:/test". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "plus" (instance 0) = "natural plus". +alias symbol "times" (instance 0) = "natural times". +alias id "mult_n_O" = "cic:/Coq/Init/Peano/mult_n_O.con". +alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". + +theorem t: \forall x:nat. x * (x + 0) = (0 + x) * (x + x * 0). + intro. + replace in \vdash (? ? (? ? %) (? % %)) with x. + reflexivity. + rewrite < mult_n_O x. + rewrite < plus_n_O x. + reflexivity. + reflexivity. + auto. +qed. \ No newline at end of file -- 2.39.2