Ошибка Coq: невозможно объединить true с is_true (0 ‹a - b - 3)

Не уверен, что делаю неправильно, но я думал, что reflexivity должен работать ниже, но это не так.

a, b : nat
H : (1 <=? a - b - 3) = true
______________________________________(1/7)
is_true (0 < a - b - 3)

Я также пробовал apply leb_complete in H., в результате чего:

a, b : nat
H : (1 <= a - b - 3)%coq_nat
______________________________________(1/7)
is_true (0 < a - b - 3)

но в обоих случаях Coq выдает ошибку Unable to unify "true" with "is_true (0 < a - b - 3)"

Это не должно быть так сложно, правда? Я что-то упустил?


coq proof coq-tactic formal-verification
person Dan Johnson    schedule 02.10.2020    source источник
comment
Можете добавить импорт?   -  person Blaisorblade    schedule 02.10.2020
comment
@Blaisorblade, вот он From mathcomp Require Import all_ssreflect. Require Import String Arith Strings.Byte Init.Byte Init.Nat Coq.Lists.List Coq.Program.Wf.   -  person Dan Johnson    schedule 02.10.2020

Ответы (1)


arrow_upward
2
arrow_downward

Во-первых, «не должно быть ничего сложного» - неправильный вопрос.

reflexivity - это тактика, которая никогда не использует предположения и пытается доказать цели очень конкретным способом. Для «простых» чисто числовых целей p вы можете использовать lia.

Он может только доказать, что цели можно преобразовать в форму R a1 a2, где R - рефлексивное отношение (например, равенство), а a1 и a2 - конвертируемые. И два члена могут быть преобразованы, если приведение их к нормальной форме дает «тот же» результат (с учетом некоторых сложностей для эта-разложения).

Например, рефлексивность может доказать, что 2 + 2 + 0 = 4 или что 0 + n = n. Но он не может доказать, что n + 0 = n (что можно доказать с помощью lia), потому что n + 0 - нормальная форма.

person Blaisorblade    schedule 02.10.2020
comment
Спасибо за разъяснения. Однако, используя lia., Coq жалуется, что Tactic failure: Cannot find witness. - person Dan Johnson; 02.10.2020
comment
Я решил проблему провала тактики, о которой упоминал ранее, переписав цель как rewrite -?(rwP ltP)., а затем использовал lia.. Для получения дополнительной информации см. Этот пост stackoverflow.com/questions/61029979/ Итак, я собираюсь принять этот ответ. - person Dan Johnson; 02.10.2020