helm/software/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
  19 definition make_eqs_smart \def
  20   \lambda Univ:Type.
  21   \lambda length:nat.
  22   \lambda initial:Univ.
  23   let rec aux (p:Univ) (n:nat) on n : Prop \def
  24     match n with
  25     [ O \Rightarrow \forall a:Univ. p = a \to initial = a
  26     | (S n) \Rightarrow \forall a:Univ. p = a \to aux a n
  27     ]
  28   in
  29     aux initial length.
  30
  31 theorem transl_smart :
  32   \forall Univ:Type.\forall n:nat.\forall initial:Univ.
  33     make_eqs_smart Univ n initial.
  34   intros.
  35   unfold make_eqs_smart.
  36   elim n
  37   [ simplify.intros.assumption
  38   | simplify.intros.rewrite < H1.assumption
  39   ]
  40 qed.
  41
  42 theorem prova:
  43   \forall Univ:Type.
  44   \forall a,b:Univ.
  45   \forall plus: Univ \to Univ \to Univ.
  46   \forall H:\forall x,y:Univ.plus x y = plus y x.
  47   \forall H1:plus b a = plus b b.
  48   plus a b = plus b b.
  49   intros.
  50   apply (transl_smart ? (S O) ? ? (H a b) ? H1).
  51 qed.
  52