Notasi yang lebih pendek untuk mencocokkan hipotesis di Coq?

Saya sering kali ingin merujuk hipotesis berdasarkan jenisnya, bukan berdasarkan namanya; terutama dalam pembuktian dengan inversi aturan semantik, yaitu aturan dengan beberapa kasus yang masing-masing mungkin memiliki banyak anteseden.

Saya tahu cara melakukan ini dengan match goal with ..., seperti pada contoh sepele berikut.

Lemma l0:
  forall P1 P2,
    P1 \/ (P1 = P2) ->
    P2 ->
    P1.
Proof.
  intros.
  match goal with H:_ \/ _ |- _ => destruct H as [H1|H2] end.
  assumption.
  match goal with H: _ = _ |- _ => rewrite H end.
  assumption.
Qed.

Apakah ada cara yang lebih ringkas? Atau pendekatan yang lebih baik?

(Pola pengenalan, seperti intros [???? HA HB|??? HA|????? HA HB HC HD], bukanlah suatu pilihan. Saya lelah menemukan jumlah ? yang tepat!)

Misalnya, apakah mungkin untuk menulis taktik grab untuk menggabungkan pola dan taktik, seperti pada

  grab [H:P1 \/ _] => rename H into HH.
  grab [H:P1 \/ _] => destruct H into [H1|H2].

  grab [P1 \/ _] => rename it into HH.
  grab [P1 \/ _] => destruct it into [H1|H2].

Dari pemahaman saya tentang Notasi Taktik, itu adalah tidak mungkin menggunakan cpattern sebagai argumen, tapi mungkin ada cara lain?

Idealnya, saya ingin dapat menggunakan pola hipotesis alih-alih pengidentifikasi dalam taktik apa pun seperti di Isabelle:

rename ⟨P1 \/ _⟩ into HH.
destruct ⟨P1 \/ _⟩ as [H1|H2].
rewrite ⟨P1 = _⟩.

Namun menurut saya ini merupakan perubahan yang cukup invasif.


theorem-proving coq coq-tactic
person tbrk    schedule 05.05.2019    source sumber

Jawaban (1)


arrow_upward
5
arrow_downward

Anda dapat mengulangi semua asumsi hingga Anda menemukan asumsi yang cocok:

Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
  match goal with H : _ |- _ => pose (id := H : ty) end.

Triknya adalah Anda mengambil tipe yang akan ditemukan bukan sebagai pola, tetapi, sebagai tipe :). Khususnya, jika Anda mengeluarkan sesuatu seperti summon (P _) as id, maka Coq akan mengambil _ sebagai variabel eksistensial yang belum terpecahkan. Pada gilirannya, setiap asumsi akan diketik terhadap P _, mencoba untuk membuat contoh lubang tersebut di sepanjang proses. Ketika seseorang berhasil, pose menamainya id. Iterasi muncul karena match goal akan terus mencoba ulang dengan kecocokan yang berbeda hingga ada yang menempel atau semuanya gagal.

Anda dapat mendefinisikan formulir tanpa as yang hanya memberi nama benda yang ditemukan it (sambil membuang yang lainnya):

Tactic Notation "summon" uconstr(ty) :=
  let new_it := fresh "it"
   in try (rename it into new_it); summon ty as it.

Ta-da!

Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
  intros.
  summon (_ \/ _).
  destruct it.
  assumption.
  summon (_ = _).
  rewrite it.
  assumption.
Qed.

Anda juga bisa mendapatkan sintaks => Anda. Menurutku itu tidak terlalu berguna, tapi...

(* assumption of type ty is summoned into id for the duration of tac
   anything that used to be called id is saved and restored afterwards,
   if possible. *)
Tactic Notation "summon" uconstr(ty) "as" ident(id) "=>" tactic(tac) :=
  let saved_id := fresh id
   in try (rename id into saved_id);
      summon ty as id; tac;
      try (rename saved_id into id).

Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
  intros.
  summon (_ \/ _) as H => destruct H.
  assumption.
  summon (_ = _) as H => rewrite H.
  assumption.
Qed.

Jawaban lama

(Anda mungkin ingin membaca ini, karena solusi di atas sebenarnya merupakan varian dari solusi ini, dan ada penjelasan lebih lanjut di sini.)

