Extensibella: Extensibella Example: matchEval:assert

Language Specification

File: defs.sos

Module matchEval:assert

Builds on matchEval:host

stmt ::= ...
       | assert(expr, expr)


-------------------------------------------- [Proj-Assert]
Names |{stmt}- assert(E, Msg) ~~>
         ifThenElse(E, noop,
            /*printVal(error) never succeeds*/
            printVal(errorExpr(Msg, intTy)))



typeOf FC TC E boolTy
typeOf FC TC Msg stringTy
------------------------------ [T-Assert]
stmtOK FC TC assert(E, Msg) TC



evalExpr FE EE E V O
matchTrue V
---------------------------------- [E-Assert]
evalStmt FE EE assert(E, Msg) EE O

Reasoning

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

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

Module matchEval:assert.

/********************************************************************
 Basic Projection Constraints
 ********************************************************************/
Prove_Constraint matchEval:host:proj_expr_unique.
Prove_Constraint matchEval:host:proj_expr_is.

Prove_Constraint matchEval:host:proj_stmt_unique. [Show Proof]

 %Proj-Assert
  case PrB. search.
Prove_Constraint matchEval:host:proj_stmt_is. [Show Proof]

 %Proj-Assert
  case IsS. search.
Prove_Constraint matchEval:host:proj_stmt_other. [Show Proof]

 %Proj-Assert
  search.

Prove_Constraint matchEval:host:proj_fun_unique.
Prove_Constraint matchEval:host:proj_fun_is.

Prove_Constraint matchEval:host:proj_param_unique.
Prove_Constraint matchEval:host:proj_param_is.

Prove_Constraint matchEval:host:proj_program_unique.
Prove_Constraint matchEval:host:proj_program_is.

Prove_Constraint matchEval:host:proj_typ_unique.
Prove_Constraint matchEval:host:proj_typ_is.

Prove_Constraint matchEval:host:proj_value_unique.
Prove_Constraint matchEval:host:proj_value_is.




/********************************************************************
 Decidable Equality
 ********************************************************************/
Add_Proj_Rel matchEval:host:is_expr, matchEval:host:is_args,
             matchEval:host:is_recFieldExprs.
Prove_Ext_Ind matchEval:host:is_expr, matchEval:host:is_args,
   matchEval:host:is_recFieldExprs.
Add_Proj_Rel matchEval:host:is_stmt.
Prove_Ext_Ind matchEval:host:is_stmt. [Show Proof]

search.

Prove matchEval:host:is_args_nilArgs_or_consArgs.
Prove matchEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs.




/********************************************************************
 Variables
 ********************************************************************/
Prove matchEval:host:vars_unique.

Prove matchEval:host:vars_is.

Prove matchEval:host:vars_exist,
      matchEval:host:varsArgs_exist,
      matchEval:host:varsRecFields_exist.

Prove_Constraint matchEval:host:proj_expr_vars.




/********************************************************************
 Typing
 ********************************************************************/
Prove matchEval:host:typeOf_isTy.
Prove matchEval:host:stmtOK_isCtx. [Show Proof]

%stmtOK_isCtx
 %T-Assert
  search.


Prove matchEval:host:stmtOK_keep_scopes. [Show Proof]

%T-Assert
 search.


Prove matchEval:host:stmtOK_older_scopes_same. [Show Proof]

%T-Assert
 search.


Prove matchEval:host:stmtOK_first_scope_lookup_same. [Show Proof]

%T-Assert
 search.


Prove matchEval:host:typeOf_unique.
Prove matchEval:host:stmtOK_unique. [Show Proof]

%stmtOK_unique
 case TyB. search.


Prove matchEval:host:paramTy_is.
Prove matchEval:host:getFunInfo_is.


Prove matchEval:host:paramTy_exists.
Prove matchEval:host:getFunInfo_exists.




/********************************************************************
 Evaluation
 ********************************************************************/
Prove matchEval:host:matchInt_is.
Prove matchEval:host:matchString_is.
Prove matchEval:host:matchRec_is.

Prove matchEval:host:evalExpr_isValue,
      matchEval:host:evalStmt_isCtx,
      matchEval:host:evalArgs_isValue,
      matchEval:host:evalRecFields_isValue. [Show Proof]

%evalStmt_isCtx
 %E-Assert
  search.


Prove matchEval:host:evalExpr_isOutput,
      matchEval:host:evalStmt_isOutput,
      matchEval:host:evalArgs_isOutput,
      matchEval:host:evalRecFields_isOutput. [Show Proof]

