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 ***@***.***> wrote: 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? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#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 ***@***.***> wrote: > 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? > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#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.