matita/matita/tests/rewrite.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
  16 include "coq.ma".
  17
  18 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
  19 alias num (instance 0) = "Coq natural number".
  20 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
  21 alias symbol "plus" (instance 0) = "Coq's natural plus".
  22 alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
  23
  24 theorem a:
  25   \forall a,b:nat.
  26   a = b \to b + a + b + a= (\lambda j.((\lambda w.((\lambda x.x + b + w + j) a)) b)) a.
  27 intros.
  28 rewrite < H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)).
  29
  30 rewrite < H in \vdash (? ? % ?).
  31
  32 simplify in \vdash (? ? ? ((\lambda _.((\lambda _.%) ?)) ?)).
  33
  34 rewrite < H in \vdash (? ? ? (% ?)).
  35 simplify.
  36 reflexivity.
  37 qed.
  38
  39 theorem t: \forall n. 0=0 \to n = n + 0.
  40  intros.
  41  apply plus_n_O.
  42 qed.
  43
  44 (* In this test "rewrite < t" should open a new goal 0=0 and put it in *)
  45 (* the goallist so that the THEN tactical closes it using reflexivity. *)
  46 theorem foo: \forall n. n = n + 0.
  47  intros.
  48  rewrite < t; reflexivity.
  49 qed.
  50
  51 theorem test_rewrite_in_hyp:
  52           \forall n,m. n + 0 = m \to m = n + 0 \to n=m \land m+0=n+0.
  53  intros.
  54  rewrite < plus_n_O in H.
  55  rewrite > plus_n_O in H1.
  56  split; [ exact H | exact H1].
  57 qed.
  58
  59 theorem test_rewrite_in_hyp2:
  60           \forall n,m. n + 0 = m \to n + 0 = m \to n=m \land n+0=m.
  61  intros.
  62  rewrite < plus_n_O in H H1 \vdash (? ? %).
  63  split; [ exact H | exact H1].
  64 qed.
  65
  66 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
  67 theorem test_rewrite_under_pi: \forall x,y. x = O \to y = O \to x = x \to O = x.
  68 intros 3.
  69 rewrite > H in \vdash (? \to ? ? % % \to ? ? ? %).
  70 intros. reflexivity.
  71 qed.