matita/library/paramodulation/paramodulation.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/paramodulation/".
  16
  17 include "nat/nat.ma".
  18 include "datatypes/bool.ma".
  19
  20 inductive List (U:Type) : nat \to Type \def
  21   | Nil : List U O
  22   | Cons : \forall n.U \to List U n \to List U (S n).
  23
  24 (*
  25 definition mk_T \def \lambda U:Type.\lambda n:nat.List U n \to Prop.
  26
  27 definition app_T' \def
  28   \lambda n:nat.
  29   \lambda U:Type.
  30   \lambda a:U.
  31   \lambda t:mk_T U (S n).
  32   \lambda l:List U n.t (Cons U n a l).
  33
  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
  36   [ O ⇒
  37      \lambda t:mk_T U O.t (Nil U)
  38   | (S m) ⇒
  39      \lambda t:mk_T U (S m).\forall a.mk_Arrow' m U (app_T' m U a t)].
  40
  41 theorem leaf':
  42   \forall U:Type.
  43   \forall n:nat.
  44   \forall actual_params:List U n.
  45   \forall pred:mk_T U n.
  46   \forall H:mk_Arrow' n U pred.
  47   pred actual_params.
  48   intros 3.
  49   elim actual_params;
  50     [ exact H.
  51     | simplify in H1.
  52       unfold app_T' in H1.
  53       lapply (H1 t).
  54       apply H.
  55       assumption
  56     ]
  57 qed.
  58 *)
  59
  60 definition mk_Tside \def \lambda U:Type.\lambda n:nat.List U n \to U.
  61
  62 definition app_T \def
  63   \lambda n:nat.
  64   \lambda U:Type.
  65   \lambda a:U.
  66   \lambda side:mk_Tside U (S n).
  67   \lambda args:List U n.side (Cons U n a args).
  68
  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
  71   [ O ⇒
  72      \lambda l:mk_Tside U O.\lambda r:mk_Tside U O.eq U (l (Nil U)) (r (Nil U))
  73   | (S m) ⇒
  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)].
  76
  77 definition sym \def
  78   \lambda eq:\forall T:Type.T\to T\to Prop.
  79   \lambda U:Type.
  80   \lambda l,r:U.
  81   \lambda b:bool.
  82   match b with
  83   [ true ⇒ eq U r l
  84   | false ⇒ eq U l r].
  85
  86 let rec mk_TsideArr (n:nat) (U:Type) on n \def
  87   match n with
  88   [ O ⇒ U
  89   | (S m) ⇒  U \to mk_TsideArr m U].
  90
  91 let rec mk_Statement
  92   (n:nat) (U:Type) (eq:\forall T:Type.T\to T\to Prop) (b:bool)
  93   (context:U \to U) on n
  94 \def
  95   match n return \lambda x.\forall l:mk_TsideArr x U.\forall r:mk_TsideArr x U.Prop with
  96   [ O ⇒
  97      \lambda predl:mk_TsideArr O U.
  98      \lambda predr:mk_TsideArr O U.
  99        sym eq U (context predl) (context predr) b
 100   | (S m) ⇒
 101      \lambda predl:mk_TsideArr (S m) U.\lambda predr:mk_TsideArr (S m) U.
 102      \forall a:U.
 103        mk_Statement m U eq b context (predl a) (predr a)].
 104
 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.
 108   \forall eq_f :
 109     \forall U,U1:Type.
 110     \forall f:U \to U1.\forall x,y:U. eq U x y \to eq U1 (f x) (f y).
 111   \forall b:bool.
 112   \forall U:Type.
 113   \forall context: U \to U.
 114   \forall n:nat.
 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.
 119   intros 7.
 120   elim n;
 121   [ simplify in H2.
 122     elim b;
 123     [ simplify.
 124       apply H1.
 125       apply H.
 126       assumption.
 127     | simplify.
 128       apply H1.
 129       assumption.
 130     ]
 131   | generalize in match H2.
 132     clear H2.
 133     elim b;
 134     [ simplify.
 135       intro.
 136       apply H2.
 137       simplify in H3.
 138       apply H3.
 139     | simplify.
 140       intro.
 141       apply H2.
 142       simplify in H3.
 143       apply H3.
 144     ]
 145   ]
 146 qed.
 147
 148 variant rewrite :
 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.
 151   \forall eq_f :
 152     \forall U,U1:Type.
 153     \forall f:U \to U1.\forall x,y:U. eq U x y \to eq U1 (f x) (f y).
 154   \forall b:bool.
 155   \forall U:Type.
 156   \forall context: U \to U.
 157   \forall n:nat.
 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
 162 \def
 163   eq_f_to_mk_Statement.
 164
 165 (*
 166
 167 definition make_eqs_smart' \def
 168   \lambda Univ:Type.
 169   \lambda length:nat.
 170   \lambda initial:Univ.
 171   let rec aux (p:Univ) (n:nat) on n : Prop \def
 172     match n with
 173     [ O \Rightarrow \forall a:Univ. p = a \to initial = a
 174     | (S n) \Rightarrow \forall a:Univ. p = a \to aux a n
 175     ]
 176   in
 177     aux initial length.
 178
 179 theorem transl_smart' :
 180   \forall Univ:Type.\forall n:nat.\forall initial:Univ.
 181     make_eqs_smart' Univ n initial.
 182   intros.
 183   unfold make_eqs_smart'.
 184   elim n
 185   [ simplify.intros.assumption
 186   | simplify.intros.rewrite < H1.assumption
 187   ]
 188 qed.
 189
 190 theorem prova':
 191   \forall Univ:Type.
 192   \forall a,b:Univ.
 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.
 196   plus a b = plus b b.
 197   intros.
 198   apply (transl_smart' ? (S O) ? ? (H a b) ? H1).
 199 qed.
 200
 201 *)