Changeset 2307 for src/common


Ignore:
Timestamp:
Aug 30, 2012, 4:47:58 PM (7 years ago)
Author:
campbell
Message:

Half the proofs for sound cost labelling check.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2305 r2307  
    979979* #_ #H @H
    980980qed.
     981
     982lemma try_remove_this : ∀tag,A,m,id,a.
     983  lookup tag A m id = Some A a →
     984  ∃m'. try_remove tag A m id = Some ? 〈a,m'〉.
     985#tag #A * #m * #id #a #L
     986cases (pm_try_remove_some' A id m a L)
     987#m' #R %{(an_id_map tag A m')} whd in ⊢ (??%?); >R %
     988qed.
    981989 
    982990
  • src/common/PositiveMap.ma

    r2305 r2307  
    548548] qed.
    549549
    550 
    551 
     550lemma pm_try_remove_some' : ∀A,p,t,a.
     551  lookup_opt A p t = Some A a →
     552  ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉.
     553#A #p elim p
     554[ * [ #a #L normalize in L; destruct
     555    | #q #l #r #a #L normalize in L; destruct % [2: % | skip ]
     556    ]
     557| #q #IH *
     558  [ #a #L normalize in L; destruct
     559  | #x #l #r #a #L cases (IH r a L) #r' #R
     560    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
     561  ]
     562| #q #IH *
     563  [ #a #L normalize in L; destruct
     564  | #x #l #r #a #L cases (IH l a L) #l' #R
     565    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
     566  ]
     567] qed.
     568
     569
Note: See TracChangeset for help on using the changeset viewer.