Булево равенство списков в Coq? - PullRequest
Новая
       5

Булево равенство списков в Coq?

0 голосов
/ 25 апреля 2018

Я хочу иметь возможность сравнить два элемента типа "список" в Coq и получить логическое значение "true" или "false" для их эквивалентности.

Сейчас я сравниваю два списка следующим образом: 

Eval vm_compute in (list 1 = list 2).

Я получаю реквизит формы: 

= nil
   :: (2 :: 3 :: nil)
      :: (2 :: nil)
         :: (3 :: nil) :: nil =
   nil
   :: (2 :: 3 :: nil)
      :: (2 :: nil)
         :: (3 :: nil) :: nil
 : Prop

Очевидно, list1 = list2, так как мне заставить его просто возвращать true или false?

Ответы [ 2 ]

0 голосов
/ 25 апреля 2018

Вы можете сгенерировать функцию логического равенства списков, которая принимает в качестве входных данных логическое равенство по элементам автоматически, используя команды Coq: 

Require Import Coq.Lists.List Coq.Bool.Bool.

Import Coq.Lists.List.ListNotations.

Scheme Equality for list.

Это печатает: 

list_beq is defined
list_eq_dec is defined

где list_beq - это функция логического равенства для списков, которая в качестве первого параметра принимает функцию сравнения для элементов списков, а затем двух списков: 

Print list_beq.

Дает 

list_beq = 
fun (A : Type) (eq_A : A -> A -> bool) =>
fix list_eqrec (X Y : list A) {struct X} : bool :=
  match X with
  | [] => match Y with
          | [] => true
          | _ :: _ => false
          end
  | x :: x0 => match Y with
               | [] => false
               | x1 :: x2 => eq_A x x1 && list_eqrec x0 x2
               end
  end
     : forall A : Type, (A -> A -> bool) -> list A -> list A -> bool

и 

Check list_eq_dec

дает 

list_eq_dec
     : forall (A : Type) (eq_A : A -> A -> bool),
       (forall x y : A, eq_A x y = true -> x = y) ->
       (forall x y : A, x = y -> eq_A x y = true) -> forall x y : list A, {x =  y} + {x <> y}

, показывающий, что равенство в списке разрешимо, если равенство базовых типов согласуется с равенством Лейбница.

0 голосов
/ 25 апреля 2018

Я использую операторы логического равенства Библиотеки математических компонентов : 

From mathcomp Require Import all_ssreflect.

...

Eval vm_compute in list 1 == list 2
...