สัญกรณ์ที่สั้นกว่าสำหรับการจับคู่สมมติฐานใน Coq?

ฉันพบว่าตัวเองมักต้องการอ้างถึงสมมติฐานตามประเภทมากกว่าตามชื่อ โดยเฉพาะอย่างยิ่งในการพิสูจน์ที่มีการผกผันกฎความหมาย กล่าวคือ กฎที่มีหลายกรณีซึ่งแต่ละกรณีอาจมีเหตุการณ์ก่อนหน้าได้หลายกรณี

ฉันรู้วิธีการทำเช่นนี้กับ match goal with ... ดังตัวอย่างเล็กๆ น้อยๆ ต่อไปนี้

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.

มีวิธีที่กระชับกว่านี้ไหม? หรือแนวทางที่ดีกว่า

(รูปแบบการแนะนำ เช่น intros [???? HA HB|??? HA|????? HA HB HC HD] ไม่ใช่ตัวเลือกฉันเบื่อที่จะหาจำนวน ?s ที่ถูกต้องแล้ว!)

ตัวอย่างเช่น เป็นไปได้ไหมที่จะเขียนกลยุทธ์ grab เพื่อรวมรูปแบบและยุทธวิธีเข้าด้วยกัน ดังเช่นใน

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

จากความเข้าใจของฉันเกี่ยวกับ สัญลักษณ์ทางกลยุทธ์ เป็นไปไม่ได้ที่จะมี cpattern เป็นอาร์กิวเมนต์ แต่อาจมีวิธีอื่นอีกไหม

ตามหลักการแล้ว ฉันอยากจะใช้รูปแบบสมมติฐานแทนตัวระบุในกลวิธีใดๆ ก็ตามเหมือนใน Isabelle:

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

แต่ฉันคิดว่านี่เป็นการเปลี่ยนแปลงที่ค่อนข้างรุกราน


theorem-proving coq coq-tactic
person tbrk    schedule 05.05.2019    source แหล่งที่มา

คำตอบ (1)


arrow_upward
5
arrow_downward

คุณสามารถทำซ้ำสมมติฐานทั้งหมดได้จนกว่าคุณจะพบข้อสันนิษฐานที่ตรงกัน:

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

เคล็ดลับคือคุณใช้ประเภทที่จะพบว่าไม่ใช่รูปแบบ แต่เป็นประเภท :) โดยเฉพาะอย่างยิ่ง หากคุณออกบางอย่างเช่น summon (P _) as id Coq จะใช้ _ เป็นตัวแปรที่มีอยู่ที่ยังไม่ได้แก้ไข ในทางกลับกัน แต่ละสมมติฐานจะถูกพิมพ์เทียบกับ P _ โดยพยายามสร้างอินสแตนซ์ของหลุมนั้นไปพร้อมกัน เมื่อทำสำเร็จ pose จะตั้งชื่อเป็น id การวนซ้ำเกิดขึ้นเนื่องจาก match goal จะลองอีกครั้งด้วยการจับคู่ที่แตกต่างกัน จนกว่าจะมีสิ่งค้างอยู่หรือทุกอย่างล้มเหลว

คุณสามารถกำหนดแบบฟอร์มโดยไม่ต้อง as ที่เพิ่งตั้งชื่อสิ่งที่พบ it (ในขณะที่เตะสิ่งอื่นออกไป):

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.

คุณยังสามารถรับไวยากรณ์ => ของคุณได้ ฉันคิดว่ามันมีประโยชน์ไม่มากนัก แต่...

