WikiHub :: coq :: tactics.txt

仮定が... f x simpl in Hで仮定Hの簡約ができる x = y rewriteで、式の一部分を書き換える。 rewrite H with (x := 1) (y := 2)のように変数の対応を指定することもできる AssociativityOfAppend < Show. 1 subgoal A : Type a : A x : list A y : list A z : list A IHx : (x +++ y) +++ z = x +++ (y +++ z) ============================ a :: (x +++ y) +++ z = a :: x +++ (y +++ z) AssociativityOfAppend < rewrite IHx. 1 subgoal A : Type a : A x : list A y : list A z