helm/matita/tests/rewrite.ma

   1 set "baseuri" "cic:/matita/tests/rewrite/".
   2
   3 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
   4 alias num (instance 0) = "natural number".
   5 alias symbol "eq" (instance 0) = "leibnitz's equality".
   6 alias symbol "plus" (instance 0) = "natural plus".
   7 alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
   8
   9 theorem a:
  10   \forall a,b:nat.
  11   a = b \to b + a + b + a= (\lambda j.((\lambda w.((\lambda x.x + b + w + j) a)) b)) a.
  12 intros.
  13 rewrite < H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)).
  14
  15 rewrite < H in \vdash (? ? % ?).
  16
  17 simplify in \vdash (? ? ? ((\lambda _.((\lambda _.%) ?)) ?)).
  18
  19 rewrite < H in \vdash (? ? ? (% ?)).
  20 simplify.
  21 reflexivity.
  22 qed.
  23
  24 theorem t: \forall n. 0=0 \to n = n + 0.
  25  intros.
  26  apply plus_n_O.
  27 qed.
  28
  29 (* In this test "rewrite < t" should open a new goal 0=0 and put it in *)
  30 (* the goallist so that the THEN tactical closes it using reflexivity. *)
  31 theorem foo: \forall n. n = n + 0.
  32  intros.
  33  rewrite < t; reflexivity.
  34 qed.