Changeset 782 for src/ASM/Util.ma


Ignore:
Timestamp:
Apr 28, 2011, 5:36:33 PM (9 years ago)
Author:
mulligan
Message:

More work on rtl-ertl pass from today, plus resolved conflict.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r777 r782  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4 
     5lemma eq_rect_Type0_r :
     6  ∀A: Type[0].
     7  ∀a:A.
     8  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     9  #A #a #P #H #x #p
     10  generalize in match H
     11  generalize in match P
     12  cases p
     13  //
     14qed.
     15 
     16let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝
     17  match n return λo. o < length A l → A with
     18  [ O ⇒
     19    match l return λm. 0 < length A m → A with
     20    [ nil ⇒ λabsd1. ?
     21    | cons hd tl ⇒ λprf1. hd
     22    ]
     23  | S n' ⇒
     24    match l return λm. S n' < length A m → A with
     25    [ nil ⇒ λabsd2. ?
     26    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
     27    ]
     28  ] ?.
     29  [ 1:
     30    @ p
     31  | 4:
     32    normalize in prf2
     33    normalize
     34    @ le_S_S_to_le
     35    assumption
     36  | 2:
     37    normalize in absd1;
     38    cases (not_le_Sn_O O)
     39    # H
     40    elim (H absd1)
     41  | 3:
     42    normalize in absd2;
     43    cases (not_le_Sn_O (S n'))
     44    # H
     45    elim (H absd2)
     46  ]
     47qed.
    448 
    549let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
     
    128172
    129173definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
    130 
    131 lemma eq_rect_Type0_r :
    132   ∀A: Type[0].
    133   ∀a:A.
    134   ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    135   #A #a #P #H #x #p
    136   generalize in match H
    137   generalize in match P
    138   cases p
    139   //
    140 qed.
    141 
    142174
    143175notation "hvbox(t⌈o ↦ h⌉)"
Note: See TracChangeset for help on using the changeset viewer.