proposition: Lemma compare_spec : forall t1 t2, CompSpec eq lt t1 t2 (compare t1 t2).
proof: Proof. intros t1 t2. case_eq (Pos.eqb (fstpp(t1)) (fstpp(t2))); intro HF. apply Pos.eqb_eq in HF. case_eq (Pos.eqb (sndpp(t1)) (sndpp(t2))); intro HS. apply Pos.eqb_eq in HS. unfold CompSpec. assert (HC : compare t1 t2 = Eq). unfold compare. assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Eq). unfold Pos.compare. rewrite HF. apply Pos.compare_cont_refl. assert (HCS : Pos.compare (sndpp(t1)) (sndpp(t2)) = Eq). unfold Pos.compare. rewrite HS. apply Pos.compare_cont_refl. rewrite HCF; rewrite HCS. intuition. rewrite HC. apply CompEq. unfold eq. rewrite HF; rewrite HS; split; intuition. case_eq (Pos.ltb (sndpp(t1)) (sndpp(t2))); intro HLS. assert (HC : compare t1 t2 = Lt). unfold compare. assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Eq). unfold Pos.compare. rewrite HF. apply Pos.compare_cont_refl. assert (HCS : Pos.compare (sndpp(t1)) (sndpp(t2)) = Lt). unfold Pos.compare. apply Pos.ltb_lt in HLS. apply Pnat.nat_of_P_lt_Lt_compare_complement_morphism. apply Pnat.Pos2Nat.inj_lt. assumption. rewrite HCF; rewrite HCS. intuition. rewrite HC. apply CompLt. unfold lt. apply Pos.eqb_eq in HF. rewrite HF. apply Pos.ltb_lt in HLS. assumption. assert (HLS2 : Pos.ltb (sndpp(t2)) (sndpp(t1)) = true). apply Pos.ltb_nlt in HLS. apply Pos.le_nlt in HLS. apply Pos.lt_eq_cases in HLS. elim HLS; intro HLS2. apply Pos.ltb_lt. assumption. apply Pos.eqb_neq in HS. rewrite HLS2 in HS. intuition. assert (HC : compare t1 t2 = Gt). unfold compare. assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Eq). unfold Pos.compare. rewrite HF. apply Pos.compare_cont_refl. assert (HCS : Pos.compare (sndpp(t1)) (sndpp(t2)) = Gt). unfold Pos.compare. apply Pos.ltb_lt in HLS2. apply Pnat.nat_of_P_gt_Gt_compare_complement_morphism. apply Pnat.Pos2Nat.inj_gt. apply Pos.gt_lt_iff. assumption. rewrite HCF; rewrite HCS. intuition. rewrite HC. apply CompGt. unfold lt. apply Pos.eqb_eq in HF. rewrite Pos.eqb_sym in HF. rewrite HF. apply Pos.ltb_lt in HLS2. assumption. case_eq (Pos.ltb (fstpp(t1)) (fstpp(t2))); intro HLF. assert (HC : compare t1 t2 = Lt). unfold compare. assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Lt). unfold Pos.compare. apply Pos.ltb_lt in HLF. apply Pnat.nat_of_P_lt_Lt_compare_complement_morphism. apply Pnat.Pos2Nat.inj_lt. assumption. rewrite HCF. intuition. rewrite HC. apply CompLt. unfold lt. rewrite HF. apply Pos.ltb_lt in HLF. assumption. assert (HLF2 : Pos.ltb (fstpp(t2)) (fstpp(t1)) = true). apply Pos.ltb_nlt in HLF. apply Pos.le_nlt in HLF. apply Pos.lt_eq_cases in HLF. elim HLF; intro HLF2. apply Pos.ltb_lt. assumption. apply Pos.eqb_neq in HF. rewrite HLF2 in HF. intuition. assert (HC : compare t1 t2 = Gt). unfold compare. assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Gt). unfold Pos.compare. apply Pos.ltb_lt in HLF2. apply Pnat.nat_of_P_gt_Gt_compare_complement_morphism. apply Pnat.Pos2Nat.inj_gt. apply Pos.gt_lt_iff. assumption. rewrite HCF. intuition. rewrite HC. apply CompGt. unfold lt. rewrite Pos.eqb_sym in HF. rewrite HF. apply Pos.ltb_lt in HLF2. assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms