Changeset 3401

Timestamp:

Dec 6, 2013, 8:58:20 PM (6 years ago)

Author:

sacerdot

Message:

More goals closed, but some are false.

File:

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

LTS/Language.ma

@@ -85 +85 @@
 ].
 
+(*
 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → 
 (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2).
 #P #p #i1 elim i1
-[ * normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ 
-  (* destruct(EQ) gives no choice for ID(instructions_discr) *) cases daemon ]
-cases daemon (*TODO*)
-qed.
+[* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
+  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
+| #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/
+  #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //]
+  [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
+  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
+| cases daemon (*TODO*)
+qed.
+*)
 
 record env_params : Type[1] ≝ 
@@ -393 +399 @@
 (* ---------------------------------------- *) ⊢ 
     eqb_list D p1 p2 ≡ eqb X p1 p2.
-    check NonFunctionalLabel
 
 definition associative_list : DeqSet → Type[0] → Type[0] ≝ 
@@ -410 +415 @@
                 | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a 
                 ].
- 
+
+let rec domain_of_associative_list (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : list A ≝ 
+ match l with
+  [ nil ⇒ [] 
+  | cons x xs ⇒ \fst x :: domain_of_associative_list … xs 
+  ].
+
+lemma get_element_append_l:
+ ∀A,B. ∀l1,l2: associative_list A B. ∀x.
+  x ∈ domain_of_associative_list … l1 →
+   get_element … (l1@l2) x = get_element … l1 x.
+#A #B #l1 elim l1 normalize [ #l2 #x * ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd))
+#H [ >(\b H) | >(\bf H) ] normalize /2/
+qed.
+
+lemma get_element_append_r:
+ ∀A,B. ∀l1,l2: associative_list A B. ∀x.
+  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) →
+   get_element ?? (l1@l2) x = get_element … l2 x.
+#A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd))
+#H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I)
+qed.
+
 definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ 
 λx.〈a_non_functional_label x,S x〉.
@@ -755 +782 @@
 ]
 qed.
-  
+
+lemma lab_map_in_domain: ∀p.∀i: Instructions p.
+ ∀x,n,l.
+  x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) →
+   x ∈ get_labels_of_code … i.
+ cases daemon
+qed.
+
 lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
 no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
@@ -814 +848 @@
          >Hx %
     ]
-  |3: whd in H1; #x #Hx <H1 (*no duplicates *) cases daemon
+  |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 whd in H2; (*come sopra*) cases daemon
+  [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
-  |4: (* come sopra *) cases daemon
+  |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l
   ]
   >m_return_bind >IH1 //
-  [2,3,4: cases daemon (*come sopra*) ]
+  [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*)
+  |4: cases no_dup #_ * #_ @no_duplicates_append_l
+  ]
   >m_return_bind normalize nodelta whd in H1; <H1 
   [2: whd in match (get_labels_of_code ??); whd in match (memb ???);
@@ -832 +884 @@
       whd in match (memb ???); >(\b (refl …)) % ]
       whd in match (get_element ????); @eq_costlabel_elim normalize nodelta
-      [ #ABS cases daemon (*no duplicates *) ] #_ whd in match (get_element ????); 
+      [ #ABS cases daemon (*CSC: FALSO!! *) ] #_ whd in match (get_element ????); 
       >(\b (refl …)) normalize nodelta >(\b (refl …)) %
 |*: cases daemon (*TODO*)