proposition: Theorem normalize_tree_correct : forall t pos, convert_tree (normalize_tree t pos) <-> if pos then convert_tree t else not (convert_tree t).
proof: Proof. induction t as [| |a|t Ht|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2] ; destruct pos ; split ; simpl ; try easy. try (intros H ; now apply H). apply (Ht false). apply (Ht false). intros H. intros H'. apply H'. now apply (Ht true). intros H. apply (Ht true). now destruct (decidable_tree t) as [H'|H']. intros (H1,H2). split. now apply (Ht1 true). now apply (Ht2 true). intros (H1,H2). split. now apply (Ht1 true). now apply (Ht2 true). intros [H|H] (H1,H2). now apply (Ht1 false). now apply (Ht2 false). specialize (Ht1 false). specialize (Ht2 false). intros H. destruct (decidable_tree t1) as [H'|H']. right. apply Ht2. contradict H. now split. left. now apply Ht1. intros [H|H]. left. now apply (Ht1 true). right. now apply (Ht2 true). intros [H|H]. left. now apply (Ht1 true). right. now apply (Ht2 true). intros (H1,H2) [H|H]. now apply (Ht1 false). now apply (Ht2 false). intros H. split. apply (Ht1 false). contradict H. now left. apply (Ht2 false). contradict H. now right. intros [H|H] H'. now apply (Ht1 false) in H. now apply (Ht2 true). intros H. destruct (decidable_tree t1) as [H'|H']. right. apply (Ht2 true). now apply H. left. now apply (Ht1 false). intros (H1,H2) H'. apply (Ht1 true) in H1. apply H' in H1. now apply (Ht2 false). intros H. split. destruct (decidable_tree t1) as [H'|H']. now apply (Ht1 true). now elim H. apply (Ht2 false). now contradict H. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library