Library CoLoR.NonTermin.AVarCond

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-11-02
violation of variable condition

Set Implicit Arguments.

Section S.

  Variable Sig : Signature.

  Notation rules := (rules Sig).

  Lemma var_cond_mod : forall E R : rules,
    ~rules_preserve_vars R -> EIS (red_mod E R).

  Lemma var_cond : forall R : rules, ~rules_preserve_vars R -> EIS (red R).

End S.

Ltac var_cond Sig :=
  (apply var_cond_mod || apply var_cond);
    rewrite <- (ko (@brules_preserve_vars_ok Sig));
      (check_eq || fail 10 "variable condition satisfied").