helm/software/matita/tests/ng_auto.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 universe constraint Type[0] < Type[1].
  16 universe constraint Type[1] < Type[2].
  17
  18 naxiom T : Type[0].
  19 naxiom P : T → T → CProp[0].
  20 naxiom Q : T → CProp[0].
  21 naxiom f : T → T → T.
  22
  23 naxiom f_com : ∀x,y. P (f x y) (f y x).
  24 naxiom f_Q : ∀x,y. P x y → Q (f x y).
  25
  26 nlemma foo : ∀x,y. Q x → Q (f (f x y) (f y x)).
  27 #x; #y; #H;
  28 ncut (Q x);
  29 ##[##2: #_; nauto;
  30 ##| nassumption;
  31 ##]
  32 nqed.
  33
  34 naxiom And : CProp[0] → CProp[0] → CProp[0].
  35 naxiom And_intro : ∀A,B.A → B → And A B.
  36
  37 naxiom zero : T.
  38 naxiom succ : T → T.
  39 naxiom is_nat : T → CProp[0].
  40 naxiom is_nat_0 : is_nat zero.
  41 naxiom is_nat_S : ∀x.is_nat x → is_nat (succ x).
  42
  43 nlemma bar : ∀P:T → CProp[0].P (succ zero) → (λx.And (is_nat x) (P x)) ?.
  44 ##[ #P; #H; nwhd; napply And_intro; ##] nauto.
  45 nqed.
  46
  47 naxiom A : CProp[0].
  48 naxiom pA : A.
  49
  50 nlemma baz : ∀P,Q:CProp[0].(A → P) → (And A P → Q) → Q.
  51 nauto depth=4;
  52 nqed.