From an Inductive predicate to list A -> list A -> bool

Question

While attempting to write reusable code on an inductive predicate on lists I naturally declared:

Parameter A:Type.

Then I proceeded to define the binary predicate (for example):

Inductive prefix : list A -> list A -> Prop :=
  | prefixNil: forall (l: list A), prefix nil l
  | prefixCons: forall (a: A)(l m:list A), prefix l m -> prefix (a::l) (a::m).

which expresses the fact that a given list is a prefix of another. One can then carry on to study this relation and show (for example) that it is a partial order. So far so good. However, it is very easy to define an inductive predicate which does not correspond to the mathematical notion in mind. I would like to validate the inductive definition by further defining a function:

isPrefixOf: list A -> list A -> bool

with the aim of proving the equivalence:

Theorem prefix_validate: forall (l m: list A), 
  prefix l m <-> isPrefixOf l m = true.

This is where I need to restrict the generality of the code as I can no longer work with list A. In Haskell, we have isPrefixOf :: Eq a => [a] -> [a] -> Bool, so I understand I need to make some assumption on A, something like 'Eq A'. Of course, I could postulate:

Parameter equal: A -> A -> bool
Axiom equal_validate: forall (a b: A),
  a = b <-> equal a b = true.

and proceed from there. I would probably do this in another file or in a section, so as not to undermine the full generality of the previous code. However, I feel I am re-inventing the wheel. This is probably a common pattern (expressing something like the Haskell Eq a => ...).

Which (idiomatic, common) declaration should I make about type A which allows me to proceed, while keeping the code as general as possible?

Answer 1

(EDIT: The Coq standard library provides a direct counterpart of the Haskell == operator with the EqDec type class), see @anton-trunov answer for more details).

In general, you have at least two options:

• Assume the type A has decidable equality. This can be done in many forms, usually you want

  Hypothesis (A_dec : forall x y : A, {x = y} + {x <> y})
  

  then, you can destruct A_dec to compare elements. This is used in several parts of the standard library, and you could use a type class for automatic resolution. I believe that several third party libraries use this approach (coq-ext-lib, TLC). The code would become:

  Require Import Coq.Lists.List.
  Section PrefixDec.
  
  Variable A : Type.
  Hypothesis (A_dec : forall x y : A, {x = y} + {x <> y}).
  Implicit Types (s t : list A).
  
  Fixpoint prefix s t := 
    match s, t with
    | nil, t         => true
    | s, nil         => false
    | x :: s, y :: t => match A_dec x y with
                        | left  _ => prefix s t
                        | right _ => false
                        end
    end.
  
  Inductive prefix_spec : list A -> list A -> Prop :=
    | prefix_nil  : forall (l: list A),
        prefix_spec nil l
    | prefix_cons : forall (a: A) (l m:list A),
        prefix_spec l m -> prefix_spec (a::l) (a::m).
  
  Hint Constructors prefix_spec.
  
  Lemma prefixP s t : prefix_spec s t <-> prefix s t = true.
  Proof.
  revert t; induction s as [|x s]; intros [|y t]; split; simpl; try congruence; auto.
  + now intros H; inversion H.
  + destruct (A_dec x y); simpl; intros H; inversion H; subst; try congruence.
    now rewrite <- IHs.
  + destruct (A_dec x y); intros H; inversion H; subst.
    now constructor; rewrite IHs.
  Qed.
  
  End PrefixDec.
  
  (* Compute example *)
  Import ListNotations.
  Compute (prefix _ PeanoNat.Nat.eq_dec [2; 3; 4] [ 2; 3; 4; 5]).
  Compute (prefix _ PeanoNat.Nat.eq_dec [2; 3; 4] [ 2; 3; 5]).
  

• Follow your approach and provide a boolean equality operator. The math-comp library provides a class hierarchy with a class of types with decidable equality eqType. Thus, for A : eqType, x y : A, you can use the == operator to compare them. See http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.seq.html for examples with lists.

  Your equal and validate assumptions are exactly encapsulated into an eqType (named == and eqP). The code would be:

  From mathcomp
  Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
  
  Section PrefixEq.
  
  Variable A : eqType.
  Implicit Types (s t : seq A).
  
  Fixpoint prefix s t :=
    match s, t with
    | nil, t          => true
    | s, nil          => false
    | x :: s, y :: t => if x == y then prefix s t else false
    end.
  
  Inductive prefix_spec : list A -> list A -> Prop :=
    | prefix_nil  : forall (l: list A),
        prefix_spec nil l
    | prefix_cons : forall (a: A) (l m:list A),
        prefix_spec l m -> prefix_spec (a::l) (a::m).
  
  Hint Constructors prefix_spec.
  
  Lemma prefixP s t : reflect (prefix_spec s t) (prefix s t).
  Proof.
  apply: (iffP idP); elim: s t => // x s ihs [|y t] //=.
  - by case: eqP => // ->; auto.
  - by move=> H; inversion H.
  - by move=> H; inversion H; subst; rewrite eqxx ihs.
  Qed.
  
  End PrefixEq.
  
  Compute (prefix _ [:: 1;2;3] [:: 1;2;3]).
  Compute (prefix _ [:: 1;2;3] [:: 1;3;3]).
  

  A nice thing about math-comp approach is that it will automatically infer eqType instances for types like nat. This helps keeping proofs lightweight. A note on the above proof is that I would avoid inversion by using and "inversion view", but that's a different topic. Also, using the already existing seq.subseq may make more sense, or you may want something like:

  Definition is_prefix (A : eqType) (s t : seq A) := s == take (size s) t.
  

