Равенство в COQ для перечисленных типов

Question

У меня есть конечный перечислимый тип (скажем T) в COQ и вы хотите проверить элементы для равенства. Это значит, мне нужна функция

bool beq_T(x:T,y:T) 

Единственный способ, которым мне удалось определить такую ​​функцию, - это анализ по каждому случаю. Это приводит к множеству утверждений о матче и выглядит очень громоздким. Поэтому я задаюсь вопросом, нет ли более простого способа достичь этого.

Answer 1

Еще проще: Scheme Equality for ... генерирует две функции, возвращающие соответственно логическое и sumbool.

Answer 2

Плохая новость заключается в том, что программа, которая реализует beq_T, обязательно должна состоять из большого утверждения соответствия для обоих своих аргументов. Хорошей новостью является то, что вы можете автоматически генерировать/синтезировать эту программу с использованием тактического языка Coq. Например, с учетом вида:

Inductive T := t0 | t1 | t2 | t3. 

Вы можете определить beq_T следующим образом. Первые две тактики destruct синтезируют код, необходимый для соответствия как x, так и y. Тактическая тактика match контролирует ветку матча, в которой она находится, и в зависимости от того, x = y, эта тактика либо синтезирует программу, которая возвращает true, либо false.

Definition beq_T (x y:T) : bool. 
    destruct x eqn:?; 
    destruct y eqn:?; 
    match goal with 
    | _:x = ?T, _:y = ?T |- _ => exact true 
    | _ => exact false 
    end. 
Defined. 

Если вы хотите увидеть синтезированную программу, запустите:

Print beq_T. 

К счастью, Coq уже поставляется с тактикой, которая делает почти то, что вы хотите. Он называется decide equality. Он автоматически синтезирует программу, которая решает, являются ли два элемента типа T равными. Но вместо того, чтобы просто возвращать логическое значение, синтезированная программа возвращает доказательство (in) равенства двух элементов.

Definition eqDec_T (x y:T) : {x = y} + {x <> y}. 
    decide equality. 
Defined. 

С этой программой синтезированного, легко реализовать beq_T.

Definition beq_T' {x y:T} : bool := if eqDec_T x y then true else false.