Coq で相互誘導を試していましたが、最初に定義した型は
Inductive IsEven : nat -> Prop :=
| EvenO : IsEven O
| EvenS n : IsOdd n -> IsEven (S n)
with IsOdd : nat -> Prop :=
| OddS n : IsEven n -> IsOdd (S n).
偶数の和が偶数であることを証明したいと思いました。Fixpoint とパターン マッチングを使用してこれを行うことができました。
Fixpoint even_plus_even (n m : nat) (evenn : IsEven n) (evenm : IsEven m) : IsEven (n + m) :=
match evenn with
| EvenO => evenm
| EvenS n' oddn' => EvenS (n' + m) (odd_plus_even n' m oddn' evenm)
end
with odd_plus_even (n m : nat) (oddn : IsOdd n) (evenm : IsEven m) : IsOdd (n + m) :=
match oddn with
| OddS n' evenn' => OddS (n' + m) (even_plus_even n' m evenn' evenm)
end.
これは、even_plus_evenと の両方を定義しodd_plus_evenます。ここで、戦術を使ってより簡潔な方法でこれを証明したいと思います (できれば事前定義された補題を多く使用せずに、コードを可能な限り自己完結型に保ちます) が、あまり進んでいません。
具体的には、フィックスポイントでできるように、両方を証明し、1 つの補題のみeven_plus_evenをodd_plus_even使用することは可能ですか?
編集:ご回答ありがとうございますLemma ... with ...。構文はまさに私が探していたものでした。実際には
Lemma even_plus_even2 (n m : nat) (evenn : IsEven n) (evenm : IsEven m) : IsEven (n + m)
with odd_plus_even2 (n m : nat) (oddn : IsOdd n) (evenm : IsEven m) : IsOdd (n + m).
Proof.
induction evenn; simpl. assumption. constructor. auto.
induction oddn; simpl. constructor. auto.
Defined.
Fixpoint私の最初の質問とまったく同じ証明用語を生成します。
たとえば、両方の補題を「anding」して 1 つの補題にすることで、同時に両方の補題を証明し、 と を使用proj1して句の左側または右側の部分を抽出できproj2ます。
Lemma even_or_odd_plus_even: forall (n m : nat),
(forall (evenn : IsEven n) (evenm : IsEven m), IsEven (n + m)) /\
(forall (oddn : IsOdd n) (evenm : IsEven m), IsOdd (n + m)).
Proof.
induction n; split; intros;
try destruct (IHn m) as [He Ho];
try apply evenm;
try inversion oddn;
try inversion evenn;
constructor; auto.
Qed.
Definition even_plus_even n m := proj1 (even_or_odd_plus_even n m).
Definition odd_plus_even n m := proj2 (even_or_odd_plus_even n m).
あなたにあげる
even_plus_even : forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
odd_plus_even : forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
2つの句がシェアを共有していることに注意してくださいnとm、彼らはお互いに依存する必要があるため句が個別に証明することができない場合は、必要があります。（ただし、この特定のケースではそうではありません。アントンが示したように、ステートメントを個別に証明できます。）
編集: Vinz ソリューションを見たところです。Lemma にwith構文があるとは知りませんでした (示してくれてありがとう!)。しかし、それは理にかなっているし、この相互依存の定義を行うためのより適切な方法だと思います。
Lemma even_plus_even: forall n m, IsEven n -> IsEven m -> IsEven (n+m)
with odd_plus_even: forall n m, IsOdd n -> IsEven m -> IsOdd (n+m).
Proof.
induction 1; simpl; auto using EvenS.
induction 1; simpl; auto using OddS.
Qed.
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加