İçindekiler için bir endüktif terim değerini ekler Coq taktiği

Question

Sadece bu konuyu basit bir örnek vermek için koşmaya devam ediyorum, varsayalım forall f : nat -> bool, exists i j, i<>j /\ f i = f j. ispat etmek istediğimi varsayın f 0, f 1, f 2, değerlerini kontrol edin ve buna göre ilerleyin . Ancak, destruct (f 0) derken, Coq hedefi değiştirmiyor, çünkü f 0 bir alt öğe olarak gerçekleşmiyor. Bu nedenle, şu anda f 0 değerinin ne kadar sürdüğü hakkında bilgim yok. İdeal olarak, Coq'un bir izleyene H : f 0 = false tanığını eklemesini istiyorum, böylece izlemeye devam edebilirim.

Bu sorunları çözmek için yaptığım şey, yardımcı bir lemma bool_destruct : forall b : bool, b = false \/ b = true olduğunu kanıtlamaktır. Şimdi, destruct (bool_destruct (f 0)) Coq diyorsam, bağlam için istenen H ekleyecektir. Doğal olarak, bu her endüktif tip için bu tür bir lemma ispat etmeniz gerektiğinde sıkıcıdır. Böylece, bu tür durumları ele alan güzel bir taktik var mı diye merak ediyorum.

Answer 1

zaten imha taktik istediğini destekler:

destruct (f 0) eqn:f_is0. 

bool_destruct Eğer, örneğin, olmasını benzer bir düşünce artı case bir model genelleme özelliğini yapmak kadar kötü değil kullanmanın Fikrin taktik, özel imha görünümleri sağlamak için matematik-comp kullanılır.