Library nijn.Syntax.Signature.RewritingSystem

Require Import Prelude.Basics.
Require Import Prelude.TransitiveClosure.
Require Import Syntax.Signature.Types.
Require Import Syntax.Signature.Contexts.
Require Import Syntax.Signature.Terms.
Require Import Syntax.Signature.TermWeakenings.
Require Import Syntax.Signature.TermSubstitutions.

Rewriting systems

First, we look at certain closure properties and how to create relations closed under these
Inductive compatibilityClosure
          {B : Type}
          {F : Type}
          {ar : F → ty B}
          (R : ∀ (C : con B) (A : ty B), tm ar C A → tm ar C A → Type)
          (C : con B)
  : ∀ (A : ty B), tm ar C A → tm ar C A → Type
  :=
| App_l : ∀ {A1 A2 : ty B}
                 {f1 f2 : tm ar C (A1 ⟶ A2)}
                 (x : tm ar C A1),
    compatibilityClosure R _ _ f1 f2
    → compatibilityClosure R _ _ (f1 · x) (f2 · x)
| App_r : ∀ {A1 A2 : ty B}
                 (f : tm ar C (A1 ⟶ A2))
                 {x1 x2 : tm ar C A1},
    compatibilityClosure R _ _ x1 x2
    → compatibilityClosure R _ _ (f · x1) (f · x2)
| CLam : ∀ {A1 A2 : ty B}
               {f1 f2 : tm ar (A1 ,, C) A2},
    compatibilityClosure R _ _ f1 f2
    → compatibilityClosure R _ _ (λ f1) (λ f2)
| CStep : ∀ {A : ty B}
                 {t1 t2 : tm ar C A},
    R _ _ t1 t2 → compatibilityClosure R _ _ t1 t2.

Arguments App_l {_ _ _ _ _ _ _ _ _} _ _.
Arguments App_r {_ _ _ _ _ _ _} _ {_ _} _.
Arguments CLam {_ _ _ _ _ _ _ _ _} _.
Arguments CStep {_ _ _ _ _ _ _ _} _.

To formulate the beta rule, we need a particular substitution
Definition beta_sub
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A : ty B}
           (t : tm ar C A)
  : sub ar C (A ,, C)
  := ExtendSub (idSub C ar) t.

Reducing a beta redex
Inductive baseBetaStep
          {B : Type}
          {F : Type}
          {ar : F → ty B}
          (C : con B)
  : ∀ (A : ty B), tm ar C A → tm ar C A → Type
  :=
| Beta : ∀ {A1 A2 : ty B}
                (f : tm ar (A1 ,, C) A2)
                (x : tm ar C A1),
    baseBetaStep _ _ ((λ f) · x) (subTm f (beta_sub x)).

Arguments Beta {_ _ _ _ _ _} _ _.

A single beta step
Definition betaStep
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A : ty B}
  : tm ar C A → tm ar C A → Type
  := compatibilityClosure baseBetaStep C A.

Notation "t1 '~>β' t2" := (betaStep t1 t2) (at level 70).

Definition betaRed
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A : ty B}
  : tm ar C A → tm ar C A → Type
  := transitiveClosure (fun t1 t2 ⇒ t1 ~>β t2).

Notation "t1 '~>β*' t2" := (betaRed t1 t2) (at level 70).

Formers for beta reduction
Definition betaRed_step
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A : ty B}
           {t1 t2 : tm ar C A}
           (p : t1 ~>β t2)
  : t1 ~>β× t2
  := TStep p.

Definition beta_Trans
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A : ty B}
           {t1 t2 t3 : tm ar C A}
           (p : t1 ~>β× t2)
           (q : t2 ~>β× t3)
  : t1 ~>β× t3
  := Trans p q.

Definition beta_App_l_help
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A1 A2 A3 : ty B}
           {f1 f2 : tm ar C A3}
           (x : tm ar C A1)
           (p : f1 ~>β× f2)
           (q : A3 = (A1 ⟶ A2))
  : ((transport (tm ar C) q f1) · x) ~>β× ((transport (tm ar C) q f2) · x).
Proof.
  induction p.
  - subst ; simpl.
    apply TStep.
    apply App_l.
    exact r.
  - exact (Trans IHp1 IHp2).
Defined.

Definition beta_App_l
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A1 A2 : ty B}
           {f1 f2 : tm ar C (A1 ⟶ A2)}
           (x : tm ar C A1)
           (p : f1 ~>β× f2)
  : (f1 · x) ~>β× (f2 · x)
  := beta_App_l_help x p eq_refl.

Definition beta_App_r
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A1 A2 : ty B}
           (f : tm ar C (A1 ⟶ A2))
           {x1 x2 : tm ar C A1}
           (p : x1 ~>β× x2)
  : (f · x1) ~>β× (f · x2).
Proof.
  induction p.
  - apply TStep.
    apply App_r.
    exact r.
  - exact (Trans IHp1 IHp2).
Defined.

Definition beta_Lam
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A1 A2 : ty B}
           {f1 f2 : tm ar (A1 ,, C) A2}
           (p : f1 ~>β× f2)
  : (λ f1) ~>β× (λ f2).
