Autosubst.v

Require Import FunctionalExtensionality.


(***************)
(* Definitions *)
(***************)
(*

t := n | t.[σ] | λ t | t1 <*> t2 
σ := ids | ↑ | t ∙ σ | σ1 ∘ σ2

*)


Inductive term :=
    | Var (n : nat)
    | Lam (t : term)
    | App (f v : term).

Notation "'λ' t"  := (Lam t)(at level 40).
Infix "<*> " := App (at level 50, left associativity).


Definition cons {X}(s : X) (σ : nat -> X) (x : nat) : X :=
    match x with 
    | O => s
    | S x' => σ x' 
    end.
Notation "s ∙ σ" := (cons s σ)(at level 30).


Notation ids := Var.
Definition shift := (fun m => S m). 
Notation "↑" := shift.


Definition compose {A B C : Type} (f : A -> B) (g : B -> C) :=
    fun a : A => g (f a).
Notation "f >>> g" := (compose f g)(at level 30).
Definition ren (ξ : nat -> nat) := ξ >>> ids.


Fixpoint rename (ξ : nat -> nat) (t : term) : term :=
    match t with 
    | Var x => Var (ξ x) 
    | f <*> v => (rename ξ f) <*> (rename ξ v) 
    | λ s => λ (rename (0 ∙ (ξ >>> ↑)) s)
             (* = s.[ren (0 ∙ (ξ >>> ↑))] *)
    end.

Definition up (σ : nat -> term) := ids 0 ∙ (σ >>> rename ↑).
Notation "⇑ σ" := (up σ)(at level 30).


Fixpoint inst (σ : nat -> term) (t : term) : term :=
    match t with
    | Var x => σ x 
    | App f v => App (inst σ f) (inst σ v)
    | Lam s => Lam (inst (⇑ σ) s) 
    end.

Notation "t .[ σ ]" := (inst σ t)(at level 30).

Notation "σ ∘ τ" := (σ >>> inst τ)(at level 30).

Hint Unfold up cons shift ren compose : core.



Theorem rename_inst : forall s ξ,
    rename ξ s = inst (ren ξ) s.
Proof.
    induction s; intros ξ; auto; simpl.
    +   rewrite (IHs (0 ∙ (ξ >>> ↑))).
        assert ((ren (0 ∙ (ξ >>> ↑))) = (⇑ (ren ξ))).
        apply functional_extensionality.
            induction x; auto.
        rewrite H; auto.
    +   rewrite (IHs1 ξ), (IHs2 ξ); auto.
Qed.


(*********)
(* Proof *)
(*********)
(*

各演算が σ-calculusの推論規則を満たす事の証明

(s <*> t).[σ] = s.[σ] <*> t.[σ]
(λ t).[σ] = λ t.[(Var 0) ∙ (σ ∘ ren ↑)]
(Var 0).[t ∙ σ] = t
(ren ↑) ∘ (t ∙ σ) = σ.
t.[ids] = t.
(Var 0).[σ] ∙ ((ren ↑) ∘ σ) = σ

ids ∘ σ = σ
σ ∘ ids = σ
(σ ∘ τ) ∘ θ = σ ∘ (τ ∘ θ)
(t ∙ σ) ∘ τ = (t.[τ]) ∙(σ ∘ τ)
t.[σ].[τ] = t.[σ ∘ τ]
(Var 0) ∙ (ren ↑) = ids

*)




Theorem app_inst f v σ: 
    (f <*> v).[σ] = f.[σ] <*> v.[σ].
Proof. auto. Qed.



Theorem inst_cons t σ:
    Var 0.[t ∙ σ] = t.
Proof. auto. Qed. 


Theorem shift_cons t (σ : nat -> term):
    ren ↑ ∘ (t ∙ σ) = σ.
Proof.
      apply functional_extensionality.
      destruct x; unfold cons, compose; simpl; auto.
Qed.




Theorem id_inst n σ: 
    (ids n).[σ] = σ n.
Proof. auto. Qed.

Theorem inst_id t :
    t.[ids] = t.
Proof.
    induction t; simpl; auto.
    +   simpl; unfold up.
        assert (ids 0 ∙ (ids >>> rename ↑) = ids).
            apply functional_extensionality.
            induction x; unfold cons; simpl; auto.
        rewrite H, IHt; auto.
    +   rewrite IHt1, IHt2; auto.
Qed.

Theorem cons_comp_dist t σ τ :
    (t ∙ σ) ∘ τ = (t.[τ]) ∙(σ ∘ τ).
Proof.
    apply functional_extensionality.
    induction x; unfold compose, cons; simpl; auto.
Qed.


Theorem inst2l t : forall ξ τ,
    t.[ren ξ].[τ] = t.[ren ξ ∘ τ].
