Changeset 3579 for LTS/utils.ma
 Timestamp:
 Jul 10, 2015, 4:08:09 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/utils.ma
r3575 r3579 159 159 ]. 160 160 161 lemma 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 166 inversion(?==?) #EQ normalize [2: @H2 % #EQ1 destruct >(\b (refl …)) in EQ; #EQ destruct] 167 @IH [ #EQ1 destruct @H1 >(\P EQ) %  * #H @H2 % #EQ1 destruct @H %] 168 qed. 169 161 170 definition DeqSet_List : DeqSet → DeqSet ≝ 162 171 λX.mk_DeqSet (list X) (eqb_list …) ?. … … 381 390 #A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/ 382 391 qed. 392 393 (* All2 *) 394 395 let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝ 396 match 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.