weblib/Cerco/ASM/Utils.ma

   1 include "basics/list2.ma".
   2 include "basics/types.ma".
   3 include "arithmetics/nat.ma".
   4
   5 include "Cerco/utilities/pair.ma".
   6 include "Cerco/ASM/JMCoercions.ma".
   7
   8 (* let's implement a daemon not used by automation *)
   9 inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
  10 axiom IMPOSSIBLE: \ 5a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,1,0)"\ 6K1DAEMONXXX\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,2,0)"\ 6K2DAEMONXXX\ 5/a\ 6.
  11 example daemon: \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6. generalize in match \ 5a href="cic:/matita/Cerco/ASM/Utils/IMPOSSIBLE.dec"\ 6IMPOSSIBLE\ 5/a\ 6; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
  12 example not_implemented: \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6. cases \ 5a href="cic:/matita/Cerco/ASM/Utils/daemon.def(2)" title="null"\ 6daemon\ 5/a\ 6 qed.
  13
  14 notation "⊥" with precedence 90
  15   for @{ match ? in False with [ ] }.
  16
  17 definition ltb ≝
  18   λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  19     \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) n.
  20
  21 definition geb ≝
  22   λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  23     \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"\ 6ltb\ 5/a\ 6 n m.
  24
  25 definition gtb ≝
  26   λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  27     \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"\ 6ltb\ 5/a\ 6 n m.
  28
  29 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
  30 let rec eq_nat (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
  31   match n with
  32   [ O ⇒ match m with [ O ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ]
  33   | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ]
  34   ].
  35
  36 let rec forall
  37   (A: Type[0]) (f: A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A)
  38     on l ≝
  39   match l with
  40   [ nil        ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
  41   | cons hd tl ⇒ f hd \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 forall A f tl
  42   ].
  43
  44 let rec prefix
  45   (A: Type[0]) (k: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A)
  46     on l ≝
  47   match l with
  48   [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
  49   | cons hd tl ⇒
  50     match k with
  51     [ O ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
  52     | S k' ⇒ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: prefix A k' tl
  53     ]
  54   ].
  55
  56 let rec fold_left2
  57   (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
  58   (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C) (proof: \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6left| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6right|)
  59     on left: A ≝
  60   match left return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6right| → A with
  61   [ nil ⇒ λnil_prf.
  62     match right return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → A with
  63     [ nil ⇒ λnil_nil_prf. accu
  64     | cons hd tl ⇒ λcons_nil_absrd. ?
  65     ] nil_prf
  66   | cons hd tl ⇒ λcons_prf.
  67     match right return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → A with
  68     [ nil ⇒ λcons_nil_absrd. ?
  69     | cons hd' tl' ⇒ λcons_cons_prf.
  70         fold_left2 …  f (f accu hd hd') tl tl' ?
  71     ] cons_prf
  72   ] proof.
  73   [ 1: normalize in cons_nil_absrd;
  74        destruct(cons_nil_absrd)
  75   | 2: normalize in cons_nil_absrd;
  76        destruct(cons_nil_absrd)
  77   | 3: normalize in cons_cons_prf;
  78        @\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6
  79        assumption
  80   ]
  81 qed.
  82
  83 let rec remove_n_first_internal
  84   (i: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (A: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6)
  85     on l ≝
  86   match l with
  87   [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
  88   | cons hd tl ⇒
  89     match \ 5a href="cic:/matita/Cerco/ASM/Utils/eq_nat.fix(0,0,1)"\ 6eq_nat\ 5/a\ 6 i n with
  90     [ true ⇒ l
  91     | _ ⇒ remove_n_first_internal (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) A tl n
  92     ]
  93   ].
  94
  95 definition remove_n_first ≝
  96   λA: Type[0].
  97   λn: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  98   λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
  99     \ 5a href="cic:/matita/Cerco/ASM/Utils/remove_n_first_internal.fix(0,2,2)"\ 6remove_n_first_internal\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 A l n.
 100
 101 let rec foldi_from_until_internal
 102   (A: Type[0]) (i: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (res: ?) (rem: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → A → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A)
 103     on rem ≝
 104   match rem with
 105   [ nil ⇒ res
 106   | cons e tl ⇒
 107     match \ 5a href="cic:/matita/Cerco/ASM/Utils/geb.def(3)"\ 6geb\ 5/a\ 6 i m with
 108     [ true ⇒ res
 109     | _ ⇒ foldi_from_until_internal A (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) (f i res e) tl m f
 110     ]
 111   ].
 112
 113 definition foldi_from_until ≝
 114   λA,n,m,f,a,l. \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until_internal.fix(0,3,4)"\ 6foldi_from_until_internal\ 5/a\ 6 A \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 a (\ 5a href="cic:/matita/Cerco/ASM/Utils/remove_n_first.def(3)"\ 6remove_n_first\ 5/a\ 6 A n l) m f.
 115
 116 definition foldi_from ≝
 117   λA: Type[0].
 118   λn.
 119   λf.
 120   λa.
 121   λl.
 122     \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"\ 6foldi_from_until\ 5/a\ 6 A n (\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|) f a l.
 123
 124 definition foldi_until ≝
 125   λA: Type[0].
 126   λm.
 127   λf.
 128   λa.
 129   λl.
 130     \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"\ 6foldi_from_until\ 5/a\ 6 A \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 m f a l.
 131
 132 definition foldi ≝
 133   λA: Type[0].
 134   λf.
 135   λa.
 136   λl.
 137     \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"\ 6foldi_from_until\ 5/a\ 6 A \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 (\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|) f a l.
 138
 139 definition hd_safe ≝
 140   λA: Type[0].
 141   λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
 142   λproof: \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|.
 143   match l return λx. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → A with
 144   [ nil ⇒ λnil_absrd. ?
 145   | cons hd tl ⇒ λcons_prf. hd
 146   ] proof.
 147   normalize in nil_absrd;
 148   cases(\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)
 149   #HYP
 150   cases(HYP nil_absrd)
 151 qed.
 152
 153 definition tail_safe ≝
 154   λA: Type[0].
 155   λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
 156   λproof: \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|.
 157   match l return λx. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A with
 158   [ nil ⇒ λnil_absrd. ?
 159   | cons hd tl ⇒ λcons_prf. tl
 160   ] proof.
 161   normalize in nil_absrd;
 162   cases(\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)
 163   #HYP
 164   cases(HYP nil_absrd)
 165 qed.
 166
 167 let rec split
 168   (A: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (index: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (proof: index \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|)
 169     on index ≝
 170   match index return λx. x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l| → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) with
 171   [ O ⇒ λzero_prf. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6], l〉
 172   | S index' ⇒ λsucc_prf.
 173     match l return λx. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 index' \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) with
 174     [ nil ⇒ λnil_absrd. ?
 175     | cons hd tl ⇒ λcons_prf.
 176       let 〈l1, l2〉 ≝ split A tl index' ? in
 177         \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: l1, l2〉
 178     ] succ_prf
 179   ] proof.
 180   [1: normalize in nil_absrd;
 181       cases(\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 index')
 182       #HYP
 183       cases(HYP nil_absrd)
 184   |2: normalize in cons_prf;
 185       @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6
 186       assumption
 187   ]
 188 qed.
 189
 190 let rec nth_safe
 191   (elt_type: Type[0]) (index: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (the_list: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 elt_type)
 192   (proof: index \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 the_list |)
 193     on index ≝
 194   match index return λs. s \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 the_list | → elt_type with
 195   [ O ⇒
 196     match the_list return λt. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 t | → elt_type with
 197     [ nil        ⇒ λnil_absurd. ?
 198     | cons hd tl ⇒ λcons_proof. hd
 199     ]
 200   | S index' ⇒
 201     match the_list return λt. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 index' \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 t | → elt_type with
 202     [ nil ⇒ λnil_absurd. ?
 203     | cons hd tl ⇒
 204       λcons_proof. nth_safe elt_type index' tl ?
 205     ]
 206   ] proof.
 207   [ normalize in nil_absurd;
 208     cases (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)
 209     #ABSURD
 210     elim (ABSURD nil_absurd)
 211   | normalize in nil_absurd;
 212     cases (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 index'))
 213     #ABSURD
 214     elim (ABSURD nil_absurd)
 215   | normalize in cons_proof
 216     @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6
 217     assumption
 218   ]
 219 qed.
 220
 221 definition last_safe ≝
 222   λelt_type: Type[0].
 223   λthe_list: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 elt_type.
 224   λproof   : \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 the_list |.
 225     \ 5a href="cic:/matita/Cerco/ASM/Utils/nth_safe.fix(0,1,6)"\ 6nth_safe\ 5/a\ 6 elt_type (\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6the_list| \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) the_list ?.
 226   normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_minus.def(12)"\ 6lt_plus_to_minus\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 227 qed.
 228
 229 let rec reduce
 230   (A: Type[0]) (B: Type[0]) (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on left ≝
 231   match left with
 232   [ nil ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]〉, \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], right〉〉
 233   | cons hd tl ⇒
 234     match right with
 235     [ nil ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], left〉, \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]〉〉
 236     | cons hd' tl' ⇒
 237       let 〈cleft, cright〉 ≝ reduce A B tl tl' in
 238       let 〈commonl, restl〉 ≝ cleft in
 239       let 〈commonr, restr〉 ≝ cright in
 240         \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: commonl, restl〉, \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd' \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: commonr, restr〉〉
 241     ]
 242   ].
 243
 244 (*
 245 axiom reduce_strong:
 246   ∀A: Type[0].
 247   ∀left: list A.
 248   ∀right: list A.
 249     Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
 250 *)
 251
 252 (*
 253 let rec reduce_strong
 254   (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
 255     on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
 256   match left with
 257   [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
 258   | cons hd tl ⇒
 259     match right with
 260     [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
 261     | cons hd' tl' ⇒
 262       let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in
 263       let 〈commonl, restl〉 ≝ cleft in
 264       let 〈commonr, restr〉 ≝ cright in
 265         〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
 266     ]
 267   ].
 268   [ 1: normalize %
 269   | 2: normalize %
 270   | 3: normalize
 271        generalize in match (sig2 … (reduce_strong A B tl tl1));
 272        >p2 >p3 >p4 normalize in ⊢ (% → ?)
 273        #HYP //
 274   ]
 275 qed.*)
 276
 277 let rec map2_opt
 278   (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
 279   (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on left ≝
 280   match left with
 281   [ nil ⇒
 282     match right with
 283     [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 C)
 284     | _ ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 285     ]
 286   | cons hd tl ⇒
 287     match right with
 288     [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 289     | cons hd' tl' ⇒
 290       match map2_opt A B C f tl tl' with
 291       [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 292       | Some tail ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (f hd hd' \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: tail)
 293       ]
 294     ]
 295   ].
 296
 297 let rec map2
 298   (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
 299   (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) (proof: \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 left | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 right |) on left ≝
 300   match left return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 x | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 right | → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C with
 301   [ nil ⇒
 302     match right return λy. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 y | → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C with
 303     [ nil ⇒ λnil_prf. \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 C
 304     | _ ⇒ λcons_absrd. ?
 305     ]
 306   | cons hd tl ⇒
 307     match right return λy. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 y | → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C with
 308     [ nil ⇒ λnil_absrd. ?
 309     | cons hd' tl' ⇒ λcons_prf. (f hd hd') \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: map2 A B C f tl tl' ?
 310     ]
 311   ] proof.
 312   [1: normalize in cons_absrd;
 313       destruct(cons_absrd)
 314   |2: normalize in nil_absrd;
 315       destruct(nil_absrd)
 316   |3: normalize in cons_prf;
 317       destruct(cons_prf)
 318       assumption
 319   ]
 320 qed.
 321
 322 let rec nub_by_internal (A: Type[0]) (f: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n ≝
 323   match n with
 324   [ O ⇒
 325     match l with
 326     [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
 327     | cons hd tl ⇒ l
 328     ]
 329   | S n ⇒
 330     match l with
 331     [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
 332     | cons hd tl ⇒
 333       hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: nub_by_internal A f (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λy. \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (f y hd)) tl) n
 334     ]
 335   ].
 336
 337 definition nub_by ≝
 338   λA: Type[0].
 339   λf: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
 340   λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
 341     \ 5a href="cic:/matita/Cerco/ASM/Utils/nub_by_internal.fix(0,3,3)"\ 6nub_by_internal\ 5/a\ 6 A f l (\ 5a href="cic:/matita/basics/list2/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l).
 342
 343 let rec member (A: Type[0]) (eq: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (a: A) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
 344   match l with
 345   [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
 346   | cons hd tl ⇒ \ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 (eq a hd) (member A eq a tl)
 347   ].
 348
 349 let rec take (A: Type[0]) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on n: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A ≝
 350   match n with
 351   [ O ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
 352   | S n ⇒
 353     match l with
 354     [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
 355     | cons hd tl ⇒ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: take A n tl
 356     ]
 357   ].
 358
 359 let rec drop (A: Type[0]) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on n ≝
 360   match n with
 361   [ O ⇒ l
 362   | S n ⇒
 363     match l with
 364     [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
 365     | cons hd tl ⇒ drop A n tl
 366     ]
 367   ].
 368
 369 definition list_split ≝
 370   λA: Type[0].
 371   λn: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 372   λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
 373     \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/Cerco/ASM/Utils/take.fix(0,1,1)"\ 6take\ 5/a\ 6 A n l, \ 5a href="cic:/matita/Cerco/ASM/Utils/drop.fix(0,1,1)"\ 6drop\ 5/a\ 6 A n l〉.
 374
 375 let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → A → B)
 376                       (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
 377   match l with
 378   [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?
 379   | cons hd tl ⇒ (f n hd) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (mapi_internal A B (n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) f tl)
 380   ].
 381
 382 definition mapi ≝
 383   λA, B: Type[0].
 384   λf: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → A → B.
 385   λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
 386     \ 5a href="cic:/matita/Cerco/ASM/Utils/mapi_internal.fix(0,4,2)"\ 6mapi_internal\ 5/a\ 6 A B \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 f l.
 387
 388 let rec zip_pottier
 389   (A: Type[0]) (B: Type[0]) (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B)
 390     on left ≝
 391   match left with
 392   [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
 393   | cons hd tl ⇒
 394     match right with
 395     [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
 396     | cons hd' tl' ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd, hd'〉 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: zip_pottier A B tl tl'
 397     ]
 398   ].
 399
 400 (*
 401 let rec zip_safe
 402   (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
 403     on left ≝
 404   match left return λx. |x| = |right| → list (A × B) with
 405   [ nil ⇒ λnil_prf.
 406     match right return λx. |[ ]| = |x| → list (A × B) with
 407     [ nil ⇒ λnil_nil_prf. [ ]
 408     | cons hd tl ⇒ λnil_cons_absrd. ?
 409     ] nil_prf
 410   | cons hd tl ⇒ λcons_prf.
 411     match right return λx. |hd::tl| = |x| → list (A × B) with
 412     [ nil ⇒ λcons_nil_absrd. ?
 413     | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ?
 414     ] cons_prf
 415   ] prf.
 416   [ 1: normalize in nil_cons_absrd;
 417        destruct(nil_cons_absrd)
 418   | 2: normalize in cons_nil_absrd;
 419        destruct(cons_nil_absrd)
 420   | 3: normalize in cons_cons_prf;
 421        @injective_S
 422        assumption
 423   ]
 424 qed. *)
 425
 426 let rec zip (A: Type[0]) (B: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (r: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on l: \ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B)) ≝
 427   match l with
 428   [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 (A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B))
 429   | cons hd tl ⇒
 430     match r with
 431     [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 432     | cons hd' tl' ⇒
 433       match zip ? ? tl tl' with
 434       [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 435       | Some tail ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd, hd'〉 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: tail)
 436       ]
 437     ]
 438   ].
 439
 440 let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on l ≝
 441   match l with
 442   [ nil ⇒ a
 443   | cons hd tl ⇒ foldl A B f (f a hd) tl
 444   ].
 445
 446 lemma foldl_step:
 447  ∀A:Type[0].
 448   ∀B: Type[0].
 449    ∀H: A → B → A.
 450     ∀acc: A.
 451      ∀pre: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B.
 452       ∀hd:B.
 453        \ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc (pre\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6hd]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (H (\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc pre) hd).
 454  #A #B #H #acc #pre generalize in match acc; -acc; elim pre
 455   [ normalize; //
 456   | #hd #tl #IH #acc #X normalize; @IH ]
 457 qed.
 458
 459 lemma foldl_append:
 460  ∀A:Type[0].
 461   ∀B: Type[0].
 462    ∀H: A → B → A.
 463     ∀acc: A.
 464      ∀suff,pre: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B.
 465       \ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc (pre\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6suff) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H (\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc pre) suff).
 466  #A #B #H #acc #suff elim suff
 467   [ #pre >\ 5a href="cic:/matita/basics/list/append_nil.def(4)"\ 6append_nil\ 5/a\ 6 %
 468   | #hd #tl #IH #pre whd in ⊢ (???%) <(\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl_step.def(2)"\ 6foldl_step\ 5/a\ 6 … H ??) applyS (IH (pre\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6hd])) ]
 469 qed.
 470
 471 definition flatten ≝
 472   λA: Type[0].
 473   λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A).
 474     \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ? ? (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 ?) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] l.
 475
 476 let rec rev (A: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
 477   match l with
 478   [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A
 479   | cons hd tl ⇒ (rev A tl) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 hd ]
 480   ].
 481
 482 (*
 483 lemma append_length:
 484   ∀A: Type[0].
 485   ∀l, r: list A.
 486     |(l @ r)| = |l| + |r|.
 487   #A #L #R
 488   elim L
 489   [ %
 490   | #HD #TL #IH
 491     normalize >IH %
 492   ]
 493 qed.
 494
 495 lemma append_nil:
 496   ∀A: Type[0].
 497   ∀l: list A.
 498     l @ [ ] = l.
 499   #A #L
 500   elim L //
 501 qed.
 502
 503 lemma rev_append:
 504   ∀A: Type[0].
 505   ∀l, r: list A.
 506     rev A (l @ r) = rev A r @ rev A l.
 507   #A #L #R
 508   elim L
 509   [ normalize >append_nil %
 510   | #HD #TL #IH
 511     normalize >IH
 512     @associative_append
 513   ]
 514 qed.
 515
 516 lemma rev_length:
 517   ∀A: Type[0].
 518   ∀l: list A.
 519     |rev A l| = |l|.
 520   #A #L
 521   elim L
 522   [ %
 523   | #HD #TL #IH
 524     normalize
 525     >(append_length A (rev A TL) [HD])
 526     normalize /2/
 527   ]
 528 qed.
 529
 530 lemma nth_append_first:
 531  ∀A:Type[0].
 532  ∀n:nat.∀l1,l2:list A.∀d:A.
 533    n < |l1| → nth n A (l1@l2) d = nth n A l1 d.
 534  #A #n #l1 #l2 #d
 535  generalize in match n; -n; elim l1
 536  [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O
 537  | #h #t #Hind #k normalize
 538    cases k -k
 539    [ #Hk normalize @refl
 540    | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
 541    ]
 542  ]
 543 qed.
 544
 545 lemma nth_append_second:
 546  ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 ->
 547   nth n A (l1@l2) d = nth (n - length A l1) A l2 d.
 548  #A #n #l1 #l2 #d
 549  generalize in match n; -n; elim l1
 550  [ normalize #k #Hk <(minus_n_O) @refl
 551  | #h #t #Hind #k normalize
 552    cases k -k;
 553    [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ]
 554    | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
 555    ]
 556  ]
 557 qed.*)
 558
 559
 560 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
 561  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
 562 notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19
 563  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
 564
 565 let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
 566                         (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → A → B → A) (x: A) (i: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on l ≝
 567   match l with
 568     [ nil ⇒ x
 569     | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) tl
 570     ].
 571
 572 definition fold_left_i ≝ λA,B,f,x. \ 5a href="cic:/matita/Cerco/ASM/Utils/fold_left_i_aux.fix(0,5,1)"\ 6fold_left_i_aux\ 5/a\ 6 A B f x \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
 573
 574 (* notation "hvbox(t\lceil o \mapsto h\rceil )"
 575   with precedence 45
 576   for @{ match (? : $o=$h) with [ refl \Rightarrow $t ] }. *)
 577
 578 definition function_apply ≝
 579   λA, B: Type[0].
 580   λf: A → B.
 581   λa: A.
 582     f a.
 583
 584 notation "f break $ x"
 585   left associative with precedence 99
 586   for @{ 'function_apply $f $x }.
 587
 588 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
 589
 590 notation "f break $ x"
 591   left associative with precedence 99
 592   for @{ 'function_apply $f $x }.
 593
 594 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
 595
 596 let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n ≝
 597   match n with
 598     [ O ⇒ a
 599     | S o ⇒ f (iterate A f a o)
 600     ].
 601
 602 (* Yeah, I probably ought to do something more general... *)
 603 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
 604 with precedence 90 for @{ 'triple $a $b $c}.
 605 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
 606
 607 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
 608 with precedence 90 for @{ 'quadruple $a $b $c $d}.
 609 interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
 610
 611 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
 612  with precedence 10
 613 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
 614
 615 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
 616  with precedence 10
 617 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
 618
 619 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
 620  with precedence 10
 621 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
 622
 623 axiom pair_elim':
 624   ∀A,B,C: Type[0].
 625   ∀T: A → B → C.
 626   ∀p.
 627   ∀P: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → Prop.
 628     (∀lft, rgt. p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 → P \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 (T lft rgt)) →
 629       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
 630
 631 axiom pair_elim'':
 632   ∀A,B,C,C': Type[0].
 633   ∀T: A → B → C.
 634   ∀T': A → B → C'.
 635   ∀p.
 636   ∀P: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → C' → Prop.
 637     (∀lft, rgt. p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 → P \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 (T lft rgt) (T' lft rgt)) →
 638       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
 639
 640 lemma pair_destruct_1:
 641  ∀A,B.∀a:A.∀b:B.∀c. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6a,b〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 c.
 642  #A #B #a #b *; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 643 qed.
 644
 645 lemma pair_destruct_2:
 646  ∀A,B.∀a:A.∀b:B.∀c. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6a,b〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 c.
 647  #A #B #a #b *; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 648 qed.
 649
 650
 651 let rec exclusive_disjunction (b: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (c: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) on b ≝
 652   match b with
 653     [ true ⇒
 654       match c with
 655         [ false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
 656         | true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
 657         ]
 658     | false ⇒
 659       match c with
 660         [ false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
 661         | true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
 662         ]
 663     ].
 664
 665 (* dpm: conflicts with library definitions
 666 interpretation "Nat less than" 'lt m n = (ltb m n).
 667 interpretation "Nat greater than" 'gt m n = (gtb m n).
 668 interpretation "Nat greater than eq" 'geq m n = (geb m n).
 669 *)
 670
 671 let rec division_aux (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (n : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (p: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) ≝
 672   match \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"\ 6ltb\ 5/a\ 6 n (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 p) with
 673     [ true ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
 674     | false ⇒
 675       match m with
 676         [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
 677         | (S q) ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (division_aux q (n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 p)) p)
 678         ]
 679     ].
 680
 681 definition division ≝
 682   λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 683     match n with
 684       [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m
 685       | S o ⇒ \ 5a href="cic:/matita/Cerco/ASM/Utils/division_aux.fix(0,0,3)"\ 6division_aux\ 5/a\ 6 m m o
 686       ].
 687
 688 notation "hvbox(n break ÷ m)"
 689   right associative with precedence 47
 690   for @{ 'division $n $m }.
 691
 692 interpretation "Nat division" 'division n m = (division n m).
 693
 694 let rec modulus_aux (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (p: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) ≝
 695   match \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n p with
 696     [ true ⇒ n
 697     | false ⇒
 698       match m with
 699         [ O ⇒ n
 700         | S o ⇒ modulus_aux o (n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 p)) p
 701         ]
 702     ].
 703
 704 definition modulus ≝
 705   λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 706     match n with
 707       [ O ⇒ m
 708       | S o ⇒ \ 5a href="cic:/matita/Cerco/ASM/Utils/modulus_aux.fix(0,0,2)"\ 6modulus_aux\ 5/a\ 6 m m o
 709       ].
 710
 711 notation "hvbox(n break 'mod' m)"
 712   right associative with precedence 47
 713   for @{ 'modulus $n $m }.
 714
 715 interpretation "Nat modulus" 'modulus m n = (modulus m n).
 716
 717 definition divide_with_remainder ≝
 718   λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 719     \ 5a href="cic:/matita/basics/types/Prod.con(0,1,2)"\ 6pair\ 5/a\ 6 ? ? (m \ 5a title="Nat division" href="cic:/fakeuri.def(1)"\ 6÷\ 5/a\ 6 n) (\ 5a href="cic:/matita/Cerco/ASM/Utils/modulus.def(3)"\ 6modulus\ 5/a\ 6 m n).
 720
 721 let rec exponential (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n ≝
 722   match n with
 723     [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
 724     | S o ⇒ m \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 exponential m o
 725     ].
 726
 727 interpretation "Nat exponential" 'exp n m = (exponential n m).
 728
 729 notation "hvbox(a break ⊎ b)"
 730  left associative with precedence 50
 731 for @{ 'disjoint_union $a $b }.
 732 interpretation "sum" 'disjoint_union A B = (Sum A B).
 733
 734 theorem less_than_or_equal_monotone:
 735   ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 736     m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n).
 737  #m #n #H
 738  elim H
 739  /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 740 qed.
 741
 742 theorem less_than_or_equal_b_complete:
 743   ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 744     \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n).
 745  #m;
 746  elim m;
 747  normalize
 748  [ #n #H
 749    destruct
 750  | #y #H1 #z
 751    cases z
 752    normalize
 753    [ #H
 754      /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace {}\ 5/span\ 6\ 5/span\ 6/
 755    | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"\ 6not_le_to_not_le_S_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 756    ]
 757  ]
 758 qed.
 759
 760 theorem less_than_or_equal_b_correct:
 761   ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 762     \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
 763  #m
 764  elim m
 765  //
 766  #y #H1 #z
 767  cases z
 768  normalize
 769  [ #H
 770    destruct
 771  | #n #H lapply (H1 … H) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_monotone.def(2)"\ 6less_than_or_equal_monotone\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 772  ]
 773 qed.
 774
 775 definition less_than_or_equal_b_elim:
 776  ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 777  ∀P: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Type[0].
 778    (m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n) → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n).
 779  #m #n #P #H1 #H2;
 780  lapply (\ 5a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_correct.def(3)"\ 6less_than_or_equal_b_correct\ 5/a\ 6 m n)
 781  lapply (\ 5a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_complete.def(6)"\ 6less_than_or_equal_b_complete\ 5/a\ 6 m n)
 782  cases (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n)
 783  /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace {}\ 5/span\ 6\ 5/span\ 6/
 784 qed.
 785
 786 lemma inclusive_disjunction_true:
 787   ∀b, c: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
 788     (\ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 c \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 789   # b
 790   # c
 791   elim b
 792   [ normalize
 793     # H
 794     @ \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6
 795     %
 796   | normalize
 797     /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 798   ]
 799 qed.
 800
 801 lemma conjunction_true:
 802   ∀b, c: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
 803     \ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6 b c \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 c \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 804   # b
 805   # c
 806   elim b
 807   normalize
 808   [ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 809   | # K
 810     destruct
 811   ]
 812 qed.
 813
 814 lemma eq_true_false: \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
 815  # K
 816  destruct
 817 qed.
 818
 819 lemma inclusive_disjunction_b_true: ∀b. \ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 b \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 820  # b
 821  cases b
 822  %
 823 qed.
 824
 825 definition bool_to_Prop ≝
 826  λb. match b with [ true ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | false ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
 827
 828 coercion bool_to_Prop: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. Prop ≝ \ 5a href="cic:/matita/Cerco/ASM/Utils/bool_to_Prop.def(1)"\ 6bool_to_Prop\ 5/a\ 6 on _b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 to Type[0].
 829
 830 lemma eq_false_to_notb: ∀b. b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 b.
 831  *; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/True.con(0,1,0)"\ 6I\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 832 qed.