私は、仮説が論理和であるCoqの単純な補題を証明しようとしています。split
ゴールで論理和が発生したときに論理和する方法は知っていますが、仮説に現れたときに論理和を分割することはできません。これが私の例です:
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) \/ (n > 8)) -> ((n > 7) \/ (n < 6)).
Proof.
intros n H1.
split H1. (** this doesn't work ... *)
そして、これがCoqの言うことです:
1 subgoal
n : nat
H1 : n < 5 \/ n > 8
______________________________________(1/1)
n > 7 \/ n < 6
エラーあり:
Error: Illegal tactic application.
私は明らかに単純なものが欠けています。どんな助けでも大歓迎です、ありがとう!
あなたが望む戦術はですdestruct
。
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) \/ (n > 8)) -> ((n > 7) \/ (n < 6)).
Proof.
intros n H1.
destruct H1.
結果の仮説に名前を付けたい場合は、次のことができますdestruct H1 as [name1 | name2].
。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加