Unverified Commit 96198532 authored by Jonas Betzendahl's avatar Jonas Betzendahl
Browse files

restore ELPI playground

parent 23dc6989
accumulate "generated/plnd".
accumulate "generic/idprove".
accumulate "generic/bc".
%accumulate "generated/plnd".
accumulate "generated/plnd".
%id_prove_run N Res F :- ded (bccert N) F, print X, Res is "Success".
%id_prove_run N Res F :- ded (bccert N) F, Res is "Success".
% id_prove_run N Res F :- alonzoDed (bccert N) F, Res is "Success".
id_prove_run N Res F :- alonzoDed (bccert N) F, Res is "Success".
id_prove_run N Res F :- ded (prodcert (bccert N) (ptcert Res)) F.
accumulate "generic/idprove".
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..NONE/$Alonzo".
accumulate "../export/lf-elpi/content/latin..-/$Alonzo".
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..-/$Alonzo$Proof".
mytest P :- P (def_alonzo bool f_omicron)
mytest P :- P (def_alonzo bool f_omicron).
main :- mytest id_prove.
main.
......
log console
log html build.html
log+ archive
log+ mmt-omdoc
log+ lf-elpi
extension info.kwarc.mmt.lf.Plugin
extension info.kwarc.mmt.lf.elpi.ELPIExporter
mathpath archive ../../urtheories
mathpath archive ..
log+ debug
//log+ object-checker
//log+ object-simplifier
//log+ structure-simplifier
//log+ structure-checker
//log+ object-parser
// build the mmt files (no need to repeat if unchanged)
build MMT/LATIN2 mmt-omdoc fundamentals
build MMT/LATIN2 mmt-omdoc logic/propositional
build MMT/LATIN2 mmt-omdoc logic/fol_like
build MMT/LATIN2 mmt-omdoc type_theory
build MMT/LATIN2 mmt-omdoc casestudies/alonzo
//build MMT/LATIN2 mmt-omdoc undefinedness
// generate the ELPI file (stored in the folder export/lf-elpi/content, one file per theory)
build MMT/LATIN2 lf-elpi fundamentals
build MMT/LATIN2 lf-elpi logic/propositional
build MMT/LATIN2 lf-elpi logic/fol_like
build MMT/LATIN2 lf-elpi type_theory
build MMT/LATIN2 lf-elpi casestudies/alonzo
//build MMT/LATIN2 lf-elpi undefinedness
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..-/$Undefined$N$D".
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..-/$Typed$Equality$N$D".
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..-/$Booleans".
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..-/$Simple$Functions".
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..-/$Simple$Products".
accumulate "/home/totoro/Development/KWARC/content/MathHub/MMT/LATIN2/export/lf-elpi/content/latin..-/tp$Equality".
/* generated from boolTy : tp */
/* generated from funTy : tp⟶tp⟶tp */
/* generated from prodTy : tp⟶tp⟶tp */
/* generated from alonzoDed : tm ο⟶type */
alonzoDed X2 X1 :- alonzoDed/hyp X3 X1 , help/alonzoDed X1 X3 X2.
help/alonzoDed X1 X3 (prodcert X2/1 X2/2) :- help/alonzoDed X1 X3 X2/1 , help/alonzoDed X1 X3 X2/2.
help/alonzoDed X1 X2 (idcert X3).
help/alonzoDed X1 X2 (ptcert (i X1)).
help/alonzoDed X1 X2 (bccert X3).
/* generated from equals : {α:tp}tm α⟶tm α⟶tm ο */
/* generated from defdes : {α:tp}(tm α⟶tm ο)⟶tm α */
/* generated from indefdes : {α:tp}(tm α⟶tm ο)⟶tm α */
/* generated from t_omicron : tm ο */
/* generated from f_omicron : tm ο */
/* generated from wedge : tm ο→(ο→ο) */
/* generated from wedge_apply : tm ο⟶tm ο⟶tm ο */
/* generated from implic : tm ο→(ο→ο) */
/* generated from implic_apply : tm ο⟶tm ο⟶tm ο */
/* generated from negation : tm ο→ο */
/* generated from negation_apply : tm ο⟶tm ο */
/* generated from vee : tm ο→(ο→ο) */
/* generated from vee_apply : tm ο⟶tm ο⟶tm ο */
/* generated from ifa : {α:tp}tm ο→(α→(α→α)) */
/* generated from ifa_apply : {α:tp}tm ο⟶tm α⟶tm α⟶tm α */
/* generated from equivalence : tm ο→(ο→ο) */
/* generated from equivalence_apply : tm ο⟶tm ο⟶tm ο */
/* generated from unequals : {α:tp}tm α→(α→ο) */
/* generated from unequals_apply : {α:tp}tm α⟶tm α⟶tm ο */
/* generated from tripequals : {α:tp}tm α→(α→(α→ο)) */
/* generated from tripequals_apply : {α:tp}tm α⟶tm α⟶tm α⟶tm ο */
/* generated from forall_alonzo : {α:tp}(tm α⟶tm ο)⟶tm ο */
/* generated from forsome_alonzo : {α:tp}(tm α⟶tm ο)⟶tm ο */
/* generated from forone_alonzo : {α:tp}(tm α⟶tm ο)⟶tm ο */
/* generated from bot_omicron : tm ο */
/* generated from bot_alpha : {α:tp}tm α */
/* generated from delta_alonzo : {α:tp,β:tp}tm α→β */
/* generated from def_alonzo : {α:tp,A:tm α}tm ο */
/* generated from undef_alonzo : {α:tp,A:tm α}tm ο */
/* generated from simeq_alonzo : {α:tp,A:tm α,B:tm α}tm ο */
/* generated from nsimeq_alonzo : {α:tp,A:tm α,B:tm α}tm ο */
/* generated from t_def : ⊢T₀⇩ */
alonzoDed X1 (def_alonzo bool t_omicron) :- help/t_def X1.
help/t_def (prodcert X2/1 X2/2) :- help/t_def X2/1 , help/t_def X2/2.
help/t_def (idcert X3) :- X3 > 0 , X2 is X3 - 1.
help/t_def (ptcert t_def).
/* latin:/?Alonzo?t_def: u: skipping due to error: can't create helper: no hypotheses found */
help/t_def (hdcert X2).
help/t_def (hd2cert X2).
help/t_def (bccert X3) :- bc/pos X3 , X2 is X3 - 1.
/* generated from f_def : ⊢F₀⇩ */
alonzoDed X1 (def_alonzo bool f_omicron) :- help/f_def X1.
help/f_def (prodcert X2/1 X2/2) :- help/f_def X2/1 , help/f_def X2/2.
help/f_def (idcert X3) :- X3 > 0 , X2 is X3 - 1.
help/f_def (ptcert f_def).
/* latin:/?Alonzo?f_def: u: skipping due to error: can't create helper: no hypotheses found */
help/f_def (hdcert X2).
help/f_def (hd2cert X2).
help/f_def (bccert X3) :- bc/pos X3 , X2 is X3 - 1.
/* generated from set : {α:tp}tp */
/* generated from elem : {α:tp}tm α⟶tm ❴α❵⟶tm ο */
/* generated from nelem : {α:tp}tm α⟶tm ❴α❵⟶tm ο */
/* generated from setcomp : {α:tp}(tm α⟶tm ο)⟶tm ❴α❵ */
/* generated from emptys : {α:tp}tm α→ο */
/* generated from fulls : {α:tp}tm α→ο */
/* generated from one_alpha_set : {α:tp}tm α→(α→ο) */
/* generated from one_alpha_set_a : {α:tp}tm α⟶tm α⟶tm ο */
/* generated from two_alpha_set : {α:tp}tm α→(α→(α→ο)) */
/* generated from two_alpha_set_a : {α:tp}tm α⟶tm α⟶tm α⟶tm ο */
/* generated from three_alpha_set : {α:tp}tm α→(α→(α→(α→ο))) */
/* generated from three_alpha_set_a : {α:tp}tm α⟶tm α⟶tm α⟶tm α⟶tm ο */
/* generated from subseteq : {α:tp}tm ❴α❵→(❴α❵→ο) */
/* generated from subseteq_a : {α:tp}tm ❴α❵⟶tm ❴α❵⟶tm ο */
/* generated from subset : {α:tp}tm ❴α❵→(❴α❵→ο) */
/* generated from subset_a : {α:tp}tm ❴α❵⟶tm ❴α❵⟶tm ο */
/* generated from union : {α:tp}tm ❴α❵→(❴α❵→❴α❵) */
/* generated from union_a : {α:tp}tm ❴α❵⟶tm ❴α❵⟶tm ❴α❵ */
/* generated from intersection : {α:tp}tm ❴α❵→(❴α❵→❴α❵) */
/* generated from intersection_a : {α:tp}tm ❴α❵⟶tm ❴α❵⟶tm ❴α❵ */
/* generated from bar : {α:tp}tm ❴α❵→❴α❵ */
/* generated from bar_a : {α:tp}tm ❴α❵⟶tm ❴α❵ */
/* generated from tuple : {α:tp,β:tp}tm α⟶tm β⟶tm α×β */
/* generated from fst : {α:tp,β:tp}tm (α×β)→α */
/* generated from fst_a : {α:tp,β:tp}tm α×β⟶tm α */
/* generated from snd : {α:tp,β:tp}tm (α×β)→β */
/* generated from snd_a : {α:tp,β:tp}tm α×β⟶tm β */
/* generated from total_alonzo : {α:tp,β:tp}tm α→β⟶tm ο */
/* generated from total2_alonzo : {α:tp,β:tp,γ:tp}tm α→(β→γ)⟶tm ο */
/* generated from surj_alonzo : {α:tp,β:tp}tm α→β⟶tm ο */
/* generated from surj2_alonzo : {α:tp,β:tp,γ:tp}tm α→(β→γ)⟶tm ο */
/* generated from inj_alonzo : {α:tp,β:tp}tm α→β⟶tm ο */
/* generated from bij_alonzo : {α:tp,β:tp}tm α→β⟶tm ο */
/* generated from distinct2 : {α:tp}tm α⟶tm α⟶tm ο */
/* generated from distinct3 : {α:tp}tm α⟶tm α⟶tm α⟶tm ο */
/* generated from distinct4 : {α:tp}tm α⟶tm α⟶tm α⟶tm α⟶tm ο */
/* generated from distinct5 : {α:tp}tm α⟶tm α⟶tm α⟶tm α⟶tm α⟶tm ο */
/* generated from quasitype : {α:tp}tp */
/* generated from qt_lambda : {α:tp,β:tp,Q:tm 𝒬α}(tm α⟶tm β)⟶tm α→β */
/* generated from qt_forall : {α:tp,Q:tm 𝒬α}(tm α⟶tm ο)⟶tm ο */
/* generated from qt_exists : {α:tp,Q:tm 𝒬α}(tm α⟶tm ο)⟶tm ο */
/* generated from qt_definite : {α:tp,Q:tm 𝒬α}(tm α⟶tm ο)⟶tm α */
/* generated from qt_def : {α:tp,Q:tm 𝒬α}tm α⟶tm ο */
/* generated from qt_ndef : {α:tp,Q:tm 𝒬α}tm α⟶tm ο */
/* generated from qt_arr : {α:tp,β:tp}tm ❴α❵→(❴β❵→❴α→β❵) */
/* generated from qt_pair : {α:tp,β:tp}tm ❴α❵→(❴β❵→❴α×β❵) */
/* generated from arr_qarb : {α:tp,β:tp,Q:tm 𝒬α,R:tm 𝒬β}tm 𝒬(α→β) */
/* generated from arr_arb : {α:tp,β:tp,R:tm 𝒬β}tm 𝒬(α→β) */
/* generated from arr_qab : {α:tp,β:tp,Q:tm 𝒬α}tm 𝒬(α→β) */
/* generated from pair_qarb : {α:tp,β:tp,Q:tm 𝒬α,R:tm 𝒬β}tm 𝒬(α×β) */
/* generated from pair_arb : {α:tp,β:tp,R:tm 𝒬β}tm 𝒬(α×β) */
/* generated from pair_qab : {α:tp,β:tp,Q:tm 𝒬α}tm 𝒬(α×β) */
/* generated from al_totalon : {α:tp,β:tp,F:tm α→β,Q:tm 𝒬α,R:tm 𝒬β}tm ο */
/* generated from al_totalon2 : {α:tp,β:tp,γ:tp,F:tm α→(β→γ),Q:tm 𝒬α,R:tm 𝒬β,S:tm 𝒬γ}tm ο */
/* generated from al_SURJon : {α:tp,β:tp,F:tm α→β,Q:tm 𝒬α,R:tm 𝒬β}tm ο */
/* generated from al_SURJon2 : {α:tp,β:tp,γ:tp,F:tm α→(β→γ),Q:tm 𝒬α,R:tm 𝒬β,S:tm 𝒬γ}tm ο */
/* generated from al_INJon : {α:tp,β:tp,F:tm α→β,Q:tm 𝒬α}tm ο */
/* generated from al_BIJon : {α:tp,β:tp,F:tm α→β,Q:tm 𝒬α,R:tm 𝒬β}tm ο */
/* generated from al_INF : {α:tp,Q:tm 𝒬α}tm ο */
/* generated from al_FIN : {α:tp,Q:tm 𝒬α}tm ο */
/* generated from al_COUNT : {α:tp,Q:tm 𝒬α}tm ο */
/* generated from alonzo_pi : {α:tp,β:tp}tm ❴α❵→((α→❴β❵)→❴α→β❵) */
/* generated from alonzo_sigma : {α:tp,β:tp}tm ❴α❵→((α→❴β❵)→❴α×β❵) */
/* generated from qt_pi : {α:tp,β:tp,Q:tm 𝒬α,R:tm 𝒬β}tm 𝒬(α→β) */
/* generated from qt_sigma : {α:tp,β:tp,Q:tm 𝒬α,R:tm 𝒬β}tm 𝒬(α×β) */
% Generic helper predicates for backchaining
% (need to be included whenever bccert is used)
bc/aux A A.
bc/val (bc/fwdLocked M) M :- !.
bc/val M M.
bc/pos (bc/fwdLocked _) :- !, fail.
bc/pos M :- M > 0.
bc/fwdable A :- ded/hyp _ T, bc/aux T A.
% generic tableau stuff
help/model (prodcert X5/1 X5/2) :- help/model X5/1 , help/model X5/2 .
help/model (idcert _).
help/model (ptcert _) :- fail.
help/model (ucert _).
help/model (hdcert S) :- save_models S.
help/model (bccert _).
save_models S :- new_safe S1, new_safe S2, collect/marktrue S1, collect/markfalse S2,
open_safe S1 L1, open_safe S2 L2, stash_in_safe S (branch_t_f L1 L2).
collect/marktrue S :- marktrue/hyp _ T0, term_to_string T0 T, stash_in_safe S T, fail.
collect/marktrue _.
collect/markfalse S :- markfalse/hyp _ T0, term_to_string T0 T, stash_in_safe S T, fail.
collect/markfalse _.
% X occurs at most N times in L
occatmost _ 0 _ :- !, fail.
occatmost X N (prep X L) :- !, N2 is N - 1, occatmost X N2 L.
occatmost X N (prep H L) :- !, occatmost X N L.
occatmost X N nil.
This diff is collapsed.
$(function() {
$("span.error-short").click(function(){$(this).parents('.error').children(".error-long").toggle()})
}
)
\ No newline at end of file
div.log {
margin: 2pt;
}
div.user {
border:solid;
border-width: 1;
}
span {
margin-right: 5pt;
}
span.caller {
color: gray;
}
span.group {
font-weight: bold;
}
span.message {
}
span.timestamp {
font-color: gray;
}
span.error-short {
font-weight: bold;
color: red;
}
div.error-long {
display: none;
margin-left: 20pt;
}
accumulate "generic/bc".
accumulate "generated/plnd".
id_prove_run N Res F :- ded (prodcert (bccert N) (ptcert Res)) F.
accumulate "generic/idprove".
mytest P :- pi a \ pi b \ P (impl a (impl b a)).
mytest P :- pi a \ pi b \ P (impl (and a b) a).
mytest P :- pi a \ pi b \ P (impl (or a b) (or b a)).
mytest P :- pi a \ pi b \ P (impl (and a b) (impl (impl a (impl b false)) false)).
mytest P :- pi a \ pi b \ pi c \ P (impl (impl a (or b c)) (impl (impl b c) (impl a c))).
mytest P :- pi a \ pi b \ P (or a (not a)).
mytest P :- pi a \ pi b \ P (or (not a) a).
main :- mytest id_prove.
main.
......@@ -228,6 +228,7 @@ theory Alonzo =
/T 𝕬 (jfrakA) is a proof system for Alonzo. ❚
/T Also, the unicode symbol can't be the theory name because Scala gets unhappy. ❚
theory AlonzoProof =
include ?Alonzo❙
......@@ -242,11 +243,11 @@ theory AlonzoProof =
a3 : { α : tp, β : tp, f : tm (α → β), g : tm (α → β) } ⊢ ((f == g) ⇔ (∀ᴬ [x : tm α] ((f@x) ≃ (g@x))))❙
/T A4 Beta Reduction❙
a4 ❙ /T ??? ❙
/T a4 ??? ❙
/T A5 Definedness❙
a5_1 ❙ /T ??? ❙
a5_2 ❙ /T ??? ❙
/T a5_1 ??? ❙
/T a5_2 ??? ❙
a5_3 : { α : tp, A : tm α, B : tm α } ⊢ ((A == B)⇩)❙
a5_4 : { α : tp, A : tm α, B : tm α } ⊢ (((A⇧) ∨ (B⇧)) ⇒ (¬(A == B)))❙
a5_5 : { α : tp, A : tm α, F : tm (α → ο) } ⊢ ((F@A)⇩)❙
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment