Changeset 1063 for src/ASM/Util.ma


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

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1062 r1063  
    1414 with precedence 10
    1515for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     16
     17definition ltb ≝
     18  λm, n: nat.
     19    leb (S m) n.
     20   
     21definition geb ≝
     22  λm, n: nat.
     23    ltb n m.
     24
     25definition gtb ≝
     26  λm, n: nat.
     27    leb n m.
     28
     29(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
     30let rec eq_nat (n: nat) (m: nat) on n: bool ≝
     31  match n with
     32  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
     33  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     34  ].
     35
     36let rec remove_n_first_internal
     37  (i: nat) (A: Type[0]) (l: list A) (n: nat)
     38    on l ≝
     39  match l with
     40  [ nil ⇒ [ ]
     41  | cons hd tl ⇒
     42    match eq_nat i n with
     43    [ true ⇒ l
     44    | _ ⇒ remove_n_first_internal (S i) A tl n
     45    ]
     46  ].
     47
     48definition remove_n_first ≝
     49  λA: Type[0].
     50  λn: nat.
     51  λl: list A.
     52    remove_n_first_internal 0 A l n.
     53   
     54let rec foldi_from_until_internal
     55  (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A)
     56    on rem ≝
     57  match rem with
     58  [ nil ⇒ res
     59  | cons e tl ⇒
     60    match geb i m with
     61    [ true ⇒ res
     62    | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f
     63    ]
     64  ].
     65
     66definition foldi_from_until ≝
     67  λA: Type[0].
     68  λn: nat.
     69  λm: nat.
     70  λf: ?.
     71  λa: ?.
     72  λl: ?.
     73    foldi_from_until_internal A 0 a (remove_n_first A n l) m f.
     74
     75definition foldi_from ≝
     76  λA: Type[0].
     77  λn.
     78  λf.
     79  λa.
     80  λl.
     81    foldi_from_until A n (|l|) f a l.
     82
     83definition foldi_until ≝
     84  λA: Type[0].
     85  λm.
     86  λf.
     87  λa.
     88  λl.
     89    foldi_from_until A 0 m f a l.
     90
     91definition foldi ≝
     92  λA: Type[0].
     93  λf.
     94  λa.
     95  λl.
     96    foldi_from_until A 0 (|l|) f a l.
    1697
    1798definition hd ≝
     
    129210*)
    130211
    131 include "ASM/FoldStuff.ma".
    132 
    133212let rec reduce_strong
    134   (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left
    135   : Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |  ≝
    136   match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    137   [ nil ⇒
    138     match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    139     [ nil ⇒ λnil_nil_prf. ?
    140     | cons hd tl ⇒ λnil_cons_absrd_prf. ?
    141     ]
     213  (A: Type[0]) (left: list A) (right: list A)
     214    on left : Σret: ((list A) × (list A)) × ((list A) × (list A)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
     215  match left with
     216  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
    142217  | cons hd tl ⇒
    143     match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    144     [ nil ⇒ λcons_nil_absrd_prf. ?
    145     | cons hd' tl' ⇒ λcons_cons_prf.
    146       let 〈commonl, commonr〉 ≝ eject … (reduce_strong A tl tl' ?) in ? (*
    147       [ dp clr their_proof ⇒ ? (*
    148         let 〈commonl, commonr〉 ≝ clr in ? *)
    149       ]*)
    150     ]
    151   ] prf.
    152   [ 5: normalize in cons_cons_prf;
    153        destruct(cons_cons_prf)
    154        assumption
    155   | 2: normalize in nil_cons_absrd_prf;
    156        destruct(nil_cons_absrd_prf)
    157   | 3: normalize in cons_nil_absrd_prf;
    158        destruct(cons_nil_absrd_prf)
    159   | 4:
     218    match right with
     219    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
     220    | cons hd' tl' ⇒
     221      let 〈cleft, cright〉 ≝ reduce_strong A tl tl' in
     222      let 〈commonl, restl〉 ≝ cleft in
     223      let 〈commonr, restr〉 ≝ cright in
     224        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
     225    ]
     226  ].
     227  [ 1: normalize %
     228  | 2: normalize %
     229  | 3: normalize
     230       generalize in match (sig2 … (reduce_strong A tl tl1));
     231       >p2 >p3 >p4 normalize in ⊢ (% → ?)
     232       #HYP //
    160233  ]
    161234qed.
    162  
    163 axiom reduce_length:
    164   ∀A: Type[0].
    165   ∀left, right: list A.
    166   ∀prf: | left | = | right |.
    167     \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)).
    168235   
    169236let rec map2_opt
     
    527594        ]
    528595    ].
    529    
    530 definition ltb ≝
    531   λm, n: nat.
    532     leb (S m) n.
    533    
    534 definition geb ≝
    535   λm, n: nat.
    536     ltb n m.
    537 
    538 definition gtb ≝
    539   λm, n: nat.
    540     leb n m.
    541    
    542 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
    543 let rec eq_nat (n: nat) (m: nat) on n: bool ≝
    544   match n with
    545   [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    546   | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
    547   ].
    548596
    549597(* dpm: conflicts with library definitions
Note: See TracChangeset for help on using the changeset viewer.