Changeset 1635 for src/common

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

Location:

src/common

Files:

• Graphs.ma (modified) (2 diffs)
• Identifiers.ma (modified) (11 diffs)

src/common/Graphs.ma

@@ -36 +36 @@
     lookup ? ? (add ? ? g l s) l ≠ None ?.
 
+axiom graph_add_eq:
+  ∀A: Type[0].
+  ∀g: graph A.
+  ∀l: label.
+  ∀s: A.
+    lookup ? ? (add ? ? g l s) l = Some ? s.
+
 axiom graph_add_lookup:
   ∀A: Type[0].
@@ -43 +50 @@
   ∀to_insert: label.
     lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
+    
+axiom graph_add_preserve :
+  ∀A: Type[0].
+  ∀g: graph A.
+  ∀l: label.
+  ∀s: A.
+  ∀to_insert: label.
+  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
 
 axiom graph_num_nodes:

src/common/Identifiers.ma

@@ -40 +40 @@
   〈id',u'〉 = fresh tag u →
   fresh_for_univ tag id u'.
-#tag * #id * #id' * #u * #u' normalize #H #E destruct /2/
+#tag * #id * #id' * #u * #u' normalize #H #E destruct /2 by le_S/
 qed.
 
@@ -47 +47 @@
   〈id',u'〉 = fresh tag u →
   id ≠ id'.
-#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2/
+#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2 by absurd/
 qed.
 
@@ -59 +59 @@
   env_fresh_for_univ tag A (〈id,a〉::env) u'.
 #tag #A #env * #u * #u' #id #a
-#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
+#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2 by fresh_remains_fresh/ ]
 qed.
 
@@ -77 +77 @@
 #P #t * #x * #y #T #F
 change with (P (eqb ??))
-@(eqb_elim x y P) [ /2/ | * #H @F % #E destruct /2/ ]
+@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
 qed.
     
@@ -98 +98 @@
 
 lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
-#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
+#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2 by not_to_not/
 qed.
 
@@ -105 +105 @@
 #E [ % | %2 ]
 lapply E @eqb_elim
-[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
+[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2 by absurd/ ]
 qed.
 
@@ -123 +123 @@
 #tag #A #l elim l
 [ //
-| * #id #a #tl #IH #r * #H1 #H2 % /2/
+| * #id #a #tl #IH #r * #H1 #H2 % /2 by All_append_l/
 ] qed.
 
@@ -129 +129 @@
 #tag #A #l elim l
 [ //
-| * #id #a #tl #IH #r * #H1 #H2 /2/
+| * #id #a #tl #IH #r * #H1 #H2 /2 by /
 ] qed.
 
@@ -202 +202 @@
   lookup tag A (add tag A m j a) i = lookup tag A m i.
 #tag #A * #m * #i * #j #a #H
-@lookup_opt_insert_miss /2/
+@lookup_opt_insert_miss /2 by not_to_not/
 qed.
 
@@ -224 +224 @@
 cases (identifier_eq ? i j)
 [ #E >E >lookup_add_hit #H %1 destruct % //
-| #NE >lookup_add_miss /2/
+| #NE >lookup_add_miss /2 by or_intror, sym_not_eq/
 ] qed. 
 
@@ -328 +328 @@
 #FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?);
 generalize in ⊢ ((?(??%?) → ?) → ??%?); *
-[ // | #a #H @False_ind lapply (H ?) /2/ % #E destruct
+[ // | #a #H @False_ind lapply (H ?) /2 by absurd/ % #E destruct
 qed.