1
私はブール値の2つのリストが同等であることを証明しようとしています（明らかにリストを構造的に歩く平等の定義を使用していれば）、それらの長さは同じです。そうすることの過程で仮説が偽であることを示すために仮説をどのようにターゲットにして変換するか？
は、しかし、私は無人島/偽であるという仮説と状況に終わるが、文字通りFalse（ひいてはcontradiction戦術の標的とすることはできません）ではありません。
これまで私がこれまで持っていたことは次のとおりです。この後
Require Import Coq.Lists.List.
Require Export Coq.Bool.Bool.
Require Import Lists.List.
Import ListNotations.
Open Scope list_scope.
Open Scope nat_scope.
Fixpoint list_bool_eq (a : list bool) (b: list bool) : bool :=
match (a, b) with
| ([], []) => true
| ([], _) => false
| (_, []) => false
| (true::a', true::b') => list_bool_eq a' b'
| (false::a', false::b') => list_bool_eq a' b'
| _ => false
end.
Fixpoint length (a : list bool) : nat :=
match a with
| [] => O
| _::a' => S (length a')
end.
Theorem equal_implies_same_length : forall (a b : list bool) , (list_bool_eq a b) = true -> (length a) = (length b).
intros.
induction a.
induction b.
simpl. reflexivity.
、のCoQの「目標状態」（何が正しい言葉だ？）coqideによって示されるように、このようになります。
余分なディテールの一部を離れてクリア2 subgoals
a : bool
b : list bool
H : list_bool_eq [] (a :: b) = true
IHb : list_bool_eq [] b = true -> length [] = length b
______________________________________(1/2)
length [] = length (a :: b)
______________________________________(2/2)
length (a :: a0) = length b
...
Focus 1.
clear IHb.
私たちは、私たちに
1 subgoal
a : bool
b : list bool
H : list_bool_eq [] (a :: b) = true
______________________________________(1/1)
length [] = length (a :: b)
を取得し、人間として、length [] = length (a :: b)は無人島/明確に偽ですが、ので、それは大丈夫ですH : list_bool_eq [] (a :: b) = trueもfalseです。
しかし、仮説Hは、文字通りFalseではないため、contradictionを使用することはできません。
仮説Hの "Coqの観点から私の注意を集中させる"ことができますので、私はそれが無人であることを示すことができます。与えられた仮説が間違っていることを示すために私の証拠の中に新しい文脈を作成する証明書箇条とおおよそ類似したものがありますか？-, +, *, { ... }