Ignore:
Timestamp:
Oct 10, 2011, 3:54:59 PM (8 years ago)
Author:
sacerdot
Message:

Ported to new Matita destruct/inversion.
One lemma fails at qed. Replaced with an axiom ATM.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1244 r1336  
    3333lemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
    3434  if b then is_true v ty else is_false v ty.
    35 #v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev //;
    36 @False_ind @(absurd ? ev ?)
    37 [ 2: @sym_neq ] @bool_val_distinct
     35#v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev' //;
     36@⊥ cases (bool_val_distinct) #X @X [2: @sym_eq] @ev'
    3837qed.
    3938
     
    5150qed.
    5251
    53 definition 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'.
    54 #m #v #ty #ty' #v'
     52axiom 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'
    5554cases v;
    5655[ #H whd in H:(??%?); destruct;
     
    123122        ]
    124123    ]
    125 ] qed.
     124] qed.*)
    126125
    127126let rec expr_lvalue_ind
Note: See TracChangeset for help on using the changeset viewer.