helm/software/matita/tests/a.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 axiom A : Prop.
  16 axiom B : Prop.
  17 axiom C : Prop.
  18 axiom a: A.
  19 axiom b: B.
  20
  21 definition xxx ≝ A.
  22
  23 notation "#" non associative with precedence 90 for @{ 'sharp }.
  24 interpretation "a" 'sharp = a.
  25 interpretation "b" 'sharp = b.
  26
  27 definition k : A → A ≝ λx.a.
  28 definition k1 : A → A ≝ λx.a.
  29
  30 axiom P : A → Prop.
  31
  32 include "nat/plus.ma".
  33
  34 ntheorem pappo : ∀n:nat.n = S n + n → S n = (S (S n)).
  35 #m; #H; napply (let pippo ≝ (S m) in ?);
  36 nchange in match (S m) in ⊢ (?) with pippo;
  37
  38 nletin pippo ≝ (S m) in H ⊢ (?);
  39
  40 nwhd in H:(???%);
  41 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
  42 ntaint;
  43
  44 ngeneralize in match m in ⊢ %;   in ⊢ (???% → ??%?);
  45 STOP
  46 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
  47 nelim (S m) in H : (??%?) ⊢ (???%);
  48 STOP;
  49
  50 ntheorem pippo : ∀x:A. P (k x).
  51 nchange in match (k x) in ⊢ (∀_.%) with (k1 x); STOP
  52
  53 ntheorem prova : (A → A → C) → C.
  54 napply (λH.?);
  55 napply (H ? ?); nchange A xxx;
  56 napply #.
  57 nqed.