proposition: Theorem gen_row_correct: forall l i z, In l (gen_row i z) <-> exists j, l = L (Pos i j) z /\ j < size.
proof: Proof. unfold gen_row, indexes. assert (Eq1: forall a l i z, In l (fold_right (fun y l => lit_insert (L (Pos i y) z) l) nil (progression size a)) <-> (exists j: nat, l = L (Pos i j) z /\ a <= j < a + size)); auto. elim size; simpl; auto. intros a l i z; split. intros H; case H. intros (j, (_, (H1, H2))); contradict H2; rewrite Nat.add_0_r; auto with arith. intros size1 Rec1 a l i z; split. intros H1. match type of H1 with In ?X (lit_insert ?Y ?Z) => case (lit_insert_in X Y Z); intros tmp _; case (tmp H1); clear tmp end; intros H2; subst. exists a; split; auto with arith. split; auto with arith. apply Nat.le_lt_trans with (a + 0); auto with arith. case (Rec1 (S a) l i z); intros tmp _; case tmp; auto; clear tmp. intros j (H3, (H4, H5)); exists j; split; auto with arith. rewrite <- plus_n_Sm; split; auto with arith. intros (j, (H3, (H4, H5))). match goal with |- In ?X (lit_insert ?Y ?Z) => case (lit_insert_in X Y Z); intros _ tmp; apply tmp; clear tmp end; auto. case le_lt_eq_dec with (1 := H4); clear H4; intros H4; auto. right; case (Rec1 (S a) l i z); intros _ tmp; apply tmp; clear tmp. rewrite <- plus_n_Sm in H5; exists j; auto with arith. subst; auto. intros l i z; split; intros H. case (Eq1 0 l i z); intros tmp _; case tmp; clear tmp Eq1; auto. rewrite Nat.add_0_l; intros j (H1, (H2, H3)); exists j; auto. case H; intros j (H1, H2); clear H. case (Eq1 0 l i z); intros _ tmp; apply tmp; clear tmp; exists j; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia