Changeset 3403

Timestamp:

Dec 19, 2013, 6:42:35 PM (6 years ago)

Author:

piccolo

Message:

 

File:

• LTS/Language.ma (modified) (4 diffs)

LTS/Language.ma

@@ -438 +438 @@
 qed.
 
+lemma get_element_append_l1 : 
+ ∀A,B. ∀l1,l2: associative_list A B. ∀x.
+  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) →
+   get_element ?? (l1@l2) x = get_element … l1 x.
+#A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ]
+#l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize
+[ * #H @⊥ @H % ] #H @IH assumption
+qed.
+   
 definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ 
 λx.〈a_non_functional_label x,S x〉.
@@ -752 +761 @@
 qed.
 
+lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
+no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
+#A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
+inversion (x == x1) normalize nodelta 
+[ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
+| #_ @IH //
+]
+qed.
+
+
+lemma same_to_keep_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l.
+no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → x ∈ dom1) →
+(∀x.x ∈ l3 → x ∈ dom3) → 
+same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l → 
+same_to_keep_on dom2 l2 l.
+#dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2
+#x #Hx inversion (x ∈ l2)
+ [ #EQkeep <H2 [> memb_append_l2 // >memb_append_l1 // ]
+   >memb_append_l2 // >memb_append_l1 // >Hx //
+ | #EQno_keep <H2
+   [2: >memb_append_l2 // >memb_append_l1 // >Hx //
+   | @sym_eq @memb_not_append [2: @memb_not_append //]
+   [ <associative_append in no_dup; #no_dup ]
+   lapply(memb_no_duplicates_append … x … no_dup) #H
+   inversion(memb ???) // #H1 cases H 
+   [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx //
+   | @sub_set3 >H1 //
+   | @sub_set1 >H1 //
+   ]
+   ]
+ ]
+qed.
+
+lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l.
+no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) →
+(∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) → 
+same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l → 
+same_fresh_map_on … dom2 l2 l.
+#dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1
+whd #x #Hx <H1
+[2: >memb_append_l2 // >memb_append_l1 // >Hx //]
+>get_element_append_r [ >get_element_append_l1 // ] % #K
+[ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS
+[ <associative_append in no_dup; #no_dup] @(memb_no_duplicates_append … x … no_dup)
+// [>memb_append_l2 | >memb_append_l1 ] // >Hx //
+qed.
+
+
 lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p.
 ∀x,n,l.
@@ -826 +883 @@
 qed.
 
-lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
-no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
-#A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
-inversion (x == x1) normalize nodelta 
-[ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
-| #_ @IH //
-]
-qed. 
+ 
   
 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
@@ -868 +918 @@
   #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
   #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 //
-  [2: #x #Hx whd in H2; inversion(x ∈ lab_to_keep … (call_post_trans …)) 
-    [ #EQkeep <H2 [ >memb_append_l2 // >memb_append_l2 // ] 
-      whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r >memb_append_l2 //
-      >memb_append_l2 // >Hx %
-    | #EQno_keep <H2 
-      [2: whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r
-          >memb_append_l2 // >memb_append_l2 // >Hx % ] @sym_eq @memb_not_append
-         [| @memb_not_append //] inversion(x ∈ lab_to_keep ??) // #Hlab @⊥
-         lapply(lab_to_keep_in_domain ????? (eq_true_to_b … Hlab)) #ABS      
-         cases no_dup #_ * #_ #ABS1
-         [ @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 //
-         | <associative_append in ABS1; #ABS1       
-           @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // >ABS %
+  [2: whd  in match (get_labels_of_code ??) in H2;
+      change with ([?;?]@?) in match (?::?) in H2;
+      <associative_append in H2; <associative_append
+      <(append_nil … (?@?)) <associative_append in ⊢ (??%? → ?);
+      <(append_nil … (?@?)) in ⊢ (??%? → ?); >associative_append
+      >associative_append in ⊢ (??%? → ?); #H2
+      @(same_to_keep_on_append … H2) // [ >append_nil
+      whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ]
+      #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r
+      [ >memb_append_l1 | >memb_append_l2 ] //
+      @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
+  |3: -H2 whd in match (get_labels_of_code ??) in H1;
+      change with ([?;?]@?) in match (?::?) in H1;
+      <associative_append in H1; <associative_append      
+      <(append_nil … (?@?)) >associative_append
+      change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?);
+      <associative_append in ⊢ (??%? → ?);
+      <associative_append in ⊢ (??%? → ?);
+      <(append_nil … (?@?)) in ⊢ (??%? → ?);
+      >associative_append in ⊢ (??%? → ?); #H1
+      @(same_fresh_map_on_append … H1) //
+      [ >append_nil >associative_append // ]
+      #x whd in match (memb ???); inversion(x == ltrue) 
+      [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue %
+      | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse)
+         [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse %
+         | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r
+           >domain_of_associative_list_append in Hx; #H
+           cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ]
+           // @(lab_map_in_domain … (eq_true_to_b … H2))
          ]
-         >Hx %
-    ]
-  |3: whd in H1; #x #Hx <H1
-    [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l2 // >Hx // ]
-    whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%);
-    >get_element_append_r [ >get_element_append_r // % #K lapply (lab_map_in_domain … K)
-    #K2 cases no_dup; #_ * #_ #no_dup3
-    @(memb_no_duplicates_append … x … (no_duplicates_append_r … no_dup3)) // ]
-    % #K lapply (lab_map_in_domain … K) #K2 cases no_dup; #_ * #_ #dup3
-    @(memb_no_duplicates_append … x … dup3) // >memb_append_l2 // >Hx // ]
-    cases no_dup #_ * #A1 #_ % #A2 <A2 in A1; * #K @K >memb_append_l2 //
-    >memb_append_l2 // @Hx ] cases no_dup #A1 #_ % #A2 <A2 in A1; * #K @K
-    >memb_cons // >memb_append_l2 // >memb_append_l2 // @Hx
+      ]
   |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |]
   ]
   normalize nodelta >IH2 //
-  [2: #x #Hx <H2
-    [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l1 // >Hx // ]
-    whd in ⊢ (???%); >memb_append_l2 [2: >memb_append_l1] //
-    cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*)
-  |3: (*no duplicates ok *) cases daemon
+  [2: whd  in match (get_labels_of_code ??) in H2;
+   change with ([?;?]@?) in match (?::?) in H2;
+   <associative_append in H2; #H2
+   @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ]
+   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
+  |3: whd  in match (get_labels_of_code ??) in H1;
+   change with ([?;?]@?) in match (?::?) in H1;
+   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
+   <associative_append in H1; <associative_append in ⊢ (??%? → ?); #H1
+   @(same_fresh_map_on_append … H1) // [2: /2 by lab_map_in_domain/ ]
+   #x >domain_of_associative_list_append #H cases(memb_append … H)
+   [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta
+     whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta
+     normalize #EQ destruct
+   | #H1 @orb_Prop_r @orb_Prop_r
+     @(lab_map_in_domain … (eq_true_to_b … H1))
+   ]
   |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l
   ]
   >m_return_bind >IH1 //
-  [2: #x #Hx <H2
-    [2: >memb_cons // >memb_cons // >memb_append_l1 // @Hx ]
-    >memb_append_l1 
-    cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*)  
-  |3: cases daemon (*come sopra*)
+  [2:  whd  in match (get_labels_of_code ??) in H2;
+   change with ([?;?]@?) in match (?::?) in H2;
+   change with ([ ] @ ?) in match (lab_to_keep ??) in H2;
+   >associative_append in H2 : (??%?); #H2
+   @(same_to_keep_on_append … H2) // [ #x *] #x #Hx cases(memb_append … Hx)
+   -Hx #Hx [ >memb_append_l1 | >memb_append_l2] //
+   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
+  |3:  whd  in match (get_labels_of_code ??) in H1;
+   change with ([?;?]@?) in match (?::?) in H1;
+   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
+    @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append
+    #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ]
+    // @(lab_map_in_domain … (eq_true_to_b … Hx))
   |4: cases no_dup #_ * #_ @no_duplicates_append_l
   ]