%evalStmt_isOutput
 %E-Assert
  case IsS. apply IH_E to _ _ _ Ev1. search.


Prove matchEval:host:paramName_is.
Prove matchEval:host:getFunEvalInfo_is.

Prove matchEval:host:evalProgram_isOutput.


Prove matchEval:host:evalStmt_names_same. [Show Proof]

%evalStmt_names_same
 %E-Assert
  NS: apply names_same_reflexive to IsEE. case NS. search.


Prove matchEval:host:matchInt_unique.
Prove matchEval:host:matchTrue_matchFalse_exclusive.
Prove matchEval:host:matchString_unique.
Prove matchEval:host:matchRec_unique.
Prove matchEval:host:matchInt_matchTrue_exclusive.
Prove matchEval:host:matchInt_matchFalse_exclusive.
Prove matchEval:host:matchInt_matchString_exclusive.
Prove matchEval:host:matchInt_matchRec_exclusive.
Prove matchEval:host:matchString_matchTrue_exclusive.
Prove matchEval:host:matchString_matchFalse_exclusive.
Prove matchEval:host:matchString_matchRec_exclusive.
Prove matchEval:host:matchRec_matchTrue_exclusive.
Prove matchEval:host:matchRec_matchFalse_exclusive.

Prove matchEval:host:evalExpr_rel,
      matchEval:host:evalExpr_rel_output,
      matchEval:host:evalStmt_newNameScopes_output,
      matchEval:host:evalStmt_newNameScopes,
      matchEval:host:evalArgs_rel,
      matchEval:host:evalArgs_rel_output,
      matchEval:host:evalRecFields_rel,
      matchEval:host:evalRecFields_rel_output. [Show Proof]

%evalStmt_newNameScopes_output
 Is: case IsS. EvB: case EvB. V: apply vars_exist to Is.
 apply IH_O_E to _ _ _ _ EvA1 EvB V _.
    intros _ LSB. apply lookupScopes_is_key to _ LSB.
    apply newNameScopes_lookupScopes to _ _ _ LSB. search.
 search.
%evalStmt_newNameScopes
 case IsS. EvB: case EvB. search.


Add_Ext_Size matchEval:host:evalExpr,
             matchEval:host:evalArgs,
             matchEval:host:evalRecFields,
             matchEval:host:evalStmt.
Add_Proj_Rel matchEval:host:evalExpr,
             matchEval:host:evalArgs,
             matchEval:host:evalRecFields,
             matchEval:host:evalStmt.


Prove matchEval:host:evalExpr_rel_exists_ES,
      matchEval:host:evalStmt_newNameScopes_exists_ES,
      matchEval:host:evalArgs_rel_exists_ES,
      matchEval:host:evalRecFields_rel_exists_ES. [Show Proof]

Is: case IsS. V: apply vars_exist to Is.
apply IH_E to _ _ _ _ EvB2 V _ with EE_A = Scope::EE_A.
   intros _ LSB. apply lookupScopes_is_key to _ LSB.
   apply newNameScopes_lookupScopes to _ _ _ LSB. search.
search.


Prove matchEval:host:evalExpr_scopes_same,
      matchEval:host:evalStmt_scopes_same,
      matchEval:host:evalStmt_scopes_same_ctx,
      matchEval:host:evalArgs_scopes_same,
      matchEval:host:evalRecFields_scopes_same. [Show Proof]

%evalStmt_scopes_same
 case IsS. EvB: case EvB. apply IH_E to _ _ _ _ SS EvA1 EvB. search.
%evalStmt_scopes_same_ctx
 case IsS. EvB: case EvB. search.

Prove matchEval:host:evalExpr_scopes_same_exists,
      matchEval:host:evalStmt_scopes_same_exists,
      matchEval:host:evalArgs_scopes_same_exists,
      matchEval:host:evalRecFields_scopes_same_exists. [Show Proof]

case IsS. apply IH_E to _ _ _ _ SS EvA1. search.


Prove_Constraint matchEval:host:proj_matchInt.
Prove_Constraint matchEval:host:proj_matchTrue.
Prove_Constraint matchEval:host:proj_matchFalse.
Prove_Constraint matchEval:host:proj_matchString.
Prove_Constraint matchEval:host:proj_matchRec.
Add_Proj_Rel matchEval:host:matchInt.
Prove_Ext_Ind matchEval:host:matchInt.
Add_Proj_Rel matchEval:host:matchTrue.
Prove_Ext_Ind matchEval:host:matchTrue.
Add_Proj_Rel matchEval:host:matchFalse.
Prove_Ext_Ind matchEval:host:matchFalse.
Add_Proj_Rel matchEval:host:matchRec.
Prove_Ext_Ind matchEval:host:matchRec.
Add_Proj_Rel matchEval:host:matchString.
Prove_Ext_Ind matchEval:host:matchString.
Prove matchEval:host:projedVal_is.
Prove matchEval:host:projedVal_matchInt.
Prove matchEval:host:projedVal_matchString.
Prove matchEval:host:projedVal_matchTrue.
Prove matchEval:host:projedVal_matchFalse.
Prove matchEval:host:projedVal_matchRec.

