сравнивающие два неравных значения в 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_boolhere.

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

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.