Commit 6c2eedb4 authored by Florian Rabe's avatar Florian Rabe

no message

parent 1e63144c
namespace http://cds.omdoc.org/examples
// A representation of homotopy type theory (HOTT) in MMT instantiated with LF-modulo.
This is a Martin-Löf-style type theory with the univalence axiom.
Simplification rules are used to offset artefacts produced by the representation.
The representation follows the HOTT book (The Univalent Foundations Program, Institute for Advanced Study, Princeton, April 2013).
theory HOTT : http://cds.omdoc.org/urtheories?LF =
// The levels of the universe hierarchy (essentially the natural numbers). 
level : type 
first : level 
next : level → level 
// The syntactic categories: LF-types for the HOTT types and terms at each level. 
// tp L represents the types at level L. 
tp : level → type 
// univ L is the universe containing the types at level L. 
univ : {L} tp (next L) 
// if A:tp L, then tm A represents the terms of type A 
tm : {L} tp L → type  # tm 2 prec -5
// Equality judgments for types (at the same level) and terms (of the same type).
These are registered as equality judgements by "role Eq", which permits registering equality rules later. 
tp_equal : {L} tp L → tp L → type  role Eq
equal : {L, A:tp L} tm A → tm A → type  # 3 ≡ 4  role Eq
// The above encoding is not quite adequate
(a) the cumulativity of the type hierarchy is not represented
(b) the fact that every type at level L is also a term of type univ L is not captured. 
// Up and up take care of (a): they move types and terms up in the hierarchy. 
Up : {L} tp L → tp (next L)  # Up 2
up : {L,A:tp L} tm A → tm (Up A)  # up 3
// shift and unshift take care of (b): they convert between types and terms. 
shift : {L} tp L → tm (univ L)  # shift 2
unshift : {L} tm (univ L) → tp L  # unshift 2
// Two equality axioms that make shift and unshift bijections.
By registering them as simplification rules, the type checker becomes aware of the bijection. 
shift_unshift : {L,A: tp L} tp_equal L (unshift (shift A)) A  role Simplify
unshift_shift : {L,A: tm univ L} (shift (unshift A)) ≡ A  role Simplify
// The usual rules for equality. Some rules are omitted (congruence and equality of types) 
refl : {L, A:tp L, X:tm A} X ≡ X  # %%prefix 2 1
sym : {L, A:tp L, X:tm A, Y: tm A} X ≡ Y → Y ≡ X  # %%prefix 4 1
trans : {L, A:tp L, X:tm A, Y: tm A, Z: tm A} X ≡ Y → Y ≡ Z → X ≡ Z  # %%prefix 5 2
// The development of HOTT type theory is now straightforward.
The following follows A.2 in the HOTT book.
Only the constructors and rules needed to state the univalence axiom are given.
Pi : {L, A:tp L} (tm A → tp L) → tp L  # Π 3 
lambda : {L, A:tp L, B: tm A → tp L} ({x:tm A} tm (B x)) → tm Π [x] B x  # λ 4 
apply : {L, A:tp L, B: tm A → tp L} tm (Π [x: tm A] B x) → {x} tm (B x)  # 4 @ 5 prec 10 
arrow : {L} tp L → tp L → tp L 
= [L,A,B] Π [x: tm A] B 
# 2 ⇒ 3 prec 3
id : {L, A: tp L} tm A ⇒ A 
= [L,A] λ [x] x 
# id 2 prec 10
comp : {L, A: tp L, B: tp L, C: tp L} tm A ⇒ B → tm B ⇒ C → tm A ⇒ C 
= [L,A,B,C] [f,g] λ [x:tm A] g @ (f @ x) 
# 6 ∘ 5 prec 10
// Registering beta as a simplification rule has the effect that computation in HOTT is automated by MMT. 
beta : {L, A: tp L, B: tm A → tp L, F: {x: tm A} tm (B x), X: tm A} (λ F) @ X ≡ (F X) 
# %%prefix 5 0  role Simplify
eta : {L, A:tp L, B: tm A → tp L, F: tm (Π [x: tm A] B x)} F ≡ λ [x: tm A] F @ x 
# %%prefix 4 0
Sigma : {L, A:tp L} (tm A → tp L) → tp L  # Σ 3 
pair : {L, A:tp L, B: tm A → tp L} {x:tm A} tm (B x) → tm Σ [x] B x  # pair 4 5
pi1 : {L, A:tp L, B: tm A → tp L} tm (Σ [x: tm A] B x) → tm A  # pi1 4 
pi2 : {L, A:tp L, B: tm A → tp L} {u:tm (Σ [x: tm A] B x)} tm (B (pi1 u))  # pi2 4 
prod : {L} tp L → tp L → tp L 
= [L,A,B] Σ [x: tm A] B 
# 2 × 3 prec 3
conv_pair : {L, A: tp L, B: tm A → tp L, u: tm Σ [x] B x} u ≡ pair (pi1 u) (pi2 u) 
# %%prefix 4 0
// conv_pi1 and conv_pi2 are registered as simplification rules in the same way as beta. 
conv_pi1 : {L, A: tp L, B: tm A → tp L, X: tm A, Y: tm (B X)} pi1 (pair L A B X Y) ≡ X 
// We have to give the implicit arguments of pair here to aid type reconstruction.
(A better solution might be Twelf's abstraction behavior that adds the {B} binder.)
# %%prefix 5 0  role Simplify 
// Note that conv_pi2 only type-checks because conv_pi1 is used as a simplification rule. 
conv_pi2 : {L, A: tp L, B: tm A → tp L, X: tm A, Y: tm (B X)} pi2 (pair L A B X Y) ≡ Y 
# %%prefix 5 0  role Simplify
// We omit the type constructors +, empty, unit, and nat. 
ident : {L, A:tp L} tm A → tm A → tp L  # 3 = 4 prec 7
idrefl : {L, A:tp L, x:tm A, y: tm A} x ≡ y → tm x = y  # idrefl 5 
// The assumption x ≡ y is omitted in the HOTT book - derivable from congruence?
idelim : {L, A: tp L}
{C: {x: tm A, y: tm A, p: tm x = y} tp L}
{c: {z: tm A} tm (C z z (idrefl (refl z)))}
{a: tm A} {b: tm A} {p: tm a = b}
tm (C a b p) 
# idelim 3 4 5 6 7 
idcomp : {L, A: tp L}
{C: {x: tm A, y: tm A, p: tm x = y} tp L}
{c: {z: tm A} tm (C z z (idrefl (refl z)))}
{a: tm A}
tm (idelim C c a a (idrefl (refl a))) = (c a) 
// An abbreviation for the identity type of two types (which requires converting the types to terms first). 
tident : {L, A:tp L, B: tp L} tp (next L) 
= [L,A,B] (shift A) = (shift B) 
# 2 == 3 prec 5
// Now the definitions of homotopy that lead to the univalence axiom. 
// Definition 2.4.1 
homotopy : {L, A: tp L, B} tm A ⇒ B → tm A ⇒ B → tp L
= [L,A,B,f,g] Π [x: tm A] f @ x = g @ x 
# 4 ∼ 5 prec 5
// 2.4.10
isequiv : {L, A: tp L, B: tp L} tm A ⇒ B → tp L 
= [L,A,B,f] (Σ [g: tm B ⇒ A] f ∘ g ∼ id B) × (Σ [h: tm B ⇒ A] h ∘ f ∼ id A) 
# isequiv 4
// 2.4.11
equivalence : {L} tp L → tp L → tp L 
= [L,A,B] Σ [f: tm A ⇒ B] isequiv f 
# 2 ≃ 3 prec 5
// We will need the reflexivity of homotopy below. 
// Note that without beta as a simplification rule, this proof would have to use a complex subterm
instead of (refl x).
≃_refl_aux : {L, A: tp L} tm (id A) ∘ (id A) ∼ (id A) 
= [L,A] λ [x: tm A] idrefl (refl x)
≃_refl : {L, A: tp L} tm A ≃ A 
= [L,A] pair (id A) (pair
(pair (id A) (≃_refl_aux L A))
(pair (id A) (≃_refl_aux L A))
)
// Lemma 2.10.1 
// This only type-checks because unshift_shift is used as a simplification rule. 
idtoeqv : {L, A: tp L, B: tp L} tm A == B ⇒ (Up (A ≃ B)) 
= [L,A,B] λ [P] idelim
([a: tm univ L, b: tm univ L, p: tm a = b] Up ((unshift a) ≃ (unshift b)))
([z: tm univ L] up (≃_refl L (unshift z)))
(shift A) (shift B) P

// Axiom 2.10.3 (univalence) 
// Intuitively, this says (A == B) ≃ (A ≃ B) 
univalence : {L,A: tp L, B} tm (isequiv (idtoeqv L A B)) 
// This is a consequence of univalence; proof to be added. 
≃_cong : {L, M, P: tp L → tp M, A: tp L, B: tp L} tm (A ≃ B) → tm ((P A) ≃ (P B)) 

\ No newline at end of file
namespace http://cds.omdoc.org/examples
// theory ObjectLevelInstances : http://cds.omdoc.org/urtheories?LF =
tp : type
tm : type
equal : tm → tm → tm # 1 = 2
of : tm → tp → type# 1 # 2
const : tp → THY = [a] {|
c : tm,
of : c # a
|}
nat : tp
zero : const nat
// alsozero : const nat = [|c : zero/c, of : zero/of|]

// theory MetaLevelInstances : http://cds.omdoc.org/urtheories?LF =
tp : type
tm : type
equal : tm → tm → tm # 1 = 2
of : tm → tp → type# 1 # 2
theory const > {|a: tp|} =
c : tm
of : c # a

// nat : tp
// structure zero : const nat
// alsozero : const nat = [|c : zero/c, of : zero/of|]

namespace http://cds.omdoc.org/examples
theory Int : http://cds.omdoc.org/urtheories?LF =
include ?Nat
int : type = nat
pred : nat → nat  # pred 1 prec 20
uminus: nat → nat  # - 1 prec 20 
minus : nat → nat → nat  # 1 - 2 prec 10 

theory IntRules : http://cds.omdoc.org/urtheories?LF =
include ?Int 
include ?NatRules
times_mono : {X:nat,Y:nat,Z:nat} ⊦ O ≤ Z → ⊦ X ≤ Y → ⊦ X * Z ≤ Y * Z
times_invmono : {X,Y,Z} ⊦ O ≤ Z → ⊦ X * Z ≤ Y * Z → ⊦ X ≤ Y 
succ_invert : {X} ⊦ pred (X') = X role Simplify
plus_invert_R : {X,Y} ⊦ (X + Y) - Y = X role Simplify
plus_invert_L : {X,Y} ⊦ (X + Y) - X = Y role Simplify

// theory IntRuleTest : http://cds.omdoc.org/urtheories?LF =
include ?IntRules
j : nat → type

namespace http://cds.omdoc.org/examples
import real scala://real.omdoc.org/
theory NatLiterals : http://cds.omdoc.org/urtheories?LF =
include ?NatRules
include real:?Bool
include real:?StandardNat
// this only type-checks because ⊦ 1+1 = 2 unifies with ⊦ true 
test : ⊦ 1+1 = 2 = trueI

theory IntLiterals : http://cds.omdoc.org/urtheories?LF =
include ?IntRules // this should include NatRules, but the last test only works with the rule IntRules?succ_invert/Solve
include real:?Bool
include real:?StandardInt
test : ⊦ 1-3 = -2  = trueI

theory Vectors : http://cds.omdoc.org/urtheories?LF =
include ?NatLiterals
a : type
c : a
a_equal : a → a → type # 1 = 2 role Eq
vec : nat → type  # vec 1 prec 5
empty : vec 0  # ∅ 
cons : {n} vec n → a → vec n'  # 2 , 3
vec_equal : {n} vec n → vec n → type # 2 == 3role Eq
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
// 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
last : {n} vec n' → a  # last 2
lastcons : {n, x, v: vec n} last (v,x) = x role Simplify
// this only type-checks because vec 3 and vec 0''' are recognized as equal 
test1 : vec 3  = ∅,c,c,c
// this only type-checks because vec 6 and vec (3+3) are recognized as equal 
test2 : vec 6  = test1 @ test1 
// this only type-checks because vec n' unifies with vec 3
test3 : a = last test1

\ No newline at end of file
namespace http://cds.omdoc.org/examples 
theory Algebra : http://cds.omdoc.org/mmt?Combinators =
// include http://cds.omdoc.org/mmt?ModExp
// include http://cds.omdoc.org/mmt?Combinators
// include ?FOLEQ 
include http://cds.omdoc.org/mmt?mmt 
theory Empty : ?FOLEQ = 
theory Carrier abbrev Empty EXTEND { U := term }  
theory Magma abbrev Carrier EXTEND { op : U → U → U }  
theory Pointed abbrev Carrier EXTEND { e : U }  
theory PointedMagma abbrev Magma AND Pointed  
theory LeftUnital abbrev PointedMagma EXTEND { leftIdentity : ded ∀ [x : U] op e x ≐ x }  
view Flip : ?Algebra/Magma → ?Algebra/Magma =
U = U 
op = [a,b] op b a

theory RightUnital abbrev (LeftUnital VIA Flip) RENAME { rightIdentity := leftIdentity }  
theory Unital abbrev LeftUnital AND RightUnital  

\ No newline at end of file
namespace http://cds.omdoc.org/examples
theory Bool : http://cds.omdoc.org/urtheories?LF =
bool : type
true : bool
false : bool

theory Logic : http://cds.omdoc.org/urtheories?LF =
include ?Bool
ded : bool → type # ⊦ 1 prec -5  role Judgment
trueI : ⊦ true

theory Nat : http://cds.omdoc.org/urtheories?LF =
nat : type
zero : nat  # O 
succ : nat → nat  # 1 ' prec 20
one : nat 
= zero'  # I 
plus : nat → nat → nat  # 1 + 2 prec 10 
times : nat → nat → nat  # 1 * 2 prec 15 
include ?Bool
equal : nat → nat → bool  # 1 = 2 prec 5role Eq
leq : nat → nat → bool  # 1 ≤ 2 prec 5

theory NatRules : http://cds.omdoc.org/urtheories?LF =
include ?Logic
include ?Nat 
refl : {X} ⊦ X = X 
sym : {X,Y} ⊦ X = Y → ⊦ Y = X 
trans : {X,Y,Z} ⊦ X = Y → ⊦ Y = Z → ⊦ X = Z 
eq_leq : {X,Y,Z} ⊦ X = Y → ⊦ Y ≤ Z → ⊦ X ≤ Z 
leq_eq : {X,Y,Z} ⊦ X ≤ Y → ⊦ Y = Z → ⊦ X ≤ Z 
plus_comm : {X,Y} ⊦ X + Y = Y + X 
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_succ_R : {X,Y} ⊦ X + Y' = (X+Y)'role Simplify 
plus_succ_L : {X,Y} ⊦ X' + Y = (X+Y)'role Simplify 
times_comm : {X,Y} ⊦ X * Y = Y * X 
times_assoc : {X,Y,Z} ⊦ (X * Y) * Z = X * (Y * Z) 
times_neut : {X} ⊦ X * I = Xrole Simplify 
times_zero : {X} ⊦ X * O = Orole Simplify 
times_succ_R : {X,Y} ⊦ X * Y' = (X*Y) + Xrole Simplify 
times_succ_L : {X,Y} ⊦ X' * Y = (X*Y) + Xrole Simplify 
distrib : {X,Y,Z} ⊦ X * (Y + Z) = X * Y + X * Zrole Simplify
leq_refl : {X} ⊦ X≤X 
leq_trans : {X,Y,Z} ⊦ X≤Y → ⊦ Y≤Z → ⊦ X≤Z 
leq_antisym : {X,Y} ⊦ X≤Y → ⊦ Y≤X → ⊦ X=Y 
plus_mono : {X,Y,Z} ⊦ X≤Y → ⊦ X+Z ≤ Y+Z 
plus_mono_L : {X,Y,Z} ⊦ X≤Y → ⊦ Z+X ≤ Z+Y 
= [X,Y,Z,p] leq_eq (eq_leq plus_comm (plus_mono p)) plus_comm
plus_invmono : {X,Y,Z} ⊦ X+Z≤Y+Z → ⊦ X≤Y 
theory NatOnly : http://cds.omdoc.org/urtheories?LF =
least : {X} ⊦ O ≤ X 
plus_larger_L : {X,Y} ⊦ X≤X+Y 
= [X][Y] eq_leq (sym plus_neut) (plus_mono_L least) 
plus_larger_R : {X,Y} ⊦ Y≤X+Y 
= [X][Y] leq_eq plus_larger_L plus_comm
times_mono : {X,Y,Z} ⊦ X ≤ Y → ⊦ X * Z ≤ Y * Z 
times_invmono : {X,Y,Z} ⊦ X * Z ≤ Y * Z → ⊦ X ≤ Y 


theory NatMinus : http://cds.omdoc.org/urtheories?LF =
include ?NatRules 
include ?NatRules/NatOnly
// A partial subtraction operation that takes a proof of definedness as a 3rd arguments. 
minus : {X,Y} ⊦ Y≤X → nat  # 1 - 2 ! 3 prec 15  ## 1 - 2 %I3
minus_pi : {X,Y,P,Q} ⊦ X-Y!P = X-Y!Q 
minus_intro_L : {X,Y,Z} {p: ⊦ X+Y=Z} ⊦ Z-Y!(leq_eq plus_larger_R p) = X 
minus_intro_R : {X,Y,Z} {p: ⊦ X+Y=Z} ⊦ Z-X!(leq_eq plus_larger_L p) = Y 
= [X,Y,Z] [p] trans minus_pi (minus_intro_L (trans plus_comm p))
minus_elim : {X,Y,Z,P} ⊦ Z-Y!P = X → ⊦ X+Y = Z 
minus_inverse : {X} ⊦ X-X!leq_refl = O 
= [X] trans minus_pi (minus_intro_R (plus_neut_Ex X)) 
// minus_neut : {X} ⊦ X-O!least = X 
= [X] trans minus_pi (minus_intro_L (plus_neut_Ex X)) 
// also provable: associativity +- (maybe X-(Y+Z)=(X-Y)-Z must be axiom) and distributivity *- 

\ No newline at end of file
namespace http://cds.omdoc.org/examples
theory FOLPatterns : ur:?LFS =
include ?FOL
pattern fun(n:NAT)# L1 : 2 =
f: term^n → term


theory Monoid : ?FOLPatterns =
fun comp : 2

namespace http://cds.omdoc.org/examples
import real scala://real.omdoc.org/
import rules scala://mmt.kwarc.info
// A first test case for writing imperative programs as MMT theories. 
theory ProgLang : http://cds.omdoc.org/urtheories?CF =
include real:?Bool
include ?NatRules
include real:?StandardNat
print : {a: type} a → None # print 2
rule rules/cf?Print

theory Counter : ?ProgLang =
counter: nat= 0
add: nat → None= [n] counter = counter + n

theory Program : ?ProgLang =
main = print 1
// This one is still experimental.
// main2 =
var c = new examples?Counter in
c.add 3;
print c.add


namespace http://cds.omdoc.org/physics
import latin http://latin.omdoc.org/
import mitm http://mathhub.info/MitM/Foundation 
theory Quantities : ur:?LF =
// real numbers (should be imported from elsewhere) 
include mitm:?Literals 
real : type = real_lit
// include scala://models.latin.omdoc.org/?RationalArithmetic
// the type of dimensions, e.g., time, length 
dim : type
scalar: dim
mult_dim : dim → dim → dim # 1 * 2
inv_dim : dim → dim # 1 ⁻ prec 10
div_dim : dim → dim → dim = [d,e] d*e⁻ # 1 / 2
square_dim : dim → dim= [d] d*d # 1 ² prec 10
cube_dim : dim → dim= [d] d*d*d # 1 ³ prec 10
eq_dim : dim → dim → type # 1 = 2 prec -10role Eq
assoc : {d:dim,e:dim,f:dim} d*(e*f)=(d*e)*f
comm : {d:dim,e:dim} d*e=e*d
mult_scalar_right : {d} d*scalar = d role Simplify
mult_scalar_left : {d} scalar*d = d role Simplify
mult_inv_right : {d:dim} d*d⁻ = scalar role Simplify
mult_inv_left : {d:dim} d⁻*d = scalar role Simplify
inv_mult : {d:dim,e:dim} (d*e)⁻ = d⁻*e⁻ role Simplify
inv_inv : {d} d⁻⁻ = d role Simplify
// the type of quantities of a certain dimension, e.g., 10 s, 100 m 
quantity : dim → type# $ 1
eq_quant : {d} $d → $d → type # 2 == 3 prec -10role Eq
// the type of units of a dimension, e.g., second, meter
units are functions that map real numbers to quantities 
unit : dim → type = [d] real → $d
// takes a real number and a unit and makes the quantity
e.g., 10'meter
makeQuantity : {d} real → unit d → $ d = [d,r,u] u r# 2 ' 3 prec 50
// addition and subtraction quantities 
add_quant : {d} $d → $d → $d # 2 ++ 3
sub_quant : {d} $d → $d → $d # 2 -- 3
add_quant_same_unit : {d,u: unit d, p, q} p'u ++ q'u == (plus_real_lit p q)'u // role Simplify
sub_quant_same_unit : {d,u: unit d, p, q} p'u -- q'u == (plus_real_lit p (minus_real_lit q))'u // role Simplify
// multiplication and division of dimensions, quantities, and units (should be imported from elsewhere) 
mult_quant : {d,e} $d → $e → $(d * e) # 3 ** 4
div_quant : {d,e} $d → $e → $(d / e) # 3 // 4
mult_unit : {d,e} unit d → unit e → unit(d * e) # 3 ** 4
= [d,e,u,v] [r] (r'u) ** (r'v)
div_unit : {d,e} unit d → unit e → unit(d / e) # 3 // 4
= [d,e,u,v] [r] (r'u) // (r'v)
mult_scalar : {d} real → $ d → $ d# 2 @ 3
multiples_of: {d} $ d → unit d = [d,q] [r] r @ q# multiples_of 2

theory Dimensions : ur:?LF =
include ?Quantities
length : dim
time : dim
mass : dim
temperature : dim
area : dim= length ²
volume : dim = length ³
velocity : dim= length / time
acceleration : dim = length * time⁻²
force : dim= mass * acceleration
pressure : dim= force * length⁻²

theory Prefixes : ur:?LF =
include ?Dimensions
// TODO 
milli : {d} unit d → unit d // = [d,u] [r] (r / 1000) ' u# milli 2
centi : {d} unit d → unit d // = [d,u] [r] (r / 100) ' u# centi 2
deci : {d} unit d → unit d // = [d,u] [r] (r / 10) ' u# deci 2

theory Units : ur:?LF =
include ?Dimensions
meter : $ length
second : $ time
gramm : $ mass
meters : unit length = multiples_of meter
seconds : unit time = multiples_of second
gramms : unit mass = multiples_of gramm
kelvin : $temperature
kelvins : unit temperature = multiples_of kelvin

theory DerivedUnits : ur:?LF =
include ?Prefixes
include ?Units
litre : $ volume // = (1 ' deci meters) ** (1 ' deci meters) ** (1 ' deci meters)
litres : unit volume = multiples_of litre

theory CookingUnit : ur:?LF =
include ?DerivedUnits
tablespoon : $ volume
teaspoon : $ volume
cup : $ volume
tablespoons : unit volume = multiples_of (15 ' milli litres)
teaspoons : unit volume = multiples_of (5 ' milli litres)
cups : unit volume = multiples_of (250 ' milli litres)

theory TimeUnits : ur:?LF =
include ?Units
minutes : unit time = multiples_of (60 ' seconds)
hours : unit time = multiples_of (60 ' minutes)

theory TemperatureUnits : ur:?LF =
include ?Units
celsius : unit temperature // = [r] (r+273+(15/100)) ' kelvins  # 1 °C
fahrenheit : unit temperature // = [r] (r-32)*5/9 °C  # 1 °F

namespace http://cds.omdoc.org/examples
// a simple language for set theory
This primarily exemplifies advanced notations for parsing and presentation. 
theory Sets : http://cds.omdoc.org/urtheories?LF =
set : type
prop : type
in : set → set → prop # 1 ‍∈ 2 prec 75
equal : set → set → prop
// No printable characters are reserved. Here = is used as a delimiter.  # 1 = 2 prec 50
ded : prop → type  # ded 1 prec 0
// Elem A yields a for elements of the set A.
Its notation is chosen such that variable attributions can be parsed and presented as x ‍∈ A instead of x : Elem A.
Elem : set → type # ∈ 1 prec 70
// The following declaration lifts equal to the types Elem A.
For parsing (#) it needs a different notation (==); for presentation (##) we can reuse =.
elemequal : {A} Elem A → Elem A → prop  # 2 == 3 prec 50 
// This notation for presentation is 2-dimensional: _ yields a subscript and %I marks an implicit (hidable) argument. 
## 2 = _ %I1 3 prec 50
// A universal quantifier over all elements of a given set.
Using Elem A, the relativization can be expressed in the type system.
forall : {A} (Elem A → prop) → prop 
// The notation uses V2T for an attributed variable (x ‍∈ A) and -3 for the scope.
Thus, forall is a binder as far as the MMT notation system is concerned.
The type system considers it as a higher-order constant of LF. The LF plugin for MMT configures the conversion between the two. 
# ∀ V2T . -3 prec -1
empty : set  # ∅ 
// Several set operators use {}-based notations and are binders.
MMT can handle that.
However, we have to use ; instead of : for replacement because the delimiter scheme { : } is already used for the Pi symbol of LF.
Because the notations are left- and right-closed, we can give them very low precedences, which has the effect that they act like brackets.
compr : {A} (Elem A → prop) → set  # { V2T | -3 } prec -100004
repl : {A}{B} (Elem A → Elem B) → set  # { -4 ; V3T } prec -100006
union : set → set → set # 1 ∪ 2 prec 120
inter : set → set → set # 1 ∩ 2 prec 120
// The big operators for union and intersection are binders with 2-dimensional notations.
In the __ produces underscripts.
bigunion : {A} (Elem A → set) → set # ⋃ V2T . -3 prec 60  ## ⋃ __ V2T -3 prec 5
biginter : {A} (Elem A → set) → set # ⋂ V2T . -3 prec 60  ## ⋂ __ V2T -3 prec 5
fun : set → set → set # 1 ⇒ 2 prec 120 // ^ produces superscripts.  ## 2 ^ 1 
lam : {A}{B} (Elem A → Elem B) → Elem (fun A B)  # λ 3
app : {A}{B} Elem (fun A B) → Elem A → Elem B  # 3 @ 4 prec 120
prod : set → set → set # 1 × 2 prec 120
pair : {A}{B} Elem A → Elem B → Elem (A × B)
// We can use () in notations as well. But the precedence has to below the precedence of the built-in notation for bracketed expressions. 
# ( 3 , 4 ) prec -1000000001
// The two projection use, e.g., ._1 for parsing and subscripts for presentation. %D1 yields 1 as a delimiter (instead of an argument marker). 
pi1 : {A}{B} Elem (A × B) → Elem A # 3 ._1 prec 200  ## 3 _ %D1 prec 200
pi2 : {A}{B} Elem (A × B) → Elem B # 3 ._2 prec 201  ## 3 _ %D2 prec 200
cardinality : set → set  # | 1 | prec -100000
// Some example expressions that use the notations. 
distributive : {A}{F: Elem A → set} ded A ∩ ⋃ x ∈ A. (F x) = ⋃ x. A ∩ (F x)
pairs : {A} ded {x ∈ A × A | x._1 == x._2} = {(x,x) ; x ∈ A} 
sizes : {A} (ded |{f∈A⇒A|∀x∈A.f@x==x}|=|∅⇒∅|)

\ No newline at end of file
namespace http://cds.omdoc.org/examples
// polymorphic equality (essentially identity types) 
theory Equality : http://cds.omdoc.org/urtheories?PLF =
equal : {a:type} a → a → type# 2 = 3 prec 50
refl : {a,x:a} x = x # refl 2
cong : {a,b,x,y} x = y → {f: a → b} (f x) = (f y)# cong 5 6
cast : {a: type, A: a → type, x:a, y:a} x = y → A x → A y
sym : {a,x:a,y} x = y → y = x
= [a,x,y][p] cast a ([u] u = x) x y p (refl x)
trans : {a,x:a,y,z} x = y → y = z → x = z
= [a,x,y,z,p,q] cast a ([u] x = u) y z q p

// polymorphic lists 
theory Lists : http://cds.omdoc.org/urtheories?PLF =
include ?Equality
list : type → type
nil : {a} list a # nil %I1
cons : {a} a → list a → list a # 2 , 3 prec 75
append : {a} list a → list a → list a # 2 + 3 prec 75
append_nil : {a, m: list a} nil + m = m
append_cons : {a, x: a, l: list a, m: list a} (x, l) + m = x , (l + m)

\ No newline at end of file
namespace http://cds.omdoc.org/examples
theory DepSumChurch : http://cds.omdoc.org/urtheories?LF =
tp : type 
tm : tp → type  # tm 1 prec -5
equal : {A} tm A → tm A → type  # 2 = 3  role Eq
Sigma : {A} (tm A → tp) → tp  # Σ 2 
pair : {A, B: tm A → tp} {x} tm (B x) → tm Σ [x] B x  # pair 3 4
pi1 : {A, B: tm A → tp} tm (Σ [x] B x) → tm A  # pi1 3 
pi2 : {A, B: tm A → tp} {u:tm (Σ [x] B x)} tm (B (pi1 u))  # pi2 3 
prod : tp → tp → tp 
= [A,B] Σ [x: tm A] B 
# 1 × 2 prec 3
conv_pair : {A, B: tm A → tp, u: tm Σ [x] B x} u = pair (pi1 u) (pi2 u) 
conv_pi1 : {A, B: tm A → tp, X, Y: tm (B X)} pi1 (pair A B X Y) = X  role Simplify 
// Note that conv_pi2 only type-checks because conv_pi1 is used as a simplification rule. 
conv_pi2 : {A, B: tm A → tp, X, Y: tm (B X)} pi2 (pair A B X Y) = Y  role Simplify

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