Quale regola usa "regola" o "prova"?

Question

Quando uso apply (rule) in uno script di applicazione, in genere è selezionata una regola appropriata. Lo stesso vale per proof in prove strutturate. Dove posso imparare/cercare il nome della regola che è stata utilizzata?

Answer 1

Puoi provare a utilizzare rule_trace come segue:

lemma "a ∧ b" 
    using [[rule_trace]] 
    apply rule 

che visualizzerà nell'output:

rules: 
    ?P ⟹ ?Q ⟹ ?P ∧ ?Q 
    ?P ⟹ ?Q ⟹ ?P ∧ ?Q 
proof (prove): step 2 

goal (2 subgoals): 
1. a 
2. b 

Se i nomi delle regole sono necessari, è quindi possibile provare a utilizzare find_theorems; Non sono sicuro che possano essere determinati direttamente.

Answer 2

Tutto ciò che viene dichiarato come Pure.intro/intro/iff (o uno dei suoi ? o ! varianti) è considerato come regola di introduzione di default (vale a dire, se non sono emersi fatti attuali sono incatenati a). Allo stesso modo, tutto ciò che viene dichiarato come Pure.elim/elim/iff viene considerato come regola di eliminazione predefinita (ad esempio, se i fatti attuali sono concatenati). Solitamente le dichiarazioni successive hanno la precedenza su quelle precedenti (almeno se viene utilizzato lo stesso tipo di dichiarazione ... la miscelazione, ad es. Pure.intro? con intro, ecc., Potrebbe risultare diversa).

Tuttavia, questo risponde solo al tipo di regole considerate in linea di principio. Non conosco un modo per scoprire direttamente quale regola è stata applicata. Ma è relativamente semplice trovare la regola corretta per find_theorems intro direttamente sopra la linea che ti stavi chiedendo. Per esempio,

lemma "A & B" 
find_theorems intro 
proof 

vi mostrerà tutte le regole che potrebbero essere applicati come regola di introduzione alla meta A & B. Uno di questi è la regola predefinita applicata da proof (lo riconoscerai dalle sotto-risposte che hai ottenuto).

Per le regole di eliminazione è possibile utilizzare, ad esempio,

lemma assumes "A | B" shows "P" 
using assms 
find_theorems elim 
proof 

Answer 3

Le altre risposte indicano già come determinare quali lemmi vengono applicati da rule. Si noti che proof non chiama lo rule, ma il metodo default. La maggior parte delle volte, default fa la stessa cosa di rule, ma ad es. per dimostrare un predicato locale chiama unfold_locales.

Non conosco alcun metodo per vedere cosa succede realmente lì.