How to prove `NoDup` in name-parametrized modules?

[andres-erbsen-sifive]

code like

  Context (name : string).
  Local Open Scope kami_action.
  Local Open Scope kami_expr.
  Local Notation "@^ x" := (name ++ "_" ++ x)%string (at level 0).

  Definition SPI := MODULE {

leads to goals like goals like

NoDup
  [@^ ("hack_for_sequential_semantics"); @^ ("tx_fifo"); 
  @^ ("tx_fifo_len"); @^ ("rx_fifo"); @^ ("rx_fifo_len"); 
  @^ ("sck")]

which are almost decidable but not quite due to the prefix. do we have any automation for solving them? Documentation?

[vmurali]

discharge_DisjKey ?

On Fri, Jul 26, 2019 at 1:20 PM Andres Erbsen notifications@github.com wrote:

code like

Context (name : string). Local Open Scope kami_action. Local Open Scope kamiexpr. Local Notation "@^ x" := (name ++ "" ++ x)%string (at level 0).

Definition SPI := MODULE {

leads to goals like goals like

NoDup [@^ ("hack_for_sequential_semantics"); @^ ("tx_fifo"); @^ ("tx_fifo_len"); @^ ("rx_fifo"); @^ ("rx_fifo_len"); @^ ("sck")]

which are almost decidable but not quite due to the prefix. do we have any automation for solving them? Documentation?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/sifive/Kami/issues/14?email_source=notifications&email_token=AABZURKZKAJHHTWT6YRXZQDQBNMCFA5CNFSM4IHG4WOKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HBZLHNA, or mute the thread https://github.com/notifications/unsubscribe-auth/AABZUROI44TOLOZAOD6HRC3QBNMCFANCNFSM4IHG4WOA .

[vmurali]

I take that back. One has to write it. It involves the theorems append_remove_prefix and append_remove_suffix

On Fri, Jul 26, 2019 at 1:22 PM Murali Vijayaraghavan vmurali@sifive.com wrote:

discharge_DisjKey ?

On Fri, Jul 26, 2019 at 1:20 PM Andres Erbsen notifications@github.com wrote:

code like

Context (name : string). Local Open Scope kami_action. Local Open Scope kamiexpr. Local Notation "@^ x" := (name ++ "" ++ x)%string (at level 0).

Definition SPI := MODULE {

leads to goals like goals like

NoDup [@^ ("hack_for_sequential_semantics"); @^ ("tx_fifo"); @^ ("tx_fifo_len"); @^ ("rx_fifo"); @^ ("rx_fifo_len"); @^ ("sck")]

which are almost decidable but not quite due to the prefix. do we have any automation for solving them? Documentation?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/sifive/Kami/issues/14?email_source=notifications&email_token=AABZURKZKAJHHTWT6YRXZQDQBNMCFA5CNFSM4IHG4WOKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HBZLHNA, or mute the thread https://github.com/notifications/unsubscribe-auth/AABZUROI44TOLOZAOD6HRC3QBNMCFANCNFSM4IHG4WOA .

[whonore]

The discharge_append tactic helps automate some of the proofs comparing strings with prefixes.

[vmurali]

Section NoDup.
  Variable name: string.
  Local Notation "@^ x" := (name ++ "_" ++ x)%string (at level 0).

  Goal NoDup
       [@^ ("hack_for_sequential_semantics"); @^ ("tx_fifo"); 
          @^ ("tx_fifo_len"); @^ ("rx_fifo"); @^ ("rx_fifo_len"); 
            @^ ("sck")].
  Proof.
    repeat econstructor; unfold not; intros; clean_hyp.
  Qed.
End NoDup.

This seems to work.

That said, clean_hyp is turning out to be a catch-all, which is not a great design. Let me see how I can simplify it, and/or use the reification approach for discharging prepended string related goals.