Library RPO

Introduction

Author: Andrew Gacek <andrew.gacek@gmail.com> In this file, we define a notion of lexicographic recursive path ordering, and we show that the reading and merging rules of the suspension calculus, under a suitable mapping, always rewrite a larger expression to a smaller expression. Given the exisiting literature on RPOs, this shows that the reading and merging rules are strongly normalizing.


Module RPO.

   Require Import List.
   Require Import Arith.
   Require Import Omega.
   Require Import Max.
   Require Import Wf_nat.

   Load Susp.

Definition of Abstract Representation

We abstract away the structure of our previous representation of the suspension calculus and treat everything as a symbol. The symbol s is indexed by a natural number which is where the measure eta will fit into this representation.

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

A notion of less than on symbol which is wellfounded

  Inductive slt : symbol -> symbol -> Prop :=
    | nil_lt : forall n, slt nil (s n)
    | one_lt : forall n, slt one (s n)
    | app_lt : forall n, slt app (s n)
    | lam_lt : forall n, slt lam (s n)
    | cons_lt : forall n, slt cons (s n)
    | s_lt : forall n m, n < m -> slt (s n) (s m).

   Hint Constructors slt.
  
  Lemma slt_wf : well_founded slt.
  Proof.
    apply well_founded_lt_compat with (f:=
      fun sym => match sym with
                 | nil => 0
                 | one => 1
                 | app => 2
                 | lam => 3
                 | cons => 4
                 | s n => n + 5
                 end).
    intros x y H; inversion H; omega.
  Qed.

  Inductive term : Set :=
    | App : symbol -> list term -> term.

  Definition Sym s := App s List.nil.
  
  Definition Fun1 t t1 := App t (t1::List.nil).

  Definition Fun2 t t1 t2 := App t (t1::t2::List.nil).

Definition of Lexicographic Recursive Path Ordering


  Inductive rpolt : term -> term -> Prop :=
    | rpolt1 : forall f g ss ts, f = g ->
        lexlt ts ss ->
        (forall ti, In ti ts -> rpolt ti (App f ss)) ->
        rpolt (App g ts) (App f ss)
    | rpolt2 : forall f g ss ts, slt g f ->
        (forall ti, In ti ts -> rpolt ti (App f ss)) ->
        rpolt (App g ts) (App f ss)
    | rpolt3 : forall f ss t,
        (exists si, In si ss /\ (si = t \/ rpolt t si)) ->
        rpolt t (App f ss)
  with lexlt : list term -> list term -> Prop :=
    | lexlt_head : forall t s ts ss,
        rpolt t s -> lexlt (t :: ts) (s :: ss)
    | lexlt_tail : forall t s ts ss,
        lexlt ts ss -> t = s -> lexlt (t :: ts) (s :: ss).

   Hint Constructors rpolt lexlt.

Abstraction Mapping


  Fixpoint E (t : Susp.term) : term :=
    match t with
    | Susp.nil => Sym nil
    | Susp.one => Sym one
    | Susp.app t1 t2 => Fun2 app (E t1) (E t2)
    | Susp.lam t' => Fun1 lam (E t')
    | Susp.s t1 t2 => Fun2 (s (Susp.eta t 0)) (E t1) (E t2)
    | Susp.cons t1 t2 => Fun2 cons (E t1) (E t2)
    end.

Hints, Lemmas, and Tactics
Hints about library predicates

  
   Hint Resolve in_cons in_eq.
   Hint Resolve max_r max_l le_max_l le_max_r.
   Hint Resolve lt_n_S plus_lt_compat_l.

  Lemma lt_max_r : forall a b, a < b -> a < max a b.
  Proof.
    intros a b H; rewrite max_r; auto with arith.
  Qed.
  
  Lemma lt_max_l : forall a b, a < b -> a < max b a.
  Proof.
    intros a b H; rewrite max_l; auto with arith.
  Qed.
  
   Hint Resolve lt_max_r lt_max_l.

Local tactics and hints


   Ltac unfolds := simpl; unfold Sym; unfold Fun2; unfold Fun1.
  
   Ltac i_subst := let H := fresh in (intro H; subst).

   Ltac i_elim_c := let H := fresh in (intro H; elim H; clear H).

   Ltac in_cases := (i_elim_c; fail) || (i_elim_c; [ i_subst | in_cases ]).
   Hint Extern 5 (In ?X1 ?X2 -> rpolt ?X3 ?X4) => in_cases.

   Ltac nat_cases :=
    match goal with
      [ |- context c [match ?X with O => _ | S _ => _ end] ] => case X
    end.
   Hint Extern 5 (_ \/ _) => nat_cases.

  Lemma le_s_cases : forall x y, x <= y -> s y = s x \/ slt (s x) (s y).
  Proof.
    intros x y H; case (le_lt_eq_dec x y); auto.
  Qed.
   Hint Resolve le_s_cases.

Sometimes we don't know if rpolt1 or rpolt2 applies, for instance if the leading symbols are (s x) and (s (max x y)), but we can prove the stronger requirements of rpolt1 anyway. This lemma allows us to deal with both cases together.

  Lemma rpolt_1or2 : forall f g ss ts, (f = g \/ slt g f) ->
                       lexlt ts ss ->
                       (forall ti, In ti ts -> rpolt ti (App f ss)) ->
                       rpolt (App g ts) (App f ss).
  Proof.
    intros f g ss ts Hfg Hlex; elim Hfg; clear Hfg; intro Hfg.
      apply rpolt1; trivial.
      apply rpolt2; trivial.
  Qed.
   Hint Resolve rpolt_1or2.

Rewriting Rroperties of rpolt



  Lemma rpolt_rm : forall t t',
    Susp.rm t t' -> rpolt (E t') (E t).
  Proof.
    intros t t' H; inversion H; simpl; unfolds; eauto 100.
    apply rpolt_1or2.
      apply le_s_cases; repeat rewrite plus_n_Sm;
        repeat rewrite plus_assoc; repeat apply plus_le_compat; auto.
        rewrite plus_comm; auto.
        repeat apply le_n_S; apply Susp.eta_i_j; omega.
      eauto 10.
      intro ti; in_cases; eauto 10.
        apply rpolt2.
          apply s_lt; unfold lt; repeat apply le_n_S; apply plus_le_compat.
            rewrite plus_comm; auto with arith.
            auto with arith.
          eauto 20.
  Qed.

   Hint Resolve rpolt_rm.

This is our main result

  Theorem step_rpolt : forall t t',
    Susp.step t t' -> rpolt (E t') (E t).
  Proof.
    intros t t' H; induction H; simpl; unfolds; eauto 20.
  Qed.
  
End RPO.
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.