proposition: Lemma loop_aux_spec e f a todo todo': below_I ((e,f)::todo) -> loop_aux e f a todo = Some todo' -> epsilon' a e = epsilon' a f /\ todo ≦ todo' /\ below_I todo' /\ forall i, In i I -> In (pderiv' a i e, pderiv' a i f) todo'.
proof: Proof. unfold loop_aux. case eqb_bool_spec. 2: discriminate. intros Heps Hvars E. split. assumption. injection E. clear E Heps. revert todo'. induction I as [|i J IH]; simpl fold_right; intro todo'. intros <-. split. reflexivity. split. intros ? ? ?. apply Hvars; now right. intros _ []. intro E. destruct todo' as [|p todo']. discriminate. injection E. intros H <-. clear E. apply IH in H as [H1 [H2 H3]]. clear IH. split. fold_cons. rewrite <- H1. lattice. split. intros ? ? [E|H]. injection E; intros <- <-. rewrite sup_app, 2deriv'_vars, <-sup_app. apply Hvars. now left. now apply H2. intros b [<-|Hb]. now left. right. now apply H3. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex