Как доказать одинаковые подцели

У меня есть две равные подцели:

prove_me (x::xs) = true

prove_me (x::xs) = true

Доказательства будут равны. Как я могу решить вторую цель, используя первую?


coq coqide coq-tactic
person he11boy    schedule 27.12.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы не можете буквально повторно использовать доказательство одной цели для другой цели, но вы можете доказать вспомогательную лемму:

assert (H : prove_me (x::xs) = true).
{ (* proof of result *) }

Затем вы можете использовать H для выполнения двух подцелей, как только они появятся.

person Arthur Azevedo De Amorim    schedule 27.12.2019
comment
Я согласен с вами. Но если у нас есть не очень большое доказательство. Я имею ввиду последовательность применения тактики лучше будет написать 1, 2 : tactic1; tactic2; ...; tacticN. Здесь 1 и 2 - номера голов - person he11boy; 28.12.2019