Changeset 1356


Ignore:
Timestamp:
Oct 11, 2011, 5:33:11 PM (8 years ago)
Author:
mulligan
Message:

deleted redundant directory. added outlines for both reports, and added a few sections to report for D4.2. more work on foldi_strong in rtlabs to rtl

Files:
3 added
1 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1354 r1356  
    8989    ]
    9090  in
    91     foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
     91    foldl initialize_local_env_internal 〈Stub …,runiverse〉 registers.
    9292
    9393definition map_list_local_env_internal ≝
     
    550550  in
    551551    translates @ tmp_destrs2'.
     552   
     553let rec remove_n_first_internal
     554  (b: Type[0]) (n: nat) (the_list: list b) (i: nat)
     555    on the_list ≝
     556  match the_list with
     557  [ nil        ⇒ [ ]
     558  | cons hd tl ⇒
     559    match eqb i n with
     560    [ true  ⇒ the_list
     561    | false ⇒ remove_n_first_internal b n tl (S i)
     562    ]
     563  ].
     564   
     565definition remove_n_first ≝
     566  λb: Type[0].
     567  λn: nat.
     568  λthe_list: list b.
     569    remove_n_first_internal b n the_list 0.
     570
     571axiom plus_m_n_eq_o_to_lt_m_o:
     572  ∀m, n, o: nat.
     573    m + n = o → m ≤ o.
     574
     575include alias "arithmetics/nat.ma".
     576
     577axiom minus_m_n_Sp_to_minus_m_Sn_p:
     578  ∀m, n, p: nat.
     579    minus m n = S p → minus m (S n) = p.
     580   
     581let rec foldi_strong_internal
     582  (a: Type[0]) (b: Type[0]) (reference: nat) (the_list: list b)
     583    (f: ∀j: nat. ∀proof: lt j (|the_list|). a → b → a) (seed: a)
     584      (counter: nat) (counter_proof: minus reference counter = |the_list|)
     585        on the_list: a ≝
     586  match the_list return λx. the_list = x → (minus reference counter = |x|) → a with
     587  [ nil        ⇒ λidentity. λbase_case. seed
     588  | cons hd tl ⇒ λidentity. λstep_case.
     589    let f' ≝ λj: nat. λproof: j < |tl|. f j ? in
     590      foldi_strong_internal a b reference tl f' (f counter ? seed hd) (S counter) ?
     591  ] (refl … the_list) counter_proof.
     592  [1: cut(reference > 0)
     593      [2: #REFERENCE_HYP
     594  |2: generalize in match counter_proof;
     595      >identity
     596      #HYP
     597      normalize in HYP:(???%);
     598      generalize in match (minus_m_n_Sp_to_minus_m_Sn_p reference counter (|tl|) HYP);
     599      #ASSM assumption
     600  |3: >identity
     601      normalize
     602      normalize in proof;
     603      generalize in match(le_S … proof);
     604      #HYP assumption
     605  ]
     606qed.
     607     
     608
     609let rec foldi_strong_from_until_internal
     610  (a: Type[0]) (b: Type[0]) (the_list: list b)
     611    (f: ∀j: nat. ∀proof: j ≤ |the_list|. a → b → a) (m: nat) (i: nat) (res: a)
     612      (proof: i ≤ |the_list|) (m_length_proof: m = |the_list|)
     613        on the_list: a ≝
     614  match the_list return λx. the_list = x → i ≤ |x| → a with
     615  [ nil        ⇒ λidentity. λsnd_proof. res
     616  | cons hd tl ⇒ λidentity. λsnd_proof.
     617    match geb i m return λx. geb i m = x → a with
     618    [ true  ⇒ λabsrd_prf. res
     619    | false ⇒ λotherwise.
     620      let f' ≝ λj. λthrd_proof: j ≤ |tl|. f j ? in
     621        foldi_strong_from_until_internal a b tl f' m (S i) (f' i ? res hd) ? ?
     622    ] (refl … (geb i m))
     623  ] (refl … the_list) proof.
     624  [1: generalize in match otherwise;
     625      >m_length_proof
     626      >identity
     627      #HYP
     628      cases(geb_false_nge … HYP)
     629      #HYP2
     630      cases(ge_m_n_False_to_lt_m_n … HYP2)
     631  |2:
     632qed.   
     633
     634definition foldi_strong_from_until ≝
     635  λa: Type[0].
     636  λb: Type[0].
     637  λn: nat.
     638  λm: nat.
     639  λthe_list: list b.
     640  λf: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
     641  λseed: a.
     642  λlength_proof: m = |the_list|.
     643    foldi_strong_from_until_internal a b the_list f m 0 seed ? length_proof.
     644  //
     645qed.
    552646 
    553 axiom foldi_strong:
    554   a: Type[0].
    555   b: Type[0].
    556   the_list: list b.
    557   f: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
    558   seed: a.
    559     a.
     647definition foldi_strong ≝
     648  λa: Type[0].
     649  λb: Type[0].
     650  λthe_list: list b.
     651  λf: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
     652  λseed: a.
     653    foldi_strong_from_until a b 0 (|the_list|) the_list f seed.
    560654 
    561655definition translate_mul ≝
Note: See TracChangeset for help on using the changeset viewer.