From 16568f4cb52cc6b2acc747fe5aceeb4bfab11191 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 15 Jun 2006 09:39:55 +0000 Subject: [PATCH] some examples of the new ApplyS tactic --- helm/software/matita/tests/applys.ma | 34 ++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 helm/software/matita/tests/applys.ma diff --git a/helm/software/matita/tests/applys.ma b/helm/software/matita/tests/applys.ma new file mode 100644 index 000000000..74573177f --- /dev/null +++ b/helm/software/matita/tests/applys.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/". + +include "nat/div_and_mod.ma". +include "nat/factorial.ma". +include "nat/primes.ma". + +theorem prova : \forall n. (n+O)*(S O) = n. +intro. +applyS times_n_SO. +qed. + +lemma foo: ∀n.(S n)! = (S n) * n!. +intro; reflexivity. +qed. + +theorem prova2 : + \forall n. S n \divides (S n)!. +intros. +applyS (witness ? ? ? (refl_eq ? ?)). +qed. -- 2.39.2