proposition: Lemma in_transitive_closure {k} (g : list (graph k)) (l : list (graph k)) (T : relation (k_tuple_type k)) (approx : approximates_family g T) : is_transitive_closure g l -> forall i, exists fam : list (graph k), (forall g, In g fam -> In g l) /\ approximates_family fam (power i T).
proof: Proof. unfold is_transitive_closure. intros. destruct H as [inS inScomp]. induction i in |- *; simp power. unfold approximates. - exists g. intuition. - destruct IHi as [famgi [Ingi gixz]]. exists (compose_family famgi g). intuition. + revert H. clear -inS inScomp Ingi. induction famgi. simpl. intros []. simpl. rewrite in_app_iff in_map_iff. intros [[x [<- Inx]]| Ing]. apply inScomp. intuition auto. apply Ingi. constructor. auto. apply IHfamgi; auto. intros. apply Ingi; eauto with datatypes. + red. intros x y [z [powxz Tzy]]. do 2 red in approx, gixz. specialize (gixz _ _ powxz). specialize (approx _ _ Tzy). eapply graphs_relation_compose; intuition. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect