Library Susp

Introduction

Author: Andrew Gacek <andrew.gacek@gmail.com> In this file, we define the reading and merging rules of the suspension calculus. We then define a measure eta for suspension expressions show that it is non-increasing on the reading and merging rules.


Module Susp.

   Require Import Arith.
   Require Import Max.
   Require Import Omega.

Definition of Term

We abstract away unnecessary details from the syntax by implicitly using the mapping E defined recursively as 
    constants, #i      -> one
    t1 t2              -> app (E t1) (E t2)
    \lambda t          -> lam (E t)
    [[t, ol, nl, e]]   -> s (E t) (E e)

    nil                -> nil
    (t, l)::e          -> cons (E t) (E e)
    {{e1, nl, ol, e2}} -> s (E e1) (E e2)


  Inductive term : Set :=
    | nil : term
    | one : term
    | app : term -> term -> term
    | lam : term -> term
    | s : term -> term -> term
    | cons : term -> term -> term.

Definition of Reading and Merging Rules

Given the mapping for terms described above, our rules are the following. 
    r1. s one e            -> one
    r2. s one nil          -> one
    r3. s one (cons t e)   -> s t nil
    r4. s one (cons t e)   -> s one e
    r5. s (app t1 t2) e    -> app (s t1 e) (s t2 e)
    r6. s (lam t) e        -> lam (s t (cons one e))

    m1. s (s t e1) e2      -> s t (s e1 e2)
    m2. s e1 nil           -> e1
    m3. s nil e2           -> e2
    m4. s nil (cons t e2)  -> s nil e2
    m5. s e1 (cons t e2)   -> s e1 e2
    m6. s (cons t e1) e2   -> cons (s t e2) (s e1 e2)


  Inductive rm : term -> term -> Prop :=
    | r1 : forall e, rm (s one e) one
    | r2 : rm (s one nil) one
    | r3 : forall t e, rm (s one (cons t e)) (s t nil)
    | r4 : forall t e, rm (s one (cons t e)) (s one e)
    | r5 : forall t1 t2 e, rm (s (app t1 t2) e) (app (s t1 e) (s t2 e))
    | r6 : forall t e, rm (s (lam t) e) (lam (s t (cons one e)))
    | m1 : forall t e1 e2, rm (s (s t e1) e2) (s t (s e1 e2))
    | m2 : forall e1, rm (s e1 nil) e1
    | m3 : forall e2, rm (s nil e2) e2
    | m4 : forall t e2, rm (s nil (cons t e2)) (s nil e2)
    | m5 : forall t e1 e2, rm (s e1 (cons t e2)) (s e1 e2)
    | m6 : forall t e1 e2, rm (s (cons t e1) e2) (cons (s t e2) (s e1 e2)).

The step relation holds between t and t' if t rewrites to t' using one of our rewrite rules at some level in the term.


  Inductive step : term -> term -> Prop :=
    | rm_step : forall t t', rm t t' -> step t t'
    | app_left_step : forall t1 t1' t2,
        step t1 t1' -> step (app t1 t2) (app t1' t2)
    | app_right_step : forall t1 t2 t2',
        step t2 t2' -> step (app t1 t2) (app t1 t2')
    | lam_step : forall t t',
        step t t' -> step (lam t) (lam t')
    | s_left_step : forall t1 t1' t2,
        step t1 t1' -> step (s t1 t2) (s t1' t2)
    | s_right_step : forall t1 t2 t2',
        step t2 t2' -> step (s t1 t2) (s t1 t2')
    | cons_left_step : forall t1 t1' t2,
        step t1 t1' -> step (cons t1 t2) (cons t1' t2)
    | cons_right_step : forall t1 t2 t2',
        step t2 t2' -> step (cons t1 t2) (cons t1 t2').

