Changeset 1060 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 8, 2011, 12:17:14 PM (8 years ago)
Author:
mulligan
Message:

work from this morning and yesterday

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1059 r1060  
    1212 with precedence 10
    1313for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     14
     15let rec nth_safe
     16  (elt_type: Type[0]) (index: nat) (the_list: list elt_type)
     17  (proof: index < | the_list |)
     18    on index ≝
     19  match index return λs. s < | the_list | → elt_type with
     20  [ O ⇒
     21    match the_list return λt. 0 < | t | → elt_type with
     22    [ nil        ⇒ λnil_absurd. ?
     23    | cons hd tl ⇒ λcons_proof. hd
     24    ]
     25  | S index' ⇒
     26    match the_list return λt. S index' < | t | → elt_type with
     27    [ nil ⇒ λnil_absurd. ?
     28    | cons hd tl ⇒
     29      λcons_proof. nth_safe elt_type index' tl ?
     30    ]
     31  ] proof.
     32  [ normalize in nil_absurd;
     33    cases (not_le_Sn_O 0)
     34    #ABSURD
     35    elim (ABSURD nil_absurd)
     36  | normalize in nil_absurd;
     37    cases (not_le_Sn_O (S index'))
     38    #ABSURD
     39    elim (ABSURD nil_absurd)
     40  | normalize in cons_proof
     41    @le_S_S_to_le
     42    assumption
     43  ]
     44qed.
     45
     46definition last_safe ≝
     47  λelt_type: Type[0].
     48  λthe_list: list elt_type.
     49  λproof   : 0 < | the_list |.
     50    nth_safe elt_type (|the_list| - 1) the_list ?.
     51  normalize /2/
     52qed.
    1453
    1554let rec reduce
     
    2867  ].
    2968
     69axiom reduce_strong:
     70  ∀A: Type[0].
     71  ∀left: list A.
     72  ∀right: list A.
     73    Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
     74
    3075(*
    3176let rec reduce_strong
     
    3479  [ nil ⇒
    3580    match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    36     [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉 ?
    37     | cons hd tl ⇒ λnil_cons_asrd_prf. ?
     81    [ nil ⇒ λnil_nil_prf. ?
     82    | cons hd tl ⇒ λnil_cons_absrd_prf. ?
    3883    ]
    3984  | cons hd tl ⇒
    4085    match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    4186    [ nil ⇒ λcons_nil_absrd_prf. ?
    42     | cons hd' tl' ⇒ λcons_cons_prf. ?
     87    | cons hd' tl' ⇒ λcons_cons_prf.
     88      let tail_call ≝ reduce_strong A tl tl' ? in ?
    4389    ]
    4490  ] prf.
    45 *)
    46 
     91  [ 5: normalize in cons_cons_prf;
     92       destruct(cons_cons_prf)
     93       assumption
     94  | 2: normalize in nil_cons_absrd_prf;
     95       destruct(nil_cons_absrd_prf)
     96  | 3: normalize in cons_nil_absrd_prf;
     97       destruct(cons_nil_absrd_prf)
     98  ]
     99qed.
     100*)   
     101 
    47102axiom reduce_length:
    48103  ∀A: Type[0].
Note: See TracChangeset for help on using the changeset viewer.