Changeset 882


Ignore:
Timestamp:
Jun 3, 2011, 5:35:32 PM (8 years ago)
Author:
campbell
Message:

Fix up fragile proofs for current version of matita.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r879 r882  
    195195| #ty #e #He whd in ⊢ (???%)
    196196    @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
    197     @eval_Ederef [ 3: >Hv in He #He @He | *: skip ]
     197    >Hv in He #He
     198    @eval_Ederef [ 3: @He | *: skip ]
    198199| #ty #e'' #ty'' #He'' @bind2_OK #x cases x #loc #ofs #tr #H
    199200  cases ty // *#pty
     
    367368    cases ty cases v // #v' #sz try #sg
    368369    @bind_OK #evs #CHECK
    369     @(evl_match_cons ??????? (P_res_to_P CHECK)) //
     370    @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECK)) //
    370371  ]
    371372] qed.
  • src/Clight/TypeComparison.ma

    r880 r882  
    1313definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
    1414#n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
    15 [ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed.
     15[ %1 | %2 ] lapply E @eqb_elim // #_ #H destruct qed.
    1616
    1717let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
  • src/Clight/toCminor.ma

    r881 r882  
    416416      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    417417      [ ASTptr r ⇒ λe1'.
    418           match access_mode ty return λx.access_mode ty = x → ? with
     418          match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    419419          [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
    420420          | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
  • src/RTLabs/import.ma

    r878 r882  
    6565  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
    6666  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    67   do graph ← foldr ?? (λp,g0. do g ← g0;
    68                               let 〈l,s〉 ≝ p in
    69                               do l' ← get_label l;
    70                               do s' ← s rmap get_label;
    71                               OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
     67  do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0.
     68                         do g ← g0;
     69                         let 〈l,s〉 ≝ p in
     70                         do l' ← get_label l;
     71                         do s' ← s rmap get_label;
     72                         OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
    7273  do entry ← get_label (pf_entry pre_f);
    7374  do exit ← get_label (pf_exit pre_f);
  • src/common/AST.ma

    r881 r882  
    213213}.
    214214
    215 (*
     215
    216216definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    217217  map ?? (fst ident F) (prog_funct ?? p).
     
    479479  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
    480480Qed.
    481 *)*)
     481*)
    482482(* * * External functions *)
    483483
  • src/utilities/extralib.ma

    r711 r882  
    387387definition div ≝ λm,n. fst ?? (divide m n).
    388388definition mod ≝ λm,n. snd ?? (divide m n).
    389 
    390 definition pairdisc ≝
    391 λA,B.λx,y:Prod A B.
    392 match x with
    393 [(pair t0 t1) ⇒
    394 match y with
    395 [(pair u0 u1) ⇒
    396   ∀P: Type[1].
    397   (∀e0: (eq A (R0 ? t0) u0).
    398    ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
    399 
    400 lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
    401 #A #B #x #y #e >e cases y;
    402 #a #b normalize;#P #PH @PH %
    403 qed.
    404389
    405390lemma pred_minus: ∀n,m. pred n - m = pred (n-m).
Note: See TracChangeset for help on using the changeset viewer.