Hints and Lemmas



  Lemma le_plus_0 : forall a b, a <= b -> a + 0 <= b.
  Proof.
    intros a b H; omega.
  Qed.

  Lemma max_plus_n : forall a b n,
    max (a + n) (b + n) <= (max a b) + n.
  Proof.
    intros a b n; case (le_gt_dec a b); intro H.
      repeat rewrite max_r; auto with arith.
      repeat rewrite max_l; auto with arith.
  Qed.

  Lemma max_plus_n_m : forall a b n m,
    max (a + n + m) (b + n + m) <= (max a b) + n + m.
  Proof.
    intros a b n m; repeat (rewrite <- plus_assoc); apply max_plus_n.
  Qed.

  Lemma max_a_b_a'_b' : forall a b a' b',
    a <= a' -> b <= b' -> max a b <= max a' b'.
  Proof.
    intros a b a' b' Ha Hb; case (max_dec a b); intro H; rewrite H.
      apply le_trans with a'; auto with arith.
      apply le_trans with b'; auto with arith.
  Qed.

  Lemma max_plus_max : forall a b c1 c2 c3,
    max c1 c2 <= c3 -> max (a + c1) (b + c2) <= max a b + c3.
  Proof.
    intros a b c1 c2 c3 H.
    case (max_dec (a + c1) (b + c2)); intro H'; rewrite H'.
      apply le_trans with (a + max c1 c2).
        auto with arith.
        apply plus_le_compat; auto with arith.
      apply le_trans with (b + max c1 c2).
        auto with arith.
        apply plus_le_compat; auto with arith.
  Qed.

  Lemma max_le_n : forall a b n, a <= n -> b <= n -> max a b <= n.
  Proof.
    intros a b n Ha Hb; apply max_case2; assumption.
  Qed.

  Lemma le_le_max_l : forall a' a b, a' <= a -> a' <= max a b.
  Proof.
    intros a' a b H; apply le_trans with a; auto with arith.
  Qed.

  Lemma plus_comm2 : forall a b c, a + b + c = a + c + b.
  Proof.
    intros a b c; omega.
  Qed.
    

   Hint Resolve le_plus_0 max_plus_n max_plus_n_m max_a_b_a'_b' max_plus_max
               max_le_n le_le_max_l.


   Hint Resolve plus_le_compat le_n_S plus_le_compat_l le_O_n
               max_r max_l le_max_l le_max_r le_plus_trans.

Definition of mu

We define our first measure, mu, and prove that it is non-increasing for all of the rewrite rules.


  Fixpoint mu (t : term) : nat :=
    match t with
    | nil => 0
    | one => 0
    | app t1 t2 => max (mu t1) (mu t2)
    | lam t' => mu t'
    | s t1 t2 => mu t1 + mu t2 + 1
    | cons t1 t2 => max (mu t1) (mu t2)
    end.

Rewriting properties of mu


  Lemma mu_rm : forall t t', rm t t' -> mu t' <= mu t.
  Proof.
    intros t t' H; inversion H; simpl; auto with arith.
    omega.
  Qed.

   Hint Resolve mu_rm.

  Lemma mu_step : forall t t', step t t' -> mu t' <= mu t.
  Proof.
    intros t t' H; induction H; simpl; auto.
  Qed.

   Hint Resolve mu_step.

Definition of eta

We define our second measure, eta, and prove that it is non-increasing for all of the rewrite rules.


  Fixpoint eta (t : term) (i : nat) {struct t} : nat :=
    match t with
    | nil => 0
    | one => 1
    | app t1 t2 => 1 + max (eta t1 i) (eta t2 i)
    | lam t' => i + eta t' i
    | s t1 t2 => 1 + eta t1 (i + 1) + eta t2 (i + 1 + mu t1)
    | cons t1 t2 => max (eta t1 i) (eta t2 i)
    end.

  Lemma eta_i_j : forall t i j,
    i <= j -> eta t i <= eta t j.
  Proof.
    induction t; simpl; auto 10.
  Qed.

   Hint Resolve eta_i_j.

Rewriting properties of eta

  
  Lemma eta_rm : forall t t' i, rm t t' -> eta t' i <= eta t i.
  Proof.
    intros t t' i H; inversion H; simpl; auto 20.
      case (eta e (i + 1 + mu t0)); [ idtac | intro H' ]; omega.
      repeat rewrite plus_n_Sm; repeat rewrite plus_assoc;
        repeat apply plus_le_compat; auto; rewrite plus_comm2; auto.
  Qed.

   Hint Resolve eta_rm.

  Lemma eta_step : forall (t t' : term) (i : nat),
    step t t' -> eta t' i <= eta t i.
  Proof.
    intros t t' i H; generalize i; clear i.
    induction H; simpl; auto 10.
  Qed.

   Hint Resolve eta_step.

End Susp.
This page has been generated by coqdoc

The views and opinions expressed in this page are strictly those of the page author.
The contents of this page have not been reviewed or approved by the University of Minnesota.