これは楽勝。
Lemma l2: forall (n:nat), n=n+0. Proof. intros. induction n. reflexivity. simpl. f_equal. apply IHn. Qed.
しかし式をforall (n:nat), n>1 -> n=n+0.にすると、
普通にやると、ゴールがn>1、仮定がS n>1となりうまくいきません。
そこで、
assert((n>1->n=n+0)->(S n>1->n=n+0)).
をはさみます。
Lemma l3: forall (n:nat), n>1 -> n=n+0. Proof. intros. induction n. reflexivity. (* ここがポイント *) assert((n>1->n=n+0)->(S n>1->n=n+0)). omega. apply H0 in IHn. simpl. f_equal. apply IHn. apply H. Qed.
こうするとうまくいきます。
・assertがomega一発で解けない場合
Lemma l4_2: forall (a b:nat), 1<a -> 1<b -> 1<a*b. Proof. intros. induction a. assert(1<0->False). omega. apply H1 in H. apply False_ind. auto. (* ここがポイント *) assert((1<a -> 1<a*b)->(1<S a -> 1<a*b)). intros. apply gt_S in H2. destruct H2 as [ HA | HB ]. omega. rewrite <- HB. omega. apply H1 in IHa. simpl. omega. apply H. Qed.
・もっと複雑な例（式としては変だけど）
Lemma l1_4: forall (n x y z:nat), n>3 -> x>1 -> y>1 -> z>1 -> 4 = 3*(1/x +1/y +1/z) -> 4 = n*(1/x +1/y +1/z). Proof. intros. induction n. assert(0>3->False). omega. apply H4 in H. apply False_ind. auto. (* ここがポイント *) assert((n>3->4=n*(1/x+1/y+1/z))->(S n>3->4=n*(1/x+1/y+1/z))). intros. apply gt_S in H5. destruct H5 as [ HA | HB ]. apply H4. apply HA. rewrite <- HB. apply H3. apply H4 in IHn. simpl. pattern x at 2. rewrite (Nat.div_small 1 x). pattern y at 2. rewrite (Nat.div_small 1 y). pattern z at 2. rewrite (Nat.div_small 1 z). simpl. apply IHn. auto. auto. auto. auto. Qed.
