Changeset 3401


Ignore:
Timestamp:
Dec 6, 2013, 8:58:20 PM (6 years ago)
Author:
sacerdot
Message:

More goals closed, but some are false.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3400 r3401  
    8585].
    8686
     87(*
    8788lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) →
    8889(i1 ≠ i2 → P false) → P (eq_instructions p i1 i2).
    8990#P #p #i1 elim i1
    90 [ * normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    91   (* destruct(EQ) gives no choice for ID(instructions_discr) *) cases daemon ]
    92 cases daemon (*TODO*)
    93 qed.
     91[* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
     92  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
     93| #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/
     94  #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //]
     95  [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
     96  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
     97| cases daemon (*TODO*)
     98qed.
     99*)
    94100
    95101record env_params : Type[1] ≝
     
    393399(* ---------------------------------------- *) ⊢
    394400    eqb_list D p1 p2 ≡ eqb X p1 p2.
    395     check NonFunctionalLabel
    396401
    397402definition associative_list : DeqSet → Type[0] → Type[0] ≝
     
    410415                | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a
    411416                ].
    412  
     417
     418let rec domain_of_associative_list (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : list A ≝
     419 match l with
     420  [ nil ⇒ []
     421  | cons x xs ⇒ \fst x :: domain_of_associative_list … xs
     422  ].
     423
     424lemma get_element_append_l:
     425 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
     426  x ∈ domain_of_associative_list … l1 →
     427   get_element … (l1@l2) x = get_element … l1 x.
     428#A #B #l1 elim l1 normalize [ #l2 #x * ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd))
     429#H [ >(\b H) | >(\bf H) ] normalize /2/
     430qed.
     431
     432lemma get_element_append_r:
     433 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
     434  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) →
     435   get_element ?? (l1@l2) x = get_element … l2 x.
     436#A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd))
     437#H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I)
     438qed.
     439
    413440definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝
    414441λx.〈a_non_functional_label x,S x〉.
     
    755782]
    756783qed.
    757  
     784
     785lemma lab_map_in_domain: ∀p.∀i: Instructions p.
     786 ∀x,n,l.
     787  x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) →
     788   x ∈ get_labels_of_code … i.
     789 cases daemon
     790qed.
     791
    758792lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
    759793no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
     
    814848         >Hx %
    815849    ]
    816   |3: whd in H1; #x #Hx <H1 (*no duplicates *) cases daemon
     850  |3: whd in H1; #x #Hx <H1
     851    [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l2 // >Hx // ]
     852    whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%);
     853    >get_element_append_r [ >get_element_append_r // % #K lapply (lab_map_in_domain … K)
     854    #K2 cases no_dup; #_ * #_ #no_dup3
     855    @(memb_no_duplicates_append … x … (no_duplicates_append_r … no_dup3)) // ]
     856    % #K lapply (lab_map_in_domain … K) #K2 cases no_dup; #_ * #_ #dup3
     857    @(memb_no_duplicates_append … x … dup3) // >memb_append_l2 // >Hx // ]
     858    cases no_dup #_ * #A1 #_ % #A2 <A2 in A1; * #K @K >memb_append_l2 //
     859    >memb_append_l2 // @Hx ] cases no_dup #A1 #_ % #A2 <A2 in A1; * #K @K
     860    >memb_cons // >memb_append_l2 // >memb_append_l2 // @Hx
    817861  |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |]
    818862  ]
    819  
    820863  normalize nodelta >IH2 //
    821   [2: #x #Hx whd in H2; (*come sopra*) cases daemon
     864  [2: #x #Hx <H2
     865    [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l1 // >Hx // ]
     866    whd in ⊢ (???%); >memb_append_l2 [2: >memb_append_l1] //
     867    cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*)
    822868  |3: (*no duplicates ok *) cases daemon
    823   |4: (* come sopra *) cases daemon
     869  |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l
    824870  ]
    825871  >m_return_bind >IH1 //
    826   [2,3,4: cases daemon (*come sopra*) ]
     872  [2: #x #Hx <H2
     873    [2: >memb_cons // >memb_cons // >memb_append_l1 // @Hx ]
     874    >memb_append_l1
     875    cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) 
     876  |3: cases daemon (*come sopra*)
     877  |4: cases no_dup #_ * #_ @no_duplicates_append_l
     878  ]
    827879  >m_return_bind normalize nodelta whd in H1; <H1
    828880  [2: whd in match (get_labels_of_code ??); whd in match (memb ???);
     
    832884      whd in match (memb ???); >(\b (refl …)) % ]
    833885      whd in match (get_element ????); @eq_costlabel_elim normalize nodelta
    834       [ #ABS cases daemon (*no duplicates *) ] #_ whd in match (get_element ????);
     886      [ #ABS cases daemon (*CSC: FALSO!! *) ] #_ whd in match (get_element ????);
    835887      >(\b (refl …)) normalize nodelta >(\b (refl …)) %
    836888|*: cases daemon (*TODO*)
Note: See TracChangeset for help on using the changeset viewer.