proposition: Lemma compute_transitive_closure_spec {k} n (gs : list (graph k)) l : compute_transitive_closure n gs = Finished _ l -> is_transitive_closure gs l.
proof: Proof. eapply (compute_transitive_closure_elim (fun k n gs r => forall l, r = Finished k l -> is_transitive_closure gs l) (fun k n gs l acc res => is_transitive_closure acc acc -> forall l', res = Finished k l' -> incl (l ++ acc) l' /\ (incl gs (l ++ acc) -> incl_transitive_closure_of gs (l ++ acc) -> becoming_transitive_closure acc l' -> incl (l ++ acc) l' /\ incl_transitive_closure_of (l ++ acc) l' /\ is_transitive_closure gs l')) (fun k n gs g l acc newc => let gs' := (g :: acc) in match newc with | None => is_transitive_closure gs' gs' /\ transitive_closure_of g gs' | Some g' => ~ In g' gs' /\ exists a, In a gs' /\ (g' = (g ⋅ a) \/ g' = (a ⋅ g)) end) (fun k n gs g l acc newc res => forall l', res = Finished k l' -> incl (l ++ acc) l' /\ (match newc with | Some c => incl gs (c :: g :: l ++ acc) /\ incl_transitive_closure_of gs (c :: g :: l ++ acc) | None => incl gs (g :: l ++ acc) /\ incl_transitive_closure_of gs (g :: l ++ acc) /\ transitive_closure_of g (g :: acc) /\ becoming_transitive_closure (g :: acc) l' end -> is_transitive_closure gs l'))); clear. all:try discriminate; eauto. + intros * H l Haux. Admitted. Definition gn_set : list (graph 2) := [ T_graph_l; T_graph_r ]. Transparent compute_transitive_closure. Local Open Scope string_scope. Equations print_fin {k} (f : fin k) : String.string := print_fin fz := "0"; print_fin (fs fz) := "1"; print_fin (fs (fs fz)) := "2"; print_fin (fs (fs (fs fz))) := "3"; print_fin f := "> 3". Equations print_nat (n : nat) : string := print_nat 0 := "0"; print_nat 1 := "1"; print_nat 2 := "2"; print_nat 3 := "3"; print_nat 4 := "4"; print_nat x := "5". Equations print_node {k'} (f : nat) (data : option (bool * fin k')) : string := print_node f None := ""; print_node f (Some (weight, f')) := print_nat f ++ (if weight then "<" else "<=") ++ print_fin f'. Equations print_fin_fn {k k'} (f : fin k -> option (bool * fin k')) : string := print_fin_fn (k := 0) f := ""; print_fin_fn (k := S k) f := print_node (k' - S k) (f fz) ++ " , " ++ print_fin_fn (fun n => f (fs n)). Equations print_graph {k} (f : graph k) : string := print_graph (k := 0) f := "empty"; print_graph (k := S n) f := print_fin_fn f. Equations print_list {A} (f : A -> string) (l : list A) : string := print_list f nil := ""; print_list f (cons a b) := f a ++ " ; " ++ print_list f b. Eval compute in print_list print_graph gn_set. Definition eq_dec_graph {k} : forall x y : graph k, { x = y } + { x <> y }. Proof. intros x y. destruct (eqb x y) eqn:Heq. left. destruct (eqb_spec x y). auto. discriminate. right. destruct (eqb_spec x y). auto. discriminate. auto. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect