Changeset 990 for src/ASM/FoldStuff.ma


Ignore:
Timestamp:
Jun 17, 2011, 1:30:01 PM (9 years ago)
Author:
sacerdot
Message:

Do no longer use the daemon automatically :-)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/FoldStuff.ma

    r980 r990  
    7676    foldl_strong_internal A P l H [ ] l acc (refl …).
    7777
     78let rec foldr_strong_internal
     79 (A:Type[0])
     80 (P: list A → Type[0])
     81 (l: list A)
     82 (H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl))
     83 (prefix: list A) (suffix: list A) (acc: P [ ]) on suffix : l = prefix@suffix → P suffix ≝
     84  match suffix return λl'. l = prefix @ l' → P (l') with
     85   [ nil ⇒ λprf. acc
     86   | cons hd tl ⇒ λprf. H prefix hd tl prf (foldr_strong_internal A P l H (prefix @ [hd]) tl acc ?) ].
     87 applyS prf
     88qed.
     89
     90lemma foldr_strong:
     91 ∀A:Type[0].
     92  ∀P: list A → Type[0].
     93   ∀l: list A.
     94    ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl).
     95     ∀acc:P [ ]. P l
     96 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …).
     97
    7898lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
    7999 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
Note: See TracChangeset for help on using the changeset viewer.