helm/software/matita/nlibrary/datatypes/list.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/pts.ma".
  16 include "logic/equality.ma".
  17 include "arithmetics/nat.ma".
  18
  19 ninductive list (A:Type[0]) : Type[0] ≝
  20   | nil: list A
  21   | cons: A -> list A -> list A.
  22
  23 notation "hvbox(hd break :: tl)"
  24   right associative with precedence 47
  25   for @{'cons $hd $tl}.
  26
  27 notation "[ list0 x sep ; ]"
  28   non associative with precedence 90
  29   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  30
  31 notation "hvbox(l1 break @ l2)"
  32   right associative with precedence 47
  33   for @{'append $l1 $l2 }.
  34
  35 interpretation "nil" 'nil = (nil ?).
  36 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  37
  38 nlet rec append A (l1: list A) l2 on l1 ≝
  39   match l1 with
  40   [ nil ⇒ l2
  41   | cons hd tl ⇒ hd :: append A tl l2 ].
  42
  43 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  44
  45 nlet rec id_list A (l: list A) on l ≝
  46   match l with
  47   [ nil ⇒ []
  48   | cons hd tl ⇒ hd :: id_list A tl ].
  49
  50
  51 ndefinition tail ≝ λA:Type[0].λl:list A.
  52   match l with
  53   [ nil ⇒  []
  54   | cons hd tl ⇒  tl].
  55
  56 nlet rec flatten S (l : list (list S)) on l : list S ≝
  57 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
  58
  59 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
  60 #A;#l;nelim l;//;
  61 #a;#l1;#IH;nnormalize;
  62 nrewrite > IH;//;
  63 nqed.
  64
  65 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
  66 #A;#x;#y;#z;nelim x
  67 ##[//
  68 ##|#a;#x1;#H;nnormalize;//]
  69 nqed.
  70
  71 ntheorem cons_append_commute:
  72   ∀A:Type[0].∀l1,l2:list A.∀a:A.
  73     a :: (l1 @ l2) = (a :: l1) @ l2.
  74 //;
  75 nqed.
  76
  77 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
  78 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
  79 nqed.
  80
  81 (*ninductive permutation (A:Type) : list A -> list A -> Prop \def
  82   | refl : \forall l:list A. permutation ? l l
  83   | swap : \forall l:list A. \forall x,y:A.
  84               permutation ? (x :: y :: l) (y :: x :: l)
  85   | trans : \forall l1,l2,l3:list A.
  86               permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
  87 with permut1 : list A -> list A -> Prop \def
  88   | step : \forall l1,l2:list A. \forall x,y:A.
  89       permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
  90
  91 (*
  92
  93 definition x1 \def S O.
  94 definition x2 \def S x1.
  95 definition x3 \def S x2.
  96
  97 theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
  98   apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
  99   apply refl.
 100   apply (step ? (x1::[]) [] x2 x3).
 101   qed.
 102
 103 theorem nil_append_nil_both:
 104   \forall A:Type.\forall l1,l2:list A.
 105     l1 @ l2 = [] \to l1 = [] \land l2 = [].
 106
 107 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
 108 reflexivity.
 109 qed.
 110
 111 theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
 112 simplify.
 113 reflexivity.
 114 qed.
 115
 116 *)
 117
 118 nlet rec nth A l d n on l ≝
 119   match l with
 120   [ nil ⇒ d
 121   | cons (x:A) tl ⇒ match n with
 122     [ O ⇒ x
 123     | S n' ⇒ nth A tl d n' ] ].
 124
 125 nlet rec map A B f l on l ≝
 126   match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
 127
 128 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
 129   match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
 130
 131 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
 132
 133 ndefinition filter ≝
 134   λT:Type[0].λl:list T.λp:T → bool.
 135   foldr T (list T)
 136     (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
 137
 138 ndefinition iota : nat → nat → list nat ≝
 139   λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
 140
 141 (* ### induction principle for functions visiting 2 lists in parallel *)
 142 nlemma list_ind2 :
 143   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
 144   length ? l1 = length ? l2 →
 145   (P (nil ?) (nil ?)) →
 146   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
 147   P l1 l2.
 148 #T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
 149 ngeneralize in match Hl; ngeneralize in match l2;
 150 nelim l1
 151 ##[#l2;ncases l2;//;
 152    nnormalize;#t2;#tl2;#H;ndestruct;
 153 ##|#t1;#tl1;#IH;#l2;ncases l2
 154    ##[nnormalize;#H;ndestruct
 155    ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
 156 ##]
 157 nqed.
 158
 159 nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 160 #A;#B;#f;#g;#l;#Efg;
 161 nelim l; nnormalize;//;
 162 nqed.
 163
 164 nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
 165 #A;#l;#p;nelim l;nnormalize
 166 ##[//
 167 ##|#a;#tl;#IH;ncases (p a);nnormalize;
 168    ##[napply le_S_S;//;
 169    ##|@2;//]
 170 ##]
 171 nqed.
 172
 173 nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
 174 #A;#l;#m;nelim l;
 175 ##[//
 176 ##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
 177 nqed.
 178
 179 ninductive in_list (A:Type): A → (list A) → Prop ≝
 180 | in_list_head : ∀ x,l.(in_list A x (x::l))
 181 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
 182
 183 ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
 184   \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
 185
 186 notation "hvbox(a break ∉ b)" non associative with precedence 45
 187 for @{ 'notmem $a $b }.
 188
 189 interpretation "list member" 'mem x l = (in_list ? x l).
 190 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
 191 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
 192
 193 nlemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
 194 #A x;@;#H1;ninversion H1;
 195 ##[#a0 al0 H2 H3;ndestruct (H3);
 196 ##|#a0 a1 al0 H2 H3 H4 H5;ndestruct (H5)
 197 ##]
 198 nqed.
 199
 200 nlemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
 201                           x = a \lor in_list A x l.
 202 #A a0 a1 al0 H1;ninversion H1
 203 ##[#a2 al1 H2 H3;ndestruct (H3);@;@
 204 ##|#a2 a3 al1 H2 H3 H4 H5;ndestruct (H5);@2;//
 205 ##]
 206 nqed.
 207
 208 nlemma in_list_tail : \forall A,l,x,y.
 209       in_list A x (y::l) \to x \neq y \to in_list A x l.
 210 #A;#l;#x;#y;#H;#Hneq;
 211 ninversion H;
 212 ##[#x1;#l1;#Hx;#Hl;ndestruct;nelim Hneq;#Hfalse;
 213    nelim (Hfalse ?);@;
 214 ##|#x1;#y1;#l1;#H1;#_;#Hx;#Heq;ndestruct;//;
 215 ##]
 216 nqed.
 217
 218 nlemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
 219 #A a0 a1 H1;ncases (in_list_cons_case ???? H1)
 220 ##[//
 221 ##|#H2;napply False_ind;ncases (not_in_list_nil ? a0);#H3;/2/
 222 ##]
 223 nqed.
 224
 225 nlemma in_list_to_in_list_append_l: \forall A.\forall x:A.
 226 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
 227 #A a0 al0 al1 H1;nelim H1
 228 ##[#a1 al2;@;
 229 ##|#a1 a2 al2 H2 H3;@2;//
 230 ##]
 231 nqed.
 232
 233 nlemma in_list_to_in_list_append_r: \forall A.\forall x:A.
 234 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
 235 #A a0 al0 al1 H1;nelim al0
 236 ##[napply H1
 237 ##|#a1 al2 IH;@2;napply IH
 238 ##]
 239 nqed.
 240
 241 nlemma in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
 242 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
 243 #A a0 al0;nelim al0
 244 ##[#al1 H1;@2;napply H1
 245 ##|#a1 al1 IH al2 H1;nnormalize in H1;
 246    ncases (in_list_cons_case ???? H1);#H2
 247    ##[@;nrewrite > H2;@
 248    ##|ncases (IH … H2);#H3
 249       ##[@;@2;//
 250       ##|@2;//
 251       ##]
 252    ##]
 253 ##]
 254 nqed.
 255
 256 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
 257  match l with
 258   [ nil ⇒ false
 259   | (cons a l') ⇒
 260     match eq x a with
 261      [ true ⇒ true
 262      | false ⇒ mem A eq x l'
 263      ]
 264   ].
 265
 266 nlemma mem_true_to_in_list :
 267   \forall A,equ.
 268   (\forall x,y.equ x y = true \to x = y) \to
 269   \forall x,l.mem A equ x l = true \to in_list A x l.
 270 #A equ H1 a0 al0;nelim al0
 271 ##[nnormalize;#H2;ndestruct (H2)
 272 ##|#a1 al1 IH H2;nwhd in H2:(??%?);
 273    nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3
 274    ##[nrewrite > (H1 … H3);@
 275    ##|@2;napply IH;nrewrite > H3 in H2;nnormalize;//;
 276    ##]
 277 ##]
 278 nqed.
 279
 280 nlemma in_list_to_mem_true :
 281   \forall A,equ.
 282   (\forall x.equ x x = true) \to
 283   \forall x,l.in_list A x l \to mem A equ x l = true.
 284 #A equ H1 a0 al0;nelim al0
 285 ##[#H2;napply False_ind;ncases (not_in_list_nil ? a0);/2/
 286 ##|#a1 al1 IH H2;nelim H2
 287    ##[nnormalize;#a2 al2;nrewrite > (H1 …);@
 288    ##|#a2 a3 al2 H3 H4;nnormalize;ncases (equ a2 a3);nnormalize;//;
 289    ##]
 290 ##]
 291 nqed.
 292
 293 nlemma in_list_filter_to_p_true : \forall A,l,x,p.
 294 in_list A x (filter A l p) \to p x = true.
 295 #A al0 a0 p;nelim al0
 296 ##[nnormalize;#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
 297 ##|#a1 al1 IH H1;nnormalize in H1;nlapply (refl ? (p a1));
 298    ngeneralize in match H1;ncases (p a1) in ⊢ (???% -> ???% → %);
 299    ##[#H2 H3;ncases (in_list_cons_case ???? H2);#H4
 300       ##[nrewrite > H4;//
 301       ##|napply (IH H4);
 302       ##]
 303    ##|#H2 H3;napply (IH H2);
 304    ##]
 305 ##]
 306 nqed.
 307
 308 nlemma in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
 309 #A al0 p a0;nelim al0
 310 ##[nnormalize;//;
 311 ##|#a1 al1 IH H1;nnormalize in H1;
 312    nlapply (refl ? (p a1));ncases (p a1) in ⊢ (???% → %);#H2
 313    ##[nrewrite > H2 in H1;#H1;ncases (in_list_cons_case ???? H1);#H3
 314       ##[nrewrite > H3;@
 315       ##|@2;napply IH;napply H3
 316       ##]
 317    ##|@2;napply IH;nrewrite > H2 in H1;#H1;napply H1;
 318    ##]
 319 ##]
 320 nqed.
 321
 322 nlemma in_list_filter_r : \forall A,l,p,x.
 323               in_list A x l \to p x = true \to in_list A x (filter A l p).
 324 #A al0 p a0;nelim al0
 325 ##[#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
 326 ##|#a1 al1 IH H1 H2;ncases (in_list_cons_case ???? H1);#H3
 327    ##[nnormalize;nrewrite < H3;nrewrite > H2;@
 328    ##|nnormalize;ncases (p a1);nnormalize;
 329       ##[@2;napply IH;//
 330       ##|napply IH;//
 331       ##]
 332    ##]
 333 ##]
 334 nqed.
 335
 336 nlemma incl_A_A: ∀T,A.incl T A A.
 337 #A al0 a0 H1;//;
 338 nqed.
 339
 340 nlemma incl_append_l : ∀T,A,B.incl T A (A @ B).
 341 #A al0 al1 a0 H1;/2/;
 342 nqed.
 343
 344 nlemma incl_append_r : ∀T,A,B.incl T B (A @ B).
 345 #A al0 al1 a0 H1;/2/;
 346 nqed.
 347
 348 nlemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 349 #A al0 al1 a0 H1 a1 H2;ncases (in_list_cons_case ???? H2);/2/;
 350 #H3;@2;napply H1;//;
 351 nqed.
 352
 353 nlet rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l ≝
 354  match l with
 355  [ nil ⇒ a
 356  | cons b bl ⇒ foldl A B f (f a b) bl ].
 357
 358 nlet rec foldl2 (A,B,C:Type[0]) (f:A → B → C → A) (a:A) (bl:list B) (cl:list C) on bl ≝
 359  match bl with
 360  [ nil ⇒ a
 361  | cons b0 bl0 ⇒ match cl with
 362    [ nil ⇒ a
 363    | cons c0 cl0 ⇒ foldl2 A B C f (f a b0 c0) bl0 cl0 ] ].
 364
 365 nlet rec foldr2 (A,B : Type[0]) (X : Type[0]) (f: A → B → X → X) (x:X)
 366                 (al : list A) (bl : list B) on al : X ≝
 367   match al with
 368   [ nil ⇒ x
 369   | cons a al1 ⇒ match bl with
 370     [ nil ⇒ x
 371     | cons b bl1 ⇒ f a b (foldr2 ??? f x al1 bl1) ] ].
 372
 373 nlet rec rev (A:Type[0]) (l:list A) on l ≝
 374  match l with
 375  [ nil ⇒ nil A
 376  | cons hd tl ⇒ (rev A tl)@[hd] ].
 377
 378 notation > "hvbox(a break \liff b)"
 379   left associative with precedence 25
 380 for @{ 'iff $a $b }.
 381
 382 notation "hvbox(a break \leftrightarrow b)"
 383   left associative with precedence 25
 384 for @{ 'iff $a $b }.
 385
 386 interpretation "logical iff" 'iff x y = (iff x y).
 387
 388 ndefinition coincl : ∀A.list A → list A → Prop ≝  λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
 389
 390 notation > "hvbox(a break ≡ b)"
 391   non associative with precedence 45
 392 for @{'equiv $a $b}.
 393
 394 notation < "hvbox(term 46 a break ≡ term 46 b)"
 395   non associative with precedence 45
 396 for @{'equiv $a $b}.
 397
 398 interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
 399
 400 nlemma refl_coincl : ∀A.∀l:list A.l ≡ l.
 401 #;@;#;//;
 402 nqed.
 403
 404 nlemma coincl_rev : ∀A.∀l:list A.l ≡ rev ? l.
 405 #A l x;@;nelim l
 406 ##[##1,3:#H;napply False_ind;ncases (not_in_list_nil ? x);
 407    #H1;napply (H1 H);
 408 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
 409    ##[napply in_list_to_in_list_append_r;nrewrite > H1;@
 410    ##|napply in_list_to_in_list_append_l;/2/
 411    ##]
 412 ##|#a l0 IH H;ncases (in_list_append_to_or_in_list ???? H);#H1
 413    ##[/3/;
 414    ##|nrewrite > (in_list_singleton_to_eq ??? H1);@
 415    ##]
 416 ##]
 417 nqed.
 418
 419 nlemma not_in_list_nil_r : ∀A.∀l:list A.l = [] → ∀x.x ∉ l.
 420 #A l;nelim l
 421 ##[#;napply not_in_list_nil
 422 ##|#a l0 IH Hfalse;ndestruct (Hfalse)
 423 ##]
 424 nqed.
 425
 426 nlemma eq_filter_append :
 427  ∀A,p,l1,l2.filter A (l1@l2) p = filter A l1 p@filter A l2 p.
 428 #A p l1 l2;nelim l1
 429 ##[@
 430 ##|#a0 l0 IH;nwhd in ⊢ (??%(??%?));ncases (p a0)
 431    ##[nwhd in ⊢ (??%%);nrewrite < IH;@
 432    ##|nwhd in ⊢ (??%(??%?));nrewrite < IH;@
 433    ##]
 434 ##]
 435 nqed.
 436
 437 nlemma map_ind :
 438  ∀A,B:Type[0].∀f:A→B.∀P:B → Prop.
 439   ∀al.(∀a.a ∈ al → P (f a)) →
 440   ∀b. b ∈ map ?? f al → P b.
 441 #A B f P al;nelim al
 442 ##[#H1 b Hfalse;napply False_ind;
 443    ncases (not_in_list_nil ? b);#H2;napply H2;napply Hfalse;
 444 ##|#a1 al1 IH H1 b Hin;nwhd in Hin:(???%);ncases (in_list_cons_case ???? Hin);
 445    ##[#e;nrewrite > e;napply H1;@
 446    ##|#Hin1;napply IH;
 447       ##[#a2 Hin2;napply H1;@2;//;
 448       ##|//
 449       ##]
 450    ##]
 451 ##]
 452 nqed.
 453
 454 nlemma map_compose :
 455  ∀A,B,C,f,g,l.map B C f (map A B g l) = map A C (λx.f (g x)) l.
 456 #A B C f g l;nelim l
 457 ##[@
 458 ##|#a0 al0 IH;nchange in ⊢ (??%%) with (cons ???);
 459    napply eq_f2; //;
 460 ##]
 461 nqed.
 462
 463 nlemma incl_incl_to_incl_append :
 464   ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'.
 465 #A al0 al1 al2 al3 H1 H2 a0 H3;
 466 ncases (in_list_append_to_or_in_list ???? H3);#H4;
 467 ##[napply in_list_to_in_list_append_l;napply H1;//
 468 ##|napply in_list_to_in_list_append_r;napply H2;//
 469 ##]
 470 nqed.
 471
 472 nlemma eq_map_append :
 473   ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.
 474 #A B f al1 al2;nelim al1
 475 ##[@
 476 ##|#a0 al3 IH;nnormalize;nrewrite > IH;@;
 477 ##]
 478 nqed.
 479
 480 nlemma not_in_list_to_mem_false :
 481   ∀A,equ.
 482   (∀x,y.equ x y = true → x = y) →
 483   ∀x:A.∀l. x ∉ l → mem A equ x l = false.
 484 #A equ H1 a0 al0;nelim al0
 485 ##[#_;@
 486 ##|#a1 al1 IH H2;nwhd in ⊢ (??%?);
 487    nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3;
 488    ##[napply False_ind;ncases H2;#H4;napply H4;
 489       nrewrite > (H1 … H3);@
 490    ##|napply IH;@;#H4;ncases H2;#H5;napply H5;@2;//
 491    ##]
 492 ##]
 493 nqed.
 494
 495 nlet rec list_forall (A:Type[0]) (l:list A) (p:A → bool) on l : bool ≝
 496  match l with
 497  [ nil ⇒ (true:bool)
 498  | cons a al ⇒ p a ∧ list_forall A al p ].
 499
 500 nlemma eq_map_f_g :
 501  ∀A,B,f,g,xl.(∀x.x ∈ xl → f x = g x) → map A B f xl = map A B g xl.
 502 #A B f g xl;nelim xl
 503 ##[#;@
 504 ##|#a al IH H1;nwhd in ⊢ (??%%);napply eq_f2
 505    ##[napply H1;@;
 506    ##|napply IH;#x Hx;napply H1;@2;//
 507    ##]
 508 ##]
 509 nqed.
 510
 511 nlemma x_in_map_to_eq :
 512   ∀A,B,f,x,l.x ∈ map A B f l → ∃x'.x = f x' ∧ x' ∈ l.
 513 #A B f x l;nelim l
 514 ##[#H;ncases (not_in_list_nil ? x);#H1;napply False_ind;napply (H1 H)
 515 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
 516    ##[nrewrite > H1;@ a;@;@
 517    ##|ncases (IH H1);#a0;*;#H2 H3;@a0;@
 518       ##[// ##|@2;// ##]
 519    ##]
 520 ##]
 521 nqed.
 522
 523 nlemma list_forall_false :
 524  ∀A:Type[0].∀x,xl,p. p x = false → x ∈ xl → list_forall A xl p = false.
 525 #A x xl p H1;nelim xl
 526 ##[#Hfalse;napply False_ind;ncases (not_in_list_nil ? x);#H2;napply (H2 Hfalse)
 527 ##|#x0 xl0 IH H2;ncases (in_list_cons_case ???? H2);#H3
 528    ##[nwhd in ⊢ (??%?);nrewrite < H3;nrewrite > H1;@
 529    ##|nwhd in ⊢ (??%?);ncases (p x0)
 530       ##[nrewrite > (IH H3);@
 531       ##|@
 532       ##]
 533    ##]
 534 ##]
 535 nqed.
 536
 537 nlemma list_forall_true :
 538  ∀A:Type[0].∀xl,p. (∀x.x ∈ xl → p x = true) → list_forall A xl p = true.
 539 #A xl p;nelim xl
 540 ##[#;@
 541 ##|#x0 xl0 IH H1;nwhd in ⊢ (??%?);nrewrite > (H1 …)
 542    ##[napply IH;#x Hx;napply H1;@2;//
 543    ##|@
 544    ##]
 545 ##]
 546 nqed.