helm/matita/tests/replace.ma

   1 set "baseuri" "cic:/matita/tests/replace/".
   2 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
   3 alias num (instance 0) = "natural number".
   4 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
   5 alias symbol "plus" (instance 0) = "Coq's natural plus".
   6 alias symbol "times" (instance 0) = "Coq's natural times".
   7 alias id "mult_n_O" = "cic:/Coq/Init/Peano/mult_n_O.con".
   8 alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
   9
  10 theorem t: \forall x:nat. x * (x + 0) = (0 + x) * (x + x * 0).
  11  intro.
  12  replace in \vdash (? ? (? ? %) (? % %)) with x.
  13  reflexivity.
  14  rewrite < mult_n_O x.
  15  rewrite < plus_n_O x.
  16  reflexivity.
  17  reflexivity.
  18  auto.
  19 qed.
  20
  21 (* This test tests "replace in match t" where t contains some metavariables *)
  22 theorem t2: 2 + (3 * 4) = (5 + 5) + 2 * 2.
  23  replace in match 5+? with 6 + 4; [reflexivity | reflexivity].
  24 qed.