Сравнивая два неравных значения в coq

Question

Я доказываю эту лемму:

Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.

Lemma test: forall (val1 val2: int), ((Vint val1) <> (Vint val2)) -> (Some (Val.cmp Ceq (Vint val1) (Vint val2)) = Some Vfalse).
Proof.

Admitted.

Я пробовал разворачиваться not, Val.cmp, ... и используя rewrite над H но никуда не ходил. Любая помощь приветствуется.

Спасибо

Answer 1

К сожалению, оригинальная теорема, которую вы имели, была ложной. Проблема заключалась в том, что Val.cmp возвращается Vundef если одно из сравниваемых значений не является целым числом Проверьте определение cmp а также cmp_bool здесь

Ваша новая теорема верна, но изложена не в очень полезной форме. Лучше сформулировать это так:

forall val1 val2, val1 <> val2 -> Val.cmp Ceq (Vint val1) (Vint val2) = Vfalse

Имея Vint а также Some Конструкторы вокруг равенств не изменяют истинность вашей теоремы, но затрудняют ее применение в большинстве конкретных ситуаций. Этот результат должен следовать разворачиваясь Val.cmp, Val.cmp_bool, а также Int.cmpи переписать с Int.eq_false,