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);
28 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
31 ngeneralize in match m in ⊢ %; in ⊢ (???% → ??%?);
33 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
34 nelim (S m) in H : (??%?) ⊢ (???%);
42 include "nat/plus.ma".
44 ntheorem foo: ∀n. n+n=n → n=n → n=n.
45 #n; #H; #K; nrewrite < H in (*K: (???%) ⊢*) ⊢ (??%?); napply (eq_ind ????? H);
47 include "logic/connectives.ma".
51 notation "†" non associative with precedence 90 for @{ 'sharp }.
52 interpretation "a" 'sharp = a.
53 interpretation "b" 'sharp = b.
55 include "nat/plus.ma".
57 (*ntheorem foo: ∀n:nat. match n with [ O ⇒ n | S m ⇒ m + m ] = n.*)
59 (*ntheorem prova : ((A ∧ A → A) → (A → B) → C) → C.
60 # H; nassert H: ((A ∧ A → A) → (A → B) → C) ⊢ C;
61 napply (H ? ?); nassert H: ((A ∧ A → A) → (A → B) → C) ⊢ (A → B)
62 H: ((A ∧ A → A) → (A → B) → C) ⊢ (A ∧ A → A);
64 definition k : A → A ≝ λx.a.
65 definition k1 : A → A ≝ λx.a.
69 include "nat/plus.ma".
71 ntheorem pappo : ∀n:nat.n = S n + n → S n = (S (S n)).
72 #m; #H; napply (let pippo ≝ (S m) in ?);
73 nchange in match (S m) in ⊢ (?) with pippo;
76 nletin pippo ≝ (S m) in H ⊢ (?);
79 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
82 ngeneralize in match m in ⊢ %; in ⊢ (???% → ??%?);
84 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
85 nelim (S m) in H : (??%?) ⊢ (???%);
88 ntheorem pippo : ∀x:A. P (k x).
89 nchange in match (k x) in ⊢ (∀_.%) with (k1 x); STOP
91 ntheorem prova : (A → A → C) → C.
93 napply (H ? ?); nchange A xxx;
101 { r1 : T1, ..., r2 : T2 }
103 reflexivity apply REFL
107 apply (reflexivite S)