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 ⊢ %; (* BUG *)
  25 STOP;
  26
  27 nwhd in H:(???%);
  28 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
  29 ntaint;
  30
  31 ngeneralize in match m in ⊢ %;   in ⊢ (???% → ??%?);
  32 STOP
  33 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
  34 nelim (S m) in H : (??%?) ⊢ (???%);
  35 STOP;
  36 axiom A : Prop.
  37 axiom B : Prop.
  38 axiom C : Prop.
  39 axiom a: A.
  40 axiom b: B.
  41
  42 include "nat/plus.ma".
  43 (*
  44 ntheorem foo: ∀n. n+n=n → n=n → n=n.
  45  #n; #H; #K; nrewrite < H in (*K: (???%) ⊢*) ⊢ (??%?); napply (eq_ind ????? H);
  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 include "nat/plus.ma".
  56
  57 (*ntheorem foo: ∀n:nat. match n with [ O ⇒ n | S m ⇒ m + m ] = n.*)
  58
  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);
  63  ##[#L | *; #K1; #K2]
  64 definition k : A → A ≝ λx.a.
  65 definition k1 : A → A ≝ λx.a.
  66 *)
  67 axiom P : A → Prop.
  68
  69 include "nat/plus.ma".
  70
  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;
  74 STOP (BUG)
  75
  76 nletin pippo ≝ (S m) in H ⊢ (?);
  77
  78 nwhd in H:(???%);
  79 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
  80 ntaint;
  81
  82 ngeneralize in match m in ⊢ %;   in ⊢ (???% → ??%?);
  83 STOP
  84 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
  85 nelim (S m) in H : (??%?) ⊢ (???%);
  86 STOP;
  87
  88 ntheorem pippo : ∀x:A. P (k x).
  89 nchange in match (k x) in ⊢ (∀_.%) with (k1 x); STOP
  90
  91 ntheorem prova : (A → A → C) → C.
  92 napply (λH.?);
  93 napply (H ? ?); nchange A xxx;
  94 napply †.
  95 nqed.
  96
  97 REFL
  98
  99 G
 100
 101 { r1 : T1, ..., r2 : T2 }
 102
 103 reflexivity  apply REFL
 104   =
 105   apply (eq_refl ?);
 106   apply (...)
 107   apply (reflexivite S)
 108   ...