Changeset 2557


Ignore:
Timestamp:
Dec 17, 2012, 2:35:30 PM (7 years ago)
Author:
tranquil
Message:

minor modification of commented (for now) proof of correctness of adds_graph

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2532 r2557  
    114114qed.
    115115
    116 
    117116(* use Russell? *)
    118117axiom adds_graph_list_ok :
     
    126125                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
    127126     src ~❨b,l❩~> dst in joint_if_code … def'.
    128 (* #p #g #l elim l
     127(*
     128#p #g #l elim l -l
    129129[ #src #def #_ #Hdef whd
    130   %{Hdef} %{[ ]} %%%
    131 | #hd #tl #IH #src #def #src_fresh #Hdef
    132   whd in match (adds_graph_list ?????);
    133   whd in match (fresh_label ???);
    134   @(pair_elim … (fresh ??)) normalize nodelta
    135   #mid #luniverse' #EQfresh
    136   whd in ⊢ (match % with [ _ ⇒ ?]);
    137   letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
    138   cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
    139   [ cases def // ] #EQ_aux
     130  %{Hdef} %{[ ]} %%% ]
     131#hd #tl #IH #src #def #src_fresh #Hdef
     132whd in match (adds_graph_list ?????);
     133whd in match (fresh_label ???);
     134@(pair_elim … (fresh ??)) normalize nodelta
     135#mid #luniverse' #EQfresh
     136whd in ⊢ (match % with [ _ ⇒ ?]);
     137letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
     138cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
     139  [ % ] #EQ_aux
    140140  lapply (IH mid def' ??)
    141141  [ #l whd in match def'; #Hpres
     
    157157  % [ % ]
    158158  [ whd in ⊢ (?%);
    159     elim (true_or_false_Prop (mid∈l)) #H >H normalize nodelta
    160     [ elim (All_memb … Hl2 H)
    161       cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in ⊢ (%→?);
    162       #H #_ @(absurd ?? H)
    163       @(fresh_remains_fresh … (eqEQfresh)
     159    cut (Not (bool_to_Prop (mid∈l)))
     160    [ % #H elim (All_memb … Hl2 H)
     161      whd in match (joint_if_luniverse ???);
     162      #G #_ @(absurd ?? G)
     163      @ (fresh_is_fresh … (sym_eq … EQfresh))
     164    | #H >H assumption
     165    ]
     166  | %
     167    [ %
     168      [
    164169      normalize #H10 #H11
    165170     
Note: See TracChangeset for help on using the changeset viewer.