Changeset 9


Ignore:
Timestamp:
Jun 21, 2010, 4:22:09 PM (7 years ago)
Author:
campbell
Message:

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

Location:
C-semantics
Files:
1 added
6 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r3 r9  
    3131Definition ident_eq := peq.
    3232*)
    33 (* TODO: define ident *)
    34 naxiom ident:Type[0].
    35 naxiom ident_eq: ∀x,y:ident. (x=y) + (x≠y).
     33(* XXX: we use nats for now, but if in future we use binary like compcert
     34        then the maps will be easier to define. *)
     35ndefinition ident ≝ nat.
     36ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
     37#x; nelim x;
     38##[ #y; ncases y; /3/;
     39##| #x'; #IH; #y; ncases y;
     40  ##[ @2; @; #H; ndestruct
     41  ##| #y'; nelim (IH y');
     42    ##[ #e; ndestruct; /2/
     43    ##| #ne; @2; /2/;
     44    ##]
     45  ##]
     46##] nqed.
    3647
    3748(* * The intermediate languages are weakly typed, using only two types:
  • C-semantics/Cexec.ma

    r5 r9  
    128128  ##| #b i t0; @ true; @; //
    129129  ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    130   ##| #i s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
    131   ##| #t; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
     130  ##| #i s; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
     131  ##| #t; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
    132132  ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    133133  ##]
     
    213213  ##| #b i t0; @ true; @; //
    214214  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
    215   ##| #i s; @ false; @; //; nwhd; nrewrite > (eq_true …); //;
    216   ##| #t; @ false; @; //; nwhd; nrewrite > (eq_true …); //;
     215  ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
     216  ##| #t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    217217  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
    218218  ##]
     
    220220
    221221(* Prove a few minor results to make proof obligations easy. *)
     222
     223nlemma bind_assoc_r: ∀A,B,C,e,f,g.
     224  bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g).
     225#A B C e f g; ncases e; nnormalize; //; nqed.
    222226
    223227nlemma bind_OK: ∀A,B,P,e,f.
     
    290294  match e' with
    291295  [ Econst_int i ⇒ Some ? (OK ? (Vint i))
     296  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
    292297  | Evar _ ⇒ Some ? (
     298      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
     299      opt_to_res ? (load_value_of_type ty m loc ofs))
     300  | Ederef _ ⇒ Some ? (
    293301      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    294302      opt_to_res ? (load_value_of_type ty m loc ofs))
     
    296304      〈loc, ofs〉 ← exec_lvalue ge en m a;:
    297305      OK ? (Vptr loc ofs))
     306  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
    298307  | Eunop op a ⇒ Some ? (
    299308      v1 ← exec_expr ge en m a;:
    300309      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
     310  | Ebinop op a1 a2 ⇒ Some ? (
     311      v1 ← exec_expr ge en m a1;:
     312      v2 ← exec_expr ge en m a2;:
     313      opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m))
    301314  | Econdition a1 a2 a3 ⇒ Some ? (
    302315      v ← exec_expr ge en m a1;:
     
    312325      l ← opt_to_res ? (get ? PTree ? id en);:
    313326      OK ? 〈l, zero〉)
     327  | Ederef a ⇒ Some ? (
     328      v ← exec_expr ge en m a;:
     329      match v with
     330      [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
     331      | _ ⇒ Error ?
     332      ])
    314333  | _ ⇒ Some ? (Error ?)
    315334  ]
     
    319338##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
    320339    napply opt_OK;  #v ev; /2/;
     340##| napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
     341    napply opt_OK;  #v ev; /2/;
    321342##| napply sig_bind2_OK; #loc ofs H;
    322343    nwhd; napply eval_Eaddrof; //;
     
    324345    napply opt_OK; #v ev;
    325346    napply (eval_Eunop … Hv1 ev);
     347##| napply sig_bind_OK; #v1 ev1 Hv1;
     348    napply sig_bind_OK; #v2 ev2 Hv2;
     349    napply opt_OK; #v ev;
     350    napply (eval_Ebinop … Hv1 Hv2 ev);
    326351##| napply sig_bind_OK; #vb evb Hvb;
    327352    napply sig_bind_OK; #b;
     
    330355    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    331356    ##]
    332 ##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
     357##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
     358##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
     359    napply eval_Ederef; //
     360
    333361##] nqed.
     362
     363(* TODO: Can we do this sensibly with a map combinator? *)
     364nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvl:list val. eval_exprlist ge e m l vl) ≝
     365match l with
     366[ nil ⇒ Some ? (OK ? (nil val))
     367| cons e1 es ⇒ Some ? (
     368  v ← exec_expr ge e m e1;:
     369  vs ← exec_exprlist ge e m es;:
     370  OK ? (cons val v vs))
     371]. nwhd; //;
     372napply sig_bind_OK; #v ev Hv;
     373napply sig_bind_OK; #vs evs Hvs;
     374nnormalize; /2/;
     375nqed.
    334376
    335377(* Don't really want to use subset rather than sigma here, but can't be bothered
     
    377419]. nwhd; //; @; #H; ndestruct; nqed.
    378420
     421ninductive decide : Type ≝
     422| dy : decide | dn : decide.
     423
     424ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
     425#P d;ncases d;/2/; nqed.
     426
     427ncoercion decide_inject :
     428  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
     429  on d:decide to ? + (¬?).
     430
     431alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
     432alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
     433ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
     434#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     435ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
     436#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     437ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
     438#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     439
     440(* Not very happy about this. *)
     441nlet rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
     442match t1 with
     443[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
     444| Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     445| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
     446| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
     447| Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
     448    match type_eq_dec t t' with [ inl _ ⇒
     449      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
     450| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl _ ⇒
     451    match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
     452| Tstruct i fl ⇒
     453    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
     454      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
     455| Tunion i fl ⇒
     456    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
     457      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
     458| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
     459]
     460and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
     461match tl1 with
     462[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
     463| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
     464    match type_eq_dec t1 t2 with [ inl _ ⇒
     465      match typelist_eq_dec ts1 ts2 with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
     466]
     467and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
     468match fl1 with
     469[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
     470| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
     471    match ident_eq i1 i2 with [ inl _ ⇒
     472      match type_eq_dec t1 t2 with [ inl _ ⇒
     473        match fieldlist_eq_dec fs1 fs2 with [ inl _ ⇒ dy | _ ⇒ dn ]
     474        | _ ⇒ dn ] | _ ⇒ dn ] ]
     475].
     476(* A poor man's clear, otherwise automation picks up recursive calls without
     477   checking that the argument is smaller. *)
     478ngeneralize in type_eq_dec;
     479ngeneralize in typelist_eq_dec;
     480ngeneralize in fieldlist_eq_dec; #avoid1 avoid2 avoid3 avoid4 avoid5 avoid6;
     481ndestruct; //; @; #H; ndestruct;
     482##[ nelim c8; /2/
     483##| nelim c6; /2/
     484##| nelim c4; /2/
     485##| nelim c4; /2/
     486##| nelim c8; /2/
     487##| nelim c6; /2/
     488##| nelim c8; /2/
     489##| nelim c6; /2/
     490##| nelim c8; /2/
     491##| nelim c6; /2/
     492##| nelim c8; /2/
     493##| nelim c6; /2/
     494##| nelim c4; /2/
     495##| nelim c8; /2/
     496##| nelim c6; /2/
     497##| nelim c12; /2/
     498##| nelim c10; /2/
     499##| nelim c8; /2/
     500##] nqed.
     501
     502ndefinition are_equal : ∀A:Type. (∀x,y:A.(x=y)+(x≠y)) → ∀x,y:A. res (x=y) ≝
     503λA,dec,x,y.
     504match dec … x y with
     505[ inl p ⇒ OK ? p
     506| inr _ ⇒ Error ?
     507].
     508
     509nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
     510match k with
     511[ Kstop ⇒ dy
     512| Kcall _ _ _ _ ⇒ dy
     513| _ ⇒ dn
     514]. nwhd; //; @; #H; nelim H; nqed.
     515
    379516nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝
    380517match st with
     
    386523    m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);:
    387524    OK ? 〈E0, State f Sskip k e m'〉)
     525  | Scall lhs a al ⇒ Some ? (
     526    vf ← exec_expr ge e m a;:
     527    vargs ← exec_exprlist ge e m al;:
     528    fd ← opt_to_res ? (find_funct Genv ? ge vf);:
     529    p ← are_equal ? type_eq_dec (type_of_fundef fd) (typeof a);:
     530    k' ← match lhs with
     531         [ None ⇒ OK ? (Kcall (None ?) f e k)
     532         | Some lhs' ⇒
     533           locofs ← exec_lvalue ge e m lhs';:
     534           OK ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
     535         ];:
     536    OK ? 〈E0, Callstate fd vargs k' m〉)
     537  | Ssequence s1 s2 ⇒ Some ? (OK ? 〈E0, State f s1 (Kseq s2 k) e m〉)
     538  | Sskip ⇒
     539      match k with
     540      [ Kseq s k' ⇒ Some ? (OK ? 〈E0, State  f s k' e m〉)
     541      | Kstop ⇒
     542          match fn_return f with
     543          [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
     544          | _ ⇒ Some ? (Error ?)
     545          ]
     546      | Kcall _ _ _ _ ⇒
     547          match fn_return f with
     548          [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
     549          | _ ⇒ Some ? (Error ?)
     550          ]
     551      | _ ⇒ Some ? (Error ?) (* TODO more *)
     552      ]
    388553  | Sreturn a_opt ⇒
    389554    match a_opt with
     
    410575| _ ⇒ Some ? (Error ?)
    411576]. nwhd; //;
    412 ##[ napply sig_bind2_OK; #loc ofs Hlval;
     577##[ nrewrite > c7; napply step_skip_call; //; napply c8;
     578##| nrewrite > c11; napply step_skip_call; //; napply c12;
     579##| napply sig_bind2_OK; #loc ofs Hlval;
    413580    napply sig_bind_OK; #v2 ev2 Hv2;
    414581    napply opt_bind_OK; #m' em';
    415582    nwhd; napply (step_assign … Hlval Hv2 em');
     583##| napply sig_bind_OK; #vf evf Hvf;
     584    napply sig_bind_OK; #vargs evargs Hvargs;
     585    napply opt_bind_OK; #fd efd;
     586    napply bind_OK; #ety ety';
     587    ncases c6; nwhd;
     588    ##[ napply (step_call_none … Hvf Hvargs efd ety);
     589    ##| #lhs'; nrewrite > (bind_assoc_r …);
     590        napply sig_bind_OK; #locofs; ncases locofs; #loc ofs elocofs Hlocofs;
     591        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
     592    ##]
    416593##| napply step_return_0; napply c9;
    417594##| napply sig_bind_OK; #u eu Hnotvoid;
     
    436613nwhd; napply (initial_state_intro … eb ef);
    437614nqed.
     615
     616ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
     617#st; nelim st;
     618##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
     619##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
     620##| #v k m; ncases k;
     621  ##[ ncases v;
     622    ##[ ##2: #i; @1; @ i; //;
     623    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     624    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     625    ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     626    ##]
     627  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     628  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     629  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     630  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     631  ##]
     632##] nqed.
     633
     634nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
     635 res (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
     636match is_final_state s with
     637[ inl _ ⇒ Some ? (OK ? 〈E0, s〉)
     638| inr _ ⇒
     639  match n with
     640  [ O ⇒ Some ? (OK ? 〈E0, s〉)
     641  | S n' ⇒ Some ? (
     642      〈t,s'〉 ← exec_step ge s;:
     643      〈t',s''〉 ← exec_steps n' ge s';:
     644      OK ? 〈t ⧺ t',s''〉)
     645  ]
     646]. nwhd; /2/;
     647napply sig_bind2_OK; #t s' H1;
     648napply sig_bind2_OK; #t' s'' IH;
     649nwhd; napply (star_step … IH); //;
     650nqed.
  • C-semantics/Integers.ma

    r4 r9  
    9494  [modulus] (excluded. *)
    9595
    96 nrecord int: Type ≝ { intval: Z; intrange: (0 ≤ intval) ∧ intval < modulus }.
     96nrecord int: Type ≝ { intval: Z ; intrange: True (*(0 ≤ intval) ∧ intval < modulus*) }.
    9797
    9898(* The [unsigned] and [signed] functions return the Coq integer corresponding
     
    110110  machine integer.  The argument is treated modulo [modulus]. *)
    111111(* TODO: prove *)
    112 naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.
     112(*naxiom repr : Z → int.*)
     113
     114(*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*)
    113115
    114116ndefinition repr : Z → int := λx.
    115   mk_int (x \mod modulus) ? (*Z_mod_lt x modulus modulus_pos*).
    116 napply repr_ax.
    117 nqed.
     117  mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*).
     118(*napply repr_ax.
     119nqed.*)
    118120
    119121ndefinition zero := repr 0.
  • C-semantics/Mem.ma

    r3 r9  
    23652365    ##]
    23662366##] nqed.
    2367 
     2367(*  XXX: reenable once I've sorted out Integers.ma a bit
    23682368nlemma valid_pointer_inject_no_overflow:
    23692369  ∀f,m1,m2,b,ofs,b',x.
     
    34333433##]
    34343434nqed.
    3435 
     3435*)
    34363436(* ** Relation between signed and unsigned loads and stores *)
    34373437
  • C-semantics/README

    r5 r9  
    1 Status of matita port of CompCert C semantics
    2 =============================================
     1Status of matita port of CompCert 1.6 C semantics
     2=================================================
    33
    4 Last seen working with matita svn r10871.
     4Last seen working with matita svn r10877 with the patch at the bottom of this
     5file.
    56
    67- Most of the memory model has been ported (common/Mem.v -> Mem.ma).
     
    3435  Cexec.ma.  At present only a small subset of expressions and statements
    3536  are handled.
     37
     38* The patch in compcert-1.7.1-matita.patch adds a -dmatita option to
     39  output a matita file containing a definition for the C program.
     40  Note that there must be a "main" function.  (This was made against
     41  1.7.1 for convenience - the Clight syntax is the same as 1.6.)
     42
     43There is a more recent version of compcert available with a revised memory
     44model that may be more closely suited to our needs.
    3645
    3746matita issues and workarounds
     
    119128  haven't been ported yet are done.  The other definitions and most of the
    120129  lemmas still remain to be done.
     130
     131
     132
     133
     134Index: matita/nlibrary/arithmetics/Z.ma
     135===================================================================
     136--- matita/nlibrary/arithmetics/Z.ma    (revision 10877)
     137+++ matita/nlibrary/arithmetics/Z.ma    (working copy)
     138@@ -13,6 +13,7 @@
     139 (**************************************************************************)
     140 
     141 include "arithmetics/nat.ma".
     142+include "arithmetics/compare.ma".
     143 
     144 ninductive Z : Type %G≝%@
     145   OZ : Z
     146@@ -508,7 +509,7 @@
     147    ##[//
     148    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
     149    ##|//]
     150-##|ncases y;//
     151+##|ncases y;/2/
     152 ##|ncases y
     153    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
     154       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
  • C-semantics/test/trivial.ma

    r3 r9  
    22include "Csyntax.ma".
    33include "Csem.ma".
     4include "Cexec.ma".
    45
    5 naxiom main : ident.
     6ndefinition main : ident ≝ O.
    67naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i).
    78
     
    1415nremark trivial_behaves : ∃behaviour. exec_program trivial behaviour.
    1516@; ##[ ##2:
    16   napply program_terminates;
     17  napply program_terminates; 
    1718  ##[ ##5: @; (* initial state *)
    1819    ##[ ##3: nnormalize; nrewrite > (ident_eq_eq ?); //;
     
    2223  ##| ##6:
    2324    @2; ##[ ##4: napply step_internal_function;
    24           ##[ ##4: //;  ##| ##5: //; ##| ##*: ##skip ##]
     25          ##[ ##4: napply alloc_variables_nil; ##| ##5: napply bind_parameters_nil; ##| ##*: ##skip ##]
    2526        ##| ##5: @2;
    2627          ##[ ##4: napply step_return_1; //; napply nmk; #H; ndestruct;
     
    3536##] nqed.
    3637
     38nlemma nab : ∀A,P,e,v. e = OK (Σv:A.P v) v → ∃v:A. P v.
     39#A P e v; ncases v; /2/; nqed.
     40
     41nremark trivial_init : ∃s. initial_state trivial s.
     42napply (nab ?? (make_initial_state trivial) ? (refl ??));
     43nqed.
     44
     45nremark hacktonormalize : True.
     46nletin s ≝ (err_eject ?? (make_initial_state trivial)).
     47nnormalize in s.
     48//; nqed.
     49
     50nremark trivial_executes : True.
     51nletin ts ≝ (s ← make_initial_state trivial;:
     52             exec_steps 10 (globalenv Genv ?? trivial) s);
     53nnormalize in ts;
     54//; nqed.
Note: See TracChangeset for help on using the changeset viewer.