matita/matita/lib/pts_dummy/ext.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 "basics/lists/list.ma".
  16
  17 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
  18
  19 (* arithmetics ****************************************************************)
  20
  21 lemma arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
  22 #x #y #HS @nmk (elim HS) -HS /3/
  23 qed.
  24
  25 lemma arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
  26 #i #p #k #H @plus_to_minus
  27 >commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
  28 qed.
  29
  30 lemma arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
  31 #x #y #z #H @nmk (elim H) -H /3/
  32 qed.
  33
  34 lemma arith4: ∀x,y. S x ≰ y → x≠y → y < x.
  35 #x #y #H1 #H2 lapply (not_le_to_lt … H1) -H1 #H1 @not_eq_to_le_to_lt /2/
  36 qed.
  37
  38 lemma arith5: ∀x,y. x < y → S (y - 1) ≰ x.
  39 #x #y #H @lt_to_not_le <minus_Sn_m /2/
  40 qed.
  41
  42 (* lists **********************************************************************)
  43
  44 lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
  45 #A #l2 #l1 elim l1 -l1; normalize //
  46 qed.
  47
  48 (* all(?,P,l) holds when P holds for all members of l *)
  49 let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
  50    [ nil        ⇒ True
  51    | cons hd tl ⇒ P hd ∧ all A P tl
  52    ].
  53
  54 lemma all_hd: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀l. all … P l → P (hd … l a).
  55 #A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl -Hl; normalize // ]
  56 qed.
  57
  58 lemma all_tl: ∀A:Type[0]. ∀P:A→Prop. ∀l. all … P l →  all … P (tail … l).
  59 #A #P #l elim l -l // #b #l #IH #Hl elim Hl -Hl; normalize //
  60 qed.
  61
  62 lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l → P (nth i … l a).
  63 #A #P #a #Ha #i elim i -i [ @all_hd // | #i #IH #l #Hl @IH /2/ ]
  64 qed.
  65
  66 lemma all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
  67 #A #P #l2 #l1 elim l1 -l1; normalize // #hd #tl #IH1 #H elim H -H /3/
  68 qed.
  69
  70 (* all2(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
  71 let rec all2 (A,B:Type[0]) (P:A→B→Prop) l1 l2 on l1 ≝ match l1 with
  72    [ nil          ⇒ l2 = nil ?
  73    | cons hd1 tl1 ⇒ match l2 with
  74       [ nil          ⇒ False
  75       | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A B P tl1 tl2
  76       ]
  77    ].
  78
  79 lemma all2_length: ∀A,B:Type[0]. ∀P:A→B→Prop.
  80                    ∀l1,l2. all2 … P l1 l2 → |l1|=|l2|.
  81 #A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
  82 #x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
  83 #x2 #l2 #_ #H elim H -H; normalize /3/
  84 qed.
  85
  86 lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
  87                ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
  88 #A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
  89 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
  90 #x2 #l2 #_ #H elim H -H; normalize //
  91 qed.
  92
  93 lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
  94                ∀l1,l2. all2 … P l1 l2 →  all2 … P (tail … l1) (tail … l2).
  95 #A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
  96 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
  97 #x2 #l2 #_ #H elim H -H; normalize //
  98 qed.
  99
 100 lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
 101                 ∀i,l1,l2. all2 … P l1 l2 → P (nth i … l1 a) (nth i … l2 b).
 102 #A #B #P #a #b #Hab #i elim i -i [ @all2_hd // | #i #IH #l1 #l2 #H @IH /2/ ]
 103 qed.
 104
 105 lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 →
 106                    ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2).
 107 #A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ]
 108 #x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ]
 109 #x2 #m2 #_ #H elim H -H /3/
 110 qed.
 111
 112 lemma all2_symmetric: ∀A. ∀P:A→A→Prop. symmetric … P → symmetric … (all2 … P).
 113 #A #P #HP #l1 elim l1 -l1 [ #l2 #H >H // ]
 114 #x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
 115 #x2 #l2 #_ #H elim H -H /3/
 116 qed.