Ignore:
Timestamp:
Nov 7, 2012, 6:02:50 PM (8 years ago)
Author:
garnier
Message:

Moved general stuff on memories from switchRemoval to MemProperties?, e.g. on loading, storing and free, as an
attempt to reduce the typechecking time of switchRemoval.ma.
Moved some other generic stuff on vectors from SimplifyCasts? to frontend_misc.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2438 r2441  
    7575 match e with
    7676 [ None ⇒ None ?
    77  | Some x ⇒ f x ] = Some ? res → 
     77 | Some x ⇒ f x ] = Some ? res →
    7878 ∃x. e = Some ? x ∧ f x = Some ? res.
    7979 #A #B #e #res #f cases e normalize nodelta
    8080[ 1: #Habsurd destruct (Habsurd)
    81 | 2: #a #Heq %{a} @conj >Heq @refl ] 
     81| 2: #a #Heq %{a} @conj >Heq @refl ]
    8282qed.
    8383
     
    330330lemma mem_append_backwards : ∀A:Type[0]. ∀elt : A. ∀l1,l2. (mem … elt l1) ∨ (mem … elt l2) → mem … elt (l1 @ l2) .
    331331#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #_ #H' @H' @H qed.
     332
     333(* "Observational" equivalence on list implies concrete equivalence. Useful to
     334 * prove equality from some reasoning on indexings. Needs a particular induction
     335 * principle. *)
     336 
     337let rec double_list_ind
     338  (A : Type[0])
     339  (P : list A → list A → Prop)
     340  (base_nil  : P [ ] [ ])
     341  (base_l1   : ∀hd1,l1. P (hd1::l1) [ ])
     342  (base_l2   : ∀hd2,l2. P [ ] (hd2::l2))
     343  (ind  : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2))
     344  (l1, l2 : list A) on l1 ≝
     345match l1 with
     346[ nil ⇒
     347  match l2 with
     348  [ nil ⇒ base_nil
     349  | cons hd2 tl2 ⇒ base_l2 hd2 tl2 ]
     350| cons hd1 tl1 ⇒ 
     351  match l2 with
     352  [ nil ⇒ base_l1 hd1 tl1
     353  | cons hd2 tl2 ⇒
     354    ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2)
     355  ]
     356]. 
     357
     358lemma nth_eq_tl :
     359  ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2.
     360  (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) →
     361  (∀i. nth_opt A i l1 = nth_opt A i l2).
     362#A #l1 #l2 @(double_list_ind … l1 l2)
     363[ 1: #hd1 #hd2 #_ #i elim i try /2/
     364| 2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
     365| 3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
     366| 4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2
     367     #Hind
     368     @(λi. Hind (S i))
     369] qed.     
     370
     371
     372lemma nth_eq_to_eq :
     373  ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2.
     374#A #l1 elim l1
     375[ 1: #l2 #H lapply (H 0) normalize
     376     cases l2
     377     [ 1: //
     378     | 2: #hd2 #tl2 normalize #Habsurd destruct ]
     379| 2: #hd1 #tl1 #Hind *
     380     [ 1: #H lapply (H 0) normalize #Habsurd destruct
     381     | 2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq)
     382          >(Hind tl2) try @refl @(nth_eq_tl … H)
     383     ]
     384] qed.
     385
     386(* --------------------------------------------------------------------------- *)
     387(* General results on vectors. *)
     388(* --------------------------------------------------------------------------- *)
     389
     390(* copied from AssemblyProof, TODO get rid of the redundant stuff. *)
     391lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
     392 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
     393 #n #hd #tl #abs @⊥ destruct (abs)
     394qed.
     395
     396lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
     397 ∃hd.∃tl.v ≃ VCons A n hd tl.
     398 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
     399 [ #abs @⊥ destruct (abs)
     400 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     401qed.
     402
     403lemma vector_append_zero:
     404  ∀A,m.
     405  ∀v: Vector A m.
     406  ∀q: Vector A 0.
     407    v = q@@v.
     408  #A #m #v #q
     409  >(Vector_O A q) %
     410qed.
     411
     412corollary prod_vector_zero_eq_left:
     413  ∀A, n.
     414  ∀q: Vector A O.
     415  ∀r: Vector A n.
     416    〈q, r〉 = 〈[[ ]], r〉.
     417  #A #n #q #r
     418  generalize in match (Vector_O A q …);
     419  #hyp
     420  >hyp in ⊢ (??%?);
     421  %
     422qed.
     423 
     424lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
     425# A #m #n elim m
     426[ 1: normalize #v
     427  elim (Vector_Sn ?? v) #hd * #tl #Eq
     428  @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
     429  >Eq normalize //
     430| 2: #n' #Hind #v
     431  elim (Vector_Sn ?? v) #hd * #tl #Eq
     432  elim (Hind tl)
     433  #tl1 * #tl2 #Eq_tl
     434  @(ex_intro … (hd ::: tl1))
     435  @(ex_intro … tl2) 
     436  destruct normalize //
     437] qed.
     438
     439lemma vsplit_zero:
     440  ∀A,m.
     441  ∀v: Vector A m.
     442    〈[[]], v〉 = vsplit A 0 m v.
     443  #A #m #v
     444  elim v
     445  [ %
     446  | #n #hd #tl #ih
     447    normalize in ⊢ (???%); %
     448  ]
     449qed.
     450
     451lemma vsplit_zero2:
     452  ∀A,m.
     453  ∀v: Vector A m.
     454    〈[[]], v〉 = vsplit' A 0 m v.
     455  #A #m #v
     456  elim v
     457  [ %
     458  | #n #hd #tl #ih
     459    normalize in ⊢ (???%); %
     460  ]
     461qed.
     462
     463lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
     464# A #m #n elim m
     465[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
     466| 2: #n' #Hind #v
     467  elim (Vector_Sn ?? v) #hd * #tl #Eq
     468  elim (Hind tl)
     469  #tl1 * #tl2 #Eq_tl
     470  @(ex_intro … (hd ::: tl1))
     471  @(ex_intro … tl2) 
     472  destruct normalize //
     473] qed.
     474
     475(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
     476 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
     477axiom vsplit_succ:
     478  ∀A, m, n.
     479  ∀l: Vector A m.
     480  ∀r: Vector A n.
     481  ∀v: Vector A (m + n).
     482  ∀hd.
     483    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
     484
     485axiom vsplit_succ2:
     486  ∀A, m, n.
     487  ∀l: Vector A m.
     488  ∀r: Vector A n.
     489  ∀v: Vector A (m + n).
     490  ∀hd.
     491    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
     492     
     493lemma vsplit_prod2:
     494  ∀A,m,n.
     495  ∀p: Vector A (m + n).
     496  ∀v: Vector A m.
     497  ∀q: Vector A n.
     498    p = v@@q → 〈v, q〉 = vsplit' A m n p.
     499  #A #m
     500  elim m
     501  [ #n #p #v #q #hyp
     502    >hyp <(vector_append_zero A n q v)
     503    >(prod_vector_zero_eq_left A …)
     504    @vsplit_zero2
     505  | #r #ih #n #p #v #q #hyp
     506    >hyp
     507    cases (Vector_Sn A r v)
     508    #hd #exists
     509    cases exists
     510    #tl #jmeq >jmeq
     511    @vsplit_succ2 [1: % |2: @ih % ]
     512  ]
     513qed.
     514
     515lemma vsplit_prod:
     516  ∀A,m,n.
     517  ∀p: Vector A (m + n).
     518  ∀v: Vector A m.
     519  ∀q: Vector A n.
     520    p = v@@q → 〈v, q〉 = vsplit A m n p.
     521  #A #m
     522  elim m
     523  [ #n #p #v #q #hyp
     524    >hyp <(vector_append_zero A n q v)
     525    >(prod_vector_zero_eq_left A …)
     526    @vsplit_zero
     527  | #r #ih #n #p #v #q #hyp
     528    >hyp
     529    cases (Vector_Sn A r v)
     530    #hd #exists
     531    cases exists
     532    #tl #jmeq >jmeq
     533    @vsplit_succ [1: % |2: @ih % ]
     534  ]
     535qed.
     536
    332537
    333538(* --------------------------------------------------------------------------- *)
Note: See TracChangeset for help on using the changeset viewer.