matita/matita/lib/reverse_complexity/bigops_compl.ma

   1 include "reverse_complexity/complexity.ma".
   2 include "reverse_complexity/sigma_diseq.ma".
   3
   4 include alias "reverse_complexity/basics.ma".
   5
   6 lemma bigop_prim_rec: ∀a,b,c,p,f,x.
   7   bigop (b x-a x) (λi:ℕ.p 〈i+a x,x〉) ? (c 〈a x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
   8     prim_rec c
   9     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
  10         then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
  11         else fst (snd i)) (b x-a x) 〈a x ,x〉.
  12 #a #b #c #p #f #x normalize elim (b x-a x)
  13   [normalize //
  14   |#i #Hind >prim_rec_S
  15    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
  16    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
  17     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
  18   ]
  19 qed.
  20
  21 lemma bigop_prim_rec_dec: ∀a,b,c,p,f,x.
  22   bigop (b x-a x) (λi:ℕ.p 〈b x -i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x-i,x〉) =
  23     prim_rec c
  24     (λi.if p 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉
  25         then plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i))
  26         else fst (snd i)) (b x-a x) 〈b x ,x〉.
  27 #a #b #c #p #f #x normalize elim (b x-a x)
  28   [normalize //
  29   |#i #Hind >prim_rec_S
  30    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
  31    cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
  32     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
  33   ]
  34 qed.
  35
  36 lemma bigop_prim_rec_dec1: ∀a,b,c,p,f,x.
  37   bigop (S(b x)-a x) (λi:ℕ.p 〈b x - i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x- i,x〉) =
  38     prim_rec c
  39     (λi.if p 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉
  40         then plus (f 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉) (fst (snd i))
  41         else fst (snd i)) (S(b x)-a x) 〈b x,x〉.
  42 #a #b #c #p #f #x elim (S(b x)-a x)
  43   [normalize //
  44   |#i #Hind >prim_rec_S
  45    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
  46    cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
  47     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
  48   ]
  49 qed.
  50
  51 lemma sum_prim_rec1: ∀a,b,p,f,x.
  52   ∑_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
  53     prim_rec (λi.0)
  54     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
  55         then f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉 + fst (snd i)
  56         else fst (snd i)) (b x-a x) 〈a x ,x〉.
  57 #a #b #p #f #x elim (b x-a x)
  58   [normalize //
  59   |#i #Hind >prim_rec_S
  60    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
  61    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
  62     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
  63   ]
  64 qed.
  65
  66 lemma bigop_plus_c: ∀k,p,f,c.
  67   c k + bigop k (λi.p i) ? 0 plus (λi.f i) =
  68     bigop k (λi.p i) ? (c k) plus (λi.f i).
  69 #k #p #f elim k [normalize //]
  70 #i #Hind #c cases (true_or_false (p i)) #Hcase
  71 [>bigop_Strue // >bigop_Strue // <associative_plus >(commutative_plus ? (f i))
  72  >associative_plus @eq_f @Hind
  73 |>bigop_Sfalse // >bigop_Sfalse //
  74 ]
  75 qed.
  76
  77
  78 (*********************************** maximum **********************************)
  79
  80 lemma max_gen: ∀a,b,p,f,x. a ≤b →
  81   max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) = max_{i < b | leb a i ∧ p 〈i,x〉 }(f 〈i,x〉).
  82 #a #b #p #f #x @(bigop_I_gen ????? MaxA)
  83 qed.
  84
  85 lemma max_prim_rec_base: ∀a,b,p,f,x. a ≤b →
  86   max_{i < b| p 〈i,x〉 }(f 〈i,x〉) =
  87     prim_rec (λi.0)
  88     (λi.if p 〈fst i,x〉 then max (f 〈fst i,snd (snd i)〉) (fst (snd i)) else fst (snd i)) b x.
  89 #a #b #p #f #x #leab >max_gen // elim b
  90   [normalize //
  91   |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
  92    cases (true_or_false (p 〈i,x〉)) #Hcase >Hcase
  93     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
  94   ]
  95 qed.
  96
  97 lemma max_prim_rec: ∀a,b,p,f,x. a ≤b →
  98   max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
  99     prim_rec (λi.0)
 100     (λi.if leb a (fst i) ∧ p 〈fst i,x〉 then max (f 〈fst i,snd (snd i)〉) (fst (snd i)) else fst (snd i)) b x.
 101 #a #b #p #f #x #leab >max_gen // elim b
 102   [normalize //
 103   |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
 104    cases (true_or_false (leb a i ∧ p 〈i,x〉)) #Hcase >Hcase
 105     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 106   ]
 107 qed.
 108
 109 lemma max_prim_rec1: ∀a,b,p,f,x.
 110   max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 111     prim_rec (λi.0)
 112     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
 113         then max (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
 114         else fst (snd i)) (b x-a x) 〈a x ,x〉.
 115 #a #b #p #f #x elim (b x-a x)
 116   [normalize //
 117   |#i #Hind >prim_rec_S
 118    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 119    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
 120     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 121   ]
 122 qed.
 123
 124 (* the argument is 〈b-a,〈a,x〉〉 *)
 125
 126 definition max_unary_pr ≝ λp,f.unary_pr (λx.0)
 127     (λi.
 128       let k ≝ fst i in
 129       let r ≝ fst (snd i) in
 130       let a ≝ fst (snd (snd i)) in
 131       let x ≝ snd (snd (snd i)) in
 132       if p 〈k + a,x〉 then max (f 〈k+a,x〉) r else r).
 133
 134 lemma max_unary_pr1: ∀a,b,p,f,x.
 135   max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 136     ((max_unary_pr p f) ∘ (λx.〈b x - a x,〈a x,x〉〉)) x.
 137 #a #b #p #f #x normalize >fst_pair >snd_pair @max_prim_rec1
 138 qed.
 139
 140 definition aux_compl ≝ λhp,hf.λi.
 141   let k ≝ fst i in
 142   let r ≝ fst (snd i) in
 143   let a ≝ fst (snd (snd i)) in
 144   let x ≝ snd (snd (snd i)) in
 145   hp 〈k+a,x〉 + hf 〈k+a,x〉 + (* was MSC r*) MSC i .
 146
 147 definition aux_compl1 ≝ λhp,hf.λi.
 148   let k ≝ fst i in
 149   let r ≝ fst (snd i) in
 150   let a ≝ fst (snd (snd i)) in
 151   let x ≝ snd (snd (snd i)) in
 152   hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 153
 154 lemma aux_compl1_def: ∀k,r,m,hp,hf.
 155   aux_compl1 hp hf 〈k,〈r,m〉〉 =
 156   let a ≝ fst m in
 157   let x ≝ snd m in
 158   hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 159 #k #r #m #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair //
 160 qed.
 161
 162 lemma aux_compl1_def1: ∀k,r,a,x,hp,hf.
 163   aux_compl1 hp hf 〈k,〈r,〈a,x〉〉〉 = hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 164 #k #r #a #x #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair
 165 >fst_pair >snd_pair //
 166 qed.
 167
 168 axiom Oaux_compl: ∀hp,hf. O (aux_compl1 hp hf) (aux_compl hp hf).
 169
 170 lemma MSC_max: ∀f,h,x. CF h f → MSC (max_{i < x}(f i)) ≤ max_{i < x}(h i).
 171 #f #h #x #hf elim x // #i #Hind >bigop_Strue [|//] >bigop_Strue [|//]
 172 whd in match (max ??);
 173 cases (true_or_false (leb (f i) (bigop i (λi0:ℕ.true) ? 0 max(λi0:ℕ.f i0))))
 174 #Hcase >Hcase
 175   [@(transitive_le … Hind) @le_maxr //
 176   |@(transitive_le … (MSC_out … hf i)) @le_maxl //
 177   ]
 178 qed.
 179
 180 lemma CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 181   CF ha a → CF hb b → CF hp p → CF hf f →
 182   O s (λx.ha x + hb x +
 183        (∑_{i ∈[a x ,b x[ }
 184          (hp 〈i,x〉 + hf 〈i,x〉 + max_{i ∈ [a x, b x [ }(hf 〈i,x〉)))) →
 185   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
 186 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #HO
 187 @ext_CF1 [|#x @max_unary_pr1]
 188 @(CF_comp ??? (λx.ha x + hb x))
 189   [|@CF_comp_pair
 190     [@CF_minus [@(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 191     |@CF_comp_pair
 192       [@(O_to_CF … CFa) @O_plus_l //
 193       | @(O_to_CF … CF_id) @O_plus_r @le_to_O @(MSC_in … CFb)
 194       ]
 195     ]
 196   |@(CF_prim_rec … MSC … (aux_compl1 hp hf))
 197      [@CF_const
 198      |@(O_to_CF … (Oaux_compl … ))
 199       @CF_if
 200        [@(CF_comp p … MSC … CFp)
 201          [@CF_comp_pair
 202            [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
 203            |@CF_comp_snd @CF_comp_snd @CF_snd]
 204          |@le_to_O #x normalize >commutative_plus >associative_plus @le_plus //
 205          ]
 206        |@CF_max1
 207          [@(CF_comp f … MSC … CFf)
 208            [@CF_comp_pair
 209              [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
 210              |@CF_comp_snd @CF_comp_snd @CF_snd]
 211            |@le_to_O #x normalize >commutative_plus //
 212            ]
 213          |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 214          ]
 215        |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 216        ]
 217      |@O_refl
 218      ]
 219   |@(O_trans … HO) -HO
 220    @(O_trans ? (λx:ℕ
 221    .ha x+hb x
 222     +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
 223      (λi:ℕ
 224       .(λi0:ℕ
 225         .hp 〈i0,x〉+hf 〈i0,x〉
 226          +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
 227           (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
 228     [
 229    @le_to_O #n @le_plus // whd in match (unary_pr ???);
 230    >fst_pair >snd_pair >bigop_prim_rec elim (b n - a n)
 231     [normalize //
 232     |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >aux_compl1_def1
 233      >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
 234      >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
 235       [-Hind @le_plus // normalize >fst_pair >snd_pair
 236        @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
 237          (λi1:ℕ.hf 〈i1+a n,n〉)))
 238         [elim x [normalize @MSC_le]
 239          #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
 240          >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
 241           [cases (true_or_false (leb (f 〈x0+a n,n〉)
 242             (prim_rec (λx00:ℕ.O)
 243              (λi:ℕ
 244             .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 245              then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
 246                            (fst (snd i))
 247                       then fst (snd i)
 248                       else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 249              else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
 250            [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 251            |@(transitive_le … (MSC_out … CFf …)) @(le_maxl … (le_n …))
 252            ]
 253          |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 254          ]
 255        |@(le_maxr … (le_n …))
 256        ]
 257      |@(transitive_le … Hind) -Hind
 258       generalize in match (bigop x (λi:ℕ.true) ? 0 max
 259               (λi1:ℕ.(λi2:ℕ.hf 〈i2,n〉) (i1+a n))); #c
 260       generalize in match (hf 〈x+a n,n〉); #c1
 261       elim x [//] #x0 #Hind
 262       >prim_rec_S >prim_rec_S normalize >fst_pair >fst_pair >snd_pair
 263       >snd_pair >snd_pair >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair
 264       >fst_pair @le_plus
 265        [@le_plus // cases (true_or_false (leb c1 c)) #Hcase
 266         >Hcase normalize // @lt_to_le @not_le_to_lt @(leb_false_to_not_le ?? Hcase)
 267        |@Hind
 268        ]
 269      ]
 270    ]
 271  |@O_plus [@O_plus_l //] @le_to_O #x
 272   <bigop_plus_c @le_plus // @(transitive_le … (MSC_pair …)) @le_plus
 273    [@MSC_out @CFa | @MSC_out @(O_to_CF MSC … (CF_const x)) @le_to_O @(MSC_in … CFb)]
 274  ]
 275 qed.
 276
 277 axiom daemon : ∀P:Prop.P.
 278 axiom O_extl: ∀s1,s2,f. (∀x.s1 x = s2 x) → O s1 f → O s2 f.
 279
 280 lemma CF_max2: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 281   CF ha a → CF hb b → CF hp p → CF hf f →
 282   O s (λx.ha x + hb x +
 283        (b x - a x)*max_{i ∈ [a x, b x [ }(hp 〈i,x〉 + hf 〈i,x〉)) →
 284   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
 285 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #Os
 286 @(O_to_CF … Os (CF_max … CFa CFb CFp CFf ?)) @O_plus
 287   [@O_plus_l @O_refl
 288   |@O_plus_r @O_ext2 [|| #x @(bigop_op  … plusAC)]
 289    @O_plus
 290     [@le_to_O normalize #x @sigma_to_Max
 291     |@le_to_O #x @transitive_le [|@sigma_const] @le_times //
 292      @Max_le #i #lti #_ @(transitive_le ???? (le_MaxI … ))
 293       [@le_plus_n | // | @lt_minus_to_plus_r // | //]
 294     ]
 295   ]
 296 qed.
 297
 298 (*
 299 lemma CF_max_monotonic: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 300   CF ha a → CF hb b → CF hp p → CF hf f →
 301   O s (λx.ha x + hb x +
 302        (b x - a x)*max_{i ∈ [a x, b x [ }(hp 〈i,x〉 + hf 〈i,x〉)) →
 303   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
 304 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #Os
 305 @(O_to_CF … Os (CF_max … CFa CFb CFp CFf ?)) @O_plus
 306   [@O_plus_l @O_refl
 307   |@O_plus_r @O_ext2 [|| #x @(bigop_op  … plusAC)]
 308    @O_plus
 309     [@le_to_O normalize #x @sigma_to_Max
 310     |@le_to_O #x @transitive_le [|@sigma_const] @le_times //
 311      @Max_le #i #lti #_ @(transitive_le ???? (le_MaxI … ))
 312       [@le_plus_n | // | @lt_minus_to_plus_r // | //]
 313     ]
 314   ]
 315 qed.
 316 *)
 317
 318 (* old
 319 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 320   CF ha a → CF hb b → CF hp p → CF hf f →
 321   O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
 322   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)). *)
 323
 324 (******************************** minimization ********************************)
 325
 326 let rec my_minim a f x k on k ≝
 327   match k with
 328   [O ⇒ a
 329   |S p ⇒ if eqb (my_minim a f x p) (a+p)
 330          then if f 〈a+p,x〉 then a+p else S(a+p)
 331          else (my_minim a f x p) ].
 332
 333 lemma my_minim_S : ∀a,f,x,k.
 334   my_minim a f x (S k) =
 335     if eqb (my_minim a f x k) (a+k)
 336     then if f 〈a+k,x〉 then a+k else S(a+k)
 337     else (my_minim a f x k) .
 338 // qed.
 339
 340 lemma my_minim_fa : ∀a,f,x,k. f〈a,x〉 = true → my_minim a f x k = a.
 341 #a #f #x #k #H elim k // #i #Hind normalize >Hind
 342 cases (true_or_false (eqb a (a+i))) #Hcase >Hcase normalize //
 343 <(eqb_true_to_eq … Hcase) >H //
 344 qed.
 345
 346 lemma my_minim_nfa : ∀a,f,x,k. f〈a,x〉 = false →
 347 my_minim a f x (S k) = my_minim (S a) f x k.
 348 #a #f #x #k #H elim k
 349   [normalize <plus_n_O >H >eq_to_eqb_true //
 350   |#i #Hind >my_minim_S >Hind >my_minim_S <plus_n_Sm //
 351   ]
 352 qed.
 353
 354 lemma my_min_eq : ∀a,f,x,k.
 355   min k a (λi.f 〈i,x〉) = my_minim a f x k.
 356 #a #f #x #k lapply a -a elim k // #i #Hind #a normalize in ⊢ (??%?);
 357 cases (true_or_false (f 〈a,x〉)) #Hcase >Hcase
 358   [>(my_minim_fa … Hcase) // | >Hind @sym_eq @(my_minim_nfa … Hcase) ]
 359 qed.
 360
 361 (* cambiare qui: togliere S *)
 362
 363
 364 definition minim_unary_pr ≝ λf.unary_pr (λx.S(fst x))
 365     (λi.
 366       let k ≝ fst i in
 367       let r ≝ fst (snd i) in
 368       let b ≝ fst (snd (snd i)) in
 369       let x ≝ snd (snd (snd i)) in
 370       if f 〈b-k,x〉 then b-k else r).
 371
 372 definition compl_minim_unary ≝ λhf:nat → nat.λi.
 373       let k ≝ fst i in
 374       let b ≝ fst (snd (snd i)) in
 375       let x ≝ snd (snd (snd i)) in
 376       hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
 377
 378 definition compl_minim_unary_aux ≝ λhf,i.
 379       let k ≝ fst i in
 380       let r ≝ fst (snd i) in
 381       let b ≝ fst (snd (snd i)) in
 382       let x ≝ snd (snd (snd i)) in
 383       hf 〈b-k,x〉 + MSC i.
 384
 385 lemma compl_minim_unary_aux_def : ∀hf,k,r,b,x.
 386   compl_minim_unary_aux hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈r,〈b,x〉〉〉.
 387 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
 388 qed.
 389
 390 lemma compl_minim_unary_def : ∀hf,k,r,b,x.
 391   compl_minim_unary hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
 392 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
 393 qed.
 394
 395 lemma compl_minim_unary_aux_def2 : ∀hf,k,r,x.
 396   compl_minim_unary_aux hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈r,x〉〉.
 397 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
 398 qed.
 399
 400 lemma compl_minim_unary_def2 : ∀hf,k,r,x.
 401   compl_minim_unary hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈S(fst x),snd x〉〉.
 402 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
 403 qed.
 404
 405 lemma min_aux: ∀a,f,x,k. min (S k) (a x) (λi:ℕ.f 〈i,x〉) =
 406   ((minim_unary_pr f) ∘ (λx.〈S k,〈a x + k,x〉〉)) x.
 407 #a #f #x #k whd in ⊢ (???%); >fst_pair >snd_pair
 408 lapply a -a (* @max_prim_rec1 *)
 409 elim k
 410   [normalize #a >fst_pair >snd_pair >fst_pair >snd_pair >snd_pair >fst_pair
 411    <plus_n_O <minus_n_O >fst_pair //
 412   |#i #Hind #a normalize in ⊢ (??%?); >prim_rec_S >fst_pair >snd_pair
 413    >fst_pair >snd_pair >snd_pair >fst_pair <plus_n_Sm <(Hind (λx.S (a x)))
 414    whd in ⊢ (???%); >minus_S_S <(minus_plus_m_m (a x) i) //
 415 qed.
 416
 417 lemma minim_unary_pr1: ∀a,b,f,x.
 418   μ_{i ∈[a x,b x]}(f 〈i,x〉) =
 419     if leb (a x) (b x) then ((minim_unary_pr f) ∘ (λx.〈S (b x) - a x,〈b x,x〉〉)) x
 420     else (a x).
 421 #a #b #f #x cases (true_or_false (leb (a x) (b x))) #Hcase >Hcase
 422   [cut (b x = a x + (b x - a x))
 423     [>commutative_plus <plus_minus_m_m // @leb_true_to_le // ]
 424    #Hcut whd in ⊢ (???%); >minus_Sn_m [|@leb_true_to_le //]
 425    >min_aux whd in ⊢ (??%?); <Hcut //
 426   |>eq_minus_O // @not_le_to_lt @leb_false_to_not_le //
 427   ]
 428 qed.
 429
 430 axiom sum_inv: ∀a,b,f.∑_{i ∈ [a,S b[ }(f i) = ∑_{i ∈ [a,S b[ }(f (a + b - i)).
 431
 432 (*
 433 #a #b #f @(bigop_iso … plusAC) whd %{(λi.b - a - i)} %{(λi.b - a -i)} %
 434   [%[#i #lti #_ normalize @eq_f >commutative_plus <plus_minus_associative
 435     [2: @le_minus_to_plus_r //
 436      [// @eq_f @@sym_eq @plus_to_minus
 437     |#i #Hi #_ % [% [@le_S_S
 438 *)
 439
 440 example sum_inv_check : ∑_{i ∈ [3,6[ }(i*i) = ∑_{i ∈ [3,6[ }((8-i)*(8-i)).
 441 normalize // qed.
 442
 443 (* rovesciamo la somma *)
 444
 445 lemma CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 446   CF sa a → CF sb b → CF sf f →
 447   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC 〈b x - i,〈S(b x),x〉〉)) →
 448   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 449 #a #b #f #ha #hb #hf #s #CFa #CFb #CFf #HO
 450 @ext_CF1 [|#x @minim_unary_pr1]
 451 @CF_if
 452   [@CF_le @(O_to_CF … HO)
 453     [@(O_to_CF … CFa) @O_plus_l @O_plus_l  @O_refl
 454     |@(O_to_CF … CFb) @O_plus_l @O_plus_r @O_refl
 455     ]
 456   |@(CF_comp ??? (λx.ha x + hb x))
 457     [|@CF_comp_pair
 458       [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 459       |@CF_comp_pair
 460         [@(O_to_CF … CFb) @O_plus_r //
 461         |@(O_to_CF … CF_id) @O_plus_r @le_to_O @(MSC_in … CFb)
 462         ]
 463       ]
 464     |@(CF_prim_rec_gen … MSC … (compl_minim_unary_aux hf))
 465       [@((λx:ℕ.fst (snd x)
 466           +compl_minim_unary hf
 467           〈fst x,
 468           〈unary_pr fst
 469             (λi:ℕ
 470              .(let (k:ℕ) ≝fst i in
 471                let (r:ℕ) ≝fst (snd i) in
 472                let (b:ℕ) ≝fst (snd (snd i)) in
 473                let (x:ℕ) ≝snd (snd (snd i)) in if f 〈b-S k,x〉 then b-S k else r ))
 474           〈fst x,snd (snd x)〉,
 475           snd (snd x)〉〉))
 476       |@CF_compS @CF_fst
 477       |@CF_if
 478         [@(CF_comp f … MSC … CFf)
 479           [@CF_comp_pair
 480             [@CF_minus [@CF_comp_fst @CF_comp_snd @CF_snd|@CF_fst]
 481             |@CF_comp_snd @CF_comp_snd @CF_snd]
 482           |@le_to_O #x normalize >commutative_plus //
 483           ]
 484         |@(O_to_CF … MSC)
 485           [@le_to_O #x normalize //
 486           |@CF_minus
 487             [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_fst]
 488           ]
 489         |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 490         ]
 491       |@O_plus
 492         [@O_plus_l @O_refl
 493         |@O_plus_r @O_ext2 [||#x >compl_minim_unary_aux_def2 @refl]
 494          @O_trans [||@le_to_O #x >compl_minim_unary_def2 @le_n]
 495          @O_plus [@O_plus_l //]
 496          @O_plus_r
 497          @O_trans [|@le_to_O #x @MSC_pair] @O_plus
 498            [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_fst …))
 499             >fst_pair @le_n]
 500          @O_trans [|@le_to_O #x @MSC_pair] @O_plus
 501            [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …))
 502             >snd_pair @(transitive_le ???? (le_fst …)) >fst_pair
 503             normalize >snd_pair >fst_pair lapply (surj_pair x)
 504             * #x1 * #x2 #Hx >Hx >fst_pair >snd_pair elim x1 //
 505             #i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
 506             cases (f ?) [@le_S // | //]]
 507          @le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …)) >snd_pair
 508          >(expand_pair (snd (snd x))) in ⊢ (?%?); @le_pair //
 509         ]
 510       ]
 511     |cut (O s (λx.ha x + hb x +
 512             ∑_{i ∈[a x ,S(b x)[ }(hf 〈a x+b x-i,x〉 + MSC 〈b x -(a x+b x-i),〈S(b x),x〉〉)))
 513       [@(O_ext2 … HO) #x @eq_f @sum_inv] -HO #HO
 514      @(O_trans … HO) -HO
 515      @(O_trans ? (λx:ℕ.ha x+hb x
 516        +bigop (S(b x)-a x) (λi:ℕ.true) ?
 517         (MSC 〈b x,x〉) plus (λi:ℕ.(λj.hf j + MSC 〈b x - fst j,〈S(b (snd j)),snd j〉〉) 〈b x- i,x〉)))
 518       [@le_to_O #n @le_plus // whd in match (unary_pr ???);
 519        >fst_pair >snd_pair >(bigop_prim_rec_dec1 a b ? (λi.true))
 520         (* it is crucial to recall that the index is bound by S(b x) *)
 521         cut (S (b n) - a n ≤ S (b n)) [//]
 522         elim (S(b n) - a n)
 523         [normalize //
 524         |#x #Hind #lex >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
 525          >compl_minim_unary_def >prim_rec_S >fst_pair >snd_pair >fst_pair
 526          >snd_pair >fst_pair >snd_pair >fst_pair whd in ⊢ (??%); >commutative_plus
 527          @le_plus [2:@Hind @le_S @le_S_S_to_le @lex] -Hind >snd_pair
 528          >minus_minus_associative // @le_S_S_to_le //
 529         ]
 530       |@O_plus [@O_plus_l //] @O_ext2 [||#x @bigop_plus_c]
 531        @O_plus
 532         [@O_plus_l @O_trans [|@le_to_O #x @MSC_pair]
 533          @O_plus
 534            [@O_plus_r @le_to_O @(MSC_out … CFb)
 535            |@O_plus_r @le_to_O @(MSC_in … CFb)
 536            ]
 537         |@O_plus_r @(O_ext2 … (O_refl …)) #x @same_bigop
 538           [//|#i #H #_ @eq_f2 [@eq_f @eq_f2 //|>fst_pair @eq_f @eq_f2  //]
 539         ]
 540       ]
 541     ]
 542   ]
 543   |@(O_to_CF … CFa) @(O_trans … HO) @O_plus_l @O_plus_l @O_refl
 544   ]
 545
 546 qed.
 547
 548 lemma CF_mu2: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 549   CF sa a → CF sb b → CF sf f →
 550   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC〈S(b x),x〉)) →
 551   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 552 #a #b #f #sa #sb #sf #s #CFa #CFb #CFf #HO
 553 @(O_to_CF … HO (CF_mu … CFa CFb CFf ?)) @O_plus [@O_plus_l @O_refl]
 554 @O_plus_r @O_ext2 [|| #x @(bigop_op  … plusAC)]
 555 @O_plus [@le_to_O #x @le_sigma //]
 556 @(O_trans ? (λx.∑_{i ∈[a x ,S(b x)[ }(MSC(b x -i)+MSC 〈S(b x),x〉)))
 557   [@le_to_O #x @le_sigma //]
 558 @O_ext2 [|| #x @(bigop_op  … plusAC)] @O_plus
 559   [@le_to_O #x @le_sigma // #i #lti #_ @(transitive_le … (MSC 〈S (b x),x〉)) //
 560    @monotonic_MSC @(transitive_le … (S(b x))) // @le_S //
 561   |@le_to_O #x @le_sigma //
 562   ]
 563 qed.
 564
 565 (* uses MSC_S *)
 566
 567 lemma CF_mu3: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s. (∀x.sf x > 0) →
 568   CF sa a → CF sb b → CF sf f →
 569   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC〈b x,x〉)) →
 570   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 571 #a #b #f #sa #sb #sf #s #sfpos #CFa #CFb #CFf #HO
 572 @(O_to_CF … HO (CF_mu2 … CFa CFb CFf ?)) @O_plus [@O_plus_l @O_refl]
 573 @O_plus_r @O_ext2 [|| #x @(bigop_op  … plusAC)]
 574 @O_plus [@le_to_O #x @le_sigma //]
 575 @le_to_O #x @le_sigma // #x #lti #_ >MSC_pair_eq >MSC_pair_eq <associative_plus
 576 @le_plus // @(transitive_le … (MSC_sublinear … )) /2 by monotonic_lt_plus_l/
 577 qed.
 578
 579 lemma CF_mu4: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s. (∀x.sf x > 0) →
 580   CF sa a → CF sb b → CF sf f →
 581   O s (λx.sa x + sb x + (S(b x) - a x)*Max_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
 582   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 583 #a #b #f #sa #sb #sf #s #sfpos #CFa #CFb #CFf #HO
 584 @(O_to_CF … HO (CF_mu3 … sfpos CFa CFb CFf ?)) @O_plus [@O_plus_l @O_refl]
 585 @O_ext2 [|| #x @(bigop_op  … plusAC)] @O_plus_r @O_plus
 586   [@le_to_O #x @sigma_to_Max
 587   |lapply (MSC_in …  CFf) #Hle
 588    %{1} %{0} #n #_ @(transitive_le … (sigma_const …))
 589    >(commutative_times 1) <times_n_1
 590    cases (decidable_le (S (b n)) (a n)) #H
 591     [>(eq_minus_O … H) //
 592     |lapply (le_S_S_to_le … (not_le_to_lt … H)) -H #H
 593      @le_times // @(transitive_le … (Hle … ))
 594      cut (b n = b n - a n + a n) [<plus_minus_m_m // ]
 595      #Hcut >Hcut in ⊢ (?%?); @(le_Max (λi.sf 〈i+a n,n〉)) /2/
 596     ]
 597   ]
 598 qed.
 599
 600 (*
 601 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 602   CF sa a → CF sb b → CF sf f →
 603   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
 604   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)). *)
 605
 606
 607