(* 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.

คำตอบเก่า

(คุณอาจต้องการอ่านสิ่งนี้ เนื่องจากวิธีแก้ปัญหาข้างต้นแตกต่างจากวิธีนี้จริงๆ และมีคำอธิบายเพิ่มเติมที่นี่)

คุณสามารถเรียกสมมติฐานที่ตรงกับรูปแบบประเภทให้เป็นชื่อด้วย 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.

เหตุใดจึงมีการปรับปรุงนี้ เนื่องจากขณะนี้ _ \/ _ และ _ = _ เป็นประเภทเต็ม ไม่ใช่แค่รูปแบบเท่านั้น พวกมันมีเพียงตัวแปรที่มีอยู่ที่ยังไม่ได้แก้ไข ระหว่าง eassert ถึง eassumption ตัวแปรเหล่านี้จะได้รับการแก้ไขในเวลาเดียวกันกับที่ตั้งสมมติฐานที่ตรงกัน สัญกรณ์ชั้นเชิงสามารถใช้ได้กับประเภทต่างๆ (เช่น เงื่อนไข) อย่างแน่นอน น่าเศร้าที่กฎการแยกวิเคราะห์ดูเหมือนจะมีอุบัติเหตุเล็กน้อย โดยเฉพาะอย่างยิ่ง สัญกรณ์ชั้นเชิงจำเป็นต้องมีคำที่ไม่ได้พิมพ์ (ดังนั้นเราจึงไม่พยายามและล้มเหลวในการแก้ไขตัวแปรเร็วเกินไป) ดังนั้นเราจึงต้องการ uconstr แต่ ไม่มี luconstr ซึ่งหมายความว่าเราถูกบังคับให้เพิ่มวงเล็บที่ไม่เกี่ยวข้อง เพื่อหลีกเลี่ยงอาการคลั่งไคล้วงเล็บ ฉันได้ทำการปรับปรุงไวยากรณ์ของ grab ของคุณใหม่ ฉันยังไม่แน่ใจด้วยซ้ำว่าไวยากรณ์ => ของคุณสมเหตุสมผลหรือไม่ เพราะเหตุใดจึงไม่ลองนำชื่อไปไว้ในขอบเขตที่ดี แทนที่จะใช้เฉพาะใน => อย่างที่คุณบอกเป็นนัย

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.

คุณสามารถสร้าง summon-sans-as ตั้งชื่อสมมติฐานที่พบ it ในขณะที่ทำการบูทสิ่งอื่นภายใต้ชื่อนั้น

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.

ตามสำนวนแล้วมันก็เป็นเช่นนั้นจริงๆ

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

ฉันเชื่อว่าคุณสามารถสร้าง Tactic Notations เฉพาะทางจำนวนมากเพื่อแทนที่อาร์กิวเมนต์ ident ใน destruct, rewrite ฯลฯ ด้วย uconstrs ประเภทโฮลลี่เหล่านี้ได้ หากคุณต้องการจริงๆ อันที่จริง summon _ as _ เกือบจะเป็น rename _ into _ ที่คุณแก้ไขแล้ว

ข้อแม้อีกประการหนึ่ง: assert ทึบแสง; คำจำกัดความที่สร้างโดย summon ดูเหมือนสมมติฐานใหม่ที่ไม่เปิดเผยว่ามีค่าเท่ากับข้อใดข้อหนึ่งแบบเก่า ควรใช้บางอย่างเช่น refine (let it := _ in _) หรือ pose เพื่อแก้ไขสิ่งนี้ แต่ Ltac-fu ของฉันไม่แข็งแกร่งพอที่จะทำเช่นนี้ ดูเพิ่มเติม: ปัญหานี้สนับสนุน transparent assert ตามตัวอักษร

(คำตอบใหม่แก้ไขข้อแม้นี้)

person HTNW    schedule 06.05.2019
comment
ยอดเยี่ยม! ขอบคุณ ฉันยอมรับว่าไวยากรณ์ => ไม่ได้เพิ่มอะไรเลย ฉันจะปรับ summon แรกของคุณเพื่อหลีกเลี่ยงการทำซ้ำสมมติฐาน (match goal with H : _ |- _ => pose (id := H : ty); clear id; rename H into id end.) และอันที่สองเป็น 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). เพื่อที่ฉันจะได้เขียนได้ เช่น take (_ \/ _) and destruct it ซึ่งเป็นสิ่งที่ฉันต้องการจริงๆ - person tbrk; 06.05.2019