gistfile1.coq

Require Import Arith List Omega Program.
 
Definition fvar : Type := nat. 
Definition bvar : Type := nat. 
 
Inductive sort : Type :=
| N : sort
| ArrowS : sort -> sort -> sort.
 
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.
 
(* 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.
 
(* Typing rules *)

Inductive sorting (e : env) : index -> sort -> Prop :=
| IFVarRule : 
    forall (i : fvar) (s : sort),
      get i e = Some s -> 
      sorting e (IFVar i) s
| ZRule : sorting e Z N
| Plus1Rule : forall (I : index), 
                sorting e I N -> sorting e (Plus1 I) N
(* Commenting out the abstraction rule to make the example simpler *)
(* | IAbsRule : forall (I : index) (s1 s2 : sort),  *)
(*                (forall (i : ifvar),  *)
(*                   i # e = true -> i \notin (ifv I) = true -> *)
(*                   sorting (i :~ s1 & e) (I ii_open_var i) 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.
 
Definition sort_eq_dec (s1 s2 : sort) : {s1 = s2} + {s1 <> s2}. 
Proof. do 2 decide equality. Defined.
 
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. 
 
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 _ _).
Defined.
 
 Hint Constructors sorting.

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 *)
      let x := 3 in (* Just for the example *)
      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 sort_eq_dec s1 s1' then Some s2
              else None
            | _ => None
          end
        | _ => None
      end
  end. 
Solve Obligations with (program_simpl; simpl; omega).  
Solve Obligations with (split; intros [H1 H2]; discriminate).
Ltac go :=
  match goal with
    | [ H : Some _ = proj1_sig (?f ?ie ?i ?pf) |- sorting ?ie ?i _ ] => 
      pose proof (proj2_sig (f ie i pf)) as H'; eauto
  end.
Next Obligation. 
  constructor; go.
Defined.
Next Obligation. 
  simpl. unfold ii_open_var. 
  rewrite size_ii_open_rec; omega. 
Defined.
Next Obligation.
  admit. (* no typing rule for abs... *)
Defined.
Next Obligation.
  econstructor; go.
Defined.

Lemma infer_sort_sound: 
  forall (i : index) (ie: env)  (s : sort),
    ` (infer_sort ie i) = Some s -> 
    sorting ie i s.
Proof.
  intros.
  pose proof (proj2_sig (infer_sort ie i)).
  auto.
Qed.