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 STOP;
  23
  24 nwhd in H:(???%);
  25 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
  26 ntaint;
  27
  28 ngeneralize in match m in ⊢ %;   in ⊢ (???% → ??%?);
  29 STOP
  30 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
  31 nelim (S m) in H : (??%?) ⊢ (???%);
  32 STOP;
  33 axiom A : Prop.
  34 axiom B : Prop.
  35 axiom C : Prop.
  36 axiom a: A.
  37 axiom b: B.
  38
  39 include "nat/plus.ma".
  40 (*
  41 ntheorem foo: ∀n. n+n=n → n=n → n=n.
  42  #n; #H; #K; nrewrite < H in (*K: (???%) ⊢*) ⊢ (??%?); napply (eq_ind ????? H);
  43 *)
  44 include "logic/connectives.ma".
  45
  46 definition xxx ≝ A.
  47
  48 notation "†" non associative with precedence 90 for @{ 'sharp }.
  49 interpretation "a" 'sharp = a.
  50 interpretation "b" 'sharp = b.
  51
  52 include "nat/plus.ma".
  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   ...