Commit efceb74e authored by Dennis Müller's avatar Dennis Müller

merge

parents 148068d9 7393fa06
......@@ -90,7 +90,7 @@ define temp
end
define temp2
server on 8081
server on 8080
log+ server
log+ debug
//log+ object-checker
......@@ -98,20 +98,22 @@ define temp2
//log+ structure-simplifier
//log+ structure-checker
//log+ object-parser
build MMT/urtheories mmt-omdoc
build MMT/urtheories mmt-omdoc module-expressions.mmt
end
define MMTTest
server on 8081
log+ server
log+ debug
log+ object-checker
//log+ object-simplifier
//log+ structure-simplifier
//log+ structure-parser
//log+ structure-checker
//log+ structure-simplifier
//log+ object-parser
log+ object-checker
//log+ object-simplifier
//build MMT/examples mmt-omdoc
mathpath archive ../../Test
mathpath archive ../LFX
build Test/General mmt-omdoc
mathpath archive ../../MitM
build Test/General mmt-omdoc views.mmt
end
\ No newline at end of file
namespace http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final
theory Types : ur:?LF =
tp : type
tm : tp → type # tm 1 prec -1

theory Logic : ur:?LF =
prop: type
ded : prop → type# ⊦ 1 prec -1role Judgment

theory Equality : ur:?LF =
include ?Types
include ?Logic
equal : {A} tm A → tm A → prop# 2 = 3
refl : {A,X:tm A} ⊦ X = X
sym : {A,X,Y:tm A} ⊦ X = Y → ⊦ Y = X
trans : {A,X,Y,Z:tm A} ⊦ X = Y → ⊦ Y = Z → ⊦ X = Z
cong : {A,B,X,Y,F:tm A → tm B} ⊦ X = Y → ⊦ (F X) = (F Y)

theory STT : ur:?LF =
include ?Equality
fun : tp → tp → tp# 1 ⇒ 2
abstract : {A,B} (tm A → tm B) → tm (A ⇒ B)# λ 3
apply : {A,B} tm (A ⇒ B) → tm A → tm B# 3 @ 4 prec 5
beta : {A,B,F: tm A → tm B,X} ⊦ (λ F) @ X = (F X)

theory Eta : ur:?LF =
include ?STT
eta : {A,B,F: tm (A ⇒ B)} ⊦ (λ [x: tm A] (F @ x)) = F

theory Extensionality : ur:?LF =
include ?STT
ext : {A,B,F,G: tm (A ⇒ B)} ({x: tm A} ⊦ F @ x = G @ x) → ⊦ F = G# ext 5

// view EtaExt : ?Eta -> ?Extensionality =
// include mmtid ?STT
eta = [A,B,F] ext [x] beta

theory List : ?STT =
list : tp → tp# < 1 >
nilOf : {A: tp} tm <A># nil %I1
cons : {A: tp} tm A → tm <A> → tm <A># 2 + 3 prec 10
fold : {A,B} tm B → (tm A → tm B → tm B) → tm <A> → tm B
fold_nil : {A,B,N,C} ⊦ fold A B N C nil = N
fold_cons : {A,B,N,C,X,L} ⊦ fold A B N C (X+L) = C X (fold A B N C L)
map : {A,B} tm (A ⇒ B) → tm <A> → tm <B>= [A,B,f] fold A <B> nil ([a,bs] (f@a)+bs)# map 3 4
append : {A} tm <A> → tm <A> ⇒ <A>= [A] fold A (<A> ⇒ <A>) (λ[x]x) ([a,f] λ[l]a+(f@l))
flatten: {A} tm < <A> > → tm <A>= [A] fold <A> <A> nil ([l,r] (append A l) @ r)

theory Monad : ?STT =
operator: tp → tp# M 1 prec 20
unit : {A} tm A → tm M A# return 2
bind : {A,B} tm M A → tm (A ⇒ M B) → tm M B# 3 > 4 prec 5
neutral_left : {A,B,F: tm (A ⇒ M B)}{X: tm A} ⊦ (return X) > F = F @ X
neutral_right : {A,m: tm M A} ⊦ m > (λ [x] return x) = m
assoc: {A,B,C, F: tm (A ⇒ M B), G: tm (B ⇒ M C),m: tm M A} ⊦ (m > F) > G = m > (λ[x]F @ x > G)

view ListMonad : ?Monad -> ?List =
operator = list
unit = [A] [x] x+nil
bind = [A,B][l,f] (flatten B) (map f l)
// neutral_left = ...
// neutral_right = ...
// assoc = ...

theory MonadPlus : ?STT =
include ?Monad
// more stuff here

