Changeset 2121 for src/ASM/Vector.ma


Ignore:
Timestamp:
Jun 27, 2012, 3:30:58 PM (8 years ago)
Author:
sacerdot
Message:

More functions moved to the places they belong to

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r2032 r2121  
    2121  VEmpty: Vector A O
    2222| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
     23
     24lemma Vector_O:
     25  ∀A: Type[0].
     26  ∀v: Vector A 0.
     27    v ≃ VEmpty A.
     28 #A #v
     29 generalize in match (refl … 0);
     30 cases v in ⊢ (??%? → ?%%??); //
     31 #n #hd #tl #absurd
     32 destruct(absurd)
     33qed.
     34
     35lemma Vector_Sn:
     36  ∀A: Type[0].
     37  ∀n: nat.
     38  ∀v: Vector A (S n).
     39    ∃hd: A. ∃tl: Vector A n.
     40      v ≃ VCons A n hd tl.
     41  #A #n #v
     42  generalize in match (refl … (S n));
     43  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
     44  [1:
     45    #absurd destruct(absurd)
     46  |2:
     47    #m #hd #tl #eq
     48    <(injective_S … eq)
     49    %{hd} %{tl} %
     50  ]
     51qed.
    2352
    2453(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    194223 vsplit' A m n v.
    195224
     225lemma vsplit_zero:
     226  ∀A,m.
     227  ∀v: Vector A m.
     228    〈[[]], v〉 = vsplit A 0 m v.
     229  #A #m #v
     230  cases v try %
     231  #n #hd #tl %
     232qed.
     233
    196234definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
    197235  λA: Type[0].
     
    326364   
    327365interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
     366
     367lemma vector_append_zero:
     368  ∀A,m.
     369  ∀v: Vector A m.
     370  ∀q: Vector A 0.
     371    v = q@@v.
     372  #A #m #v #q
     373  >(Vector_O A q) %
     374qed.
     375
     376lemma vector_cons_empty:
     377  ∀A: Type[0].
     378  ∀n: nat.
     379  ∀v: Vector A n.
     380    [[ ]] @@ v = v.
     381  #A #n #v
     382  cases v try %
     383  #n' #hd #tl %
     384qed.
    328385
    329386lemma vector_cons_append:
     
    367424qed.
    368425
     426lemma tail_head:
     427  ∀a: Type[0].
     428  ∀m, n: nat.
     429  ∀hd: a.
     430  ∀l: Vector a m.
     431  ∀r: Vector a n.
     432    tail a ? (hd:::(l@@r)) = l@@r.
     433  #a #m #n #hd #l #r
     434  cases l try %
     435  #m' #hd' #tl' %
     436qed.
     437
     438lemma head_head':
     439  ∀a: Type[0].
     440  ∀m: nat.
     441  ∀hd: a.
     442  ∀l: Vector a m.
     443    hd = head' … (hd:::l).
     444  #a #m #hd #l cases l try %
     445  #m' #hd' #tl %
     446qed.
     447
    369448axiom vsplit_elim':
    370449  ∀A: Type[0].
     
    386465      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
    387466        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
    388    
     467
     468lemma vsplit_succ:
     469  ∀A: Type[0].
     470  ∀m, n: nat.
     471  ∀l: Vector A m.
     472  ∀r: Vector A n.
     473  ∀v: Vector A (m + n).
     474  ∀hd: A.
     475    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
     476  #A #m
     477  elim m
     478  [1:
     479    #n #l #r #v #hd #eq #hyp
     480    destruct >(Vector_O … l) %
     481  |2:
     482    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
     483    destruct
     484    cases (Vector_Sn … l) #hd' #tl'
     485    whd in ⊢ (???%);
     486    >tail_head
     487    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
     488    try (<hyp <head_head' %)
     489    elim l normalize //
     490  ]
     491qed.
     492
     493corollary prod_vector_zero_eq_left:
     494  ∀A, n.
     495  ∀q: Vector A O.
     496  ∀r: Vector A n.
     497    〈q, r〉 = 〈[[ ]], r〉.
     498  #A #n #q #r
     499  generalize in match (Vector_O A q …);
     500  #hyp destruct %
     501qed.
     502
     503lemma vsplit_prod:
     504  ∀A: Type[0].
     505  ∀m, n: nat.
     506  ∀p: Vector A (m + n).
     507  ∀v: Vector A m.
     508  ∀q: Vector A n.
     509    p = v@@q → 〈v, q〉 = vsplit A m n p.
     510  #A #m elim m
     511  [1:
     512    #n #p #v #q #hyp
     513    >hyp <(vector_append_zero A n q v)
     514    >(prod_vector_zero_eq_left A …)
     515    @vsplit_zero
     516  |2:
     517    #r #ih #n #p #v #q #hyp
     518    >hyp
     519    cases (Vector_Sn A r v) #hd #exists
     520    cases exists #tl #jmeq
     521    >jmeq @vsplit_succ try %
     522    @ih %
     523  ]
     524qed.
     525
     526definition vsplit_elim:
     527  ∀A: Type[0].
     528  ∀l, m: nat.
     529  ∀v: Vector A (l + m).
     530  ∀P: (Vector A l) × (Vector A m) → Prop.
     531    (∀vl: Vector A l.
     532     ∀vm: Vector A m.
     533      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
     534  λa: Type[0].
     535  λl, m: nat.
     536  λv: Vector a (l + m).
     537  λP. ?.
     538  cases daemon
     539qed.
     540
     541axiom vsplit_append:
     542  ∀A: Type[0].
     543  ∀m, n: nat.
     544  ∀v, v': Vector A m.
     545  ∀q, q': Vector A n.
     546    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
     547      v = v' ∧ q = q'.
     548
     549lemma vsplit_vector_singleton:
     550  ∀A: Type[0].
     551  ∀n: nat.
     552  ∀v: Vector A (S n).
     553  ∀rest: Vector A n.
     554  ∀s: Vector A 1.
     555    v = s @@ rest →
     556    ((get_index_v A ? v 0 ?) ::: rest) = v.
     557  [1:
     558    #A #n #v cases daemon (* XXX: !!! *)
     559  |2:
     560    @le_S_S @le_O_n
     561  ]
     562qed.
     563
    389564let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
    390565                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
     
    593768qed.
    594769
     770lemma mem_monotonic_wrt_append:
     771  ∀A: Type[0].
     772  ∀m, o: nat.
     773  ∀eq: A → A → bool.
     774  ∀reflex: ∀a. eq a a = true.
     775  ∀p: Vector A m.
     776  ∀a: A.
     777  ∀r: Vector A o.
     778    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
     779  #A #m #o #eq #reflex #p #a
     780  elim p try (#r #assm assumption)
     781  #m' #hd #tl #inductive_hypothesis #r #assm
     782  normalize
     783  cases (eq ??) try %
     784  @inductive_hypothesis assumption
     785qed.
     786
     787
    595788let rec subvector_with
    596789  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
     
    622815 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
    623816qed.
     817
     818lemma subvector_multiple_append:
     819  ∀A: Type[0].
     820  ∀o, n: nat.
     821  ∀eq: A → A → bool.
     822  ∀refl: ∀a. eq a a = true.
     823  ∀h: Vector A o.
     824  ∀v: Vector A n.
     825  ∀m: nat.
     826  ∀q: Vector A m.
     827    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
     828  #A #o #n #eq #reflex #h #v
     829  elim v try (normalize #m #irrelevant @I)
     830  #m' #hd #tl #inductive_hypothesis #m #q
     831  change with (bool_to_Prop (andb ??))
     832  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
     833  [1:
     834    @mem_monotonic_wrt_append try assumption
     835    @mem_monotonic_wrt_append try assumption
     836    normalize >reflex %
     837  |2:
     838    #assm >assm
     839    >vector_cons_append
     840    change with (bool_to_Prop (subvector_with ??????))
     841    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
     842    try @associative_plus
     843    @inductive_hypothesis
     844  ]
     845qed.
     846
     847
    624848
    625849(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.