1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "nat/plus.ma".
17 ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).
19 nassert m:nat H: (m=S m + m) ⊢ (S m = S (S m));
20 nletin pippo ≝ (S m) in H: % ⊢ (???%);
21 nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → S m = S pippo);
22 #H; nchange in match pippo in H:% with (pred (S pippo));
23 nassert m:nat pippo : nat ≝ (S m) H:(m = pred (S pippo) + m) ⊢ (S m = S pippo);
24 ngeneralize in match m in H:(??%?) ⊢ %;
25 (* nassert m:nat pippo : nat ≝ (S m) ⊢ (nat → eq nat __1 (pippo+m) → pippo=S pippo); *)
27 nassert m:nat pippo : nat ≝ (S m) x: nat H:(x = pred (S pippo) + m) ⊢ (S x = S pippo);
28 nwhd in H: (?%? (?%?));
29 nassert m:nat pippo:nat≝(S m) x:nat H:(x=S m + m) ⊢ (S x = S pippo);
30 nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?));
31 ngeneralize in match H;
33 nelim m in ⊢ (???(?%?) → %); (*SBAGLIA UNIFICATORE*)
35 ##[ ncases x in H ⊢ (? → % → ?);
46 include "logic/connectives.ma".
50 notation "†" non associative with precedence 90 for @{ 'sharp }.
51 interpretation "a" 'sharp = a.
52 interpretation "b" 'sharp = b.
54 ntheorem foo: ∀n:nat. match n with [ O ⇒ n | S m ⇒ m + m ] = n.
56 (*ntheorem prova : ((A ∧ A → A) → (A → B) → C) → C.
57 # H; nassert H: ((A ∧ A → A) → (A → B) → C) ⊢ C;
58 napply (H ? ?); nassert H: ((A ∧ A → A) → (A → B) → C) ⊢ (A → B)
59 H: ((A ∧ A → A) → (A → B) → C) ⊢ (A ∧ A → A);
61 definition k : A → A ≝ λx.a.
62 definition k1 : A → A ≝ λx.a.
66 include "nat/plus.ma".
68 ntheorem pappo : ∀n:nat.n = S n + n → S n = (S (S n)).
69 #m; #H; napply (let pippo ≝ (S m) in ?);
70 nchange in match (S m) in ⊢ (?) with pippo;
73 nletin pippo ≝ (S m) in H ⊢ (?);
76 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
79 ngeneralize in match m in ⊢ %; in ⊢ (???% → ??%?);
81 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
82 nelim (S m) in H : (??%?) ⊢ (???%);
85 ntheorem pippo : ∀x:A. P (k x).
86 nchange in match (k x) in ⊢ (∀_.%) with (k1 x); STOP
88 ntheorem prova : (A → A → C) → C.
90 napply (H ? ?); nchange A xxx;
98 { r1 : T1, ..., r2 : T2 }
100 reflexivity apply REFL
104 apply (reflexivite S)