Changeset 1350


Ignore:
Timestamp:
Oct 11, 2011, 2:27:53 AM (8 years ago)
Author:
sacerdot
Message:

Porting to latest destruct tactic.

Note: the tactics has a few remaining bugs to be ironed out.
Look for "Wilmer: XXX" comments in the .ma files to see where
these are avoided ATM using axioms.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1344 r1350  
    176176            [ #o2 #k2 #E whd in E:(??%??); destruct (E)
    177177            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    178                 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     178                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
     179                change in match (is_final ?????) with (is_final s2)
    179180                @IFE
    180181                [ #r' #FINAL #E whd in E:(??%??);
     
    416417            [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct
    417418            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    418                 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     419                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
     420                change in match (is_final ?????) with (is_final s2)
    419421                @IFE [ #r ] #F #EXECK
    420422                whd in EXECK:(??%??); destruct;
     
    687689    >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
    688690    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
     691    change in match (is_final ?????) with (is_final s'')
    689692    @is_final_elim
    690693    [ #r #F whd in ⊢ (?%? → ?); #S
     
    879882            cases (exec_step ge s');
    880883            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    881                 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     884                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    882885                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    883886                >(exec_inf_aux_unfold …)
     
    896899            cases (exec_step ge s');
    897900            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    898                 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     901                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    899902                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    900903                >(exec_inf_aux_unfold …)
  • src/Clight/CexecSound.ma

    r1342 r1350  
    2828
    2929lemma bool_val_distinct: Vtrue ≠ Vfalse.
    30 % #H whd in H:(??%%); destruct; @(absurd ? e0 one_not_zero)
     30% #H whd in H:(??%%); (*Wilmer: XXX*) cases daemon (*destruct; @(absurd ? e0 one_not_zero)*)
    3131qed.
    3232
     
    5151
    5252axiom exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
    53 (*#m #v #ty #ty' #v'
     53(*Wilmer: XXXX #m #v #ty #ty' #v'
    5454cases v;
    5555[ #H whd in H:(??%?); destruct;
  • src/Clight/TypeComparison.ma

    r1198 r1350  
    8787        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    8888        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    89 ]. destruct; //; qed.
     89]. try destruct // (*Wilmer:XXXX*) cases daemon qed.
    9090
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
  • src/common/AST.ma

    r1268 r1350  
    354354    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
    355355      cases (map_partial … f tl) in IH ⊢ %
    356       #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
     356      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize
    357357      >(IH x) // ]]
    358358qed.
     
    486486 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
    487487 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
    488    #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
     488   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ % >e0 //
    489489   >e0 in e1; normalize #H @H ]
    490490qed.
  • src/utilities/extralib.ma

    r1338 r1350  
    522522 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
    523523#m #n @(pos_cases … n)
    524 [ >(divide_by_one m) #dv #md #H destruct /2/
     524[ >(divide_by_one m) #dv #md #H destruct normalize /2/
    525525| #n' elim m;
    526526  [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/
     
    540540          lapply (partial_minus_to_Prop md'' n);
    541541          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
    542           #lt #e destruct % [ /3/ | *: /2/ ] @plt_pos
     542          #lt #e destruct % [ normalize /3/ | *: normalize /2/ ] @plt_pos
    543543          [ 1,3,5,7: @double_lt1 /2/;
    544544          | 2,4: @double_lt3 /2/;
Note: See TracChangeset for help on using the changeset viewer.