helm/software/matita/tests/continuationals.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 set "baseuri" "cic:/matita/tests/continuationals".
  16 include "../legacy/coq.ma".
  17
  18 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
  19 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
  20 alias id "trans_equal" = "cic:/Coq/Init/Logic/trans_equal.con".
  21 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
  22 alias id "Z" = "cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1)".
  23
  24 theorem semicolon: \forall p:Prop.p\to p\land p.
  25 intros (p); split; assumption.
  26 qed.
  27
  28 theorem branch:\forall x:nat.x=x.
  29 intros (n);
  30 elim n
  31 [ reflexivity;
  32 | reflexivity ].
  33 qed.
  34
  35 theorem pos:\forall x:Z.x=x.
  36 intros (n);
  37 elim n;
  38 [ 3: reflexivity;
  39 | 2: reflexivity;
  40 | reflexivity ]
  41 qed.
  42
  43 theorem dot:\forall x:Z.x=x.
  44 intros (x).
  45 elim x.
  46 reflexivity. reflexivity. reflexivity.
  47 qed.
  48
  49 theorem dot_slice:\forall x:Z.x=x.
  50 intros (x).
  51 elim x;
  52 [ elim x. reflexivity. reflexivity. reflexivity;
  53 | reflexivity
  54 | reflexivity ];
  55 qed.
  56
  57 theorem focus:\forall x:Z.x=x.
  58 intros (x); elim x.
  59 focus 16 17;
  60   reflexivity;
  61 unfocus.
  62 reflexivity.
  63 qed.
  64
  65 theorem skip:\forall x:nat.x=x.
  66 intros (x).
  67 apply trans_equal;
  68 [ 2: apply (refl_equal nat x);
  69 | skip
  70 | reflexivity
  71 ]
  72 qed.
  73
  74 theorem skip_focus:\forall x:nat.x=x.
  75 intros (x).
  76 apply trans_equal;
  77 [ focus 18; apply (refl_equal nat x); unfocus;
  78 | skip
  79 | reflexivity ]
  80 qed.