Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (10 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Smallstep.ma

    r20 r487  
    3636(* * * Closures of transitions relations *)
    3737
    38 nrecord transrel : Type[1] ≝ {
    39   genv : Type;
    40   state: Type;
     38record transrel : Type[1] ≝ {
     39  genv : Type[0];
     40  state: Type[0];
    4141  step : genv → state → trace → state → Prop
    4242}.
     
    5858(* * No transitions: stuck state *)
    5959
    60 ndefinition nostep ≝ λtr:transrel. λge: genv tr. λs: state tr.
     60definition nostep ≝ λtr:transrel. λge: genv tr. λs: state tr.
    6161  ∀t,s'. ¬((step tr) ge s t s').
    6262
     
    6464    or reflexive transitive closure. *)
    6565
    66 ninductive star (tr:transrel) (ge: genv tr): state tr -> trace -> state tr -> Prop :=
     66inductive star (tr:transrel) (ge: genv tr): state tr -> trace -> state tr -> Prop :=
    6767  | star_refl: ∀s.
    6868      star tr ge s E0 s
     
    7171      star tr ge s1 t s3.
    7272
    73 nlemma star_one:
     73lemma star_one:
    7474  ∀tr,ge,s1,t,s2. (step tr) ge s1 t s2 -> star tr ge s1 t s2.
    75 #tr ge s1 t s2 H; napply (star_step … H (star_refl …));
    76 nrewrite > (E0_right …); //;
    77 nqed.
    78 
    79 nlemma star_trans:
     75#tr #ge #s1 #t #s2 #H @(star_step … H (star_refl …))
     76>(E0_right …) //;
     77qed.
     78
     79lemma star_trans:
    8080  ∀tr,ge,s1,t1,s2. star tr ge s1 t1 s2 ->
    8181  ∀t2,s3,t. star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> star tr ge s1 t s3.
    82 #tr ge s1 t1 s2 H; nelim H;
    83 ##[ #s t2 s3 t H0 H1; nrewrite > H1; nnormalize; //;
    84 ##| #s t s' t' s'' t'' H0 H1 H2 H3;
    85     #t2 s3 t3 H4 H5;
    86     napply (star_step … H0 (H3 … H4 …) ?);
    87     ##[ napply (t'⧺t2);
    88     ##| //
    89     ##| nrewrite < (Eapp_assoc …); //;
    90     ##]
    91 ##]
    92 nqed.
    93 
    94 nlemma star_left:
     82#tr #ge #s1 #t1 #s2 #H elim H;
     83[ #s #t2 #s3 #t #H0 #H1 >H1 normalize; //;
     84| #s #t #s' #t' #s'' #t'' #H0 #H1 #H2 #H3
     85    #t2 #s3 #t3 #H4 #H5
     86    @(star_step … H0 (H3 … H4 …) ?)
     87    [ @(t'⧺t2)
     88    | //
     89    | <(Eapp_assoc …) //;
     90    ]
     91]
     92qed.
     93
     94lemma star_left:
    9595  ∀tr,ge,s1,t1,s2,t2,s3,t.
    9696  (step tr) ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 ->
    9797  star tr ge s1 t s3.
    98 napply star_step;
    99 nqed.
    100 
    101 nlemma star_right:
     98@star_step
     99qed.
     100
     101lemma star_right:
    102102  ∀tr,ge,s1,t1,s2,t2,s3,t.
    103103  star tr ge s1 t1 s2 -> (step tr) ge s2 t2 s3 -> t = t1 ⧺ t2 ->
    104104  star tr ge s1 t s3.
    105 #tr ge s1 t1 s2 t2 s3 t H1 H2 H3;
    106 napply (star_trans … H1 … (star_one … H2)); //;
    107 nqed.
     105#tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3
     106@(star_trans … H1 … (star_one … H2)) //;
     107qed.
    108108
    109109(* * One or several transitions.  Also known as the transitive closure. *)
    110110
    111 ninductive plus (tr:transrel) (ge: genv tr): state tr → trace → state tr → Prop ≝
     111inductive plus (tr:transrel) (ge: genv tr): state tr → trace → state tr → Prop ≝
    112112  | plus_left: ∀s1,t1,s2,t2,s3,t.
    113113      step tr ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 ->
    114114      plus tr ge s1 t s3.
    115115
    116 nlemma plus_one:
     116lemma plus_one:
    117117  ∀tr,ge,s1,t,s2.
    118118  step tr ge s1 t s2 -> plus tr ge s1 t s2.
    119 #tr ge s1 t s2 H; napply (plus_left … H (star_refl …));
    120 nrewrite > (E0_right …); //;
    121 nqed.
    122 
    123 nlemma plus_star:
     119#tr #ge #s1 #t #s2 #H @(plus_left … H (star_refl …))
     120>(E0_right …) //;
     121qed.
     122
     123lemma plus_star:
    124124  ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 -> star tr ge s1 t s2.
    125 #tr ge s1 t s2 H; nelim H; #s1' t1' s2' t2' s3' t3' H1 H2 e1;
    126 napply (star_step … H1 H2 …); //;
    127 nqed.
    128 
    129 nlemma plus_right:
     125#tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1
     126@(star_step … H1 H2 …) //;
     127qed.
     128
     129lemma plus_right:
    130130  ∀tr,ge,s1,t1,s2,t2,s3,t.
    131131  star tr ge s1 t1 s2 -> step tr ge s2 t2 s3 -> t = t1 ⧺ t2 ->
    132132  plus tr ge s1 t s3.
    133 #tr ge s1 t1 s2 t2 s3 t3 Hstar Hstep e1; ninversion Hstar;
    134 ##[ #s2' e2 e3 e4; ndestruct; napply plus_one; //;
    135 ##| #s1' t1' s1'' t1'' s2' t2' H1 H2 e2 foo e3 e4 e5; ndestruct;
    136     nrewrite > (Eapp_assoc …); napply (plus_left … H1);
    137     ##[ ##2: napply (star_right … H2 Hstep); //;
    138     ##| ##skip;
    139     ##| //
    140     ##]
    141 ##]
    142 nqed.
     133#tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar;
     134[ #s2' #e2 #e3 #e4 destruct; @plus_one //;
     135| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 destruct;
     136    >(Eapp_assoc …) @(plus_left … H1)
     137    [ 2: @(star_right … H2 Hstep) //;
     138    | skip;
     139    | //
     140    ]
     141]
     142qed.
    143143(*
    144144Lemma plus_left':
     
    206206(* * Infinitely many transitions *)
    207207
    208 ncoinductive forever (tr:transrel) (ge: genv tr): state tr -> traceinf -> Prop :=
     208coinductive forever (tr:transrel) (ge: genv tr): state tr -> traceinf -> Prop :=
    209209  | forever_intro: ∀s1,t,s2,T.
    210210      step tr ge s1 t s2 -> forever tr ge s2 T ->
    211211      forever tr ge s1 (t ⧻ T).
    212212
    213 nlemma star_forever:
     213lemma star_forever:
    214214  ∀tr,ge,s1,t,s2. star tr ge s1 t s2 ->
    215215  ∀T. forever tr ge s2 T ->
    216216  forever tr ge s1 (t ⧻ T).
    217 #tr ge s1 t1 s2 H; nelim H;
    218 ##[ #s' T H2; //;
    219 ##| #s1' t1 s0 t0 s2' t2' H1 H2 e1 IH T H3;
    220     nrewrite > e1; nrewrite > (Eappinf_assoc …);
    221     @; /2/;
    222 ##] nqed.
     217#tr #ge #s1 #t1 #s2 #H elim H;
     218[ #s' #T #H2 //;
     219| #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3
     220    >e1 >(Eappinf_assoc …)
     221    % /2/;
     222] qed.
    223223(*
    224224(** An alternate, equivalent definition of [forever] that is useful
     
    309309(* * Infinitely many silent transitions *)
    310310
    311 ncoinductive forever_silent (tr:transrel) (ge: genv tr): state tr → Prop ≝
     311coinductive forever_silent (tr:transrel) (ge: genv tr): state tr → Prop ≝
    312312  | forever_silent_intro: ∀s1,s2.
    313313      step tr ge s1 E0 s2 → forever_silent tr ge s2 →
     
    361361(* * Infinitely many non-silent transitions *)
    362362
    363 ncoinductive forever_reactive (tr:transrel) (ge: genv tr): state tr → traceinf → Prop ≝
     363coinductive forever_reactive (tr:transrel) (ge: genv tr): state tr → traceinf → Prop ≝
    364364  | forever_reactive_intro: ∀s1,s2,t,T.
    365365      star tr ge s1 t s2 → t ≠ E0 → forever_reactive tr ge s2 T →
    366366      forever_reactive tr ge s1 (t ⧻ T).
    367367(*
    368 nlemma star_forever_reactive:
     368lemma star_forever_reactive:
    369369  ∀tr,ge,s1,t,s2,T.
    370370  star tr ge s1 t s2 → forever_reactive tr ge s2 T →
    371371  forever_reactive tr ge s1 (t ⧻ T).
    372 #tr ge s1 t s2 T H1 H2; ninversion H2;
     372#tr #ge #s1 #t #s2 #T #H1 #H2 inversion H2;
    373373Proof.
    374374  intros. inv H0. rewrite <- Eappinf_assoc. econstructor.
     
    393393*)
    394394
    395 ninductive program_behavior: Type :=
     395inductive program_behavior: Type[0] :=
    396396  | Terminates: trace -> int -> program_behavior
    397397  | Diverges: trace -> program_behavior
     
    399399  | Goes_wrong: trace -> program_behavior.
    400400
    401 ndefinition not_wrong : program_behavior → Prop ≝ λbeh.
     401definition not_wrong : program_behavior → Prop ≝ λbeh.
    402402  match beh with
    403403  [ Terminates _ _ => True
     
    415415Variable final_state: state -> int -> Prop.
    416416*)
    417 ninductive program_behaves (tr:transrel)
     417inductive program_behaves (tr:transrel)
    418418                           (initial_state:state tr → Prop)
    419419                           (final_state : state tr → int → Prop)
     
    463463*)
    464464
    465 nrecord semantics : Type[1] ≝
     465record semantics : Type[1] ≝
    466466{ trans :> transrel
    467467; initial : (state trans) → Prop
     
    473473(** The second small-step semantics is also axiomatized. *)
    474474
    475 Variable genv2: Type.
    476 Variable state2: Type.
     475Variable genv2: Type[0].
     476Variable state2: Type[0].
    477477Variable step2: genv2 -> state2 -> trace -> state2 -> Prop.
    478478Variable initial_state2: state2 -> Prop.
     
    497497*)
    498498
    499 nrecord related_semantics : Type[1] ≝
     499record related_semantics : Type[1] ≝
    500500{ sem1 : semantics
    501501; sem2 : semantics
     
    528528  /\ match_states st1' st2'.
    529529*)
    530 nrecord order_sim : Type[1] ≝
     530record order_sim : Type[1] ≝
    531531{ sem :> related_semantics
    532532; order : state (sem1 sem) → state (sem1 sem) → Prop
     
    540540}.
    541541
    542 nlemma simulation_star_star: ∀sim:order_sim.
     542lemma simulation_star_star: ∀sim:order_sim.
    543543  ∀st1,t,st1'. star (sem1 sim) (ge (sem1 sim)) st1 t st1' →
    544544  ∀st2. match_states sim st1 st2 →
    545545  ∃st2'. star (sem2 sim) (ge (sem2 sim)) st2 t st2' ∧ match_states sim st1' st2'.
    546 #sim st1 t st1' H; nelim H;
    547 ##[ #st1'' st2 Hmatch;
    548     @ st2; @; //;
    549 ##| #st1 tA st1A tB st1B t Hstep Hstar Ht IH st2 Hmatch;
    550     nelim (simulation sim ??? Hstep ? Hmatch); #st2'; *; #A B;
    551     nelim (IH ? B); #st3'; *; #C D;
    552     @ st3'; @; //;
    553     napply (star_trans ??? tA st2' ? tB); //;
    554     nelim A; /2/; *; //;
    555 ##] nqed.
     546#sim #st1 #t #st1' #H elim H;
     547[ #st1'' #st2 #Hmatch
     548    %{ st2} % //;
     549| #st1 #tA #st1A #tB #st1B #t #Hstep #Hstar #Ht #IH #st2 #Hmatch
     550    elim (simulation sim ??? Hstep ? Hmatch); #st2' *; #A #B
     551    elim (IH ? B); #st3' *; #C #D
     552    %{ st3'} % //;
     553    @(star_trans ??? tA st2' ? tB) //;
     554    elim A; /2/; *; //;
     555] qed.
    556556
    557557(*
Note: See TracChangeset for help on using the changeset viewer.