Jak mogę łatwo napisać prostą taktykę na poziomie ML Isabelle?

Question

w pliku teorii Isabelle, mogę pisać proste taktyki jednego wiersza, takich jak:

apply (clarsimp simp: split_def split: prod.splits) 

Uważam jednak, kiedy zaczynam pisać kod ML zautomatyzować dowodów, w celu wytworzenia przedmiotu ML tactic, te jednej wkładki stać raczej gadatliwy:

clarsimp_tac (Context.proof_map (
    Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits}) 
    #> Simplifier.map_ss (fn ss => ss addsimps [@{thm split_def}])) 
    @{context}) 1 

Czy istnieje prostszy sposób pisania prostych taktyk jedną linię na poziomie Isabelle/ml?

Na przykład, coś w stylu anty-oferty: @{tactic "clarsimp simp: split_def split: prod.splits"} produkującej funkcję typu context -> tactic, byłoby idealnym rozwiązaniem.

Answer 1

Widzę różne możliwości, zależy to trochę od kontekstu aplikacji, co jest najlepsze. Zauważ, że na ogół indywidualny kod ML dla dowodu zautomatyzowanego był zwykłym miejscem w dawnych czasach, ale dziś jest stosunkowo rzadki. Na przykład porównaj liczbę niestandardowych taktyk w raczej małym numerze HOL-Bali (rozpoczętym w 1997 r.) Z dużym JinjaThreads w AFP (rozpoczęty w 2007 r. I kontynuowany do niedawna).

Zagnieżdżanie antytokacji ML, takich jak @{tactic}, z zasady zadziałałoby, ale szybko natknąłbyś się na dalsze pytania, np. Co się stanie, jeśli argumenty teorematyczne będą znowu źródłem Isar lub ML.

Zamiast antiquoting taktyczne cegiełki w ml, bardziej podstawowe podejście jest cytatem dowód precedure w Isar poprzez nadanie mu regularne składni metody tak:

ML {* 
    (*foo_tac -- the payload of what you want to do, 
    note the dependency on ctxt: Proof.context*) 
    fun foo_tac ctxt = 
    let 
     val my_ctxt = 
     ctxt |> Simplifier.map_simpset 
     (fold Splitter.add_split @{thms prod.splits} #> 
      Simplifier.add_simp @{thm split_def}) 
    in ALLGOALS (clarsimp_tac my_ctxt) end 
*} 

method_setup foo = {* 
    (*concrete syntax like "clarsimp", "auto" etc.*) 
    Method.sections Clasimp.clasimp_modifiers >> 
    (*Isar method boilerplate*) 
    (fn _ => fn ctxt => SIMPLE_METHOD (CHANGED (foo_tac ctxt))) 
*} 

Tutaj mam pierwszy utworzyłem standardową definicję foo_tac w Isabelle/ML, a następnie zapakowałem ją w zwykły sposób Isar jako metodę sprawdzającą. To ostatnie oznacza, że ​​masz opakowania takie jak SIMPLE_METHOD, które zajmują się wypychaniem "przykutych faktów" do stanu docelowego, oraz CHANGED, aby zapewnić postęp procesu Isar (np. simp lub auto).

Przykład foo_tac zakłada, że ​​modyfikacja kontekstu (lub jego Simpset) jest stała, według sztywnych reguł podziału. Jeśli chcesz mieć dalsze parametry, możesz to uwzględnić w składni konkretnej metody. Zauważ, że Method.sections jest już dość wyrafinowany pod tym względem. Więcej podstawowych analizatorów argumentów podano w rozdziale "Definiowanie metod sprawdzania" w podręczniku isar-ref. Powinieneś także przyjrzeć się istniejącym przykładom, szukając źródeł dla method_setup (w Isabelle/Isar) lub Method.setup (w Isabelle/ML).

Jeśli nadal chcesz zrobić ML antiquotations zamiast konkretnej składni metody, można wypróbować wariant @{context} który pozwala modyfikatory tak:

@{context simp add: ...} 

To jest nieco spekulacyjny, wymyślone na poczekaniu, a może okazać się złą praktyką. Jak już powiedziałem, precyzyjne programowanie taktyki w Isabelle stało się w ostatnich latach nieco niecelowe, chociaż ML jest integralną częścią struktury Isabelle. Jeśli stawiasz bardziej konkretne pytanie z większą ilością kontekstu aplikacji, możemy ponownie rozważyć podejście antydotywacyjne.

Answer 2

Klasa Method wydają się zapewniać wystarczającą ilość interfejs do wyekstrahowania taktyki, poprzez cases_tactic następująco:

(* 
* Generate an ML tactic object of the given Isar string. 
* 
* For example, 
* 
* mk_tac "auto simp: field_simps intro!: ext" @{context} 
* 
* will generate the corresponding "tactic" object. 
*) 
fun mk_tac str ctxt = 
let 
    val parsed_str = Outer_Syntax.scan Position.start str 
     |> filter Token.is_proper 
     |> Args.name 
    val meth = Method.method (Proof_Context.theory_of ctxt) 
     (Args.src (parsed_str, Position.start)) ctxt 
in 
    Method.apply (K meth) ctxt [] #> Seq.map snd 
end 

lub alternatywnie jako anty-notowania:

(* 
* Setup an antiquotation of the form: 
* 
* @{tactic "auto simp: foo intro!: bar"} 
* 
* which returns an object of type "context -> tactic". 
* 
* While this doesn't provide any benefits over a direct call to "mk_tac" just 
* yet, in the future it may generate code to avoid parsing the tactic at 
* run-time. 
*) 
val tactic_antiquotation_setup = 
let 
    val parse_string = 
    ((Args.context -- Scan.lift Args.name) >> snd) 
     #>> ML_Syntax.print_string 
     #>> (fn s => "mk_tac "^s) 
     #>> ML_Syntax.atomic 
in 
    ML_Antiquote.inline @{binding "tactic"} parse_string 
end 

i konfiguracji w pliku teoretycznym:

setup {* 
    tactic_antiquotation_setup 
*} 

, które można następnie użyte w następujący sposób:

lemma "(a :: nat) * (b + 1) = (a * b) + a" 
    by (tactic {* @{tactic "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"} @{context} *}) 

zgodnie z potrzebami.

Answer 3

Oprócz innych odpowiedzi, myślę, że warto wspomnieć, że istnieje nowy wysokopoziomowy język konstrukcji taktycznej/metody proof (podobny do Ltac w Coq) o nazwie Eisbach w Isabelle2015, który ma być łatwiejszy do zrozumienia i utrzymania .