]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/ng_auto.ma
update in basic_2
[helm.git] / matitaB / 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=3;
52 nqed.
53
54 nlemma traz:
55   ∀T:Type[0].
56   ∀And: CProp[0] → CProp[0] → CProp[0] → CProp[0].
57   ∀And_elim : ∀a,b,c.a → b → c → And a b c. 
58   ∀C: T → T → T → CProp[0].
59   ∀B: T → T → CProp[0].
60   ∀A: T → CProp[0].
61   ∀a,b,c:T.
62   ∀p2:A b.
63   ∀p1:A a.
64   ∀p3:B a b. 
65   ∀p3:B b b. 
66   ∀p4:B b a.  
67   ∀p3:B a a. 
68   ∀p5:C a a a.
69   (λx,y,z:T.And (A x) (B x y) (C x y z)) ???.
70 ##[ #T; #And; #And_intro; #A; #B;  #C; #a;  #b; #p1; #p2; #p3; #p4; #p5;
71     #p6; #p7; nauto;