setoid_rewrite терпит неудачу в сценарии сопоставления с образцом - PullRequest
Новая
       8

setoid_rewrite терпит неудачу в сценарии сопоставления с образцом

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

Ранее , мне сказали, как используйте setoid_rewrite для работы с functions_extensionality . К сожалению, я обнаружил, что это хорошее решение не работает в следующем сценарии. предполагать что мы определили класс Monoid: 

Class Monoid (m : Type) :=
{ mzero : m
; mappend : m -> m -> m
}.
Notation "m1 * m2" := (mappend m1 m2) (at level 40, left associativity).

Class MonoidLaws m `{Monoid m} :=
{ left_unit  : forall m, mzero * m = m (* ; other laws... *) }.

Если мы добавим pointwise_eq_ext в картинка monoid_proof становится тривиальной: 

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Generalizable All Variables.

Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
  : subrelation (pointwise_relation A RB) eq.
Proof.
  intros f g Hfg.
  apply functional_extensionality.
  intro x.
  apply sb.
  apply (Hfg x).
Qed.

Example monoid_proof `{ml : MonoidLaws m} :
  (fun m => mzero * m) = (fun m => m).
Proof. now setoid_rewrite left_unit. Qed.

Однако, если то же самое моноидное выражение появляется в качестве аргумента для option_fold, тактика не удалась: 

Definition option_fold {A B} (some : A -> B) (none : B) (oa : option A) : B :=
  match oa with
  | Some a => some a
  | None => none
  end.

(* Expression is an argument for [option_fold] *)
Example monoid_proof' `{ml : MonoidLaws m} :
  forall om,
    option_fold (fun m => mzero * m) mzero om = option_fold (fun m => m) mzero om.
Proof. intros. now setoid_rewrite left_unit. (* error! *) Qed.

Я не знаком с деталями setoid_rewrite, но кажется, что сопоставление с образцом соответствует контексту, который мешает этой тактике выполнить правильно. Есть ли способ научить setoid_rewrite как иметь дело с такого рода ситуации? Я пытался предоставить несколько subrelation случаи, но мне не хватает теоретического фона, чтобы понять весь картина. Общее решение было бы замечательно, но я был бы достаточно счастлив с ad hoc подход к переписыванию выражений в аргументах (вложенных) вызовы option_fold.

1 Ответ

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

Экземпляр pointwise_eq_ext позволяет переписать цели, подобные этой: 

(fun m => mzero * m) = (fun m => m)

но вещи ломаются, если у вас есть функция внутри некоторого контекста. Чтобы это исправить, вам нужно добавить следующую подотношения: 

Instance subrel_eq_respect {A B : Type}
         `(sa : subrelation A RA eq)
         `(sb : subrelation B eq RB) :
   subrelation eq (respectful RA RB).
Proof. intros f g -> a a' Raa'. apply sb. f_equal. apply (sa _ _ Raa'). Qed.

Возможно, вы захотите взглянуть на полный код в этой записи Coq Club от Matthieu Sozeau.

...