From: Andrea Asperti Date: Thu, 15 Jun 2006 09:39:55 +0000 (+0000) Subject: some examples of the new ApplyS tactic X-Git-Tag: 0.4.95@7852~1311 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1a4e36e57d838a43ab9765a9e9c7a602ae9c0124;p=helm.git some examples of the new ApplyS tactic --- diff --git a/matita/tests/applys.ma b/matita/tests/applys.ma new file mode 100644 index 000000000..74573177f --- /dev/null +++ b/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.