Library CoLoR.RPO.VRPO_Results

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Solange Coupet-Grimal and William Delobel, 2006-01-09
  • Adam Koprowski, 2007-06-03, added section proving that RPO is a reduction ordering + a number of smaller things for certification of examples.
Proofs of a relation verifying Hypotheses in RPO_Type is a well-founded monotonic strict order

Set Implicit Arguments.

Module RPO_Results (Export RPO : RPO_Model).

  Lemma var_are_min : forall x t, lt t (Var x) -> False.

  Inductive in_term_vars : variable -> term -> Prop :=
    | is_var : forall x, in_term_vars x (Var x)
    | is_in_list : forall x f ss,
      ex (fun s => In s ss /\ in_term_vars x s) -> in_term_vars x (Fun f ss).

  Lemma var_in : forall x t, lt (Var x) t -> in_term_vars x t.

  Lemma eq_elem_to_eq_list_dec : forall ss : terms,
    (forall s, In s ss -> forall t, s = t \/ s <> t) ->
    forall ts, ss = ts \/ ss <> ts.

  Lemma in_var : forall x t, t <> Var x -> in_term_vars x t -> lt (Var x) t.

  Lemma immediate_subterm_property : forall s f ss, In s ss -> lt s (Fun f ss).

  Lemma var_inclusion : forall t s, lt t s -> forall x,
    in_term_vars x t -> in_term_vars x s.

  Lemma lt_eq_f : forall t s, lt s t -> forall f ts, t = Fun f ts ->
    forall g, g =F= f -> lt s (Fun g ts).

  Lemma lt_eq_f' : forall s f g ts,
    g =F= f -> lt s (Fun f ts) -> lt s (Fun g ts).

  Lemma SPO_lt : forall u,
    (forall t s, lt u t -> lt t s -> lt u s) /\ (lt u u -> False).

  Lemma monotonic_lt : forall f ss ts,
    one_less lt ss ts -> lt (Fun f ss) (Fun f ts).

  Lemma lt_trans : transitive lt.

  Lemma lt_irrefl : irreflexive lt.

  Lemma acc_eq_f : forall f g ss,
    f =F= g -> Acc lt (Fun f ss) -> Acc lt (Fun g ss).

  Lemma Acc_lt_var : forall x, Acc lt (Var x).

  Import ListExtras.

  Lemma eqF_sym : forall f g, f =F= g -> g =F= f.

  Import VSubstitution VContext.

  Section subst_closed.

  Variable status_homomorphic : forall F ss ts f,
    (forall s t, In s ss -> In t ts -> lt s t -> lt (F s) (F t)) ->
    tau f lt ss ts -> tau f lt (map F ss) (map F ts).

  Lemma lt_subst_closed : substitution_closed lt.

  End subst_closed.

  Lemma wf_lt : well_founded lt.

  Lemma eqF_dec : forall f g, {f =F= g} + {~f =F= g}.

  Lemma ltF_dec : forall f g, {f <F g} + {~f <F g}.

  Definition term_eq (tu : term * term) :=
    let (t, u) := tu in if term_eq_dec t u then true else false.

  Lemma term_eq_correct : forall t u, term_eq (t, u) = true -> t = u.

  Notation term_eq_dec := (@term_eq_dec Sig).

  Definition ge p q := lt q p \/ p = q.

  Lemma rpo_lt_subterm_dec : forall p v
    (IH : forall t, Inb term_eq_dec t v = true
      -> forall p, {lt p t} + {~lt p t}),
    { a : term | In a v /\ ge a p } + { ~exists a : term, In a v /\ ge a p }.

  Lemma rpo_lt_dec : rel_dec lt.

End RPO_Results.