matitaB/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   ...