Changeset 998 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 20, 2011, 5:05:23 PM (8 years ago)
Author:
sacerdot
Message:

Half repaired, half broken. Most functions no longer return option types,
taking in input dependent types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r993 r998  
    139139  ].
    140140
     141lemma foldl_step:
     142 ∀A:Type[0].
     143  ∀B: Type[0].
     144   ∀H: A → B → A.
     145    ∀acc: A.
     146     ∀pre: list B.
     147      ∀hd:B.
     148       foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd).
     149 #A #B #H #acc #pre generalize in match acc; -acc; elim pre
     150  [ normalize; //
     151  | #hd #tl #IH #acc #X normalize; @IH ]
     152qed.
     153
     154lemma foldl_append:
     155 ∀A:Type[0].
     156  ∀B: Type[0].
     157   ∀H: A → B → A.
     158    ∀acc: A.
     159     ∀suff,pre: list B.
     160      foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff).
     161 #A #B #H #acc #suff elim suff
     162  [ #pre >append_nil %
     163  | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
     164qed.
     165
    141166definition flatten ≝
    142167  λA: Type[0].
Note: See TracChangeset for help on using the changeset viewer.