]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/ng_tactics.ma
init_copy init_match
[helm.git] / matita / matita / tests / ng_tactics.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 include "ng_pts.ma".
16 include "nat/plus.ma".
17
18 ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).
19 #m; #H;
20                                  nassert m:nat H: (m=S m + m) ⊢ (S m = S (S m));
21 nletin pippo ≝ (S m) in H: % ⊢ (???%);
22             nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → S m = S pippo);
23 #H; nchange in match pippo in H:% with (pred (S pippo));
24  nassert m:nat pippo : nat ≝ (S m) H:(m = pred (S pippo) + m) ⊢ (S m = S pippo);
25 ngeneralize in match m in H:(??%?) ⊢ %;
26  nassert m:nat pippo : nat ≝ (S m) ⊢ (∀n:nat. n=(pred (S pippo)+m) → (S n)=S pippo);
27 #x; #H;
28  nassert m:nat pippo : nat ≝ (S m) x: nat H:(x = pred (S pippo) + m) ⊢ (S x = S pippo);
29 nwhd in H: (?%? (?%?));
30            nassert m:nat pippo:nat≝(S m) x:nat H:(x=S m + m) ⊢ (S x = S pippo);
31 nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?));
32 ngeneralize in match H;
33 napply (? H);
34 nelim m in ⊢ (???(?%?) → %);
35 nnormalize;
36  ##[ ncases x in H ⊢ (? → % → ?);
37  ##|
38  ##]
39 STOP;
40
41 axiom A : Prop.
42 axiom B : Prop.
43 axiom C : Prop.
44 axiom a: A.
45 axiom b: B.
46
47 include "logic/connectives.ma".
48
49 definition xxx ≝ A.
50
51 notation "†" non associative with precedence 90 for @{ 'sharp }.
52 interpretation "a" 'sharp = a.
53 interpretation "b" 'sharp = b.
54
55 ntheorem foo: ∀n:nat. match n with [ O ⇒ n | S m ⇒ m + m ] = n.
56
57 (*ntheorem prova : ((A ∧ A → A) → (A → B) → C) → C.
58 # H; nassert H: ((A ∧ A → A) → (A → B) → C) ⊢ C;
59 napply (H ? ?); nassert H: ((A ∧ A → A) → (A → B) → C) ⊢ (A → B)
60                         H: ((A ∧ A → A) → (A → B) → C) ⊢ (A ∧ A → A);
61  ##[#L | *; #K1; #K2]
62 definition k : A → A ≝ λx.a.
63 definition k1 : A → A ≝ λx.a.
64 *)
65 axiom P : A → Prop.
66
67 include "nat/plus.ma".
68
69 ntheorem pappo : ∀n:nat.n = S n + n → S n = (S (S n)).
70 #m; #H; napply (let pippo ≝ (S m) in ?);
71 nchange in match (S m) in ⊢ (?) with pippo;
72 STOP (BUG)
73
74 nletin pippo ≝ (S m) in H ⊢ (?); 
75
76 nwhd in H:(???%); 
77 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));  
78 ntaint;
79
80 ngeneralize in match m in ⊢ %;   in ⊢ (???% → ??%?);
81 STOP 
82 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
83 nelim (S m) in H : (??%?) ⊢ (???%);
84 STOP;
85
86 ntheorem pippo : ∀x:A. P (k x).
87 nchange in match (k x) in ⊢ (∀_.%) with (k1 x); STOP
88
89 ntheorem prova : (A → A → C) → C.
90 napply (λH.?);
91 napply (H ? ?); nchange A xxx; 
92 napply †.
93 nqed. 
94
95 REFL
96
97 G
98
99 { r1 : T1, ..., r2 : T2 }
100
101 reflexivity  apply REFL
102   =
103   apply (eq_refl ?);
104   apply (...)
105   apply (reflexivite S)
106   ...