What is more idiomatic? IMHO it really depends. AFAICT different developers prefer different techniques. I find that the second approach works best for me, at the cost of some extra eqP applications in proofs.

Code is here: https://x80.org/collacoq/akumoyutaz.coq

Answer 2

To complete @ejgallego's answer, you could also use the module system to make the corresponding assumptions. If you Require Import Structures.Equalities, you have some useful module types. For instance, Typ just contains a type t, while UsualBoolEq assumes the existence of an operator eqb : t -> t -> bool verifying eqb_eq : forall x y : t, eqb x y = true <-> x = y.

You could put your definition in functors.

Require Import Structures.Equalities.
Require Import List. Import ListNotations.
Require Import Bool.

Module Prefix (Import T:Typ).
  Inductive prefix : list t -> list t -> Prop :=
  | prefixNil: forall (l: list t), prefix nil l
  | prefixCons: forall (a: t)(l m:list t), prefix l m -> prefix (a::l) (a::m).
End Prefix.

Module PrefixDecidable (Import T:UsualBoolEq).
  Include Prefix T.

  Fixpoint isPrefixOf (l m : list t) :=
    match l with
    | [] => true
    | a::l' =>
      match m with
      | [] => false
      | b::m' => andb (eqb a b) (isPrefixOf l' m')
      end
    end.

  Theorem prefix_validate: forall (l m: list t), 
    prefix l m <-> isPrefixOf l m = true.
  Proof.
    split; intros H.
    - induction H.
      + reflexivity.
      + simpl. rewrite andb_true_iff. split; [|assumption].
        apply eqb_eq; reflexivity.
    - revert dependent m; induction l as [|a l']; intros m H.
      + constructor.
      + destruct m as [|b m'].
        * discriminate.
        * simpl in H. rewrite andb_true_iff in H. destruct H as [H H0].
          apply eqb_eq in H. subst b.
          constructor. apply IHl'; assumption.
  Qed.
End PrefixDecidable.

Note however that the module system is not the part of Coq the most convenient to use. I tend to prefer the options presented by @ejgallego. This answer is provided mainly for completeness.

Answer 3

Yet another version, using decidable equivalences (Coq.Classes.EquivDec).

Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Classes.EquivDec.

Set Implicit Arguments.

Section Prefix.

  Variable A : Type.
  Context `{EqDec A eq}.  (* A has decidable equivalence *)

  Inductive prefix : list A -> list A -> Prop :=
  | prefixNil: forall (l: list A), prefix nil l
  | prefixCons: forall (a: A)(l m:list A), prefix l m -> prefix (a::l) (a::m).
  Hint Constructors prefix.

  Fixpoint isPrefixOf (l1 l2 : list A) : bool :=
    match l1, l2 with
    | [], _ => true
    | _, []   => false
    | h1 :: t1, h2 :: t2 => if h1 == h2 then isPrefixOf t1 t2
                            else false
    end.

  Theorem prefix_validate : forall (l m: list A), 
      prefix l m <-> isPrefixOf l m = true.
  Proof.
    induction l; split; intro Hp; auto; destruct m; inversion Hp; subst.
    - simpl. destruct (equiv_dec a0 a0).
      + apply IHl. assumption.
      + exfalso. apply c. reflexivity.
    - destruct (equiv_dec a a0).
      + rewrite e. constructor. apply IHl. assumption.
      + discriminate H1.
  Qed.
End Prefix.

Let me provide some examples of using isPrefixOf for computations. For nats it's super easy, since nat is already an instance of EqDec:

Eval compute in isPrefixOf [1;2] [1;2;3;4]. (* = true *)
Eval compute in isPrefixOf [1;9] [1;2;3;4]. (* = false *)

And here is a test for a user-defined type:

Inductive test : Type :=
  | A : test
  | B : test
  | C : test.
Lemma test_dec : forall x y:test, {x = y} + {x <> y}.
Proof. decide equality. Defined.

Instance test_eqdec : EqDec test _ := test_dec.

Eval compute in isPrefixOf [A;B] [A;B;C;A]. (* = true *)
Eval compute in isPrefixOf [A;C] [A;B;C;A]. (* = false *)