helm/matita/tests/rewrite.ma

   1 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
   2 alias num (instance 0) = "natural number".
   3 alias symbol "eq" (instance 0) = "leibnitz's equality".
   4 alias symbol "plus" (instance 0) = "natural plus".
   5
   6 (* with the unary [[ - ]] we point the term that the path refers to *)
   7 theorem a:
   8   \forall a,b:nat.
   9   a = b \to a + b = ((\lambda w.((\lambda x.x + b) a)) b).
  10 intros.
  11
  12 (* a + b = (\w.(\x. [[ x + b ]] ) a) b *)
  13 rewrite right H in \vdash (? ? ? ((\lambda x.%) ?)).
  14
  15 (* [[ a + b ]] = (\w.(\x.x + a) a) b *)
  16 rewrite right H in \vdash (? ? % ?).
  17
  18 (* a + a = (\w. [[ (\x.x + a) a ]] b *)
  19 simplify in \vdash (? ? ? ((\lambda x.%) ?)).
  20
  21 (* a + a = (\w.a + a) [[ b ]] *)
  22 rewrite right H in \vdash (? ? ? (? %)).
  23 simplify.
  24 reflexivity.
  25 qed.