Coq如何定位並轉換假設以表明它們是假的？

我試圖證明，如果兩個布爾表的列表是相等的（使用一個相等的定義，以明顯的方式在結構上列出結構列表），那麼它們具有相同的長度。然而，在這樣做的過程中，我最終處於一種錯誤/無人居住的假設，但不是字面上的False（因此不能以contradiction策略爲目標）。Coq如何定位並轉換假設以表明它們是假的？

這是我到目前爲止。

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.

在此之後，如圖coqide COQ的「目標國家」（什麼是正確的字？）看起來是這樣的。

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也是錯誤的。

但是，假設H並非字面上False，所以我們不能只使用contradiction。

我該如何針對假設H的目標/「將我的注意力從Coq的角度着眼」，這樣我就可以證明它是無人居住的。是否有類似於證明子彈-, +, *, { ... }的東西在我的證明中創建了一個新的上下文，專門用於顯示給定的假設是錯誤的？

來源

2017-07-11 Gregory Nisbet

如果你簡化你的假設（simpl in H），你會看到它相當於false = true。在這一點上，你可以用easy策略來完成目標，即使它們在語法上等於False，它也能夠排除這種「明顯」的矛盾。事實上，你甚至不需要事先進行簡化; easy應該足夠強大以找出矛盾本身。

（最好證明以下更強的結果：forall l1 l2, list_bool_eq l1 l2 = true <-> l1 = l2。）

來源

2017-07-11 22:27:44

Coq如何定位並轉換假設以表明它們是假的？

回答

相關問題