Commit db6e41d0 authored by Florian Rabe's avatar Florian Rabe

changes related to revised type checking

parent 09ed0b60
This source diff could not be displayed because it is too large. You can view the blob instead.
<errors>
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: http://cds.omdoc.org/examples?NatMinus?minus_inverse?definition: Judgment |- [X]trans minus_pi minus_intro_R plus_neut_Ex X : {X}⊦X-X!leq_refl =O" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:90)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15$adapted(RuleBasedChecker.scala:89)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$13(RuleBasedChecker.scala:89)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:86)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16(MMTStructureChecker.scala:301)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16$adapted(MMTStructureChecker.scala:277)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:277)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:715)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:715)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:39)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: http://cds.omdoc.org/examples?NatMinus?minus_inverse?definition: Judgment |- [X]trans minus_pi minus_intro_R plus_neut_Ex X : {X}⊦X-X!leq_refl =O" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:90)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15$adapted(RuleBasedChecker.scala:89)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$13(RuleBasedChecker.scala:89)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:86)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16(MMTStructureChecker.scala:301)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16$adapted(MMTStructureChecker.scala:277)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:277)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:715)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:715)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:39)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</errors>
......@@ -2,6 +2,7 @@ document http://docs.omdoc.org/examples
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/opaque_-1915976980
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/IJCAR2018_example.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/argumentation.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/arithmetic_rules.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/base-arith.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/dummy.omdoc
......
......@@ -3,7 +3,6 @@ dataconstructor http://cds.omdoc.org/examples?NatMinus?minus_pi
dataconstructor http://cds.omdoc.org/examples?NatMinus?minus_intro_L
dataconstructor http://cds.omdoc.org/examples?NatMinus?minus_intro_R
dataconstructor http://cds.omdoc.org/examples?NatMinus?minus_elim
dataconstructor http://cds.omdoc.org/examples?NatMinus?minus_inverse
theory http://cds.omdoc.org/examples?NatMinus
HasMeta http://cds.omdoc.org/examples?NatMinus http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples?NatMinus http://cds.omdoc.org/examples?Bool
......@@ -21,5 +20,3 @@ Declares http://cds.omdoc.org/examples?NatMinus http://cds.omdoc.org/examples?Na
constant http://cds.omdoc.org/examples?NatMinus?minus_intro_R
Declares http://cds.omdoc.org/examples?NatMinus http://cds.omdoc.org/examples?NatMinus?minus_elim
constant http://cds.omdoc.org/examples?NatMinus?minus_elim
Declares http://cds.omdoc.org/examples?NatMinus http://cds.omdoc.org/examples?NatMinus?minus_inverse
constant http://cds.omdoc.org/examples?NatMinus?minus_inverse
......@@ -34,7 +34,7 @@ theory Vectors : http://cds.omdoc.org/urtheories?LF =
append : {m,n} vec m ⟶ vec n ⟶ vec (m + n) ❘ # 3 @ 4❙
// this only type-checks because vec n+0 and vec n are recognized as equal ❙
// appendempty : {n, v: vec n} v @ ∅ == v❙
appendempty : {n, v: vec n} v @ ∅ == v❙
// this only type-checks because vec m + (n') and vec (m + n)' are recognized as being equal ❙
appendcons : {m,n, x, v: vec m, w: vec n} v @ (w,x) == (v @ w, x) ❘ role Simplify❙
......
......@@ -18,9 +18,12 @@ theory Syntax : http://cds.omdoc.org/urtheories?LF =
0 : o❙
⊸ : o ⟶ o ⟶ o ❘# 1 ⊸ 2 prec 80❙
! : o ⟶ o ❘# ! 1 prec 110❙
⇒ : o ⟶ o ⟶ o ❘# 1 ⇒ 2 prec 80❘
= [x,y] !x ⊸ y❙
theory CommutativeMonoid : /examples?FOLEQNatDed =
theory Worlds : /examples?FOLEQNatDed =
// worlds contain resources ❙
world : type❘= term❙
// union of worlds, corresponds to multiset union of resources ❙
......@@ -28,39 +31,51 @@ theory CommutativeMonoid : /examples?FOLEQNatDed =
// empty world with no resources ❙
empty : world❘# ε❙
// * is a commutative monoid❙
// * is a monoid❙
neutL : {P} ⊦ ε*P ≐ P❙
neutR : {P} ⊦ P*ε ≐ P❙
assoc : {P,Q,R} ⊦ (P*Q)*R ≐ P*(Q*R)❙
// ordering with monotonicity❙
weaker : world ⟶ world ⟶ prop ❘ # 1 ≤ 2 prec 80❙
≤_refl : {P} ⊦ P ≤ P❙
≤_antisym: {P,Q} ⊦ P ≤ Q ⟶ ⊦ Q ≤ P ⟶ ⊦ P≐Q❙
≤_trans : {P,Q,R} ⊦ P≤Q ⟶ ⊦ Q≤R ⟶ ⊦ P≤R ❙
≤_monotone: {a,b,c,d} ⊦ a ≤ b ⟶ ⊦ c ≤ d ⟶ ⊦ a*c ≤ b*d❙
theory Exchange : /examples?FOLEQNatDed =
include ?Worlds❙
// exchange is commutativity❙
comm : {P,Q} ⊦ P*Q ≐ Q*P❙
rule rules?NormalizeWorlds❙
rule rules?EquateWorlds❙
test : {p,q,r} ⊦ r*(p*q)*ε*r ≐ r*(r*(q*p)) ❘= [p,q,r] refl❙
theory Contraction : /examples?FOLEQNatDed =
include ?Worlds❙
// contraction is idempotence ❙
idem : {P} ⊦ P*P ≐ P❙
// least world is weaking (without this, the order is trivial, i.e., there is no weakening)❙
theory Weakening : /examples?FOLEQNatDed =
include ?Worlds❙
// least world is weakening (without this, the order is trivial, i.e., there is no weakening)❙
≤_least : {P} ⊦ ε ≤ P❙
rule rules?NormalizeWorlds❙
rule rules?EquateWorlds❙
divisibility: {P,Q} ⊦ P ≤ P*Q ❘
= [P,Q] (≤_monotone ≤_refl ≤_least)❙
test : {p,q,r} ⊦ r*(p*q)*ε*r ≐ r*(r*(q*p)) ❘= [p,q,r] refl❙
// Proofs of the linear sequent A1, ..., An |- A are represented as terms of type
(A1 ⊗ ... ⊗ An) ⊸ A @ ε❚
theory ResourceSemantics : /examples?FOLEQNatDed =
include ?Syntax❙
include ?CommutativeMonoid❙
include ?Worlds❙
include ?Exchange❙
// A @ P: A can be produced by using all resources available in world P❙
at : o ⟶ world ⟶ prop❙
......@@ -71,6 +86,10 @@ theory ResourceSemantics : /examples?FOLEQNatDed =
// should be a subtyping rule❙
weaken: {A,v,w} A @ v ⟶ ⊦v≤w ⟶ A @ w❙
⊗_R : {A,B,a,b} A @ a ⟶ B @ b ⟶ A ⊗ B @ a*b❙
⊗_L : {A,B,C,u,v} A ⊗ B @ u ⟶ ({a}{b} A @ a ⟶ B @ b ⟶ C @ a*b*v) ⟶ C @ u*v❘
# ⊗_L 6 7❙
1_R : 1 @ ε❙
1_L : {C,u,v} 1 @ u ⟶ C @ v ⟶ C @ u*v❙
......@@ -97,21 +116,44 @@ theory ResourceSemantics : /examples?FOLEQNatDed =
!_R : {A} A @ ε ⟶ ! A @ ε❙
!_L : {A,C,u,v} ! A @ u ⟶ (A @ ε ⟶ C @ v) ⟶ C @ u*v❙
⊗_R : {A,B,a,b} A @ a ⟶ B @ b ⟶ A ⊗ B @ a*b❙
⊗_L : {A,B,C,u,v} A ⊗ B @ u ⟶ ({a}{b} A @ a ⟶ B @ b ⟶ C @ a*b*v) ⟶ C @ u*v❘
# ⊗_L 6 7❙
⊗_commute : {A,B} valid A⊗B ⊸ B⊗A❘
= [A,B] ⊸_R [ab,h] ⊗_L h [a,b,p,q] ⊗_R q p❙
// needs to solve abc * X = abc and ab * Y * X = ab * c, solution: X = epsilon, Y = c❙
⊗_assoc1 : {A,B,C} valid (A⊗B)⊗C ⊸ A⊗(B⊗C)❘
= [A,B,C] ⊸_R [abc,h] ⊗_L h
[ab,c,pq,r] ⊗_L pq
[ab,c,pq,r] ⊗_L pq
([a,b,p,q] ⊗_R p (⊗_R q r))❙
⊗_assoc2 : {A,B,C} valid A⊗(B⊗C) ⊸ (A⊗B)⊗C❘
= [A,B,C] ⊸_R [abc,h] ⊗_L h
[a,bc,p,qr] ⊗_L qr
([b,c,q,r] ⊗_R (⊗_R p q) r)❙
⊗_neutral1 : {A} valid A⊗1 ⊸ A❘
= [A] ⊸_R [ao,h] ⊗_L h [a,b,p,q] 1_L q p❙
⊗_neutral2 : {A} valid A ⊸ A⊗1❘
= [A] ⊸_R [ao,h] ⊗_R h 1_R❙
= [A] ⊸_R [a,h] ⊗_R h 1_R❙
⊕_commute : {A,B} valid A⊕B ⊸ B⊕A❘
= [A,B] ⊸_R [ab,h] ⊕_L h ([a,p] ⊕_Rr p) ([b,q] ⊕_Rl q)❙
⊕_neutral1 : {A} valid A⊕0 ⊸ A❘
= [A] ⊸_R [ao,h] ⊕_L h ([a,p] p) ([o,q] 0_L q)❙
⊕_neutral2 : {A} valid A ⊸ A⊕0❘
= [A] ⊸_R [a,h] ⊕_Rl h❙
!_over_⊕ : {A,B} valid (!A⊕!B) ⊸ !(A⊕B)❘
= [A,B] ⊸_R [ab,h] ⊕_L h ([a,p] !_L p ([pE] !_R (⊕_Rl pE)))
([b,q] !_L q ([qE] !_R (⊕_Rr qE)))❙
!_over_& : {A,B} valid !(A&B) ⊸ (!A&!B)❘
= [A,B] ⊸_R [ab,h] &_R (!_L h [pqE] &_Ll pqE ([a,p] !_R p))
(!_L h [pqE] &_Lr pqE ([b,q] !_R q))❙
!_idempotent1 : {A} valid !!A ⊸ !A❘
= [A] ⊸_R [a,h] !_L h [k] !_L k [l] !_R l❙
!_idempotent2 : {A} valid !A ⊸ !!A❘
= [A] ⊸_R [a,h] !_L h [k] !_R (!_R k)❙
!_weaken : {A} valid !A ⊸ A❘
= [A] ⊸_R [a,h] !_L h [k] k❙
\ No newline at end of file
......@@ -41,6 +41,7 @@ theory NatRules : http://cds.omdoc.org/urtheories?LF =
plus_assoc : {X,Y,Z} ⊦ (X + Y) + Z = X + (Y + Z) ❙
plus_neut_Ex : {X} ⊦ X + O = X ❘ # %%prefix 0 1❙
plus_neut : {X} ⊦ X + O = X ❘ = [X] plus_neut_Ex X ❘role Simplify ❙
plus_neut_L : {X} ⊦ O + X = X❘ = [X] trans plus_comm plus_neut❘ role Simplify ❙
plus_succ_R : {X,Y} ⊦ X + Y' = (X+Y)'❘role Simplify ❙
plus_succ_L : {X,Y} ⊦ X' + Y = (X+Y)'❘role Simplify ❙
......
......@@ -11,7 +11,7 @@
namespace http://cds.omdoc.org/examples/tutorial❚
/T A theory defines a language. It may optionally use a meta-theory, which is given by its URI.❚
theory FOL : http://cds.omdoc.org/urtheories?LF =
theory FOL : http://cds.omdoc.org/urtheories?PLF =
/T The simplest declaration in an MMT theory introduces a named symbol.
Every declaration can have multiple attributes following the name.
......@@ -82,6 +82,19 @@ theory FOL : http://cds.omdoc.org/urtheories?LF =
forall : {s} (tm s ⟶ prop) ⟶ prop❘# ∀ 2❙
exists : {s} (tm s ⟶ prop) ⟶ prop❘# ∃ 2❙
nat : sort❙
N = tm nat❙
zero : N❙
plus: N ⟶ N ⟶ N ❘ # 1 + 2 prec 100❙
leq: N ⟶ N ⟶ prop ❘ # 1 ≤ 2 prec 100❙
prod : type ⟶ type ⟶ type ❘ # 1 * 2❙
pair : {A,B} A ⟶ B ⟶ A * B ❘ # 3 ∙ 4 prec 50❙
bigplus : {s} (tm s ⟶ prop * N) ⟶ N ❘ # Σ 2 prec 40❙
test : N ⟶ N ❘ = [x] Σ [i] i ≤ x ∙ i❙
/T Finally, we need to be able to talk about the truth of propositions.
For that, we introduce a Curry-Howard style judgment: The LF-type '⊢ P' is the type of proofs of the proposition 'P'.
......@@ -89,6 +102,11 @@ theory FOL : http://cds.omdoc.org/urtheories?LF =
❘ role Judgment❙
/T It's practical to give ⊢ a very low precedence to avoid brackets later on.❙
test2 : {R,S,F} ⊢ (Σ [x:N] R x ∙ Σ [y:N] S x y ∙ F x y) =
(Σ [y:N] S y y ∙ Σ [x:N] R x ∙ F x y)❙
/T The 'role Judgment' is an attribute introduced by the LF plugin (which tells MMT to be loaded automatically whenever LF is used).
By annotation the symbol 'proof' in this way, the plugin can add some LF-specific language support, in particular, it can generate appropriate default notations.
......
Markdown is supported
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