1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/paramodulation/".
18 include "datatypes/bool.ma".
20 inductive List (U:Type) : nat \to Type \def
22 | Cons : \forall n.U \to List U n \to List U (S n).
25 definition mk_T \def \lambda U:Type.\lambda n:nat.List U n \to Prop.
27 definition app_T' \def
31 \lambda t:mk_T U (S n).
32 \lambda l:List U n.t (Cons U n a l).
34 let rec mk_Arrow' (n:nat) (U:Type) on n \def
35 match n return \lambda x.\forall t:mk_T U x.Prop with
37 \lambda t:mk_T U O.t (Nil U)
39 \lambda t:mk_T U (S m).\forall a.mk_Arrow' m U (app_T' m U a t)].
44 \forall actual_params:List U n.
45 \forall pred:mk_T U n.
46 \forall H:mk_Arrow' n U pred.
60 definition mk_Tside \def \lambda U:Type.\lambda n:nat.List U n \to U.
66 \lambda side:mk_Tside U (S n).
67 \lambda args:List U n.side (Cons U n a args).
69 let rec mk_Arrow (n:nat) (U:Type) (eq:\forall T:Type.T\to T\to Prop) on n \def
70 match n return \lambda x.\forall l:mk_Tside U x.\forall r:mk_Tside U x.Prop with
72 \lambda l:mk_Tside U O.\lambda r:mk_Tside U O.eq U (l (Nil U)) (r (Nil U))
74 \lambda l:mk_Tside U (S m).\lambda r:mk_Tside U (S m).\forall a.
75 mk_Arrow m U eq (app_T m U a l) (app_T m U a r)].
78 \lambda eq:\forall T:Type.T\to T\to Prop.
86 let rec mk_TsideArr (n:nat) (U:Type) on n \def
89 | (S m) ⇒ U \to mk_TsideArr m U].
92 (n:nat) (U:Type) (eq:\forall T:Type.T\to T\to Prop) (b:bool)
93 (context:U \to U) on n
95 match n return \lambda x.\forall l:mk_TsideArr x U.\forall r:mk_TsideArr x U.Prop with
97 \lambda predl:mk_TsideArr O U.
98 \lambda predr:mk_TsideArr O U.
99 sym eq U (context predl) (context predr) b
101 \lambda predl:mk_TsideArr (S m) U.\lambda predr:mk_TsideArr (S m) U.
103 mk_Statement m U eq b context (predl a) (predr a)].
105 theorem eq_f_to_mk_Statement:
106 \forall eq:\forall T:Type.T\to T\to Prop.
107 \forall sym_eq: \forall T:Type.\forall l,r:T.eq T l r \to eq T r l.
110 \forall f:U \to U1.\forall x,y:U. eq U x y \to eq U1 (f x) (f y).
113 \forall context: U \to U.
115 \forall predl:mk_TsideArr n U.
116 \forall predr:mk_TsideArr n U.
117 \forall H:mk_Statement n U eq false (\lambda x.x) predl predr.
118 mk_Statement n U eq b context predl predr.
131 | generalize in match H2.
149 \forall eq:\forall T:Type.T\to T\to Prop.
150 \forall sym_eq: \forall T:Type.\forall l,r:T.eq T l r \to eq T r l.
153 \forall f:U \to U1.\forall x,y:U. eq U x y \to eq U1 (f x) (f y).
156 \forall context: U \to U.
158 \forall predl:mk_TsideArr n U.
159 \forall predr:mk_TsideArr n U.
160 \forall H:mk_Statement n U eq false (\lambda x.x) predl predr.
161 mk_Statement n U eq b context predl predr
163 eq_f_to_mk_Statement.
167 definition make_eqs_smart' \def
170 \lambda initial:Univ.
171 let rec aux (p:Univ) (n:nat) on n : Prop \def
173 [ O \Rightarrow \forall a:Univ. p = a \to initial = a
174 | (S n) \Rightarrow \forall a:Univ. p = a \to aux a n
179 theorem transl_smart' :
180 \forall Univ:Type.\forall n:nat.\forall initial:Univ.
181 make_eqs_smart' Univ n initial.
183 unfold make_eqs_smart'.
185 [ simplify.intros.assumption
186 | simplify.intros.rewrite < H1.assumption
193 \forall plus: Univ \to Univ \to Univ.
194 \forall H:\forall x,y:Univ.plus x y = plus y x.
195 \forall H1:plus b a = plus b b.
198 apply (transl_smart' ? (S O) ? ? (H a b) ? H1).