Proof.
    induction t; intros; simpl; auto.
    +   unfold up.
        assert (ren (0 ∙ (ξ >>> ↑)) = ids 0 ∙ (ren ξ >>> rename ↑)).
            apply functional_extensionality.
            induction x; unfold ren, compose; auto.
        rewrite <- H.
        rewrite (IHt (0 ∙ (ξ >>> ↑)) ( ids 0 ∙ (τ >>> rename ↑))).
        assert (ren (0 ∙ (ξ >>> ↑)) ∘ (ids 0 ∙ (τ >>> rename ↑)) =
                    ids 0 ∙ ((ren ξ ∘ τ) >>> rename ↑) ).
            apply functional_extensionality.
            induction x; unfold ren, compose; simpl; auto.
        rewrite H0; auto.
    +   rewrite (IHt1 ξ τ), (IHt2 ξ τ); auto.
Qed.  

Theorem inst2r t : forall σ ξ,
    t.[σ].[ren ξ] = t.[σ ∘ ren ξ ].
Proof.
    induction t; auto; intros; simpl.
    +   unfold up.
        assert (( ids 0 ∙ (ren ξ >>> rename ↑)) = (ren (0 ∙ (ξ >>> ↑)))).
            apply functional_extensionality.
            induction x; unfold ren, compose; simpl; auto.
        rewrite H.
        rewrite (IHt (ids 0 ∙ (σ >>> rename ↑)) ((0 ∙ (ξ >>> ↑)))).
        replace ((ids 0 ∙ (σ >>> rename ↑)) ∘ ren (0 ∙ (ξ >>> ↑)))
            with (ids 0 ∙ ((σ ∘ ren ξ) >>> rename ↑)); auto.
        apply functional_extensionality.
        induction x; simpl; unfold compose; simpl; auto.
        repeat rewrite rename_inst.
        repeat rewrite inst2l.
        assert (ren ξ ∘ ren ↑ = ren ↑ ∘ ren (0 ∙ (fun a : nat => ↑ (ξ a)))).
            apply functional_extensionality.
            induction x; unfold ren, compose; simpl; auto.
        rewrite H0; auto.
    +   rewrite (IHt1 σ ξ), (IHt2 σ ξ); auto.
Qed.   


Theorem shift_compose σ τ : 
    (⇑ σ) ∘ (⇑ τ) = ⇑ (σ ∘ τ).
Proof.
    apply functional_extensionality; intro.
    destruct x; auto.

    unfold compose; simpl; unfold compose.
    repeat rewrite rename_inst.
    rewrite inst2l, inst2r.
    replace (ren ↑ ∘ (⇑ τ)) with (τ ∘ ren ↑); auto.
    apply functional_extensionality; intro y.
    induction y; unfold ren, compose; simpl; unfold compose;
    rewrite rename_inst; auto.
Qed.
    

Theorem inst2 t : forall σ τ,
    t.[σ].[τ] = t.[σ ∘ τ].
Proof.
    induction t; intros σ τ; simpl; auto.
    +   rewrite (IHt (⇑ σ) (⇑ τ )).
        rewrite shift_compose; auto.
    +   rewrite (IHt1 σ τ), (IHt2 σ τ); auto.    
Qed. 


Theorem abs_inst t σ : 
    (λ t).[σ] = λ t.[(Var 0) ∙ (σ ∘ ren ↑)].
Proof.
    induction t; simpl.
    +   induction n.
        -   unfold up, cons, compose; simpl; auto.
        -   unfold up, cons, compose; simpl.            
            rewrite rename_inst; auto.
    +   unfold up; simpl.
        assert (σ >>> rename ↑ = σ ∘ ren ↑).
            apply functional_extensionality.
            induction x; unfold compose; rewrite rename_inst; auto.
        rewrite H; auto.
    +   unfold up, compose.
        replace (fun a : nat => rename ↑ (σ a)) with (fun a : nat => σ a .[ ren ↑]); auto.
        apply functional_extensionality; intro.
        rewrite rename_inst; auto.
Qed.        


Theorem zero_cons_shift σ :
    (Var 0).[σ] ∙ ((ren ↑) ∘ σ) = σ.
Proof.
    apply functional_extensionality.
    induction x; unfold cons; simpl; auto.
Qed.

Theorem idl σ :
    ids ∘ σ = σ.
Proof.
    apply functional_extensionality; induction x; unfold compose; simpl; auto.
Qed.

Theorem idr (σ : nat -> term) :
    σ ∘ ids = σ.
Proof.
    apply functional_extensionality.
    induction x; unfold compose; simpl;
    rewrite (inst_id); auto.
Qed.

Theorem compose_assoc (σ τ θ : nat -> term):
    (σ ∘ τ) ∘ θ = σ ∘ (τ ∘ θ).
Proof.
    apply functional_extensionality.
    induction x; unfold compose; simpl;
    rewrite inst2; unfold compose; simpl; auto.
Qed.



Theorem zeroshift_id :
    (Var 0) ∙ (ren ↑) = ids.