Prove_Constraint matchEval:host:matchInt_proj.
Prove_Constraint matchEval:host:matchTrue_proj.
Prove_Constraint matchEval:host:matchFalse_proj.
Prove_Constraint matchEval:host:matchString_proj.
Prove_Constraint matchEval:host:matchRec_proj.
Prove matchEval:host:matchInt_projedVal.
Prove matchEval:host:matchTrue_projedVal.
Prove matchEval:host:matchFalse_projedVal.
Prove matchEval:host:matchString_projedVal.
Prove matchEval:host:matchRec_projedVal.

Prove_Constraint matchEval:host:proj_evalExpr_forward.

Theorem is_list_values_append_nil : forall L,
  is_list is_value L -> L ++ [] = L. [Show Proof]

induction on 1. intros IsL. Is: case IsL.
  %nil
   search.
  %cons
   apply IH to Is1. search.

Prove_Constraint matchEval:host:proj_evalStmt_forward. [Show Proof]

case IsS. Ev: case Ev. exists EE'. split.
  %eval
   unfold. exists V, O, [], []. split.
     %eval E
      search.
     %matchTrue
      search.
     %eval noop
      search.
     %append
      IsO: apply evalExpr_isOutput to _ _ _ Ev.
      backchain is_list_values_append_nil.
  %scopes_same
   backchain scopes_same_reflexive.


Prove_Ext_Ind matchEval:host:evalExpr,
              matchEval:host:evalArgs,
              matchEval:host:evalRecFields,
              matchEval:host:evalStmt. [Show Proof]

case IsS. apply ext_size_is_int_evalExpr to R2. Acc: case Acc.
L: apply lt_plus_one to R1 _. apply ext_size_pos_evalExpr to R2.
A: apply Acc to _ L. apply IH to R2 A _ _ _.
Names: apply names_exists to IsEE. unfold.
exists N1, ifThenElse E noop (printVal (errorExpr Msg intTy)),
       EE', O, V.
split.
  %eval E
   search.
  %matchTrue
   search.
  %names
   search.
  %proj
   search.
  %eval proj
   unfold. exists V, O, [], []. split.
     %eval E
      search.
     %matchTrue
      search.
     %eval noop
      search.
     %append output
      Ev: apply drop_ext_size_evalExpr to R2.
      apply evalExpr_isOutput to _ _ _ Ev.
      backchain is_list_values_append_nil.


Prove matchEval:host:paramName_unique.
Prove_Constraint matchEval:host:proj_paramName_forward.
Prove_Constraint matchEval:host:proj_paramName_back.
Prove matchEval:host:getFunEvalInfo_unique.
Prove_Constraint matchEval:host:proj_getFunEvalInfo_forward.
Prove_Constraint matchEval:host:proj_getFunEvalInfo_back.

Prove matchEval:host:evalProgram_unique.
Prove_Constraint matchEval:host:proj_evalProgram_forward.
Prove_Constraint matchEval:host:proj_evalProgram_back.


Prove matchEval:host:matchRec_typePres.
Prove matchEval:host:evalExpr_typePres,
      matchEval:host:evalStmt_typePres,
      matchEval:host:evalArgs_typePres,
      matchEval:host:evalRecFields_typePres. [Show Proof]

%evalStmt_typePres
 %E-Assert
  Ty: case Ty. search.


Prove matchEval:host:paramTy_paramName_same.
Prove matchEval:host:funOK_getFunEvalInfo_related.


Prove matchEval:host:evalExpr_output_forms,
      matchEval:host:evalStmt_output_forms,
      matchEval:host:evalArgs_output_forms,
      matchEval:host:evalRecFields_output_forms. [Show Proof]

%evalStmt_output_forms
 %E-Assert
  case IsS. apply IH_E to _ _ _ Ev1. search.


Prove matchEval:host:evalProgram_output_forms.


Prove matchEval:host:paramName_exists.
Prove matchEval:host:getFunEvalInfo_exists.