proposition: Lemma oplus_assoc_0 (alpha: T1): nf alpha -> forall a b c, nf a -> nf b -> nf c -> T1.lt a alpha -> T1.lt b alpha -> T1.lt c alpha -> a o+ (b o+ c) = (a o+ b) o+ c.
proof: Proof. transfinite_induction_lt alpha. clear alpha ; intros alpha Hrec Halpha. intros; destruct a, b, c; try reflexivity. - repeat rewrite oplus_0_l; repeat rewrite oplus_0_r; trivial. - now repeat rewrite oplus_0_r. - { nf_decomp H; nf_decomp H0; nf_decomp H1. repeat rewrite oplus_cons_cons. destruct (compare b1 c1) eqn:Hbc; destruct (compare a1 b1) eqn:Hab; repeat rewrite oplus_cons_cons; try compare trans Hab Hbc as Hac; try rewrite Hab; try rewrite Hbc; try rewrite Hac. - apply compare_eq_iff in Hbc as <-, Hac as <-. ass_rw Hrec (cons a1 n a2) a2 b2 c2; trivial. + f_equal; abstract lia. + apply tail_lt_cons; auto. + apply lt_le_trans with (phi0 a1). * now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n0. * now apply le_phi0. + apply lt_le_trans with (phi0 a1). * now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n0. * now apply le_phi0. - apply compare_eq_iff in Hbc as <-. ass_rw Hrec (cons b1 n0 b2) (cons a1 n a2) b2 c2; trivial. + now apply head_lt. + now apply tail_lt_cons. + apply lt_le_trans with (phi0 b1). * now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n1. * now apply le_phi0. - apply compare_eq_iff in Hbc as <-. f_equal. ass_rw_rev Hrec (cons a1 n a2) a2 (cons b1 n0 b2) (cons b1 n1 c2) ; trivial. + f_equal. now rewrite oplus_cons_cons, compare_refl. + now apply tail_lt_cons. + now apply head_lt, compare_gt_iff. + now apply head_lt, compare_gt_iff. - f_equal. ass_rw Hrec (cons c1 n1 c2) (cons a1 n a2) (cons a1 n0 b2) c2 ; trivial. + f_equal; now rewrite oplus_cons_cons, Hab. + now apply head_lt. + now apply head_lt. + now apply tail_lt_cons. - f_equal. ass_rw Hrec (cons c1 n1 c2) (cons a1 n a2) (cons a1 n0 b2) c2 ; trivial. + f_equal; now rewrite oplus_cons_cons, Hab. + now apply head_lt. + now apply head_lt. + now apply tail_lt_cons. - destruct (compare a1 c1) eqn: Hac; f_equal. + ass_rw Hrec (cons a1 n a2) a2 (cons b1 n0 b2) c2 ; trivial. * now apply tail_lt_cons. * now apply head_lt, compare_gt_iff. * apply lt_le_trans with (phi0 a1). -- apply compare_eq_iff in Hac as ->. now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n1. -- now apply le_phi0. + ass_rw Hrec (cons c1 n1 c2) (cons a1 n a2) (cons b1 n0 b2) c2 ; trivial. * now rewrite oplus_cons_cons, Hab. * now apply head_lt, compare_lt_iff. * now apply head_lt, compare_lt_iff. * now apply tail_lt_cons. + ass_rw_rev Hrec (cons a1 n a2) a2 (cons b1 n0 b2) (cons c1 n1 c2) ; trivial. * now rewrite oplus_cons_cons, Hbc. * now apply tail_lt_cons. * now apply head_lt, compare_gt_iff. * now apply head_lt, compare_gt_iff. - ass_rw_rev Hrec (cons a1 n a2) a2 b2 (cons c1 n1 c2); trivial. + now apply tail_lt_cons. + apply lt_le_trans with (phi0 a1). * apply compare_eq_iff in Hab as ->. now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n0. * now apply le_phi0. + now apply head_lt, compare_gt_iff. - ass_rw_rev Hrec (cons b1 n0 b2) (cons a1 n a2) b2 (cons c1 n1 c2) ; trivial. + now apply head_lt, compare_lt_iff. + now apply tail_lt_cons. + now apply head_lt, compare_gt_iff. - f_equal. ass_rw_rev Hrec (cons a1 n a2) a2 (cons b1 n0 b2) (cons c1 n1 c2); trivial. * f_equal; now rewrite oplus_cons_cons, Hbc. * now apply tail_lt_cons. * now apply head_lt, compare_gt_iff. * now apply head_lt, compare_gt_iff. } Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)