Library Rewriting_defs
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.
| 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
.
| 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
.
| 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.
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.