proposition: Lemma prog_loop n: forall rel todo, loop n rel todo = Some true -> prog rel (rel++todo) -> below_I todo -> exists rel', rel++todo ≦ rel' /\ prog rel' rel'.
proof: Proof. unfold loop. rewrite powerfix_linearfix. generalize (pow2 n). clear n. intro n. induction n; intros rel todo Hloop Hrel Hvars. discriminate. simpl in Hloop. destruct todo as [|[e f] todo]. exists rel. split. now rewrite app_nil_r. now rewrite app_nil_r in Hrel. revert Hloop. case rel_mem_spec. intros Hef Hloop. apply IHn in Hloop as (rel'&H1&H2). eexists. split. 2: eassumption. rewrite <- H1. rewrite <-(In_cons Hef) at 2. fold_cons. lattice. eapply prog_x_leq. apply Hrel. rewrite <-(In_cons Hef) at 2. fold_cons. lattice. intros ? ? ?. apply Hvars. now right. intros _. fold_ugregex_type. case_eq (ofold (X:=ord Pred -> bool) (loop_aux e f) A todo). 2: discriminate. intros todo' Htodo' Hloop. apply fold_loop_aux_spec in Htodo' as [Htodo' [Hvars' Hef]]. 2: assumption. destruct (IHn _ _ Hloop) as (rel'&Hrel'&Hrel''). 2: assumption. clear - Hef Hvars Hvars' Hrel Htodo'. apply (@prog_cup_x [_]). eapply prog_x_leq. intros ? ? [E|[]]. injection E; intros <- <-; clear E. split. apply Hvars. now left. apply Hef. lattice. eapply prog_x_leq. apply Hrel. rewrite <- Htodo'. fold_cons. lattice. eexists. split. 2: eassumption. rewrite <-Hrel', <-Htodo'. fold_cons. lattice. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex