Improvements

* New definition of System F terms
* bound is no more admitted

Coq/f.v

@@ -33,46 +33,29 @@ Fixpoint type_subst (n : nat) (T : type) (U : type) : type :=
   | TForall T => TForall (type_subst (S n) T (type_lift 0 U))
  end.
 
-(* Curch-style terms of System F.
+(* Derivations in System F.
    de Bruijn indices again. *)
-Inductive fterm : Type :=
- | FVar : nat -> fterm
- | FAbs : type -> fterm -> fterm
- | FApp : fterm -> fterm -> fterm
- | FTAbs : fterm -> fterm
- | FTApp : fterm -> type -> fterm.
+Inductive fvar : list type -> type -> Type :=
+ | FVar0 : forall {context : list type} (T : type), fvar (T::context) T
+ | FVarS : forall {context : list type} {T : type} {U : type}, fvar context T -> fvar (U::context) T.
+Inductive fterm : list type -> type -> Type :=
+ | FVar : forall {context : list type} {T : type}, fvar context T -> fterm context T
+ | FAbs : forall {context : list type} {T : type} {U : type}, fterm (T::context) U -> fterm context (TArrow T U)
+ | FApp : forall {context : list type} {T : type} {U : type}, fterm context (TArrow T U) -> fterm context T -> fterm context U
+ | FTAbs : forall {context : list type} {T : type}, fterm (map (type_lift 0) context) T -> fterm context (TForall T)
+ | FTApp : forall {context : list type} {T : type}, fterm context (TForall T) -> forall (U : type), fterm context (type_subst 0 T U).
+Definition fterm_get_context {context : list type} {T : type} (t : fterm context T) := context.
+Definition fterm_get_type {context : list type} {T : type} (t : fterm context T) := T.
+(* ∀X.(X→X) *)
+Definition type1 : type := TForall (TArrow (TVar 0) (TVar 0)).
 (* ΛX.λx:X.x *)
-Definition term1 : fterm :=  FTAbs (FAbs (TVar 0) (FVar 0)).
+Definition term1 : fterm [] type1 :=
+  FTAbs (FAbs (FVar (FVar0 (TVar 0)))).
+(* ∀X.(X→X)→∀X.(X→X) *)
+Definition type2 : type := (TArrow type1 type1).
 (* λx:∀X(X→X).x(∀X(X→X))x *)
-Definition term2 : fterm :=  FAbs (TForall (TArrow (TVar 0) (TVar 0))) (FApp (FTApp (FVar 0) (TForall (TArrow (TVar 0) (TVar 0)))) (FVar 0)).
-(* "type_get context t" is the type
-   of t in context context. *)
-Fixpoint type_get (context : list type) (t : fterm) : type :=
- match t with
-  | FVar n => nth n context (TVar 0)
-  | FAbs T t => TArrow T (type_get (T::context) t)
-  | FApp t u =>
-   match type_get context t with
-    | TArrow T U => U
-    | _ => TVar 0
-   end
-  | FTAbs t => TForall (type_get (map (type_lift 0) context) t)
-  | FTApp t T =>
-   match type_get context t with
-    | TForall U => type_subst 0 U T
-    | _ => TVar 0
-   end
- end.
-(* "type_correct context t" holds if
-   t is typable in context context. *)
-Fixpoint type_correct (context : list type) (t : fterm) : Prop :=
- match t with
-  | FVar n => n < length context
-  | FAbs T t => type_correct (T::context) t
-  | FApp t u => type_correct context t /\ type_correct context u /\ exists T, type_get context t = TArrow (type_get context u) T
-  | FTAbs t => type_correct (map (type_lift 0) context) t
-  | FTApp t T => type_correct context t /\ exists T, type_get context t = TForall T
- end.
+Definition term2 : fterm [] type2 :=
+  FAbs (FApp (FTApp (FVar (FVar0 type1)) type1) (FVar (FVar0 type1))).
 
 (* Untyped lambda-terms.
    Still de Bruijn indices. *)
@@ -82,13 +65,18 @@ Inductive term : Type :=
  | App : term -> term -> term.
 (* Erasure from Church-style System F
    terms to untyped (Curry-style) terms *)
-Fixpoint fterm_to_term (t : fterm) : term :=
+Fixpoint fvar_to_nat {context : list type} {T : type} (t : fvar context T) : nat :=
  match t with
-  | FVar n => Var n
-  | FAbs T t => Abs (fterm_to_term t)
+  | FVar0 _ => 0
+  | FVarS t => S (fvar_to_nat t)
+ end.
+Fixpoint fterm_to_term {context : list type} {T : type} (t : fterm context T) : term :=
+ match t with
+  | FVar t => Var (fvar_to_nat t)
+  | FAbs t => Abs (fterm_to_term t)
   | FApp t u => App (fterm_to_term t) (fterm_to_term u)
   | FTAbs t => fterm_to_term t
-  | FTApp t T => fterm_to_term t
+  | FTApp t _ => fterm_to_term t
  end.
 (* "term_equal t u" is true if t and u
    are syntactically equal. *)
@@ -311,6 +299,23 @@ Fixpoint form_lift2 (n : nat) (f : form) : form :=
   | FForallp f => FForallp (form_lift2 n f)
   | FForall2 f => FForall2 (form_lift2 (S n) f)
  end.
+Lemma form_lift2_substt : forall m n f t, form_lift2 m (form_substt n f t) = form_substt n (form_lift2 m f) t.
+intros m n f; revert m n; induction f; intros m p t; simpl.
+destruct (n <? m); reflexivity.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
 (* "form_subst2 n f g" is f[g/n].
    2nd-order variables of f with
    index >= n are decremented. *)
@@ -358,6 +363,33 @@ Fixpoint rc (T : type) : form :=
   | TArrow T U => FForallt (FImp (rc T) (form_substt 0 (rc U) (LApp (LMetavar 1) (LLList [LMetavar 0]))))
   | TForall T => FForall2 (FImp redcand (rc T))
  end.
+Lemma form_lift2_rc : forall n U, form_lift2 n (rc U) = rc (type_lift n U).
+intros n U; revert n; induction U; intro m; simpl.
+destruct (n <? m); reflexivity.
+f_equal.
+f_equal.
+apply IHU1.
+rewrite form_lift2_substt.
+rewrite IHU2.
+reflexivity.
+rewrite IHU.
+reflexivity.
+Qed.
+Lemma form_subst2_lift2 : forall m T n U, form_subst2 m (rc T) (form_lift2 n (rc U)) = form_subst2 m (rc T) (rc (type_lift n U)).
+intros m T; revert m; induction T; intros m p U; simpl.
+destruct (n ?= m).
+rewrite form_lift2_rc.
+reflexivity.
+reflexivity.
+reflexivity.
+rewrite IHT1.
+rewrite form_lift2_rc.
+reflexivity.
+rewrite IHT.
+rewrite form_lift2_rc.
+rewrite form_lift2_rc.
+reflexivity.
+Qed.
 
 (* "form_to_type f" is the type of
    realizers of f. *)
@@ -511,6 +543,21 @@ reflexivity.
 rewrite IHf.
 reflexivity.
 Qed.
+Lemma form_to_type_subst2_type_subst : forall T U n, form_to_type (form_subst2 n (rc T) (rc U)) = form_to_type (rc (type_subst n T U)).
+intro t; induction t; intros U m; simpl.
+destruct (n ?= m); simpl.
+apply form_to_type_substt.
+reflexivity.
+reflexivity.
+rewrite IHt1.
+rewrite form_to_type_substt.
+rewrite form_to_type_subst2_substt.
+rewrite IHt2.
+reflexivity.
+rewrite <- IHt.
+rewrite form_subst2_lift2.
+reflexivity.
+Qed.
 (*Lemma form_to_type_subst2_fin2 : forall (f : form) (n : nat) (t : logterm), form_to_type (form_subst2 n (FIn t n) f) = form_to_type f.
 intros f n t; simpl.
 rewrite Nat.compare_refl.
@@ -840,70 +887,43 @@ Qed.
    H is a proof that t is well-typed
    in context context) is the realizer of
    RC_{(type_get context t)[U_1...U_n/0]}(t[u_1...u_n/0]) *)
-Program Fixpoint adeq (context : list (term * {T : type & form_to_type (rc T)})) (tcontext : list (form_to_type redcand)) (t : fterm) (H : type_correct (map (fun a => projT1 (snd a)) context) t) : form_to_type (rc (type_get (map (fun a => projT1 (snd a)) context) t)) :=
+Program Fixpoint adeq_var (tcontext : list (form_to_type redcand)) (context : list (term * {T : type & form_to_type (rc T)})) (T : type) (t : fvar (map (@projT1 type (fun T => form_to_type (rc T))) (map snd context)) T) : form_to_type (rc T) :=
+   match t with
+    | FVar0 T => match context with [] => match _ : False with end | (t, existT _ T x)::context => x end
+    | FVarS t => match context with [] => match _ : False with end | _::context => rew [id] _ in adeq_var tcontext context T t end
+   end.
+Program Fixpoint adeq (tcontext : list (form_to_type redcand)) (context : list (term * {T : type & form_to_type (rc T)})) (T : type) (t : fterm (map (@projT1 type (fun T => form_to_type (rc T))) (map snd context)) T) : form_to_type (rc T) :=
  match t with
-  | FVar n => rew [id] _ in projT2 (snd (nth n context (Var 0, existT _ (TVar 0) 0)))
-  | FAbs T t =>
+  | @FVar _ _ t => adeq_var tcontext context _ t
+  | @FAbs _ T U t =>
    fun u y =>
     let context := (u, existT _ T y)::context in
-    rew [id] _ in snd (isrc tcontext (type_get (map (fun a => projT1 (snd a)) context) t)) (term_subst 1 (fterm_to_term t) (map (fun a => term_lift 0 (fst a)) context)) u [] (rew [id] _ in adeq context tcontext t _)
-  | FApp t u => (rew [id] _ in adeq context tcontext t _) (term_subst 0 (fterm_to_term u) (map (fun a => fst a) context)) (adeq context tcontext u _)
-  | FTAbs t => fun x => rew [id] _ in adeq (map (fun a => (fst a, existT _ (type_lift 0 (projT1 (snd a))) (rew [id] _ in projT2 (snd a)))) context) (x::tcontext) t _
-  | FTApp t T =>
-   let U := match type_get (map (fun a => projT1 (snd a)) context) t with TForall U => U | _ => TVar 0 end in
-   rew [id] _ in elim (FImp redcand (form_substt 0 (rc U) (term_to_logterm (term_subst 0 (fterm_to_term t) (map (fun a => fst a) context))))) (rc T) (rew [id] _ in adeq context tcontext t _) (isrc tcontext T)
+    rew [id] _ in snd (isrc tcontext U) (term_subst 1 (fterm_to_term t) (map (fun a => term_lift 0 (fst a)) context)) u [] (rew [id] _ in adeq tcontext context U t)
+  | @FApp _ T U t u => rew [id] _ in adeq tcontext context (TArrow T U) t (term_subst 0 (fterm_to_term u) (map (fun a => fst a) context)) (adeq tcontext context T u)
+  | @FTAbs _ T t => fun x => rew [id] _ in adeq (x::tcontext) (map (fun a => (fst a, existT _ (type_lift 0 (projT1 (snd a))) (rew [id] _ in projT2 (snd a)))) context) T t
+  | @FTApp _ T t U => rew [id] _ in elim (FImp redcand (form_substt 0 (rc T) (term_to_logterm (term_subst 0 (fterm_to_term t) (map (fun a => fst a) context))))) (rc U) (rew [id] _ in adeq tcontext context (TForall T) t) (isrc tcontext U)
  end.
 Next Obligation.
-revert n H.
-induction context; intros n H.
-rewrite nth_overflow; [ | apply le_0_n ].
-rewrite nth_overflow; [ | apply le_0_n ].
-reflexivity.
-rewrite map_cons.
-destruct n.
-reflexivity.
-simpl nth.
-apply IHcontext.
-simpl type_correct in *.
-apply lt_S_n.
-apply H.
-Qed.
-Next Obligation.
+fold form_to_type.
 rewrite form_to_type_substt.
 reflexivity.
 Qed.
 Next Obligation.
+fold form_to_type.
+fold rc.
 rewrite form_to_type_substt.
 rewrite form_to_type_substt.
 reflexivity.
 Qed.
 Next Obligation.
-simpl type_correct in H.
-destruct H.
-apply H.
-Qed.
-Next Obligation.
-simpl type_correct in H.
-destruct H.
-destruct H0.
-destruct H1.
-destruct (type_get _ t); try discriminate.
-simpl.
+fold form_to_type.
+fold rc.
 rewrite form_to_type_substt.
-injection H1 as H11 H12.
-rewrite <- H11.
 reflexivity.
 Qed.
 Next Obligation.
-simpl type_correct in H.
-destruct H.
-destruct H0.
-apply H0.
-Qed.
-Next Obligation.
-simpl; clear.
-generalize 0.
-induction s; simpl; intro m.
+simpl.
+generalize 0; clear; induction s; intro m; simpl.
 destruct (n <? m); reflexivity.
 rewrite form_to_type_substt.
 rewrite form_to_type_substt.
@@ -914,88 +934,22 @@ rewrite <- IHs.
 reflexivity.
 Qed.
 Next Obligation.
-simpl type_correct in H.
 rewrite map_map.
-simpl.
-rewrite map_map in H.
-apply H.
-Qed.
-Next Obligation.
 rewrite map_map.
 rewrite map_map.
+rewrite map_map.
+apply map_ext.
 reflexivity.
 Qed.
 Next Obligation.
-simpl type_correct in H.
-destruct H.
-apply H.
-Qed.
-Next Obligation.
-simpl type_correct in H.
-destruct H.
-destruct H0.
-rewrite H0.
-simpl.
 rewrite form_to_type_substt.
 reflexivity.
 Qed.
 Next Obligation.
-simpl type_correct in H.
-destruct H.
-destruct H0.
-rewrite H0.
-rewrite form_to_type_subst2_substt.
-clear; revert T.
-generalize 0.
-clear; induction x; intros m T.
-simpl.
-destruct (n ?= m); simpl.
-rewrite form_to_type_substt.
-reflexivity.
-reflexivity.
-reflexivity.
-simpl.
-rewrite IHx1.
-rewrite form_to_type_substt.
+fold form_to_type.
+fold form_subst2.
 rewrite form_to_type_subst2_substt.
-rewrite IHx2.
-reflexivity.
-simpl.
-rewrite (form_to_type_subst2 _ _ _ (rc T)).
-rewrite IHx.
-assert (forall a b c, b = c -> (a -> b) = (a -> c)).
-intros a b c Heq; rewrite Heq; reflexivity.
-apply H; clear H.
-generalize (S m); clear.
-revert T; induction x; intros T m.
-simpl.
-destruct (n ?= m).
-generalize 0; clear; induction T; intro m.
-simpl.
-destruct (n <? m); reflexivity.
-simpl.
-rewrite form_to_type_substt.
-rewrite form_to_type_substt.
-rewrite <- IHT1.
-rewrite <- IHT2.
-reflexivity.
-simpl.
-rewrite <- IHT.
-reflexivity.
-reflexivity.
-reflexivity.
-simpl.
-rewrite form_to_type_substt.
-rewrite form_to_type_substt.
-rewrite <- IHx1.
-rewrite <- IHx2.
-reflexivity.
-simpl.
-rewrite <- IHx.
-rewrite <- IHx.
-rewrite <- IHx.
-reflexivity.
-rewrite form_to_type_lift2.
+rewrite form_to_type_subst2_type_subst.
 reflexivity.
 Qed.
 
@@ -1004,11 +958,12 @@ Qed.
    context) computes a bound a bound
    on the number of reduction steps
    of t *)
-Program Definition bound (t : fterm) (H : type_correct [] t) : nat :=
- snd (fst (isrc [] (type_get [] t))) (fterm_to_term t) (adeq [] [] t H) id.
+Program Definition bound (T : type) (t : fterm [] T) : nat :=
+ snd (fst (isrc [] T)) (fterm_to_term t) (rew [id] _ in adeq [] [] T t) id.
 Next Obligation.
-Admitted.
-
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
 
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].