Ignore:
Timestamp:
Jan 7, 2012, 12:33:17 AM (9 years ago)
Author:
tranquil
Message:
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1631 r1635  
    4040  〈id',u'〉 = fresh tag u →
    4141  fresh_for_univ tag id u'.
    42 #tag * #id * #id' * #u * #u' normalize #H #E destruct /2/
     42#tag * #id * #id' * #u * #u' normalize #H #E destruct /2 by le_S/
    4343qed.
    4444
     
    4747  〈id',u'〉 = fresh tag u →
    4848  id ≠ id'.
    49 #tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2/
     49#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2 by absurd/
    5050qed.
    5151
     
    5959  env_fresh_for_univ tag A (〈id,a〉::env) u'.
    6060#tag #A #env * #u * #u' #id #a
    61 #H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
     61#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2 by fresh_remains_fresh/ ]
    6262qed.
    6363
     
    7777#P #t * #x * #y #T #F
    7878change with (P (eqb ??))
    79 @(eqb_elim x y P) [ /2/ | * #H @F % #E destruct /2/ ]
     79@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
    8080qed.
    8181   
     
    9898
    9999lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
    100 #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
     100#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2 by not_to_not/
    101101qed.
    102102
     
    105105#E [ % | %2 ]
    106106lapply E @eqb_elim
    107 [ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
     107[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2 by absurd/ ]
    108108qed.
    109109
     
    123123#tag #A #l elim l
    124124[ //
    125 | * #id #a #tl #IH #r * #H1 #H2 % /2/
     125| * #id #a #tl #IH #r * #H1 #H2 % /2 by All_append_l/
    126126] qed.
    127127
     
    129129#tag #A #l elim l
    130130[ //
    131 | * #id #a #tl #IH #r * #H1 #H2 /2/
     131| * #id #a #tl #IH #r * #H1 #H2 /2 by /
    132132] qed.
    133133
     
    202202  lookup tag A (add tag A m j a) i = lookup tag A m i.
    203203#tag #A * #m * #i * #j #a #H
    204 @lookup_opt_insert_miss /2/
     204@lookup_opt_insert_miss /2 by not_to_not/
    205205qed.
    206206
     
    224224cases (identifier_eq ? i j)
    225225[ #E >E >lookup_add_hit #H %1 destruct % //
    226 | #NE >lookup_add_miss /2/
     226| #NE >lookup_add_miss /2 by or_intror, sym_not_eq/
    227227] qed.
    228228
     
    328328#FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?);
    329329generalize in ⊢ ((?(??%?) → ?) → ??%?); *
    330 [ // | #a #H @False_ind lapply (H ?) /2/ % #E destruct
     330[ // | #a #H @False_ind lapply (H ?) /2 by absurd/ % #E destruct
    331331qed.
    332332
Note: See TracChangeset for help on using the changeset viewer.