Changeset 891 for src/Clight


Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

Location:
src/Clight
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r880 r891  
    344344] qed.
    345345
    346 definition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
    347 λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
     346definition is_Sskip : ∀s:statement. (s = Sskip) (s ≠ Sskip) ≝
     347λs.match s return λs'.(s' = Sskip) (s' ≠ Sskip) with
    348348[ Sskip ⇒ inl ?? (refl ??)
    349349| _ ⇒ inr ?? (nmk ? (λH.?))
  • src/Clight/CexecComplete.ma

    r879 r891  
    167167| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    168168    [ #id | #e' | #e' #id ] #H3
    169     whd in ⊢ (??%?);
     169    whd in ⊢ (??%?)
     170    [ change in H3:(??%?) with (exec_lvalue' ge env m (Evar id) ty)
     171    | change in H3:(??%?) with (exec_lvalue' ge env m (Ederef e') ty)
     172    | change in H3:(??%?) with (exec_lvalue' ge env m (Efield e' id) ty)
     173    ]
    170174    >(yields_eq ??? H3)
    171     whd in ⊢ (??%?); >H2 @refl
     175    whd in ⊢ (??%?) change in H2:(??%?) with (load_value_of_type' ty m 〈l,off〉)
     176    >H2 @refl
    172177| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
    173178    >(yields_eq ??? H2) whd in ⊢ (??%?)
     
    352357#ge #s #tr #s' #H elim H;
    353358[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
    354     >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
    355     >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
     359    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?)
     360    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?)
     361    change in H3:(??%?) with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)
    356362    >H3 @refl
    357363| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
     
    443449    @refl
    444450| #v #f #env #k #m @refl
    445 | #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?);
    446     >H @refl
     451| #v #f #env #k #m1 #m2 #loc #ofs #ty
     452    change in ⊢ (??%? → ?) with (store_value_of_type' ty m1 〈loc,ofs〉 v)
     453    #H whd in ⊢ (??%?) >H @refl
    447454| #f #l #s #k #env #m @refl
    448455] qed.
  • src/Clight/CexecEquiv.ma

    r798 r891  
    5252 (∀r. final_state s r → P (Some ? r)) →
    5353 ((¬∃r.final_state s r) → P (None ?)) →
    54 P (is_final ?? clight_exec s).
    55 #s #P #F #NF lapply (refl ? (is_final ?? clight_exec s))
    56 cases (is_final ?? clight_exec s) in ⊢ (???% → %)
    57 [ #E @NF % * #r #H > (is_final_complete … H) in E #H destruct
     54P (is_final s).
     55#s #P #F #NF lapply (refl ? (is_final s))
     56cases (is_final s) in ⊢ (???% → %)
     57[ #E @NF % * #r #H whd in E:(??%?) > (is_final_complete … H) in E #H destruct
    5858| #r #E @F @is_final_sound @E
    5959] qed.
     60
     61lemma is_final_elim': ∀s.∀P:option int → Type[0].
     62 (∀r. final_state s r → P (Some ? r)) →
     63 ((¬∃r.final_state s r) → P (None ?)) →
     64P (is_final io_out io_in clight_fullexec s).
     65@is_final_elim qed.
    6066
    6167lemma exec_e_step: ∀ge,x,tr,s,e.
     
    6672[ #o #k #EXEC whd in EXEC:(??%?); destruct
    6773| #y cases y #tr' #s' whd in ⊢ (??%? → ?)
    68   @is_final_elim 
     74  @is_final_elim'
    6975  [ #r #FINAL | #FINAL ]
    7076  #EXEC whd in EXEC:(??%?); destruct @refl
     
    7985[ #o #k #EXEC whd in EXEC:(??%?); destruct
    8086| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    81   @is_final_elim
     87  @is_final_elim'
    8288  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
    8389  destruct @refl
     
    9298[ #o #k #EXEC whd in EXEC:(??%?); destruct
    9399| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
    94   @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
     100  @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    95101| #msg #EXEC whd in EXEC:(??%?); destruct
    96102] qed.
     
    143149        ]
    144150    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
    145         whd in ⊢ (??%? → ?); @is_final_elim
     151        whd in ⊢ (??%? → ?); @is_final_elim'
    146152        [ #r ] #F #E whd in E:(??%?); destruct
    147153    | #msg >(exec_inf_aux_unfold …)
     
    170176            [ #o2 #k2 #E whd in E:(??%?); destruct (E)
    171177            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    172                 @is_final_elim
     178                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     179                @IFE
    173180                [ #r' #FINAL #E whd in E:(??%?);
    174181                    destruct (E);
     
    184191       ]
    185192   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
    186        @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E)
     193       @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct (E)
    187194   | #msg #E whd in E:(??%?); destruct (E)
    188195   ]
     
    281288    [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    282289    | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);
    283         @is_final_elim [ #r'' #FINAL | #F ]
     290        @is_final_elim' [ #r'' #FINAL | #F ]
    284291        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    285292    | #msg #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     
    299306>(exec_inf_aux_unfold …) cases x;
    300307[ #o #k #EXEC whd in EXEC:(??%?); destruct;
    301 | #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim
     308| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim'
    302309  [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
    303310      destruct (EXEC); @refl
     
    365372    cases (exec_step ge s);
    366373  [ #o #k #msg' #EXEC whd in EXEC:(??%?); destruct
    367   | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim
     374  | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim'
    368375      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    369376  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?); destruct @refl
     
    381388    cases (exec_step ge s);
    382389    [ #o #k #EXEC whd in EXEC:(??%?); destruct
    383     | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
     390    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim'
    384391        [ #r ] #F #E whd in E:(??%?); destruct @F
    385392    | #msg #E whd in E:(??%?); destruct
     
    409416            [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct
    410417            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    411                 @is_final_elim [ #r ] #F #EXECK
     418                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     419                @IFE [ #r ] #F #EXECK
    412420                whd in EXECK:(??%?); destruct;
    413421                @(absurd ?? F)
     
    419427        ]
    420428    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
    421         @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct;
     429        @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct;
    422430    | #msg #E whd in E:(??%?); destruct
    423431    ]
     
    707715    ]
    708716| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?)
    709     @is_final_elim [ #r ] #F #E whd in E:(?%?);
     717    @is_final_elim' [ #r ] #F #E whd in E:(?%?);
    710718    inversion E;
    711719    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
     
    898906                #F #S whd in S:(?%?); cases (se_inv … S);
    899907            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
    900                 @is_final_elim [ #r ] #F #S whd in S:(?%?);
     908                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    901909                cases (se_inv … S);
    902910            | #msg #S cases (se_inv … S);
     
    915923                #F #S whd in S:(?%?); cases (se_inv … S);
    916924            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
    917                 @is_final_elim [ #r ] #F #S whd in S:(?%?);
     925                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    918926                cases (se_inv … S);
    919927            | #msg #S cases (se_inv … S);
     
    9951003  ∃e'.e = e_step ??? E0 s e'.
    9961004#ge #s #e >(exec_inf_aux_unfold …)
    997 whd in ⊢ (??%? → ?) @is_final_elim
     1005whd in ⊢ (??%? → ?) @is_final_elim'
    9981006[ #r #FINAL #EXEC #NOTFINAL
    9991007    @False_ind @(absurd ?? NOTFINAL)
     
    10091017#classic #constructive_indefinite_description #p #e
    10101018whd in ⊢ (?%? → ??(λ_.?(?%?)%));
    1011 lapply (make_initial_state_sound p);
    1012 lapply (the_initial_state p);
    1013 cases (make_initial_state p);
     1019lapply (make_initial_state_sound p)
     1020lapply (the_initial_state p)
     1021whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?)
     1022cases (make_initial_state p)
    10141023[ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    10151024    cases INITIAL; #Ege #INITIAL''
    1016     >(exec_inf_aux_unfold …)
     1025    >exec_inf_aux_unfold
    10171026    whd in ⊢ (?%? → ?)
    1018     @is_final_elim
     1027    @is_final_elim'
    10191028    [ #r #F @False_ind
    10201029        @(absurd ?? (initial_state_not_final … INITIAL''))
     
    10251034    lapply (behavior_of_execution ??
    10261035              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
    1027         *; #b #MATCHES %{b} % //;
     1036        *; #b #MATCHES %{b} % [ @MATCHES ]
    10281037        #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ]
    10291038        inversion MATCHES;
  • src/Clight/CexecSound.ma

    r882 r891  
    33(*include "Plogic/connectives.ma".*)
    44
     5(* Is rather careful about using destruct because it currently uses excessive
     6   normalization. *)
    57lemma exec_bool_of_val_sound: ∀v,ty,r.
    68 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    79#v #ty #r
    810cases v; [ | #i | #f | #r1 | #r' #b #pc #of ]
    9 cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #r #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    10 #H whd in H:(??%?); destruct;
    11 [ lapply (eq_spec i zero); elim (eq i zero);
    12   [ #e >e @bool_of_val_false //;
    13   | #ne (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vint i) (Tint sz sg)) normalize #H @H /2/;
    14   ]
    15 | elim (eq_dec f Fzero);
    16   [ #e >e >(Feq_zero_true …) @bool_of_val_false //;
    17   | #ne >(Feq_zero_false …) //; (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vfloat f) (Tfloat sz)) normalize #H @H /2/;
    18   ]
    19 | @bool_of_val_false //
    20 | (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vptr r' b pc of) (Tpointer r ty)) normalize #H @H //
     11cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
     12#H whd in H:(??%?);
     13[ 2: lapply (eq_spec i zero) cases (eq i zero) in H ⊢ %
     14  [ #E1 #E2 destruct @bool_of_val_false @is_false_int
     15  | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E2 | destruct @refl ]
     16  ]
     17| 8: cases (eq_dec f Fzero)
     18  [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
     19  | #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne | destruct @refl ]
     20  ]
     21| 14: >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
     22| 15: >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
     23| *: destruct
    2124] qed.
    2225
     
    197200    >Hv in He #He
    198201    @eval_Ederef [ 3: @He | *: skip ]
    199 | #ty #e'' #ty'' #He'' @bind2_OK #x cases x #loc #ofs #tr #H
    200   cases ty // *#pty
     202| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
     203  cases ty // * #pty
    201204  cases loc in H ⊢ % * #loc' #H
    202205  whd try @I
    203   @eval_Eaddrof >H in He'' #He'' @He''
     206  @eval_Eaddrof whd in H:(??%?) >H in He'' #He'' @He''
    204207| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    205208    @opt_bind_OK #v #ev
     
    221224    @bind_OK #b
    222225    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
    223     @bind2_OK #v #tr #Hv
     226    @bind2_OK #v #tr #Hv whd in Hv:(??%?)
    224227    [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
    225228        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
     
    248251| #ty #e' #ty' #i cases ty'; //;
    249252    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
    250         @bind_OK #delta #Hdelta >H in He' #He'
     253        @bind_OK #delta #Hdelta whd in H:(??%?) >H in He' #He'
    251254        @(eval_Efield_struct …  He' (refl ??) Hdelta)
    252     | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
     255    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?)
    253256        >H in He' #He'
    254257        @(eval_Efield_union … He' (refl ??))
     
    300303cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    301304[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
    302     @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ /2/ ]
     305    @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
    303306    lapply (addrof_exec_lvalue … H) #H'
    304307    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
  • src/Clight/TypeComparison.ma

    r882 r891  
    1616
    1717let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
    18 match t1 return λt'. (t' = t2) + (t' ≠ t2) with
    19 [ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    20 | Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
     18match t1 return λt'. Sum (t' = t2) (t' ≠ t2) with
     19[ Tvoid ⇒ match t2 return λt'. Sum (Tvoid = t') (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     20| Tint sz sg ⇒ match t2 return λt'. Sum (Tint ?? = t') (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
    2121    match sz_eq_dec sz sz' with [ inl e1 ⇒
    2222    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
     
    2424    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    2525    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    26 | Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
     26| Tfloat f ⇒ match t2 return λt'. Sum (Tfloat ? = t') (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
    2727    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
    2828    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    2929    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    30 | Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
     30| Tpointer s t ⇒ match t2 return λt'. Sum (Tpointer ?? = t') (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
    3131    match eq_region_dec s s' with [ inl e1 ⇒
    3232      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
    3333      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
    3434    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    35 | Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
     35| Tarray s t n ⇒ match t2 return λt'. Sum (Tarray ??? = t') (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
    3636    match eq_region_dec s s' with [ inl e1 ⇒
    3737      match type_eq_dec t t' with [ inl e2 ⇒
     
    4141        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    4242        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    43 | Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
     43| Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
    4444    match typelist_eq_dec tl tl' with [ inl e1 ⇒
    4545    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
     
    4848  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    4949| Tstruct i fl ⇒
    50     match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
     50    match t2 return λt'. Sum (Tstruct ?? = t') (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
    5151    match ident_eq i i' with [ inl e1 ⇒
    5252    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
     
    5555    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    5656| Tunion i fl ⇒
    57     match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
     57    match t2 return λt'. Sum (Tunion ?? = t') (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
    5858    match ident_eq i i' with [ inl e1 ⇒
    5959    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
     
    6161    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    6262    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
    63 | Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
     63| Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
    6464    match eq_region_dec r r' with [ inl e1 ⇒
    6565      match ident_eq i i' with [ inl e2 ⇒ inl ???
     
    6868    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    6969]
    70 and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
    71 match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
    72 [ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    73 | Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
     70and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝
     71match tl1 return λtl'. Sum (tl' = tl2) (tl' ≠ tl2) with
     72[ Tnil ⇒ match tl2 return λtl'. Sum (Tnil = tl') (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     73| Tcons t1 ts1 ⇒ match tl2 return λtl'. Sum (Tcons ?? = tl') (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
    7474    match type_eq_dec t1 t2 with [ inl e1 ⇒
    7575    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
     
    7777    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    7878]
    79 and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
    80 match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
    81 [ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    82 | Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
     79and fieldlist_eq_dec (fl1,fl2:fieldlist) : Sum (fl1 = fl2) (fl1 ≠ fl2) ≝
     80match fl1 return λfl'. Sum (fl' = fl2) (fl' ≠ fl2) with
     81[ Fnil ⇒ match fl2 return λfl'. Sum (Fnil = fl') (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     82| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. Sum (Fcons ??? = fl') (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
    8383    match ident_eq i1 i2 with [ inl e1 ⇒
    8484      match type_eq_dec t1 t2 with [ inl e2 ⇒
Note: See TracChangeset for help on using the changeset viewer.