Library CFP

Require Export Omega Coq.Setoids.Setoid List Base Util AutoIndTac.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Syntax of Context-Free Programs

Inductive cfp :=
| CFPEps
| CFPSeq (s t : cfp)
| CFPChoice (s t: cfp)
| CFPFix (s: {bind cfp})
| CFPVar (x: var).

Instance Ids_term : Ids cfp. derive. Defined.
Instance Rename_term : Rename cfp. derive. Defined.
Instance Subst_term : Subst cfp. derive. Defined.
Instance SubstLemmas_term : SubstLemmas cfp. derive. Qed.

Null Program and Iteration

Definition Null := CFPFix (CFPVar 0).
Definition part s t := CFPChoice s (CFPSeq t (CFPVar 0)).
Definition Star s := CFPFix (part CFPEps s).

Functional extensionality for substitutions

Lemma extens s sigma1 sigma2
  : (∀ n, sigma1 n = sigma2 n) → s.[sigma1] = s.[sigma2].
Proof.
  general induction s; asimpl; eauto.
  - rewrite IHs2 with (sigma2 := sigma2); eauto.
    rewrite IHs1 with (sigma2 := sigma2); eauto.
  - rewrite IHs2 with (sigma2 := sigma2); eauto.
    rewrite IHs1 with (sigma2 := sigma2); eauto.
  - f_equal. apply IHs. intros. destruct n; asimpl; eauto.
    rewrite H. eauto.
Qed.

Decidability of syntactic equivalence

Lemma cfp_eq_dec (s t: cfp)
  : {s = t } + {s ≠ t }.
Proof.
  general induction s.
  - general induction t.
    + left. eauto.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + right. intros A. inv A.
  - general induction t.
    + right. intros A. inv A.
    + destruct (IHs1 t1).
      × destruct (IHs2 t2).
        { left. rewrite e, e0. eauto. }
        { right. intros A. inv A. apply n. eauto. }
      × right. intros A. inv A. apply n. eauto.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + right. intros A. inv A.
  - general induction t.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + destruct (IHs1 t1).
      × destruct (IHs2 t2).
        { left. rewrite e, e0. eauto. }
        { right. intros A. inv A. apply n. eauto. }
      × right. intros A. inv A. apply n. eauto.
    + right. intros A. inv A.
    + right. intros A. inv A.
  - general induction t.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + destruct (IHs s).
      × left. rewrite e. eauto.
      × right. intros A. inv A. apply n. eauto.
    + right. intros A. inv A.
  - general induction t.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + right. intros A. inv A.
    + decide (x0 = x).
      × left. rewrite e. eauto.
      × right. intros A. inv A. apply n. eauto.
Qed.

Instance cfp_dec (s t: cfp): dec (s = t).
Proof. unfold dec. apply cfp_eq_dec. Qed.

Notions for substitutions

Definition shift := fun x ⇒ match x with 0 ⇒ 0 | S n ⇒ n end.

Definition simulatesI (sigma sigma': var → cfp) n k
  := (∀ i, i < n → sigma i = sigma' i )
     ∧ (∀ i, i ≥ n + k → sigma i = sigma' i ).

Fact up_change s t sigma
  : s.[up sigma].[t/] = s.[t.: sigma].
Proof.
  asimpl. eauto.
Qed.

Fact subst_Fix_distribute s sigma
  : s.[CFPFix s/].[sigma] = s.[CFPFix s.[up sigma] .: sigma].
Proof.
  asimpl. eauto.
Qed.

Lemma shift_id s
  : s.[ren((+1)>>> shift)] = s.[ren(id)].
Proof.
  apply extens. intros.
  simpl. eauto.
Qed.

Fact id_shift u
  : u = (u.[ren (+1)]).[ren shift].
Proof.
  asimpl. rewrite shift_id. asimpl.
  eauto.
Qed.

Fact simulate_shift s n
  : ∀ i : nat,
    i ≥ (S n ) → (s .: ids) i = ids (shift i).
Proof.
  intros. destruct i; inv H; simpl; eauto.
Qed.

Lemma simulatesI_shift s
  : simulatesI (s .: ids) (shift >>> ids) 0 1.
Proof.
  split; intros; try omega.
  destruct i; asimpl; try omega; eauto.
Qed.

Definition substPos i t := fun x ⇒ if (decision (x =i)) then t
                                    else if (decision (x < i)) then (CFPVar x)
                                         else (CFPVar (x -1)).
Lemma substPos_eq x t
  : substPos x t x = t.
Proof.
  unfold substPos. decide (x=x); eauto.
  exfalso. omega.
Qed.

Lemma substPos_lt x t i
  : x < i → substPos i t x = CFPVar x.
Proof.
  intros. unfold substPos. decide (x=i); try omega.
  decide (x< i); eauto; omega.
Qed.

Lemma substPos_gt x t i
  : x > i → substPos i t x = CFPVar (x -1).
Proof.
  intros. unfold substPos. decide (x=i); try omega.
  decide (x<i); try omega; eauto.
Qed.

Lemma substPos_zero t x
  : (t.: ids) x = substPos 0 t x.
Proof.
  destruct x; asimpl; eauto; unfold substPos; asimpl; eauto.
  assert (x= x-0); try omega.
  rewrite H. eauto.
Qed.

Lemma substPos_zero_extens s t
  : s.[t/] = s.[substPos 0 t].
Proof.
  apply extens. apply substPos_zero.
Qed.

Lemma substPos_up s i t
  : s.[up (substPos i t)] = s.[substPos (S i) t.[ren(+1)]].
Proof.
  apply extens. intros n.
  destruct n; unfold substPos; asimpl; eauto.
  decide (n=i); simpl.
  - decide (S n = S i); eauto; try omega.
  - decide (n < i); asimpl.
    + decide (S n = S i); try omega.
      decide (S n < S i); eauto; try omega.
    + decide (S n = S i); try omega.
      decide (S n < S i); try omega.
      assert (S (n-1) = n - 0).
      { destruct n; asimpl; omega. }
      rewrite H. eauto.
Qed.