Changeset 3579 for LTS/utils.ma


Ignore:
Timestamp:
Jul 10, 2015, 4:08:09 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/utils.ma

    r3575 r3579  
    159159].
    160160
     161lemma eqb_list_elim : ∀P : bool → Prop.
     162∀D,l1,l2.(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eqb_list D l1 l2).
     163#P #D #l1 lapply P -P elim l1
     164[ #P * /2/ #x #xs #H1 #H2 @H2 % #EQ destruct]
     165#x #xs #IH #P * /2/ #y #ys #H1 #H2 normalize
     166inversion(?==?) #EQ normalize [2: @H2 % #EQ1 destruct >(\b (refl …)) in EQ; #EQ destruct]
     167@IH [ #EQ1 destruct @H1 >(\P EQ) % | * #H @H2 % #EQ1 destruct @H %]
     168qed.
     169
    161170definition DeqSet_List : DeqSet → DeqSet ≝
    162171λX.mk_DeqSet (list X) (eqb_list …) ?.
     
    381390#A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/
    382391qed.
     392
     393(* All2 *)
     394
     395let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝
     396match l1 with
     397[ nil ⇒ match l2 with [nil ⇒ True | cons _ _ ⇒ False]
     398| cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
     399].
Note: See TracChangeset for help on using the changeset viewer.