Da un predicato induttivo alla lista A -> Lista A -> bool

Question

Durante il tentativo di scrivere il codice riutilizzabile su un predicato induttiva su liste mi viene spontaneo dichiarato:

Parameter A:Type. 

Poi ho proceduto a definire il predicato binario (per esempio):

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

che esprime il fatto che un dato elenco è un prefisso di un altro. Si può quindi continuare a studiare questa relazione e mostrare (per esempio) che si tratta di un ordine parziale. Fin qui tutto bene. Tuttavia, è molto facile definire un predicato induttivo che non corrisponda alla nozione matematica in mente. Vorrei convalidare la definizione induttiva definendo inoltre una funzione:

isPrefixOf: list A -> list A -> bool 

con lo scopo di dimostrare l'equivalenza:

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

Questo è dove devo limitare la generalità del codice mentre non può più funzionare con list A. In Haskell, abbiamo isPrefixOf :: Eq a => [a] -> [a] -> Bool, quindi capisco che devo fare qualche ipotesi su A, qualcosa come 'Eq A'. Naturalmente, potrei ipotizzare:

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

e procedere da lì. Probabilmente lo farei in un altro file o in una sezione, in modo da non compromettere la piena generalità del codice precedente. Tuttavia, sento di re-inventare la ruota. Questo è probabilmente un modello comune (che esprime qualcosa come Haskell Eq a => ...).

Quale dichiarazione (idiomatica, comune) dovrei fare riguardo al tipo A che mi consente di procedere mantenendo il codice il più generale possibile?

Answer 1

(MODIFICA: la libreria standard Coq fornisce una controparte diretta dell'operatore Haskell == con la classe di tipo EqDec), vedere la risposta @ anton-trunov per ulteriori dettagli).

In generale, si dispone di almeno due opzioni:

• assumono il tipo A ha uguaglianza decidibile. Questo può essere fatto in molte forme, di solito si vuole

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

  allora, è possibile distruggere A_dec per confrontare gli elementi. Questo è usato in diverse parti della libreria standard e potresti usare una classe di tipo per la risoluzione automatica. Credo che diverse librerie di terze parti utilizzino questo approccio (coq-ext-lib, TLC). Il codice sarebbe diventato:

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

• Seguite il vostro approccio e di fornire un operatore di uguaglianza booleano. La libreria di matematica fornisce una gerarchia di classi con una classe di tipi con uguaglianza decidibile eqType. Pertanto, per A : eqType, x y : A, è possibile utilizzare l'operatore == per confrontarli. Vedi http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.seq.html per esempi con elenchi.

  vostri equal e validate assunzioni sono esattamente incapsulati in un eqType (di nome e ==eqP).Il codice sarebbe:

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

  Una cosa bella di approccio matematico-comp è che sarà inferire automaticamente eqType casi per i tipi come nat. Ciò aiuta a mantenere le prove leggere. Una nota sulla dimostrazione di cui sopra è che eviterei l'inversione usando "view di inversione", ma questo è un argomento diverso. Inoltre, utilizzando il già esistente seq.subseq può avere più senso, oppure si potrebbe desiderare qualcosa di simile:

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

Che cosa è più idiomatica? IMHO dipende davvero. AFAICT diversi sviluppatori preferiscono tecniche diverse. Trovo che il secondo approccio funzioni al meglio per me, al costo di alcune applicazioni supplementari in eqP nelle prove.

Codice è qui: https://x80.org/collacoq/akumoyutaz.coq

Answer 2

Per completare la risposta di @ ejgallego, si potrebbe anche utilizzare il sistema di moduli per effettuare le assunzioni corrispondenti. Se hai Require Import Structures.Equalities, hai alcuni tipi di moduli utili. Ad esempio, Typ contiene solo un tipo t, mentre UsualBoolEq presuppone l'esistenza di un operatore eqb : t -> t -> bool che verifica eqb_eq : forall x y : t, eqb x y = true <-> x = y.

È possibile inserire la propria definizione nei funtori.

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. 

Si noti tuttavia che il sistema di moduli non è la parte di Coq più comoda da utilizzare. Tendo a preferire le opzioni presentate da @ejgallego. Questa risposta è fornita principalmente per completezza.

Answer 3

Un'altra versione, utilizzando equivalenze decidibili (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. 

Consentitemi di fornire alcuni esempi sull'utilizzo di isPrefixOf per i calcoli. Per nat s è super facile, dal momento che nat è già un esempio di EqDec:

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

E qui è un test per un tipo definito dall'utente:

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