Library Rewriting_defs


Require Import Metatheory.
Require Import LambdaES_Defs.
Require Import LambdaES_Infrastructure.

Given a relation Red, constructs its contextual closure
Inductive contextual_closure (Red : pterm -> pterm -> Prop) : pterm -> pterm -> Prop :=
  | redex : forall t s, Red t s -> contextual_closure Red t s
  | beta_app_left : forall t t' u, term u -> contextual_closure Red t t' ->
                        contextual_closure Red (pterm_app t u) (pterm_app t' u)
  | beta_app_right : forall t u u', term t -> contextual_closure Red u u' ->
                        contextual_closure Red (pterm_app t u) (pterm_app t u')
  | beta_abs : forall t t' L, (forall x, x \notin L -> contextual_closure Red (t^x) (t'^x))
      -> contextual_closure Red (pterm_abs t) (pterm_abs t')
  | beta_subst_left : forall t t' u L, term u ->
                (forall x, x \notin L -> contextual_closure Red (t^x) (t'^x)) ->
                contextual_closure Red (pterm_sub t u) (pterm_sub t' u)
  | beta_subst_right : forall t u u', body t -> contextual_closure Red u u' ->
                contextual_closure Red (pterm_sub t u) (pterm_sub t u') .

Hint Constructors contextual_closure.

Given a relation Red, constructs its reflexive closure
Inductive star_closure (Red : pterm -> pterm -> Prop) : pterm -> pterm -> Prop :=
  | reflexive_reduction : forall t, star_closure Red t t
  | one_step_reduction : forall t u, Red t u -> star_closure Red t u
  | transitive_reduction : forall t u v, Red t u -> star_closure Red u v -> star_closure Red t v
.

Given a relation and an equation, constructs the relation modulo
Inductive modulo_reduction (Red : pterm -> pterm -> Prop) (Eq : pterm -> pterm -> Prop) : pterm -> pterm -> Prop :=
 | direct_reduction : forall t u, Red t u -> modulo_reduction Red Eq t u
 | left_equation : forall t u v, Eq t u -> modulo_reduction Red Eq u v -> modulo_reduction Red Eq t v
 | right_equation : forall t u v, Eq u v -> modulo_reduction Red Eq t u -> modulo_reduction Red Eq t v
.

Given a reduction, the composition of two star closure is still a star closure
Lemma transitive_closure_composition :
    forall Red t u v, star_closure Red t u -> star_closure Red u v -> star_closure Red t v.
Proof.
  intros.
  induction H.
    assumption.
    apply transitive_reduction with (u := u); trivial.
    apply transitive_reduction with (u := u) ; auto.
Qed.