proposition: Theorem simplify_tree_correct : forall t, convert_tree t -> convert_tree (simplify_tree t).
proof: Proof. induction t as [| |a|t Ht|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2] ; try easy. destruct t ; try easy. intros H. now apply H. intros (H1,H2). specialize (Ht1 H1). specialize (Ht2 H2). simpl. destruct (simplify_tree t1) ; try easy ; destruct (simplify_tree t2) ; try easy ; split ; easy. intros [H|H]. specialize (Ht1 H). simpl. destruct (simplify_tree t1) ; try easy ; destruct (simplify_tree t2) ; try easy ; left ; easy. specialize (Ht2 H). simpl. destruct (simplify_tree t1) ; try easy ; destruct (simplify_tree t2) ; try easy ; right ; easy. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library