Anda dapat memanggil asumsi yang cocok dengan pola tipe ke dalam nama dengan eassert (name : ty) by eassumption..

Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
  intros.
  eassert (HH : _ \/ _) by eassumption.
  destruct HH.
  assumption.
  eassert (HH : _ = _) by eassumption.
  rewrite HH.
  assumption.
Qed.

Mengapa ini merupakan peningkatan? Karena _ \/ _ dan _ = _ sekarang bertipe full, bukan sekedar pola. Mereka hanya berisi variabel eksistensial yang belum terpecahkan. Antara eassert dan eassumption, variabel-variabel ini diselesaikan pada saat yang sama dengan asumsi pencocokan ditemukan. Notasi taktik pasti dapat bekerja dengan tipe (yaitu istilah). Sayangnya, tampaknya ada sedikit kesalahan dalam aturan parsing. Secara khusus, notasi taktik memerlukan istilah yang belum diketik (jadi kita tidak mencoba dan gagal menyelesaikan variabel terlalu dini), jadi kita memerlukan uconstr, tetapi tidak ada luconstr, artinya kami terpaksa menambahkan tanda kurung asing. Untuk menghindari bracket-mania, saya telah mengerjakan ulang sintaks grab Anda. Saya juga tidak sepenuhnya yakin apakah sintaks => Anda masuk akal, karena mengapa tidak memasukkan nama tersebut ke dalam cakupan untuk selamanya, daripada hanya pada =>, seperti yang Anda maksudkan?

Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
  eassert (id : ty) by eassumption.

Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
  intros.
  summon (_ \/ _) as HH.
  destruct HH.
  assumption.
  summon (_ = _) as HH.
  rewrite HH.
  assumption.
Qed.

Anda dapat membuat summon-sans-as memberi nama asumsi yang ditemukan it, sambil mem-boot apa pun dengan nama itu.

Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
  eassert (id : ty) by eassumption.

Tactic Notation "summon" uconstr(ty) :=
  let new_it := fresh "it"
   in (try (rename it into new_it); summon ty as it).

Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
  intros.
  (* This example is actually a bad demonstration of the name-forcing behavior
     because destruct-ion, well, destroys.
     Save the summoned proof under the name it, but destroy it from another,
     then observe the way the second summon shoves the original it into it0. *)
  summon (_ \/ _) as prf.
  pose (it := prf).
  destruct prf.
  assumption.
  summon (_ = _).
  rewrite it.
  assumption.
Qed.

Secara idiomatis, itu memang benar adanya

Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
  intros.
  summon (_ \/ _).
  destruct it.
  assumption.
  summon (_ = _).
  rewrite it.
  assumption.
Qed.

Saya yakin Anda dapat membuat sekumpulan Tactic Notation khusus untuk menggantikan argumen ident di destruct, rewrite, dll. dengan uconstrs tipe berlubang ini, jika Anda benar-benar menginginkannya. Memang, summon _ as _ hampir merupakan rename _ into _ Anda yang dimodifikasi.

Peringatan lain: assert buram; definisi yang dihasilkan oleh summon tampak seperti asumsi baru yang tidak mengungkapkan bahwa definisi tersebut sama dengan salah satu asumsi lama. Sesuatu seperti refine (let it := _ in _) atau pose harus digunakan untuk memperbaiki ini, tapi Ltac-fu saya tidak cukup kuat untuk melakukan ini. Lihat juga: masalah ini menganjurkan transparent assert secara literal.

(Jawaban baru memecahkan peringatan ini.)

person HTNW    schedule 06.05.2019
comment
Besar! Terima kasih. Saya setuju bahwa sintaks => tidak menambahkan apa pun. Saya akan mengadaptasi summon pertama Anda untuk menghindari duplikasi hipotesis (match goal with H : _ |- _ => pose (id := H : ty); clear id; rename H into id end.), dan hipotesis kedua menjadi Tactic Notation "take" uconstr(ty) "and" tactic(tac) := let new_it := fresh "it" in try (rename it into new_it); summon ty as it; tac; try (rename new_it into it)., sehingga saya dapat menulis, misalnya, take (_ \/ _) and destruct it yang persis seperti yang saya inginkan. - person tbrk; 06.05.2019