From b045623a30fbaa3efb5fc0afa5762ada997201f4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Jun 2006 09:02:56 +0000 Subject: [PATCH] csc trick on steroids --- .../library/paramodulation/paramodulation.ma | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 helm/software/matita/library/paramodulation/paramodulation.ma diff --git a/helm/software/matita/library/paramodulation/paramodulation.ma b/helm/software/matita/library/paramodulation/paramodulation.ma new file mode 100644 index 000000000..aaaf36312 --- /dev/null +++ b/helm/software/matita/library/paramodulation/paramodulation.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/paramodulation/". + +include "nat/nat.ma". + +definition make_eqs_smart \def + \lambda Univ:Type. + \lambda length:nat. + \lambda initial:Univ. + let rec aux (p:Univ) (n:nat) on n : Prop \def + match n with + [ O \Rightarrow \forall a:Univ. p = a \to initial = a + | (S n) \Rightarrow \forall a:Univ. p = a \to aux a n + ] + in + aux initial length. + +theorem transl_smart : + \forall Univ:Type.\forall n:nat.\forall initial:Univ. + make_eqs_smart Univ n initial. + intros. + unfold make_eqs_smart. + elim n + [ simplify.intros.assumption + | simplify.intros.rewrite < H1.assumption + ] +qed. + +theorem prova: + \forall Univ:Type. + \forall a,b:Univ. + \forall plus: Univ \to Univ \to Univ. + \forall H:\forall x,y:Univ.plus x y = plus y x. + \forall H1:plus b a = plus b b. + plus a b = plus b b. + intros. + apply (transl_smart ? (S O) ? ? (H a b) ? H1). +qed. + -- 2.39.2