Extensibella Example: mtc:arith

Language Specification

File: defs.sos

[Reduce File] [Raw File] 
Module mtc:arith

Builds on mtc:shared_declarations

e ::= ...
    | num(nat)
    | plus(e, e)

v ::= ...
    | numVal(nat)

ty ::= ...
     | natTy

nat ::= z | s(nat)
Projection nat :


--------------------- [T-Num]
typeOf G num(N) natTy


typeOf G E1 natTy
typeOf G E2 natTy
--------------------------- [T-Plus]
typeOf G plus(E1, E2) natTy



----------------------- [E-Num]
eval G num(N) numVal(N)


eval G E1 numVal(N1)
eval G E2 numVal(N2)
plusRel N1 N2 N
----------------------------- [E-Plus]
eval G plus(E1, E2) numVal(N)



Fixed Judgment plusRel : nat nat nat

============= [PR-Z]
plusRel z N N


plusRel N1 N2 N3
====================== [PR-S]
plusRel s(N1) N2 s(N3)



------------------------- [VT-NumVal]
valueType numVal(N) natTy



evalStep E1 E11
----------------------------------- [ES-Plus-Step1]
evalStep plus(E1, E2) plus(E11, E2)


value E1
evalStep E2 E21
----------------------------------- [ES-Plus-Step2]
evalStep plus(E1, E2) plus(E1, E21)


plusRel N1 N2 N
-------------------------------------- [ES-Plus-Add]
evalStep plus(num(N1), num(N2)) num(N)



------------ [V-Num]
value num(N)



----------------------- [S-Num]
subst X R num(N) num(N)


subst X R E1 E11
subst X R E2 E21
------------------------------------- [S-Plus]
subst X R plus(E1, E2) plus(E11, E21)



------------------ [C-NatTy]
canon natTy num(N)






--------------------- [Proj-Num]
|{e}- num(N) ~~> nilE


--------------------------- [Proj-Plus]
|{e}- plus(E1, E2) ~~> nilE


------------------------ [Proj-NumVal]
|{v}- numVal(N) ~~> nilV


---------------------- [Proj-NatTy]
|{ty}- natTy ~~> nilTy

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

Click on a command or tactic to see a detailed view of its use.

Module mtc:arith.

/*
  Sterling doesn't let us declare fixed types, but we can fix a type
  by introducing a property like this
*/
Extensible_Theorem
  fix_nat : forall N,
    IsN : is_nat N ->
    N = z \/ exists N', N = s N'
  on IsN. [Show Proof]



Prove mtc:shared_declarations:type_preservation. [Show Proof]



Prove mtc:shared_declarations:value_evalStep_false. [Show Proof]



Theorem plusRel_unique : forall N1 N2 A B,
  plusRel N1 N2 A -> plusRel N1 N2 B -> A = B. [Show Proof]



Prove mtc:shared_declarations:subst_unique. [Show Proof]



Prove mtc:shared_declarations:evalStep_unique. [Show Proof]



Prove mtc:shared_declarations:ty_lookup. [Show Proof]



Prove mtc:shared_declarations:subst_preservation. [Show Proof]



Prove mtc:shared_declarations:evalStep_type_preservation. [Show Proof]



Prove mtc:shared_declarations:canonical_form. [Show Proof]



Prove mtc:shared_declarations:subst_is. [Show Proof]



Theorem plusRel_is : forall A B C,
  is_nat A -> is_nat B -> plusRel A B C -> is_nat C. [Show Proof]



Prove mtc:shared_declarations:evalStep_is. [Show Proof]



Prove mtc:shared_declarations:subst_total. [Show Proof]



Theorem plusRel_total : forall N1 N2,
  is_nat N1 -> exists N, plusRel N1 N2 N. [Show Proof]



Prove mtc:shared_declarations:progress. [Show Proof]
Back to example home