証明支援システムの一つで、プログラミング言語Gallinaを用いています。
Q&A
1回答
620閲覧
総合スコア6
0グッド
0クリップ
投稿2020/06/28 03:29
0
coqで2 ^ k + 2 ^ k = 2 ^ (k + 1)の等式でexpnD.を適応したい
expnD : forall m n1 n2 : nat, m ^ (n1 + n2) = m ^ n1 * m ^ n2 Lemma expn_twice: forall (k : nat), 2^k + 2^k = 2^(k+1).
左側の2^(k+1)の部分にexpnDを適応したいが出来ない
気になる質問をクリップする
クリップした質問は、後からいつでもMYページで確認できます。
またクリップした質問に回答があった際、通知やメールを受け取ることができます。
バッドをするには、ログインかつ
こちらの条件を満たす必要があります。
質問へのコメント
回答1件
move=> k. rewrite expnD.
すると、左辺が 2 ^ k * 2 ^ 1 になりますから、さらに
rewrite expn1 muln2 -addnn.
で書き換えると右辺と同じになります。
すこしまとめると、以下のようになります。
Lemma expn_twice: forall (k : nat), 2^k + 2^k = 2^(k+1). Proof. move=> k. rewrite expnD expn1 muln2 -addnn. done. Qed.
以上
投稿2021/06/19 23:24
総合スコア12
あなたの回答
tips
太字
斜体
打ち消し線
見出し
引用テキストの挿入
コードの挿入
リンクの挿入
リストの挿入
番号リストの挿入
表の挿入
水平線の挿入
プレビュー
まだベストアンサーが選ばれていません
アカウントをお持ちの方はログイン
15分調べてもわからないことはteratailで質問しよう!
ただいまの回答率85.29%
質問をまとめることで思考を整理して素早く解決
テンプレート機能で簡単に質問をまとめる
バッドをするには、ログインかつ
こちらの条件を満たす必要があります。