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