をリストする - >リストA - > BOOL

Question

私は自然に宣言リストの誘導述語に再利用可能なコードを記述しようとしているとき：

Parameter A:Type. 

は、その後、私はバイナリ述語を定義するために進めた（用例：

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). 

これは、与えられたリストが別のリストの接頭辞であるという事実を表しています。次に、この関係を研究し、（例えば）それが部分的な順序であることを示すことができます。ここまでは順調ですね。しかし、数学的概念に対応していない帰納的述語を念頭において定義するのは非常に簡単です。等価性を証明する目的で

isPrefixOf: list A -> list A -> bool 

：私は別の機能を定義することによって誘導定義を検証したいと思います

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

私は私のように、コードの一般性を制限する必要がある場所ですlist Aで動作しなくなりました。ハスケルでは、isPrefixOf :: Eq a => [a] -> [a] -> Boolがあるので、私はAのようなものを仮定する必要があることを理解しています。 'Eq A'のようなものです。もちろん、私は仮定することができます：

そしてそこから進んでください。私はおそらくこれを前のコードの完全性を損なわないように、別のファイルまたはセクションで行うでしょう。しかし、私は車輪を再発明していると感じています。これはたぶん一般的なパターンです（Haskell Eq a => ...のようなものを表現しています）。

できるだけ一般的なコードを維持しながら、私が進めることができるタイプAについて（慣用句、共通の）宣言をしてください。

Answer 1

（編集：Coq標準ライブラリは、EqDecタイプのクラスを持つHas​​kell ==演算子の直接の対応を提供します）、詳しくは@ anton-trunov answerを参照してください）。

一般的に、あなたは、少なくとも2つのオプションがあります。

• はタイプAが決定可能平等を持っていると仮定します。これは通常、あなたが、あなたが要素を比較するA_decを破棄させることができる

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

  をしたい、多くの形態で行うことができます。これは標準ライブラリのいくつかの部分で使用され、自動解決のために型クラスを使うことができます。私は、いくつかの第三者図書館がこのアプローチ（coq-ext-lib、TLC）を使用していると考えています。コードはなる：

  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]). 
  

• はあなたのアプローチに従って、ブール等価演算子を提供しています。 math-compライブラリは、決定可能な等価性を持つクラスのクラスを持つクラス階層を提供しますeqType。したがって、A : eqType, x y : Aの場合は、==演算子を使用して比較することができます。リストの例については、http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.seq.htmlを参照してください。

  あなたequalとvalidate仮定は正確に（==とeqP命名）eqTypeにカプセル化されています。コードは次のようになります。

  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]). 
  

  数学-COMPのアプローチの良いところは、それが自動的にnatのようなタイプのためにeqTypeインスタンスを推測することです。これは、証明を軽量に保つのに役立ちます。上記の証拠には、「反転ビュー」を使用して反転を避けることができますが、これは別のトピックです。また、より多くの意味を行うことがあり、既存のseq.subseqを使用して、またはあなたが何かしたいことがあります。より多くの慣用句は何ですか

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

を？ IMHOそれは本当に依存しています。 AFAICTの異なる開発者は、異なる技術を好む。私は、2番目のアプローチが証明書の中でいくつかの余分な代償を払って私のために最もよく働くことが分かりました。

コードはここにある：https://x80.org/collacoq/akumoyutaz.coq

Answer 2

@のejgallegoの答えを完了するために、あなたはまた、対応する仮定をするモジュールシステムを使用することができます。 Require Import Structures.Equalitiesの場合、いくつかの便利なモジュールタイプがあります。たとえば、Typにはタイプtが含まれていますが、UsualBoolEqはeqb : t -> t -> boolというベリファイeqb_eq : forall x y : t, eqb x y = true <-> x = yの演算子が存在すると仮定しています。

あなたは定義をFunctorに置くことができます。

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. 

ただし、モジュールシステムはCoqの一部ではありません。私は@ejgallegoが提示するオプションを好む傾向があります。この回答は、主に完全性のために提供されています。

Answer 3

さらに別のバージョンでは、決定可能な等価性（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. 

ここでは、計算にisPrefixOfを使用する例を示します。

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

そして、ここでユーザー定義型のためのテストです：nat秒間natがEqDecのインスタンスが既にあるので、それは、超簡単です

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 *)