Proof.
    apply functional_extensionality.
    induction x; unfold cons; simpl; auto.
Qed.    



(**************)
(* confluence *)
(**************)
(*



*)


Reserved Notation "t1 ⊳ t2" (at level 60).

Inductive reduce  : term -> term -> Prop :=
    | r_var n : Var n ⊳ Var n
    | r_beta s1 s2 t1 t2 : s1 ⊳ s2 -> t1 ⊳ t2 -> (λ s1) <*> t1 ⊳ s2.[t2 ∙ ids]    
    | r_app s1 s2 t1 t2 : s1 ⊳ s2 -> t1 ⊳ t2 -> s1 <*> t1 ⊳ s2 <*> t2
    | r_abs t1 t2 : t1 ⊳ t2 -> λ t1 ⊳ λ t2
    where "t1 ⊳ t2" := (reduce t1 t2).

Hint Constructors reduce.

Definition reduceS (σ τ : nat -> term) := forall n, σ n ⊳ τ n.
Notation "σ ⊳⊳ τ" := (reduceS σ τ)(at level 30).

Fixpoint ρ t :=
    match t with 
    | Var n => Var n 
    | Lam t' => λ (ρ t')
    | App f v => 
        match f with 
        | Lam t' => ρ t' .[ρ v ∙ ids]
        | _ => ρ f <*> ρ v 
        end 
    end.



Theorem inst_up_cons s t τ :
    s.[⇑ τ].[t.[τ] ∙ ids] = s.[t ∙ ids].[τ].
Proof.
    repeat rewrite inst2.
    replace ((⇑ τ) ∘ ((t .[ τ]) ∙ ids))
        with ((t ∙ ids) ∘ τ); auto.
    apply functional_extensionality; intro.
    destruct x; auto.
    unfold compose; simpl; unfold compose.
    rewrite rename_inst, inst2, shift_cons, inst_id; auto.
Qed.



Theorem substitutivity' : forall s t ξ τ,
    s ⊳ t ->  (ren ξ) ⊳⊳ τ  -> s.[ren ξ] ⊳ t.[τ].
Proof.
    intros.
    generalize dependent ξ.
    generalize dependent τ.
    induction H; simpl; auto; intros.
    +   rewrite <- inst_up_cons.
        apply r_beta; auto.
        assert (⇑ ren ξ = ren (0 ∙ (ξ >>> ↑))).
            apply functional_extensionality; intro.
            unfold up, ren, compose, cons.
            destruct x; auto.
        rewrite H2.
        apply IHreduce1; intro.
        rewrite <- H2.
        unfold up, cons.
        destruct n; auto.        
        unfold compose.
        repeat rewrite rename_inst.
        specialize (H1 n).
        inversion H1.
        unfold ren, compose.
        apply r_var.
    +    assert (⇑ ren ξ = ren (0 ∙ (ξ >>> ↑))).
            apply functional_extensionality; intro.
            unfold up, ren, compose, cons.
            destruct x; auto.
        apply r_abs.
        rewrite H1.
        apply IHreduce.
        rewrite <- H1.
        intro n.
        unfold up, cons.
        destruct n; auto.
        specialize (H0 n).        
        unfold compose.
        repeat rewrite rename_inst.
        unfold ren, compose.
        inversion H0; subst.
        apply r_var.
Qed.   


Lemma reduceS_up σ τ :
     σ ⊳⊳ τ -> (⇑ σ) ⊳⊳ (⇑ τ).
Proof.
    intros; intro.
    destruct n; simpl; auto.
    unfold compose; repeat rewrite rename_inst.
    apply substitutivity'; auto.
    intro; unfold ren, compose; auto.
Qed.    
   



Theorem substitutivity : forall s t σ τ,
    s ⊳ t ->  σ ⊳⊳ τ  -> s.[σ] ⊳ t.[τ].
Proof.
    intros.
    generalize dependent σ.
    generalize dependent τ.
    induction H; intros; simpl.
    +   apply H0.
    +   rewrite <- inst_up_cons.
        apply r_beta.
        -   apply IHreduce1.
            apply reduceS_up; auto.
        -   apply IHreduce2; auto.
    +   apply r_app; auto.  
    +   apply r_abs.
        apply IHreduce.
        apply reduceS_up; auto.
Qed.    

Theorem triangle : forall t s,
    t ⊳ s -> s ⊳ ρ t.
Proof.
    intros.    
    induction H; simpl; auto.
    +   apply substitutivity; auto.
        intro n; destruct n; simpl; auto.
    +   destruct s1; simpl in *; auto.
        destruct s2; inversion H; subst.
        apply r_beta; auto.
        inversion IHreduce1; subst; auto.
Qed.

Theorem chrch_rosser s t t' :
    s ⊳ t -> s ⊳ t' -> exists s', t ⊳ s' /\ t' ⊳ s'.
Proof.
    intros; exists (ρ s); split; apply triangle; auto.
Qed.