+
+lemma loop_S_true :
+ ∀A,n,f,p,a. p a = true →
+ loop A (S n) f p a = Some ? a.
+#A #n #f #p #a #pa normalize >pa //
+qed.
+
+lemma loop_S_false :
+ ∀A,n,f,p,a. p a = false →
+ loop A (S n) f p a = loop A n f p (f a).
+normalize #A #n #f #p #a #Hpa >Hpa %
+qed.
+
+lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
+ loop A k1 f p a1 = Some ? a2 →
+ loop A (k2+k1) f p a1 = Some ? a2.
+#A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
+[normalize #a0 #Hfalse destruct
+|#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
+ cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
+]
+qed.
+
+lemma loop_merge : ∀A,f,p,q.(∀b. p b = false → q b = false) →
+ ∀k1,k2,a1,a2,a3,a4.
+ loop A k1 f p a1 = Some ? a2 →
+ f a2 = a3 → q a2 = false →
+ loop A k2 f q a3 = Some ? a4 →
+ loop A (k1+k2) f q a1 = Some ? a4.
+#Sig #f #p #q #Hpq #k1 elim k1
+ [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
+ |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
+ cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
+ [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
+ whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
+ whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
+ |normalize >(Hpq … pa1) normalize
+ #H1 #H2 #H3 @(Hind … H2) //
+ ]
+ ]
+qed.
+
+lemma loop_split : ∀A,f,p,q.(∀b. q b = true → p b = true) →
+ ∀k,a1,a2.
+ loop A k f q a1 = Some ? a2 →
+ ∃k1,a3.
+ loop A k1 f p a1 = Some ? a3 ∧
+ loop A (S(k-k1)) f q a3 = Some ? a2.
+#A #f #p #q #Hpq #k elim k
+ [#a1 #a2 normalize #Heq destruct
+ |#i #Hind #a1 #a2 normalize
+ cases (true_or_false (q a1)) #Hqa1 >Hqa1 normalize
+ [ #Ha1a2 destruct
+ @(ex_intro … 1) @(ex_intro … a2) %
+ [normalize >(Hpq …Hqa1) // |>Hqa1 //]
+ |#Hloop cases (true_or_false (p a1)) #Hpa1
+ [@(ex_intro … 1) @(ex_intro … a1) %
+ [normalize >Hpa1 // |>Hqa1 <Hloop normalize //]
+ |cases (Hind …Hloop) #k2 * #a3 * #Hloop1 #Hloop2
+ @(ex_intro … (S k2)) @(ex_intro … a3) %
+ [normalize >Hpa1 normalize // | @Hloop2 ]
+ ]
+ ]
+ ]
+qed.
+
+(*
+lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
+ ∀k1,k2,a1,a2,a3.
+ loop A k1 f p a1 = Some ? a2 →
+ loop A k2 f q a2 = Some ? a3 →
+ loop A (k1+k2) f q a1 = Some ? a3.
+#Sig #f #p #q #Hpq #k1 elim k1
+ [normalize #k2 #a1 #a2 #a3 #H destruct
+ |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
+ cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
+ [#eqa1a2 destruct #H @loop_incr //
+ |normalize >(Hpq … pa1) normalize
+ #H1 #H2 @(Hind … H2) //
+ ]
+ ]
+qed.
+*)