Library CoLoR.HORPO.HorpoWf

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
This file is the development of the proof of well-foundedness of the higher-order recursive path ordering due to Jouannaud and Rubio.

Set Implicit Arguments.

Require Import RelExtras.
Require Import ListExtras.
Require Import Horpo.
Require Import Computability.
Require Import LexOrder.
Require Import HorpoComp.

Module HorpoWf (S : TermsSig.Signature)
               (Prec : Horpo.Precedence with Module S := S).

  Module HC := HorpoComp.HorpoComp S Prec.
  Export HC.

  Lemma acc_mul_acc_wfmul_aux : (M: Multiset),
    Acc horpo_mul_lt M
     (WM: WFterms), M = WM Acc H_WFterms_lt WM.

    intros M AccM.
    apply Acc_ind with
      (R := MultisetLT horpo)
      (P := fun M (WM: WFterms),
                       M = WFterms_to_mul WM Acc H_WFterms_lt WM).
    intros x acc_mul acc_WM WM x_WM.
    intros y y_lt_WM.
    apply acc_WM with (WFterms_to_mul y).
    rewrite x_WM.

  Lemma acc_mul_acc_wfterms : (WM: WFterms),
    Acc horpo_mul_lt WM Acc H_WFterms_lt WM.

    intros WM acc_WM.
    apply acc_mul_acc_wfmul_aux with (WFterms_to_mul WM); trivial.

  Lemma wf_MulLt_WFterms : well_founded H_WFterms_lt.

    unfold well_founded; intro W.
    destruct W as [Ts CompTs].
    apply acc_mul_acc_wfterms.
    unfold horpo_mul_lt; apply mOrd_acc.
    apply (Eqset_def_gtA_eqA_compat horpo).
    intros x x_comp.
    assert (xComp: CompH x).
    apply CompTs.
    destruct (member_multiset_list Ts x_comp).
    unfold eqA in H0; unfold TermsEqset.eqA in H0; rewrite H0; trivial.
    apply horpo_comp_imp_acc; trivial.

  Module H_WFmul_ord <: Ord.

    Module SetWF <: SetA.
      Definition A := WFterms.
    End SetWF.
    Module S := Eqset_def SetWF.
    Definition A := WFterms.
    Definition gtA := transp H_WFterms_lt.
    Definition gtA_eqA_compat := Eqset_def_gtA_eqA_compat gtA.

  End H_WFmul_ord.

  Module Lex := LexOrder.LexicographicOrder Prec.P.O H_WFmul_ord.
  Import Lex.

  Lemma compTerms : M N Ns, M [>>] Ns CompTerms (appArgs M)
    ( n, In n Ns subterm n N)
    ( N', subterm N' N M >> N' CompH N')
    CompTerms Ns.

    intros M N Ns M_red_Ns argsMcomp Ns_sub_N IH.
    induction M_red_Ns as
      [ M
      | M Th Tt M_red_Th M_red_Tt IHargs
      | M Th Tt Marg_red_Th M_red_Tt IHargs
      ]; unfold CompTerms.
    intros x in_x_nil; absurd (In x nil); auto.
    intros x x_Th_Tt; case x_Th_Tt; intro xT.
    rewrite <- xT.
    apply IH.
    apply Ns_sub_N; auto with datatypes.
    fold (In x Tt) in xT; apply IHargs; auto with datatypes.
    intros x x_Th_Tt; case x_Th_Tt; intro xT.
    rewrite <- xT.
    destruct Marg_red_Th as [M' M'arg M'_red_Th].
    destruct M'_red_Th as [M' Th M_red_Th | M'].
    unfold CompH; apply horpo_comp_step_comp with M'.
    apply argsMcomp; trivial.
    apply argsMcomp; trivial.
    fold (In x Tt) in xT; apply IHargs; auto with datatypes.

  Lemma arg_mul_arg : m M, m in (list2multiset (appArgs M)) isArg m M.

    intros m M m_in_M.
    destruct (member_multiset_list (appArgs M) m_in_M) as
      [m' m'_in_M m_m'].
    unfold eqA in m_m'; unfold TermsEqset.eqA in m_m'; rewrite m_m'; trivial.

  Lemma argsComp_appComp_aux :
     Px: pair,
      ( Py: pair, Py <lex Px
         M, algebraic M term (appHead M) = ^fst Py
          appArgs M = proj1_sig (snd Py) CompH M)
     M N,
      algebraic M term (appHead M) = ^fst Px appArgs M = proj1_sig (snd Px)
      ( N', subterm N' N M >> N' CompH N')
      M >> N CompH N.

    intros Px IH_out M N Mnorm Mhead Margs IH_in MN.
    destruct Px as [f fArgs]; simpl in × .
    destruct MN as [M N eqTypeMN eqEnvMN _ Nnorm horpoMN].
    destruct horpoMN as
      [ M N _ Msub
      | M N f' g Mhead' Nhead f'_gt_g Margs_gt_N
      | M N f' Mhead' Nhead argsM_mul_argsN
      | M N Ns Napp Ns_flat_N Margs_Ns
      | M N Mapp' Napp Mhead' Margs_mul_Nargs
      | M N Mabs Nabs _
      | M N MNbeta
    destruct Msub as [M' M'arg M'_ge_N].
    assert (M'comp: CompH M').
    apply (proj2_sig fArgs); rewrite <- Margs; exact M'arg.
    destruct M'_ge_N as [M' N M'_N | M'].
    unfold CompH; apply horpo_comp_step_comp with M'; auto with horpo.
    assert (argsNcomp: CompTerms (appArgs N)).
    apply compTerms with M N; trivial.
    rewrite Margs; exact (proj2_sig fArgs).
    intros; apply appUnit_subterm; auto with terms.
    term_inv N.
    set (Nmul := exist (fun Ts: TermsCompTerms Ts)
         (appArgs N) argsNcomp).
    apply IH_out with (Py := (g, Nmul)); auto with terms.
    assert (ff': f = f'); [congruence | idtac].
    constructor 1; rewrite ff'; auto with terms.
    inversion argsM_mul_argsN as [aM aN argsM_horpo_argsN aMdef aNdef].
    assert (argsNcomp: CompTerms (appArgs N)).
    unfold CompTerms; intros n n_arg_N.
    assert (n_in_N: n in (list2multiset (appArgs N))).
    apply member_list_multiset; trivial.
    destruct (mOrd_elts_ge argsM_horpo_argsN n_in_N)
       as [m m_in_M [m_gt_n | m_eq_n]].
    apply horpo_comp_step_comp with m.
    apply (proj2_sig fArgs); rewrite <- Margs.
    apply arg_mul_arg; trivial.
    unfold eqA in m_eq_n; unfold TermsEqset.eqA in m_eq_n; rewrite <- m_eq_n.
    apply (proj2_sig fArgs); rewrite <- Margs.
    apply arg_mul_arg; trivial.
    set (Nmul := exist (fun Ts: TermsCompTerms Ts)
          (appArgs N) argsNcomp).
    assert (NfApp: isFunApp N).
    unfold isFunApp; apply funS_is_funS with f'; trivial.
    apply IH_out with (Py := (f', Nmul)); auto with terms.
    constructor 2.
    assert (ff': f = f'); [congruence | rewrite ff'; auto with sets].
    unfold H_WFmul_ord.gtA, H_WFterms_lt, WFterms_to_mul,
           horpo_mul_lt, MultisetLT, transp.
    simpl; apply mOrd_inclusion with horpo.
    intros x y x_y; trivial.
    rewrite <- Margs; trivial.
    assert (Ns_comp: CompTerms Ns).
    apply compTerms with M N; trivial.
    rewrite Margs; exact (proj2_sig fArgs).
    intros; apply partialFlattening_subterm with Ns; trivial.
    unfold CompH; apply horpo_comp_pflat with Ns; trivial.
    absurd (isFunApp M); eauto with terms.
    rewrite appHead_notApp in Mhead; term_inv M.
    assert (Napp: isApp N).
    apply app_beta_isapp with M f; trivial.
    assert (Mapp: isApp M).
    term_inv M.
    apply beta_notFunS with Tr N; unfold Tr; auto with terms.
    assert (NargsComp: CompTerms (appArgs N)).
    unfold CompTerms; intros P P_arg_N.
    case (app_beta_args_eq P Mapp MNbeta Mhead P_arg_N).
    intro Parg.
    apply (proj2_sig fArgs P).
    rewrite <- Margs; exact Parg.
    destruct 1 as [Mb Mb_P M_Mb].
    unfold CompH; apply horpo_comp_step_comp with Mb.
    apply (proj2_sig fArgs); rewrite <- Margs; trivial.
    apply beta_imp_horpo; trivial.
    apply algebraic_arg with M; trivial.
    set (Nmul := exist (fun Ts: TermsCompTerms Ts)
           (appArgs N) NargsComp).
    fold CompH;
      apply IH_out with (Py := (f, Nmul))(M := N);
      auto with terms.
    constructor 2.
    auto with sets.
    destruct (app_beta_args Mapp MNbeta Mhead) as
      [[al ar] [[tl tr] [tlM [trN [tltr [Mb_args Nb_args]]]]]].
    unfold H_WFmul_ord.gtA, transp, H_WFterms_lt, horpo_mul_lt,
      MultisetLT, transp, WFterms_to_mul; simpl in × .
    rewrite <- Margs.
    rewrite Mb_args; rewrite Nb_args.
    apply mulOrd_oneElemDiff.
    intros x x' y y' xx' yy'.
    unfold eqA in xx', yy'. unfold TermsEqset.eqA in xx', yy'.
    rewrite <- xx'; rewrite <- yy'; trivial.
    apply beta_imp_horpo; trivial. apply algebraic_arg with M; trivial.
    apply app_beta_headSymbol with M; trivial.

  Lemma argsComp_appComp_ind : (P: pair) M,
    algebraic M term (appHead M) = Fun (fst P)
    appArgs M = proj1_sig (snd P) CompH M.

    intro P.
    apply well_founded_ind with
      (R := LexProd_Lt)
      (P := fun (Px: pair) ⇒
           algebraic M
           term (appHead M) = Fun (fst Px)
           appArgs M = proj1_sig (snd Px)
         CompH M).
    apply lexprod_wf.
    apply Prec.Ord_wf.
    apply wf_MulLt_WFterms.
    clear P.
    intros P IH_out M Mnorm Mhead Margs.
    assert (Mneutral: isNeutral M).
    term_inv M.
    rewrite_rl (horpo_neutral_comp_step Mnorm Mneutral).
    intros N; fold CompH.
    apply well_founded_ind with
      (R := subterm)
      (P := fun (N: Term) ⇒
         M >> N CompH N).
    apply subterm_wf.
    clear N.
    intros N IH_in M_red_N.
    apply argsComp_appComp_aux with P M; trivial.

  Lemma argsComp_appComp : M, algebraic M isFunS (appHead M)
    ( P, isArg P M CompH P) CompH M.

    intros M Mnorm Mhead argsComp.
    set (Args := exist (fun Ts: TermsCompTerms Ts)
      (appArgs M) argsComp).
    assert (Mf: f, term (appHead M) = ^f).
    set (MH := appHead M) in ×.
    term_inv MH.
     f; trivial.
    destruct Mf as [f Mhead_f].
    apply argsComp_appComp_ind with (P := (f, Args))(M := M); trivial.

  Lemma subst_comp : M G (MG: correct_subst M G),
    algebraic M CompSubst G algebraicSubstitution G
    CompH (subst MG).

    intro M.
    apply well_founded_ind with
      (R := subterm)
      (P := fun (M: Term) ⇒
          G (MG: correct_subst M G),
           algebraic M
           CompSubst G
           ( i T, G |-> i/T algebraic T)
           CompH (subst MG)).
    apply subterm_wf.
    clear M; intros M IH G MG Mnorm Gcomp Gnorm.
    destruct M as [E Pt TM TypM]; simpl in × .
    destruct Pt.
    assert (Mvar: isVar (buildT TypM)).
    dependent inversion TypM; simpl; trivial.
    destruct (var_subst MG) as [[T [p GpT MGterm]] | MG_M]; trivial.
    apply horpo_comp_conv with T.
    apply Gcomp; trivial.
    apply nth_some_in with p; trivial.
    apply terms_conv_criterion; auto.
    apply env_comp_sym.
    apply subst_env_compat with p; trivial.
    apply horpo_var_comp; trivial.
    apply var_is_var with x; trivial.
    assert (termMG: term (subst MG) = term (buildT TypM)).
    apply funS_presubst.
    apply funS_is_funS with f; trivial.
    apply argsComp_appComp; term_inv (subst MG).
    apply funS_algebraic.
    simpl; inversion termMG.
    replace (f_type f) with (type (buildT TypM)).
    apply algebraic_funS; trivial.
    apply funS_is_funS with f; trivial.
    destruct TypM; try_solve.
    apply funS_is_funS with f; trivial.

    assert (Mabs: isAbs (buildT TypM)).
    apply abs_isAbs with A0 Pt; trivial.
    unfold CompH; apply horpo_comp_abs with (abs_subst_abs Mabs MG).
    apply algebraic_subst; trivial.
    intros S CS T TS Tcomp.
    destruct (abs_subst Mabs MG) as [MG_type MG_body].
    set (CS_Mbody := subst_abs_c Mabs MG).
    assert (CSj : correct_subst (absBody Mabs)
             (Some T :: lift_subst G 1)).
    rewrite MG_body in CS.
    apply subst_disjoint_c with (subst_abs_c Mabs MG); trivial.
    apply singleton_correct_single with S; trivial.
    assert (CS_all: correct_subst (subst CS_Mbody) S).
    rewrite MG_body in CS; trivial.
    assert (S_Sj: subst CS = subst CSj).
    rewrite (subst_eq CS CS_all); trivial.
    set (CS_all' := singleton_correct_single CS_all TS).
    rewrite <- (singleton_subst CS_all' CS_all TS).
    apply subst_disjoint.
    rewrite S_Sj.
    apply IH.
    apply absBody_subterm.
    apply algebraic_absBody; trivial.
    intros Q Qin.
    case (in_inv Qin).
    intro Q_P.
    inversion Q_P; rewrite <- H0; trivial.
    intro Q_G.
    destruct (in_lift_subst Q G 1 Q_G) as [W W_G Q_lift_W].
    rewrite Q_lift_W.
    unfold CompH; apply horpo_comp_lift.
    apply Gcomp; trivial.
    intros i W SW.
    destruct i.
    inversion SW.
    rewrite <- H0; apply horpo_comp_algebraic; trivial.
    inversion SW.
    destruct (var_subst_lift_rev G 1 H0) as [W' [GW' WW']].
    rewrite WW'.
    apply algebraic_lift.
    apply (Gnorm i); trivial.

    set (M := buildT TypM) in × .
    assert (Mapp: isApp M).
    eapply app_isApp; simpl; trivial.
    destruct (app_subst Mapp MG) as [SL SR].
    destruct (isFunApp_dec M).

    apply argsComp_appComp.
    apply algebraic_subst; trivial.
    apply funS_head_subst; trivial.
    intros P Parg.
    destruct (list_In_nth (tail (appUnits (subst MG))) P Parg) as [p unit_p].
    assert (nth_error (appUnits (subst MG)) (S p) = Some P).
    destruct (appUnits (subst MG)); trivial.
    destruct p; try_solve.
    destruct (appUnits_subst_rev (S p) MG i H) as [P' [MP' PP']].
    rewrite PP'.
    assert (P'arg_aux: nth_error (tail (appUnits M)) p = Some P').
    inversion MP'.
    clear PP'; destruct (appUnits M); try_solve.
    assert (P'arg: isArg P' M).
    unfold isArg, appArgs.
    apply nth_some_in with p; trivial.
    apply IH; trivial.
    apply appUnit_subterm; trivial.
    apply appArg_is_appUnit; trivial.
    apply algebraic_arg with M; trivial.

    unfold CompH; apply horpo_comp_app with (app_subst_app Mapp MG).
    rewrite SL.
    apply IH; trivial.
    apply appBodyL_subterm.
    apply algebraic_appBodyL; trivial.
    rewrite SR.
    apply IH; trivial.
    apply appBodyR_subterm.
    apply algebraic_appBodyR; trivial.

  Require SN.

  Lemma horpo_beta_wf : M, algebraic M SN.SN horpo M.

    intros M Mnorm.
    apply SN.Acc_transp_SN.
    apply horpo_comp_imp_acc.
    assert (Mid_comp: CompH (subst (emptySubst_correct M))).
    apply subst_comp; trivial.
    red; contradiction.
    intros p T; destruct p; try_solve.
    rewrite <- (emptySubst_neutral (emptySubst_correct M)); trivial.
    apply emptySubst_empty.

End HorpoWf.