Program Fixpoint and simpl/unfold

gistfile1.coq

Require Import Arith List ListSet Omega Program.
 
Definition fvar : Type := nat. 
Definition bvar : Type := nat. 
 
Inductive sort : Type :=
| N : sort
| ArrowS : sort -> sort -> sort.

Definition eq_sort_dec (s1 s2 : sort) : {s1 = s2} + {s1 <> s2}. 
Proof. do 2 decide equality. Defined.

(* A very simple language with locally nameless binder representation *) 
Inductive index : Type :=
| IBVar : bvar -> index 
| IFVar : fvar -> index
| Z : index
| Plus1 : index -> index  
| IAbs : sort -> index -> index
| IApp : index -> index -> index.

(* Set notations *)
Notation "\{}" := (empty_set fvar).
  
Notation "\{ x }" := ([x]).

Notation "E \u F" := (set_union eq_nat_dec E F)
                       (at level 37, right associativity).

Notation "x \in E" := (set_In x E) (at level 38).

Notation "x \notin E" := (~ (x \in E)) (at level 38).


(* Environments *)
Definition env := list (fvar * sort).
 
Definition get (x : fvar) (e : env) : option sort :=
  match 
    find (fun p => if eq_nat_dec x (fst p) then true else false) e
  with 
    | Some p => Some (snd p) 
    | None => None
  end.

Definition dom (e : env) : set fvar := fold_left (fun s x => \{fst x} \u s) e \{}. 

(* Free variables *)
Fixpoint ifv (i : index) : set fvar :=
  match i with
    | IFVar x => \{x}
    | IBVar _ | Z => \{}
    | Plus1 i => ifv i
    | IAbs _ i => ifv i
    | IApp i1 i2 => ifv i1 \u ifv i2 
  end. 
 
Definition var_gen (E : set fvar) :=
  1 + fold_right max O E.

Lemma var_gen_spec : forall E, (var_gen E) \notin E.
Proof.
  intros E.
  assert (Hlt : forall n, n \in E -> n < var_gen E).
  { intros n H. induction E as [|x xs IHxs];
      unfold var_gen in *; simpl in *; try (now exfalso; auto).
    destruct H; subst;
    rewrite Max.succ_max_distr, NPeano.Nat.max_lt_iff; auto. }
  intros contra. apply Hlt in contra. omega.
Qed.

Fixpoint ii_open_rec (k : nat) (i : index) (x : fvar) : index :=
  match i with
    | IBVar n => if eq_nat_dec k n then (IFVar x) else (IBVar n)
    | IFVar _ | Z => i 
    | Plus1 i => Plus1 (ii_open_rec k i x)
    | IAbs s i => IAbs s (ii_open_rec (S k) i x)
    | IApp i1 i2 => IApp (ii_open_rec k i1 x) (ii_open_rec k i2 x)
  end.
 
Definition ii_open_var (i : index) (x : fvar) := ii_open_rec 0 i x. 


(* Typing rules *)
Inductive sorting (e : env) : index -> sort -> Prop :=
| IFVarRule : 
    forall (x : fvar) (s : sort),
      get x e = Some s -> 
      sorting e (IFVar x) s
| ZRule : sorting e Z N
| Plus1Rule : forall (I : index), 
                sorting e I N -> sorting e (Plus1 I) N
| IAbsRule : forall (I : index) (s1 s2 : sort),
               (* Cheating a bit to make the proof easier, but this
                  rule should be equivalent with the previous one - 
                  the proof must be cumbersome though *)
               let x := var_gen (dom e \u ifv I) in
               sorting ((x, s1) :: e) (ii_open_var I x) s2 ->
               sorting e (IAbs s1 I) (ArrowS s1 s2)
| IAppRule : forall (I1 I2 : index) (S1 S2 : sort),
               sorting e I1 (ArrowS S1 S2) -> sorting e I2 S1 -> 
               sorting e (IApp I1 I2) S2.


Fixpoint index_size (i : index) : nat :=
  match i with
    | IBVar _ | IFVar _ | Z => 0
    | Plus1 i | IAbs _ i  => 1 + index_size i 
    | IApp i1 i2 => 1 + (index_size i1 + index_size i2)
  end.
 
Lemma size_ii_open_rec :
  forall (i : index) (x : fvar) (rec :nat), 
    index_size (ii_open_rec rec i x) = index_size i.
Proof.
  intros i x. 
  induction i; intros n; simpl;
  repeat
    (match goal with
       | [ H : forall (_ : nat), _ = _ |- _ ] => 
         rewrite H
     end); try omega.
  now destruct (eq_nat_dec _ _).
Qed.

Program Fixpoint infer_sort (ie : env) (i : index) {measure (index_size i)} :
  {o : option sort | forall s, o = Some s -> sorting ie i s } :=
  match i with
    | IBVar x => None
    | IFVar x => get x ie
    | Z => Some N
    | Plus1 i => 
      match infer_sort ie i with 
        | Some N => Some N
        | _ => None 
      end
    | IAbs s i =>
      let x := var_gen (dom ie \u ifv i) in
      match infer_sort ((x, s) :: ie) (ii_open_var i x) with
        | Some s' => Some (ArrowS s s')
        | _ => None
      end
    | IApp i1 i2 =>
      match infer_sort ie i1 with
        | Some (ArrowS s1 s2) =>
          match infer_sort ie i2 with
            | Some s1' => 
              if eq_sort_dec s1 s1' then Some s2
              else None
            | _ => None
          end
        | _ => None
      end
  end. 
Solve Obligations using 
      program_simpl; constructor; auto.
Solve Obligations using  
      program_simpl; simpl; unfold ii_open_var; 
      try rewrite size_ii_open_rec; omega.
Solve Obligations using
      program_simpl;
      (repeat (match goal with 
                | [ H : Some _ = ` ?P |- _] => 
                  destruct P; simpl in *; subst; clear H
              end); econstructor; eauto).