3

I want to be able to compare two items of type "list" in Coq and get a boolean "true" or "false" for their equivalence.

Right now, I'm comparing the two lists this way:

Eval vm_compute in (list 1 = list 2).

I get a Prop of the form:

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

Obviously list1 = list2, so how do I get it to just return true or false?

Alyssa Byrnes
  • 31
  • 2
  • 1
    Have you made your own definition of `list`? Usually it is a type constructor, such that `list nat` is the **type** of lists of numbers. But you seem to be using it as a (value) constructor, creating a concrete list, so you must have cooked up something of your own, right? – larsr Apr 25 '18 at 10:01
  • Note that `=` returns a `Prop`, which is not the same thing as a boolean. [This answer](https://stackoverflow.com/a/31568076/1633770) explains the issue in more detail. – Arthur Azevedo De Amorim Apr 25 '18 at 11:28

2 Answers2

3

I use the Mathematical Components Library boolean equality operators:

From mathcomp Require Import all_ssreflect.

...

Eval vm_compute in list 1 == list 2
ejgallego
  • 6,709
  • 1
  • 14
  • 29
  • In the context of one of my proofs, I have ``H0 : (a1 == a2) = true``. How should I use ``a1`` or ``a2`` interchangeably in my proof? I mean how I should change this hypothesis to something like ``a1=a2``. For example, how should I change the goal like ``equalityfunction a1 b=true`` to ``equalityfunction a2 b=true``, based on the hypothesis. – Tom And. Mar 17 '19 at 05:35
  • 1
    @TomAnd., mathcomp indeed provides extremely good support for that, you would use for example `rewrite (eqP H0)`, `eqP` is the lemma that relates boolean equality with its propositional counterpart. – ejgallego Mar 17 '19 at 16:11
  • This works for me. I appreciate it. I wonder if you refer to a good resource to learn Mathcomp. – Tom And. Mar 17 '19 at 16:22
  • 1
    The math comp book is the main reference. – ejgallego Mar 17 '19 at 16:26
2

You can generate a boolean list equality function that takes as input a boolean equality over the elements automatically using Coq's commands:

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

Import Coq.Lists.List.ListNotations.

Scheme Equality for list.

This prints:

list_beq is defined
list_eq_dec is defined

where list_beq is a boolean equality function on lists that takes as first parameter a comparison function for the lists elements and then two lists:

Print list_beq.

Gives

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

and

Check list_eq_dec

gives

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}

showing that list equality is decidable if the underlying types equality is agrees with leibniz equality.

Heiko Becker
  • 556
  • 3
  • 16