Proof.
  induction p.
  - apply TStep.
    apply CLam.
    exact r.
  - exact (Trans IHp1 IHp2).
Defined.

Definition beta_betaRed
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {C : con B}
           {A1 A2 : ty B}
           (f : tm ar (A1 ,, C) A2)
           (x : tm ar C A1)
  : ((λ f) · x) ~>β× (subTm f (beta_sub x)).
Proof.
  apply TStep.
  apply CStep.
  apply Beta.
Defined.

Rewriting system in an AFS

First we look at the base steps in an AFS
Inductive baseRewStep
          {B : Type}
          {F : Type}
          {ar : F → ty B}
          {R : Type}
          {Rcon : R → con B}
          {Rtar : R → B}
          (lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r)))
          (C : con B)
  : ∀ (A : ty B), tm ar C A → tm ar C A → Type
  :=
| AFSBeta : ∀ {A : ty B}
                   (t1 t2 : tm ar C A),
    baseBetaStep _ _ t1 t2 → baseRewStep lhs rhs _ _ t1 t2
| AFSRew : ∀ (r : R)
                  (s : sub ar C (Rcon r)),
    baseRewStep lhs rhs _ _ (subTm (lhs r) s) (subTm (rhs r) s).

Arguments AFSBeta {_ _ _ _ _ _} _ _ {_ _ _ _} _.
Arguments AFSRew {_ _ _ _ _ _} _ _ {_} _ _.

Now we introduce the single step relation
Definition rewStep
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           (lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r)))
           {C : con B}
           {A : ty B}
  : tm ar C A → tm ar C A → Type
  := compatibilityClosure (baseRewStep lhs rhs) C A.

The rewriting relation in an AFS
Definition rew
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           (lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r)))
           {C : con B}
           {A : ty B}
  : tm ar C A → tm ar C A → Type
  := transitiveClosure (fun t1 t2 ⇒ rewStep lhs rhs t1 t2).

Formers for reduction in an AFS
Definition rew_step
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           (lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r)))
           {C : con B}
           {A : ty B}
           {t1 t2 : tm ar C A}
           (p : rewStep lhs rhs t1 t2)
  : rew lhs rhs t1 t2
  := TStep p.

Definition rew_Trans
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           {lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r))}
           {C : con B}
           {A : ty B}
           {t1 t2 t3 : tm ar C A}
           (p : rew lhs rhs t1 t2)
           (q : rew lhs rhs t2 t3)
  : rew lhs rhs t1 t3
  := Trans p q.

Definition rew_App_l_help
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           {lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r))}
           {C : con B}
           {A1 A2 A3 : ty B}
           {f1 f2 : tm ar C A3}
           (x : tm ar C A1)
           (p : rew lhs rhs f1 f2)
           (q : A3 = (A1 ⟶ A2))
  : rew lhs rhs ((transport (tm ar C) q f1) · x) ((transport (tm ar C) q f2) · x).
Proof.
  induction p.
  - subst ; simpl.
    apply TStep.
    apply App_l.
    exact r.
  - exact (Trans IHp1 IHp2).
Defined.

Definition rew_App_l
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           {lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r))}
           {C : con B}
           {A1 A2 : ty B}
           {f1 f2 : tm ar C (A1 ⟶ A2)}
           (x : tm ar C A1)
           (p : rew lhs rhs f1 f2)
  : rew lhs rhs (f1 · x) (f2 · x)
  := rew_App_l_help x p eq_refl.

Definition rew_App_r
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           {lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r))}
           {C : con B}
           {A1 A2 : ty B}
           {f : tm ar C (A1 ⟶ A2)}
           (x1 x2 : tm ar C A1)
           (p : rew lhs rhs x1 x2)
  : rew lhs rhs (f · x1) (f · x2).
Proof.
  induction p.
  - apply TStep.
    apply App_r.
    exact r.
  - exact (Trans IHp1 IHp2).
Defined.

Definition rew_Lam
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           (lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r)))
           {C : con B}
           {A1 A2 : ty B}
           {f1 f2 : tm ar (A1 ,, C) A2}
           (p : rew lhs rhs f1 f2)
  : rew lhs rhs (λ f1) (λ f2).
Proof.
  induction p.
  - apply TStep.
    apply CLam.
    exact r.
  - exact (Trans IHp1 IHp2).
Defined.

Definition rew_betaRed
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           (lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r)))
           {C : con B}
           {A1 A2 : ty B}
           (f : tm ar (A1 ,, C) A2)
           (x : tm ar C A1)
  : rew lhs rhs ((λ f) · x) (subTm f (beta_sub x)).
Proof.
  apply TStep.
  apply CStep.
  apply AFSBeta.
  apply Beta.
Defined.

Definition rew_baseStep
           {B : Type}
           {F : Type}
           {ar : F → ty B}
           {R : Type}
           {Rcon : R → con B}
           {Rtar : R → B}
           (lhs rhs : ∀ (r : R), tm ar (Rcon r) (Base (Rtar r)))
           {C : con B}
           (r : R)
           (s : sub ar C (Rcon r))
  : rew lhs rhs (subTm (lhs r) s) (subTm (rhs r) s).
Proof.
  apply TStep.
  apply CStep.
  apply AFSRew.
Defined.