Ignore:
Timestamp:
Oct 10, 2011, 5:47:15 PM (10 years ago)
Author:
sacerdot
Message:

Ported to new destruct.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/CexecEquiv.ma

    r1244 r1344  
    136136    cases (exec_step ge s0) in H2 ⊢ %;
    137137    [ #o' #k' >(exec_inf_aux_unfold …)
    138         #E' whd in E':(??%?); destruct (E');
     138        #E' whd in E':(??%??); destruct (E');
    139139        #STEP
    140140        inversion H1;
    … …  
    149149        ]
    150150    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
    151         whd in ⊢ (??%? → ?); @is_final_elim'
    152         [ #r ] #F #E whd in E:(??%?); destruct
     151        whd in ⊢ (??%?? → ?); @is_final_elim'
     152        [ #r ] #F #E whd in E:(??%??); destruct
    153153    | #msg >(exec_inf_aux_unfold …)
    154         #E' whd in E':(??%?); destruct (E');
     154        #E' whd in E':(??%??); destruct (E');
    155155    ]
    156156] qed.
    … …  
    168168    cases (exec_step ge s0);
    169169    [ #o' #k'
    170         #E' whd in E':(??%?); destruct (E');
     170        #E' whd in E':(??%??); destruct (E');
    171171        #STEP
    172172        inversion H1;
    … …  
    174174            >(exec_inf_aux_unfold …) in E1;
    175175            cases (k' i);
    176             [ #o2 #k2 #E whd in E:(??%?); destruct (E)
    177             | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
     176            [ #o2 #k2 #E whd in E:(??%??); destruct (E)
     177            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    178178                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
    179179                @IFE
    180                 [ #r' #FINAL #E whd in E:(??%?);
     180                [ #r' #FINAL #E whd in E:(??%??);
    181181                    destruct (E);
    182182                    inversion FINAL;
    183183                    #r'' #m'' #E1 #E2 destruct (E1 E2); //;
    184                 | #NF #E whd in E:(??%?); destruct (E)
     184                | #NF #E whd in E:(??%??); destruct (E)
    185185                ]
    186             | #msg #E whd in E:(??%?); destruct (E)
     186            | #msg #E whd in E:(??%??); destruct (E)
    187187            ]
    188188       | #tr #s #e #e' #H #EXEC #E destruct (E)
    … …  
    190190       | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E)
    191191       ]
    192    | #x cases x; #tr #s whd in ⊢ (??%? → ?);
    193        @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct (E)
    194    | #msg #E whd in E:(??%?); destruct (E)
     192   | #x cases x; #tr #s whd in ⊢ (??%?? → ?);
     193       @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct (E)
     194   | #msg #E whd in E:(??%??); destruct (E)
    195195   ]
    196196] qed.
    … …  
    286286    >(exec_inf_aux_unfold …) in EXEC';
    287287    cases (exec_step ge s);
    288     [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    289     | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);
     288    [ #o #k #EXEC' whd in EXEC':(??%??); destruct (EXEC');
     289    | #x cases x; #tr'' #s' whd in ⊢ (??%?? → ?);
    290290        @is_final_elim' [ #r'' #FINAL | #F ]
    291         #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    292     | #msg #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     291        #EXEC' whd in EXEC':(??%??); destruct (EXEC');
     292    | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    293293    ]
    294294    inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2);
    … …  
    371371| >(exec_inf_aux_unfold …)
    372372    cases (exec_step ge s);
    373   [ #o #k #msg' #EXEC whd in EXEC:(??%?); destruct
    374   | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim'
    375       [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    376   | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?); destruct @refl
     373  [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct
     374  | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?) @is_final_elim'
     375      [ #r ] #F #EXEC whd in EXEC:(??%??); destruct
     376  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl
    377377  ]
    378378| #o #k #i #e #H #EXEC #E destruct
    … …  
    387387    >(exec_inf_aux_unfold …) in EXEC;
    388388    cases (exec_step ge s);
    389     [ #o #k #EXEC whd in EXEC:(??%?); destruct
    390     | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim'
    391         [ #r ] #F #E whd in E:(??%?); destruct @F
    392     | #msg #E whd in E:(??%?); destruct
     389    [ #o #k #EXEC whd in EXEC:(??%??); destruct
     390    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?) @is_final_elim'
     391        [ #r ] #F #E whd in E:(??%??); destruct @F
     392    | #msg #E whd in E:(??%??); destruct
    393393    ]
    394394| #msg #EXEC #E destruct
    … …  
    408408    >(exec_inf_aux_unfold …) in EXEC;
    409409    cases (exec_step ge s);
    410     [ #o1 #k1 #EXEC1 whd in EXEC1:(??%?); destruct (EXEC1);
     410    [ #o1 #k1 #EXEC1 whd in EXEC1:(??%??); destruct (EXEC1);
    411411        inversion H;
    412412        [ #tr1 #r1 #m1 #EXECK #E destruct (E);
    … …  
    414414            >(exec_inf_aux_unfold …) in EXECK;
    415415            cases (k1 i');
    416             [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct
    417             | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
     416            [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct
     417            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    418418                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
    419419                @IFE [ #r ] #F #EXECK
    420                 whd in EXECK:(??%?); destruct;
     420                whd in EXECK:(??%??); destruct;
    421421                @(absurd ?? F)
    422422                %{ r'} //;
    423             | #msg #E whd in E:(??%?); destruct
     423            | #msg #E whd in E:(??%??); destruct
    424424            ]
    425         | #msg #EXECK #E  whd in E:(??%?); destruct
     425        | #msg #EXECK #E  whd in E:(??%??); destruct
    426426        | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct
    427427        ]
    428     | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
    429         @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct;
    430     | #msg #E whd in E:(??%?); destruct
     428    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?);
     429        @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct;
     430    | #msg #E whd in E:(??%??); destruct
    431431    ]
    432432] qed.
    … …  
    659659    @isteps_interact //;
    660660] qed.
    661 
    662 (* XXX == > jmeq notation and coercion *)
    663 
    664 lemma jmeq_to_eq : ∀A:Type[0].∀a,b:A.jmeq A a A b → a = b.
    665 #A #a #b #E @gral @jm_to_eq_sigma @E
    666 qed.
    667 
    668 coercion jmeq_to_eq : ∀A:Type[0].∀a,b:A.∀p:jmeq A a A b.a = b ≝
    669   jmeq_to_eq on _p: jmeq ???? to eq ???.
    670 
    671 notation > "hvbox(a break ≃ b)"
    672   non associative with precedence 45
    673 for @{ 'jmeq ? $a ? $b }.
    674 
    675 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
    676   non associative with precedence 45
    677 for @{ 'jmeq $t $a $u $b }.
    678 
    679 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
    680 
    681 (* XXX < == *)
    682661
    683662lemma se_inv: ∀e1,e2.
Note: See TracChangeset for help on using the changeset viewer.