Extensibella Example: library:list

Language Specification

File: syntax.sos

[Reduce File] [Raw File] 
Module library:list

Builds on library:host

e ::= ...
    | nil
    | cons(e, e)
    | null(e)
    | head(e)
    | tail(e)

ty ::= ...
     | list(ty)

s ::= ...
    | splitlist(string, string, e)


------------------- [P-null]
|{e}- null(E) ~~> E


------------------- [P-head]
|{e}- head(E) ~~> E


------------------- [P-tail]
|{e}- tail(E) ~~> E


------------------- [P-nil]
|{e}- nil ~~> trueE


--------------------------------- [P-cons]
|{e}- cons(E1, E2) ~~> eq(E1, E2)


Hd != Tl
----------------------------------------- [P-splitlist]
|{s}- splitlist(Hd, Tl, E) ~~>
      seq(seq(assign(Hd, E),
              assign(Tl, tail(var(Hd)))),
              assign(Hd, head(var(Hd))))


---------------------- [P-list]
|{ty}- list(Ty) ~~> Ty

File: vars.sos

[Reduce File] [Raw File] 
Module library:list

----------- [VR-nil]
vars nil []


vars E1 Vr1
vars E2 Vr2
Vr1 ++ Vr2 = V
------------------- [VR-cons]
vars cons(E1, E2) V


vars E V
-------------- [VR-null]
vars null(E) V


vars E V
-------------- [VR-head]
vars head(E) V


vars E V
-------------- [VR-tail]
vars tail(E) V

File: typing.sos

[Reduce File] [Raw File] 
Module library:list

------------------- [T-nil]
ty_e G nil list(Ty)


ty_e G E1 Ty
ty_e G E2 list(Ty)
---------------------------- [T-cons]
ty_e G cons(E1, E2) list(Ty)


ty_e G E list(Ty)
------------------- [T-null]
ty_e G null(E) bool


ty_e G E list(Ty)
----------------- [T-head]
ty_e G head(E) Ty


ty_e G E list(Ty)
----------------------- [T-tail]
ty_e G tail(E) list(Ty)





ty_e G E list(Ty)
lookup G Hd Ty
lookup G Tl list(Ty)
----------------------------- [TS-splitlist]
ty_s G splitlist(Hd, Tl, E) G

File: eval.sos

[Reduce File] [Raw File] 
Module library:list

--------- [V-nil]
value nil


value E1
value E2
------------------ [V-cons]
value cons(E1, E2)





---------------- [E-nil]
eval_e G nil nil


eval_e G E1 V1
eval_e G E2 V2
---------------------------------- [E-cons]
eval_e G cons(E1, E2) cons(V1, V2)


eval_e G E nil
---------------------- [E-null-true]
eval_e G null(E) trueE


eval_e G E cons(V1, V2)
----------------------- [E-null-false]
eval_e G null(E) falseE


eval_e G E cons(V1, V2)
----------------------- [E-head]
eval_e G head(E) V1


eval_e G E cons(V1, V2)
----------------------- [E-tail]
eval_e G tail(E) V2





eval_e G E cons(V1, V2)
Hd != Tl /*Need this to prove ext_ind*/
select (Hd, VHd) GHd G
select (Tl, VTl) GTl GHd
----------------------------------------------------- [X-splitlist]
eval_s G splitlist(Hd, Tl, E) (Hd, V1)::(Tl, V2)::GTl

Reasoning

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

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

Module library:list.


Prove_Constraint library:host:proj_e_unique. [Show Proof]

Prove_Constraint library:host:proj_e_is. [Show Proof]



Prove_Constraint library:host:proj_s_unique. [Show Proof]

Prove_Constraint library:host:proj_s_is. [Show Proof]



Prove_Constraint library:host:proj_ty_unique. [Show Proof]

Prove_Constraint library:host:proj_ty_is. [Show Proof]



Add_Proj_Rel library:host:is_e.


Prove_Ext_Ind library:host:is_e. [Show Proof]



Prove library:host:is_e_var_or_not. [Show Proof]

Prove library:host:is_e_intlit_or_not. [Show Proof]

Prove library:host:is_e_trueE_or_not. [Show Proof]

Prove library:host:is_e_falseE_or_not. [Show Proof]

Prove library:host:is_e_add_or_not. [Show Proof]

Prove library:host:is_e_eqC_or_not. [Show Proof]

Prove library:host:is_e_gt_or_not. [Show Proof]

Prove library:host:is_e_not_or_not. [Show Proof]

Extensible_Theorem
  is_e_nil_or_not : forall E,
    IsE: is_e E ->
    E = library:list:nil \/ (E = library:list:nil -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_cons_or_not : forall E,
    IsE: is_e E ->
    (exists E1 E2, E = cons E1 E2) \/
    ((exists E1 E2, E = cons E1 E2) -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_null_or_not : forall E,
    IsE: is_e E ->
    (exists E', E = null E') \/
    ((exists E', E = null E') -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_head_or_not : forall E,
    IsE: is_e E ->
    (exists E', E = head E') \/
    ((exists E', E = head E') -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_tail_or_not : forall E,
    IsE: is_e E ->
    (exists E', E = tail E') \/
    ((exists E', E = tail E') -> false)
  on IsE. [Show Proof]

Prove library:host:is_e_eq_or_not. [Show Proof]



Prove library:host:vars_unique. [Show Proof]



Prove_Constraint library:host:proj_e_vars_exist. [Show Proof]

Prove_Constraint library:host:proj_e_vars. [Show Proof]



Prove library:host:vars_is. [Show Proof]



Prove library:host:vars_exist. [Show Proof]



Prove library:host:value_empty_typable. [Show Proof]



Prove library:host:eval_e_is. [Show Proof]



Prove library:host:type_preservation_e. [Show Proof]



Prove library:host:var_types_maintained. [Show Proof]



Prove library:host:type_preservation_s. [Show Proof]



Prove_Constraint library:host:proj_eval_e. [Show Proof]



Prove library:host:eval_e_unique. [Show Proof]



Prove_Constraint library:host:proj_s_eval. [Show Proof]

Add_Ext_Size library:host:eval_s.
Add_Proj_Rel library:host:eval_s.
Prove_Ext_Ind library:host:eval_s. [Show Proof]



Prove_Constraint library:host:proj_s_eval_results. [Show Proof]



Prove_Constraint library:host:proj_s_eval_results_back. [Show Proof]



Prove library:host:eval_e_value. [Show Proof]



Prove library:host:eval_s_value. [Show Proof]



Prove library:host:vars_eval_same_result. [Show Proof]
Back to example home