namespace http://cds.omdoc.org/examples
// binary arithmetic 
theory Binary : http://cds.omdoc.org/urtheories?LF =
num : type
// the number 0
zero : num # b
// double, i.e., append the digit 0
db: num → num # 1 ₀ prec 10
// double and increment, i.e., append the digit 1
dbI: num → num # 1 ₁ prec 10
equal : num → num → type# 1 = 2 prec 0 role Eq
refl : {n} n = n# refl %I1
// successor and its rules
succ: num → num# 1 ' prec 5
succ_zero: b ' = b ₁  role Simplify
succ_db: {n} n ₀ ' = n ₁ ₁  role Simplify
succ_dbI: {n} n ₁ ' = n'₀ role Simplify
test : b₁₁' = b₁₀₀ = refl
// addition and its rules
plus: num → num → num# 1 + 2 prec 3
plus_zero_right: {n} n + b = n  role Simplify
plus_zero_left: {n} b + n = n  role Simplify
// these rules cannot be picked up by the SimplificationRuleGenerator yet
plus_db_db: {m,n} m ₀ + n ₀ = (m + n) ₀  // role Simplify
plus_db_dbI: {m,n} m ₀ + n ₁ = (m + n) ₁  // role Simplify
plus_dbI_db: {m,n} m ₁ + n ₀ = (m + n) ₁  // role Simplify
plus_dbI_dbI: {m,n} m ₁ + n ₁ = ((m + n) ')₀ // role Simplify

\ No newline at end of file
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
......@@ -18,7 +18,7 @@ theory FOLNatDed : http://cds.omdoc.org/urtheories?LF =
existsI : {A} {c} ⊦ (A c) ⟶ ⊦ ∃ [x] (A x) ❘# existsI 2 3❙
existsE : {A,C} ⊦ (∃ [x] A x) ⟶ ({x} ⊦ (A x) ⟶ ⊦ C) ⟶ ⊦ C❙
theory FOLEQ : http://cds.omdoc.org/urtheories?LF =
include ?FOL❙
equal : term ⟶ term ⟶ prop❘# 1 ≐ 2 prec 30❙
......
namespace http://cds.omdoc.org/examples
// intuitionistic first-order logic with natural deduction rules and a few example proofs 
theory FOL : http://cds.omdoc.org/urtheories?LF =
include ?PL
term : type
forall : (term → prop) → prop# ∀ 1 ## ∀ V1 2
exists : (term → prop) → prop# ∃ 1 ## ∃ V1 2

theory FOLNatDed : http://cds.omdoc.org/urtheories?LF =
include ?FOL
include ?PLNatDed 
forallI : {A} ({x} ded (A x)) → ded ∀ A 
forallE : {A} ded (∀ A) → {x} ded (A x) role ForwardRule
existsI : {A} {c} ded (A c) → ded ∃ [x] (A x) # existsI 2 3
existsE : {A,C} ded (∃ [x] A x) → ({x} ded (A x) → ded C) → ded C

theory FOLEQ : http://cds.omdoc.org/urtheories?LF =
include ?FOL
equal : term → term → prop# 1 ≐ 2 prec 30

theory FOLEQNatDed : http://cds.omdoc.org/urtheories?LF =
include ?FOLEQ
include ?FOLNatDed 
refl : {x} ded x ≐ x
congT : {T}{x,y} ded x ≐ y → ded (T x) ≐ (T y)
congF : {F}{x,y} ded x ≐ y → ded (F x) → ded (F y)
sym : {x,y} ded x ≐ y → ded y ≐ x
trans : {x,y,z} ded x ≐ y → ded y ≐ z → ded x ≐ z

\ No newline at end of file
namespace http://cds.omdoc.org/examples❚
/T
Intuitionistic propositional logic with natural uction rules and a few example proofs ❚
Intuitionistic propositional logic with natural deduction rules and a few example proofs ❚
/T
We start with the syntax of propositional logic.❚
......@@ -56,9 +56,8 @@ theory PLNatDed : http://cds.omdoc.org/urtheories?LF =
orIl : {A,B} ⊦ A ⟶ ⊦ A ∨ B ❙
orIr : {A,B} ⊦ B ⟶ ⊦ A ∨ B ❙
orE : {A,B,C} ⊦ A ∨ B ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C
orE : {A,B,C} ⊦ A ∨ B ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C❙
impI : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ A ⇒ B ❙
impE : {A,B} ⊦ A ⇒ B ⟶ ⊦ A ⟶ ⊦ B ❘ role ForwardRule❙
......
namespace http://cds.omdoc.org/examples
/T
Intuitionistic propositional logic with natural deduction rules and a few example proofs 
/T
We start with the syntax of propositional logic.
theory PL : http://cds.omdoc.org/urtheories?LF =
# :types The Basic Concepts
/T the type of propositions 
prop : type 
/T Given [F:prop], the type $ded F$ holds the proofs of $F$.
ded : prop → type  # ded 1 prec 0## ⊦ 1 prec 0role Judgment
## Abbreviations
/T The type $contra$ abbreviates the judgment of inconsistency.
If we can give an element of the type, then every proposition has a proof.
contra : type  = {a} ded a # ↯ 
# Constructors
/T The constructors provide the expressions of the types above.
true : prop 
and : prop → prop → prop  # 1 ∧ 2 prec 15
or : prop → prop → prop  # 1 ∨ 2 prec 15
impl : prop → prop → prop  # 1 ⇒ 2 prec 10
not : prop → prop  # ¬ 1 prec 20
/T Equivalence is taken as a non-primitive here and defined such that for [F:prop,G:prop] we define $F⇔G$ as $(F ⇒ G) ∧ (G ⇒ F)$.
equiv : prop → prop → prop  # 1 ⇔ 2 prec 10
= [x,y] (x ⇒ y) ∧ (y ⇒ x)

/T Now we describe the proof theory.
theory PLNatDed : http://cds.omdoc.org/urtheories?LF =
include ?PL 
/T We use natural deduction proof rules that construct expressions of type $ded F$ for some [F:prop].
{For example, assume two propositions [F: prop, G: prop].
{If [p:ded F, q: ded G], then $andI p q$ is a proof of $F∧G$.}
{If [p:ded F∧G], then $andEl p$ is a proof of $F$.}
}

trueI : ded true
andI : {A,B} ded A → ded B → ded A ∧ B 
andEl : {A,B} ded A ∧ B → ded A  role ForwardRule
andEr : {A,B} ded A ∧ B → ded B  role ForwardRule
orIl : {A,B} ded A → ded A ∨ B 
orIr : {A,B} ded B → ded A ∨ B 
orE : {A,B,C} ded A ∨ B → (ded A → ded C) → (ded B → ded C) → ded C

impI : {A,B} (ded A → ded B) → ded A ⇒ B 
impE : {A,B} ded A ⇒ B → ded A → ded B  role ForwardRule
notI : {A} (ded A → ↯) → ded ¬ A# notI 2
notE : {A} ded ¬ A → ded A → ↯ # notE 2 3 role ForwardRule
equivI : {A,B} (ded A → ded B) → (ded B → ded A) → ded A ⇔ B 
= [A,B,p,q] andI (impI [x] p x) (impI [x] q x) 
equivEl : {A,B} ded A ⇔ B → ded A → ded B  role ForwardRule
= [A,B,p,a] impE (andEl p) a 
equivEr : {A,B} ded A ⇔ B → ded B → ded A  role ForwardRule
= [A,B,p,b] impE (andEr p) b 
imp2I : {A,B,C} (ded A → (ded B → ded C)) → ded A ⇒ (B ⇒ C) 
= [A,B,C] [f] impI [p] (impI ([q] f p q)) 
imp2E : {A,B,C} ded A ⇒ (B ⇒ C) → ded A → ded B → ded C 
= [A,B,C] [p,q,r] impE (impE p q) r 
example : {A} ded A ⇒ (A ∧ A) 
= [A]impI [p]andI p p
interactive_example : {A} ded A ⇒ (A ∧ A)
= ≪{A} ded A⇒A∧A≫ 

\ No newline at end of file
namespace http://cds.omdoc.org/examples
theory ProverTest : http://cds.omdoc.org/urtheories?LF =
a: type
b: type
c: type
d: type
k: a
r: a → b role ForwardRule
s: a → b → c role ForwardRule
t: a → b → c → d
q: d → d
test : a → a → d  = [x,y] ≪d ≫

theory PLProofs : http://cds.omdoc.org/urtheories?LF =
include ?PLNatDed
/T this doesn't work currently 
// test : {a,b} ded (a ∧ b) ⇒ (b ∧ a) = _
// test2 : {a,b} ded (a ∨ b) ⇒ (b ∨ a) = _

theory FOLProofs : http://cds.omdoc.org/urtheories?LF =
include ?FOLNatDed
// test : {f} ded (forall [x] forall [y] f x y) ⇒ (forall [y] forall [x] f x y) = _
// test2 : {f} ded (exists [x] exists [y] f x y) ⇒ (exists [y] exists [x] f x y) = _

namespace http://cds.omdoc.org/examples
namespace http://cds.omdoc.org/examples 
theory Algebra : http://cds.omdoc.org/urtheories?LFComb =
theory Empty : ?FOLEQ = ❚
theory Carrier abbrev Empty EXTEND { U := term } ❘ ❙
theory Magma abbrev Carrier EXTEND { op : U ⟶ U ⟶ U # nt"1 op 2 prec 10"} ❘ ❙
theory Pointed abbrev Carrier EXTEND { e : U } ❘ ❙
theory PointedMagma abbrev Magma AND Pointed ❘ ❙
theory LeftUnital abbrev PointedMagma EXTEND { leftIdentity : ded ∀ [x : U] e op x ≐ x } ❘ ❙
......
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