Coq proof тактика

Question

Я новичок в Coq proof system (около 4 дней). Я очень старался, но я не могу доказать следующее.

forall a b c : nat, S (S (a + b)) = S (S (a + c)) -> b = c. 

Насколько я знаю, мы должны доказать биективность +, так что мы можем каким-то образом использовать f(b) = f(c) -> b = c. Как мне это сделать ?

Answer 1

Как указано в ответе Винца, вы можете найти теорему о биективности около plus непосредственно в стандартной библиотеке Coq. Вы также можете доказать это напрямую, используя примитивную тактику и математическую индукцию на a следующим образом.

Theorem plus_l_bij: forall a b c : nat, a + b = a + c -> b = c. 
Proof. 
induction a as [|a']. 
    intros b c H. apply H. 
    intros b c H. simpl plus in H. inversion H. apply IHa' in H1. apply H1. 
Qed. 

После induction a, базовый вариант a = 0 тривиально.

Доказательство для второго случая a = S a', перестраивает

S a' + b = S a' + c 

в

S (a' + b) = S (a' + c) 

, а затем удаляет конструктор S используя его биективность. Наконец, предположение индукции может быть применено для завершения доказательства.

Answer 2

Используя SearchAbout plus или SearchPattern (_ + _ = _ + _ -> _), вы можете проверить доступные леммы о +. Но если вы не импортировали правильные модули, это может быть бесполезным. То, что я обычно делаю, это то, что я смотрю онлайн-документацию. Here is the documentation for plus, и вы можете иметь конкретный вид plus_reg_l и plus_reg_r.