Как использовать неравенство для упрощения if-then-else в Coq?

Я нахожусь в середине доказательства, где я сгенерировал два случая

destruct (eq_id_dec Y X)

(eq_id_dec по характеру похож на eq_nat_dec).

Это дает два случая с добавленными предположениями e: Y = X для равенства и n: Y <> X для неравенства соответственно.

В первом случае я могу легко использовать rewrite e или rewrite <- e.

Но как я могу эффективно использовать неравенство во втором случае? Рассмотрим, например. такая цель, как

(if eq_id_dec X Y then AAA else BBB) = BBB

?

Я попробовал unfold eq_id_dec и немного rewriteS, но застрял.


coq coq-tactic
person tinlyx    schedule 07.12.2015    source источник
comment
Есть ли причина, по которой вы не уничтожаете eq_id_dec X Y? Если вы хотите, чтобы функции сокращались, хорошей стратегией всегда будет выполнение точного анализа прецедентов, который они делают.   -  person gallais    schedule 07.12.2015
comment
@gallais Это просто случайно, и мне нужна была симметрия в случае равенства. Но я мог бы использовать (eq_.. X Y), чтобы сделать это немного проще.   -  person tinlyx    schedule 07.12.2015
comment
Я хочу сказать, что если бы вы использовали eq_id_dec X Y, if...then...else... вычислил бы, и вы бы не столкнулись с проблемой, с которой вы столкнулись сейчас.   -  person gallais    schedule 07.12.2015

Ответы (1)


arrow_upward
1
arrow_downward

В идеале вы хотели бы сказать что-то вроде

forall (P : Prop)
       (b : {P} + {~ P})
       (H : ~ P), b = right H.

К сожалению, невозможно показать этот результат без допущения функциональной экстенсиональности, поскольку не существует полезного принципа, позволяющего показать равенство двух доказательств отрицания.

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

Require Import Coq.Arith.Peano_dec.

Lemma sumboolF T P (b : {P} + {~ P}) x y : ~ P -> (if b then x else y) = y :> T.
Proof.
intros; destruct b; tauto.
Qed.

Lemma test n m : n <> m -> (if eq_nat_dec n m then 1 else 0) = 0.
Proof.
intros H; rewrite sumboolF; auto.
Qed.

Это помогает решить ваш случай, но может потребовать отображения аналогичных результатов для других применений типа sumbool.

Это одна из причин, по которой мы рассматриваем возможность удаления sumbool из книги Software Foundations и использования вместо этого простых логических значений.

person Arthur Azevedo De Amorim    schedule 07.12.2015