Require Import Utf8. Set Implicit Arguments. Require Import Omega. Require Import Nat. Require Import List. Require Import Coq.Program.Equality. Section F_Upsilon. Notation "[ Y , A ]":=(cons A Y) (at level 3). Notation "[ Y ; Y' ]":=(app Y' Y) (at level 3). (** Auxiliary lemmas *) Lemma cons_nonempty T Y0 Y1 (A:T): nil = [[Y0, A]; Y1] -> False. Proof. intro H. destruct Y1; simpl in H; discriminate H. Qed. Lemma app_cons_S T Y0 Y1 (A:T) n: n = (length Y0) -> S n = length [[Y0, A]; Y1] -> Y1 = nil. Proof. intros H0 H. rewrite app_length in H;simpl in H. assert (length Y1=0) by omega. destruct Y1. - reflexivity. - simpl in H1. discriminate H1. Qed. Lemma app_revcons : forall T Y0 (A:T) Y1, [[Y0, A ]; Y1 ] = [Y0; [[nil, A ]; Y1 ] ]. Proof. intros. revert Y0 A. induction Y1. - reflexivity. - intros. do 2 rewrite <- app_comm_cons. rewrite IHY1. reflexivity. Qed. (** We first define a structure of heterogeneous lists to represent lists of term. *) Inductive hlist:= |hnil : hlist |hcons : forall A, A → hlist -> hlist . Definition happ : hlist → hlist → hlist := fix happ (l m : hlist) {struct l} : hlist:= match l with | hnil => m | hcons a l1 => hcons a (happ l1 m) end. Notation "[]":=(hnil). Notation "[ τ , t ]₁":=(hcons t τ) (at level 3). Notation "[ Y ; Y' ]₁":=(happ Y' Y) (at level 3). Definition happ_comm_cons : ∀ (A:Type) (x y : hlist) (a : A), [[y; x]₁, a]₁ = [y; [x, a]₁]₁ := λ (A:Type) (x y : hlist) (a : A), eq_refl. Lemma happ_revcons : forall A τ0 (t0:A) τ1, [[τ0, t0 ]₁; τ1 ]₁ = [τ0; [[[], t0 ]₁; τ1 ]₁ ]₁. Proof. intros. revert t0 τ0. revert A. induction τ1. - reflexivity. - intros. do 2 rewrite <- happ_comm_cons. rewrite IHτ1. reflexivity. Qed. Lemma happ_nil_r : forall τ,[[]; τ ]₁ = τ. Proof. intros. induction τ. - reflexivity. - simpl. f_equal. assumption. Qed. (** To ease the presentation, we will represent the simple types of the source calculus and their translation as a parameter. We can now define: - any store τ as a hlist, - its type Y as a list of Ty *) (** * Definitions of terms *) Parameter Ty:Type. Definition storeT := list Ty. Definition store := hlist. Parameter translation : storeT -> Ty -> Type. Notation "Y ▸ A":=(translation Y A) (at level 3). Notation "∅":=(@nil Ty). Inductive subt : storeT -> storeT -> Type:= | empty : subt nil nil | lift : forall Y' Y A, subt Y' Y -> subt [Y',A] Y | plus : forall Y' Y A, subt Y' Y -> subt [Y',A] [Y,A] . Notation "Y' <: Y":= (subt Y' Y) (at level 3). Notation "σ +":= (plus _ σ) (at level 3). Notation "↑ σ ":= (lift _ σ) (at level 3). Context (F:storeT -> Ty -> Type) (translation_sound:forall Y A, (Y ▸ A) = forall Z, Z<:Y -> F Z A). (** ** λ-terms *) Definition abs_Y (T:Type) t : storeT -> T := fun Y => t Y. Definition abs_s (T:Type) Y Y' t: (Y'<:Y) -> T := fun (s:Y'<:Y) => t s. Definition abs_δ (T:Type) t : store -> T := fun (δ:store) => t δ. Definition abs_x (T U:Type) t : U -> T := fun (x:U) => t x. Definition app_Y (T:Type) t (Y:storeT) : T := t Y. Definition app_s (T:Type) Y Y' t (σ:Y'<:Y) : T := t σ. Definition app_δ (T:Type) t (τ:store) : T := t τ. Definition app_x (T U:Type) (t:U -> T) (u:U): T := t u. Notation "λY· t" := (abs_Y t) (at level 5). Notation "λs· t" := (abs_s t) (at level 5). Notation "λδ· t" := (abs_δ t) (at level 5). Notation "λx· t" := (abs_x t) (at level 5). Notation "t Y@ Y" := (app_Y t Y) (at level 5). Notation "t s@ σ" := (app_s t σ) (at level 5). Notation "t δ@ τ" := (app_δ t τ) (at level 5). Notation "t x@ u" := (app_x t u) (at level 5). (** ** Coercions *) Fixpoint plusN Y Y0 Y1 (σ:Y0 <: Y1):[Y0;Y]<:[Y1;Y] := match Y with | nil => σ | [Y',A]=> plus A (plusN Y' σ) end. Fixpoint liftN (Y Y0 Y1:storeT) (σ: Y0 <: Y1): [Y0;Y]<:Y1 := match Y with | nil => σ | [Y',A] => lift A (liftN Y' σ) end. Definition composition :forall Y2 Y1 Y0 (σ2:Y2 <: Y1) (σ1:Y1 <: Y0), Y2 <: Y0. intro Y2. induction Y2 as [|?A ?Y];intros;inversion σ2;subst. - inversion σ1. exact empty. - apply lift. now apply (IHY2 Y1). - inversion σ1;subst. + now apply lift, (IHY2 Y2). + now apply plus, (IHY2 Y2). Defined. Notation " σ ∘ σ' " := (composition σ σ') (at level 5). Definition id Y : Y <: Y. induction Y. - exact empty. - exact IHY+. Defined. Definition acc_subt Y0 Y1 Z0 Z1 (σ0:Y0<:Z0) (σ1:Y1<:Z1): [Y0;Y1]<:[Z0;Z1]. revert σ0. revert Y0 Z0. induction σ1;intros. - exact σ0. - rewrite <- app_comm_cons. exact (lift A (IHσ1 _ _ σ0)). - do 2 rewrite <- app_comm_cons. exact (plus A (IHσ1 _ _ σ0)). Qed. Definition precomp_t (F:storeT -> Type) Y Y' (σ:Y'<:Y) (t:forall Z, Z<:Y -> F Z) : (forall Z, Z<:Y' -> F Z) := (fun Z (σ':Z<:Y') => t Z (σ' ∘ σ)). Lemma presig_t Y Y' T (σ:Y'<:Y) (t:Y ▸ T) : Y' ▸ T. Proof. rewrite translation_sound in *. now apply (precomp_t _ σ). Qed. (** ** Stores *) Inductive typedStore:store → storeT → storeT → Type := | nilT : forall Y, typedStore hnil Y nil | consT : forall (A:Ty) τ Y0 Y1 (t:[Y0;Y1] ▸ A), typedStore τ Y0 Y1 -> typedStore (hcons t τ) Y0 [Y1,A]. Notation " τ # Y ▹ Z " := (typedStore τ Y Z ) (at level 7). (** Definition of ↑^σ_Z τ *) Definition presig_τ Z : forall τ Y0 Y1 (σ:Y1 <:Y0) (H:typedStore τ Y0 Z), store. Proof. induction Z;intros;inversion H;subst. - exact hnil. - exact ([IHZ τ0 Y0 Y1 σ X,presig_t (plusN Z σ) t]₁). Defined. (** Soundness of the typing rule: Γ ⊢ τ : Y₀ ▹ Z Γ ⊢ σ:Y1 <:Y0 ——————————————————————————————————– Γ ⊢ ↑^σ_Z τ : Y₁ ▹ Z *) Lemma presig_sound Z : forall τ Y0 Y1 (σ:Y1 <:Y0) (H:typedStore τ Y0 Z), typedStore (presig_τ σ H) Y1 Z. Proof. induction Z;intros;dependent destruction H;subst. - simpl. apply nilT. - simpl. apply consT. apply IHZ. Defined. (** ** λ/@ w.r.t. □ *) (** The validity of the typing rules follows directly from the very definition of the different terms. We only show here that the typing rules for □ are indeed admissible. *) Definition square := fun (F:storeT -> Type) => (fun (Y:storeT) => forall Y' (σ:Y'<:Y) (δ:store) (p:typedStore δ ∅ Y'), F Y' -> False). Notation " □ F " := (square F) (at level 5). Definition abs_pack (Y0:storeT) (F:storeT -> Type) (t : forall (Y:storeT) (s:Y<:Y0) (δ:store) (p:typedStore δ ∅ Y), F Y -> False) : □ F Y0:= ( fun Y s δ p x => t Y s δ p x). Definition app_pack (Y0:storeT) (F:storeT -> Type) (t : □ F Y0) (Y:storeT) (σ:Y<:Y0) (τ:store) (p:typedStore τ ∅ Y) (x:F Y): False := t Y σ τ p x. (** ** Split *) Definition rwStore A Y Y' (t:Y▸A) (eq: Y = Y'):= @eq_rect storeT Y (λ (l:storeT), l ▸ A) t Y' eq. Definition subt_split: (* Proposition 3.6 *) ∀ Y Γ0 A Γ1 (σ:Y<:[[Γ0,A];Γ1]) (τ:store) (p:τ # ∅ ▹ Y), {Y0:storeT & {Y1:storeT & {σ0:Y0<:Γ0 & {σ1:Y1<:Γ1 & {τ0:store & {u : Y0 ▸ A & {τ1:store & { p0: τ0 # ∅ ▹ Y0 & { p1: τ1 # [Y0,A] ▹ Y1 & [[Y0,A];Y1]=Y /\ [[τ0,u]₁;τ1]₁ = τ }}}}}}}}}. intro Y; induction Y;intros;inversion σ;subst. - exfalso; eapply cons_nonempty;exact H. - dependent destruction τ; dependent destruction p. destruct (IHY Γ0 A Γ1 X τ p) as (Y0,(Y1,(σ0,(σ1,(τ0,(u,(τ1,(p0,(p1,(eqY,eqτ)))))))))). exists Y0,[Y1,a],σ0,↑σ1,τ0,u,[τ1,a0]₁,p0. pose (p2:=@consT a τ1 [Y0,A] Y1). rewrite eqY,<- (app_nil_r Y) in p2. exists (p2 a0 p1). split;simpl; now f_equal . - destruct Γ1 as [|T Γ1]. + simpl in *. inversion H;subst. dependent destruction τ; dependent destruction p. pose (u:= (rwStore a (app_nil_r Y))). rewrite <- (app_nil_r Y) in X,p. exists [∅;Y],nil,X,empty,τ,a,hnil,p,(nilT _). split;simpl;f_equal;try reflexivity. apply app_nil_r. + simpl in *. inversion H;subst. dependent destruction τ; dependent destruction p. destruct (IHY Γ0 A Γ1 X τ p) as (Y0,(Y1,(σ0,(σ1,(τ0,(u,(τ1,(p0,(p1,(eqY,eqτ)))))))))). pose (r:= rwStore a (eq_trans (app_nil_r Y) (eq_sym eqY))). exists Y0,[Y1,T],σ0,σ1 +,τ0,u,[τ1,a]₁,p0. pose (p2:=@consT T τ1 [Y0,A] Y1). rewrite eqY,<- (app_nil_r Y) in p2. exists (p2 a p1). split;simpl;now f_equal. Defined. (* The expected definition of: split τ at n along σ:Y<:[Γ0,A,Γ1] as (Y0,s0,δ0),x,(Y1,s1,δ1) in t *) Definition splitalong T : forall (Y Γ0 Γ1:storeT) (A:Ty) (σ:Y<:[[Γ0, A]; Γ1]) (τ:store) (p:τ # ∅ ▹ Y) (t: forall (Y0:storeT) (s0:Y0<:Γ0) (δ0:store) (p0:δ0 # ∅ ▹ Y0) (x:Y0▸A) (Y1:storeT) (s1:Y1<:Γ1) (δ1:store) (p1:δ1 # [Y0,A] ▹ Y1),T),T. intros Y Γ0 Γ1 A σ τ p t. destruct (@subt_split Y Γ0 A Γ1 σ τ p) as (Y0,(Y1,(σ0,(σ1,(τ0,(u,(τ1,(p0,(p1,eq))))))))). apply (t Y0 σ0 τ0 p0 u Y1 σ1 τ1 p1). Defined. (** ** Auxiliary lemmas *) Lemma empty_unique: forall σ : ∅ <: ∅, σ = empty. Proof. intros σ. dependent induction σ. reflexivity. Defined. (** * Reduction rules *) (** We show that the different reduction rules from F_Upsilon are validated by equalities through the embedding, that is: if t → t' then [t] = [t']. (1) Obviously, this is not enough to formally prove the normalization of F_Upsilon from the normalization of Coq, since it would require : if t → t' then [t] →⁺ [t']. (2) To reason formally on Coq inner reductions, we shall do it at a meta level, for instance using TemplateCoq which reifies Coq syntax and reductions. Yet, it is easy to convince ourself that in each case, the equalities we will obtain directly comes from the definitions of the terms through the shallow embedding and are "well-oriented", in the sense that they actually verifies (2). *) Section Reduction. (** ** ß-reductions *) (** (λs.t) σ → t[σ/s] *) Lemma beta_s : forall (T:Type) Y Y' (t:Y'<:Y -> T) (σ:Y'<:Y) , λs·t s@ σ = t σ. Proof. reflexivity. Qed. (** (λδ.t) τ → t[τ/δ] *) Lemma beta_δ : forall (T:Type) (t:store -> T) (τ:store) , λδ·t δ@ τ = t τ. Proof. reflexivity. Qed. (** (λx.t) u → t[u/x] *) Lemma beta_x : forall (T U:Type) (t:U -> T) (u:U), λx·t x@ u = t u. Proof. reflexivity. Qed. (** For instance, it is clear that the three cases actually verify (2), since in each case, λ_·t is defined as an η-expansion of t. *) (** ** Split*) (** split τ at |Γ₀| along (σ:Z<: Γ₀,A,Γ₁) as (Y₀,s₀,δ₀),x,(Υ₁,s₁,δ₁) in t → t[Z0/Y0][σ0/s0][τ0/δ0][u/x][Z1/Y1][σ1/s1][τ1/δ1] where Z=Z₀,A,Z₁ / σ=σ₀+;σ₁ / σ₀:Z₀<:Γ₀ / σ₁:Z<:Γ₀,A,Γ₁ τ=τ₀,u,τ₁ / τ₀:Z₀ / τ₁: Z₀,A▹Z₁ *) Lemma split_eq T (Y Γ0 Γ1:storeT) (A B:Ty) (σ:Y<:[[Γ0,A];Γ1]) τ (p: τ # ∅ ▹ Y) t: {Y0 : storeT & {Y1 : storeT & {σ0:Y0<:Γ0 & {σ1:Y1<:Γ1 & {τ0:store & {u : Y0▸A & {τ1:store & { p0:τ0 # ∅ ▹ Y0 & { p1:τ1 # [Y0,A] ▹ Y1 & [[Y0,A];Y1] = Y /\ [[τ0,u]₁;τ1]₁ = τ /\ @splitalong T Y Γ0 Γ1 A σ τ p t = t Y0 σ0 τ0 p0 u Y1 σ1 τ1 p1 }}}}}}}}}. Proof. unfold splitalong. pose (bli:= (@subt_split Y Γ0 A Γ1 σ τ p)). fold bli. destruct bli as (Y0,(Y1,(σ0,(σ1,(τ0,(u,(τ1,(p0,(p1,(eqY,eqτ)))))))))). exists Y0, Y1, σ0, σ1, τ0, u, τ1, p0, p1. repeat split;trivial. Qed. (** ** Coercions *) (** σ₁⁺ ∘ ⇑σ₀ → ⇑(σ₁ ∘ σ₀) *) Lemma plus_lift {Y2 Y1 Y0} A (σ1:Y2<:Y1) (σ0:Y1<:Y0): (plus A σ1) ∘ (lift A σ0) = lift A (σ1 ∘ σ0). Proof. reflexivity. Qed. (** σ₁⁺ ∘ σ₀⁺ → (σ₁ ∘ σ₀)⁺ *) Lemma plus_plus {Y2 Y1 Y0} A (σ1:Y2<:Y1) (σ0:Y1<:Y0): (plus A σ1) ∘ (plus A σ0) = plus A (σ1 ∘ σ0). Proof. reflexivity. Qed. (** ⇑σ₁ ∘ σ₀ → ⇑(σ₁ ∘ σ₀) *) Lemma lift_comp {Y2 Y1 Y0} A (σ1:Y2<:Y1) (σ0:Y1<:Y0): (lift A σ1) ∘ σ0 = lift A (σ1 ∘ σ0). Proof. reflexivity. Qed. (** ⇑_{Y,A} σ → ⇑ (⇑_Y σ) *) Lemma liftN_lift {Y1 Y0 Y} A (σ:Y1<:Y0): (liftN [Y,A] σ) = lift A (liftN Y σ). Proof. reflexivity. Qed. (** σ+_{Y,A} → (σ+_Y)⁺ *) Lemma plusN_plus {Y1 Y0 Y} A (σ:Y1<:Y0): (plusN [Y,A] σ) = plus A (plusN Y σ). Proof. reflexivity. Qed. (** σ ∘ ε → σ *) Lemma comp_empty_r {Y:storeT} (σ:Y<:∅): σ ∘ empty = σ. Proof. revert σ. induction Y;intros σ. - rewrite (empty_unique σ). reflexivity. - dependent destruction σ. rewrite lift_comp. now rewrite (IHY σ). Qed. (** ε ∘ σ → σ *) (** NB: in a typed situation σ is necessarily ε, but we have to express it that way to avoid inconsistencies with: σ ← id_∅ ∘ σ → ε ∘ σ (see below). *) Lemma comp_empty_l σ: empty ∘ σ = empty. Proof. - rewrite (empty_unique σ). reflexivity. Qed. (** id_∅ → ε *) Lemma id_nil: id ∅ = empty. Proof. reflexivity. Defined. (** id_{Y,A} → (id_Y)⁺ *) Lemma id_cons Y A: id [Y,A] = (id Y)+. Proof. reflexivity. Defined. (** id_Y ∘ σ → σ *) Lemma id_comp_l { Y1 Y0:storeT} (σ:Y1<:Y0): (id Y1) ∘ σ = σ. Proof. revert Y0 σ. induction Y1;intros Y0 σ. - rewrite id_nil. inversion σ. subst. rewrite empty_unique . exact (comp_empty_l σ). - rewrite id_cons. dependent destruction σ. + rewrite plus_lift. now rewrite IHY1. + rewrite plus_plus. now rewrite IHY1. Qed. (** ** Stores *) (** [τ;[τ',t]₁]₁ → [[τ;τ']₁,t]₁ *) Lemma store_cat_cons {A:Type} τ τ' (t:A) : [τ;[τ',t]₁]₁ = [[τ;τ']₁,t]₁. Proof. apply happ_comm_cons. Qed. (** ↑^σ_{Z,T} [τ,t]₁ → [ ↑^σ_Z τ, ↑^{σ+Z} t]₁ *) Lemma store_presig {A:Ty} : ∀ (Z Y0 Y1: storeT) (τ : store) (t :[Y0;Z] ▸ A) (σ:Y1 <: Y0) (H:τ # Y0 ▹ Z), presig_τ σ (consT t H) = [presig_τ σ H,presig_t (plusN Z σ) t]₁. Proof. intros. reflexivity. Qed. End Reduction. (** * About coercions *) Section AboutCoercions. (** We show that coercions in normal forms can indeed be associated with a partial function from [0,n] to [0,p] *) (** ** Domain/codomain of a coercion *) Fixpoint domain Y Y' (σ:Y<:Y'):nat:= match σ with |empty => 0 |lift _ σ => domain σ |plus _ σ => S(domain σ) end. Fixpoint codomain Y Y' (σ:Y<:Y'):nat:= match σ with |empty => 0 |lift _ σ => S(codomain σ) |plus _ σ => S(codomain σ) end. (** Type of partial functions, either as a function or as a list (that is the underlying functional relation). *) Definition coer_fun := nat -> option nat. Definition coer_list := list (nat * nat). Definition empty_fun : coer_fun := fun n => match n with | 0 => Some 0 | _ => None end. (** ** The associated function *) Fixpoint list_of_coer Y Y' (σ:Y<:Y') : coer_list := match σ with | empty => (0,0)::nil | plus _ r => let l := list_of_coer r in match l with |nil => nil |(a,b)::q => (S(a),S(b))::l end | lift _ r => let l := list_of_coer r in match l with |nil => @nil (nat * nat) |(a,b)::q => (a,S(b))::q end end. Fixpoint fun_of_list (l:coer_list):coer_fun := match l with | nil => fun _ => None | (a,b)::q => let f := fun_of_list q in fun n => match Nat.leb n a with | true => match Nat.eqb n a with | false => f n | true => Some b end | false => None end end. Definition fun_of_coer Y Y' (σ:Y<:Y') := fun_of_list (list_of_coer σ). (** ** Examples *) Section Examples. Context (A B C D E : Ty). Definition id3:= id [[[nil,A],B],C]. Definition l3:= list_of_coer id3. Definition im2 := (fun_of_coer id3) 2. Eval compute in l3. Eval compute in im2. Definition test:= plus E (lift D (plus C (lift B (plus A empty)))). Definition lσ:= list_of_coer test. Definition σ2:= (fun_of_coer test) 2. Check test. Eval compute in lσ. Eval compute in σ2. End Examples. (** ** Soundness *) Lemma nth_length_lt m (l l':storeT): m nth m [l;l'] = nth m l'. Proof. revert m. revert l. induction l';intros. - simpl in H. omega. - simpl. destruct m;[reflexivity|]. simpl in H. apply lt_S_n in H. now rewrite (IHl' l m H). Qed. Lemma nth_length_eq m (l l':storeT): m=length l' -> nth m [l;l'] = nth 0 l. Proof. revert m. revert l. induction l';intros. - simpl in H. rewrite H; now simpl. - simpl in H. rewrite H. simpl. now rewrite (IHl' l (length l') eq_refl). Qed. Lemma subt_length: ∀ Y Y' (σ:Y'<:Y), length Y <= length Y'. Proof. intros. induction σ;simpl; omega. Qed. Lemma list_coer_cons : forall Y Y' (σ:Y'<: Y), { n:nat & { m:nat & { q:_ & list_of_coer σ = (n,m)::q}}}. Proof. intros *. induction σ;simpl; [|destruct IHσ as (n,(m,(q,H))); rewrite H|destruct IHσ as (n,(m,(q,H))); rewrite H]; now repeat eexists; reflexivity. Qed. Lemma list_coer_length: forall Y Y' (σ:Y'<: Y), length (list_of_coer σ) = S (length Y). Proof. intros. induction σ. + reflexivity. + simpl. destruct (list_coer_cons σ) as (p,(q,(l,Hl))). rewrite Hl in *. now simpl in *. + simpl. destruct (list_coer_cons σ) as (p,(q,(l,Hl))). rewrite Hl in *. simpl. now f_equal. Qed. Lemma list_coer_last Y Y' (σ:Y'<: Y) : {q:list (nat*nat) & (list_of_coer σ)=(length Y,length Y')::q}. Proof. dependent induction σ. - simpl in *. now exists nil. - simpl. destruct (IHσ) as (t,Ht). destruct (list_coer_cons σ) as (p,(q,(l,Hl))). rewrite Hl in *. simpl in *. inversion Ht. now exists t. - simpl in *. destruct (list_coer_cons σ) as (p,(q,(l,Hl)));subst. destruct IHσ as (t,Ht). rewrite Hl in *. simpl in *. inversion Ht. subst. repeat eexists. Qed. Theorem list_coer_sound Y Y' (σ:Y'<: Y) : forall n, n< length Y -> ∃ m, n<=m /\ m (forall c d, In (c,d) l -> c sorted [l,(a,b)]. Lemma sorted_lt l (a b c d : nat): sorted [l,(a,b)] -> In (c,d) l -> c < a. Proof. intros H H0. inversion H. apply (H5 _ _ H0). Qed. Lemma list_coer_sorted Y Y' (σ:Y'<:Y): sorted (list_of_coer σ). Proof. induction σ. - simpl. apply sorted_cons. + apply sorted_nil. + intros c d H. now inversion H. - simpl. destruct (list_coer_last σ) as (t,Ht). rewrite Ht in *. inversion IHσ. apply (sorted_cons _ H1). intros c d H4. now apply (H3 _ d). - simpl. destruct (list_coer_last σ) as (t,Ht). rewrite Ht in *. inversion IHσ. apply (sorted_cons _ IHσ). intros c d H4. destruct H4. + inversion H4. omega. + apply (lt_trans _ _ _ (H3 _ d H4)). omega. Qed. Lemma fun_list_sound l : forall n m, In (n,m) l -> sorted l -> fun_of_list l n = Some m. Proof. induction l;intros n m H Srt. - simpl in H. exfalso. exact H. - destruct a as (a,b). destruct (lt_eq_lt_dec n a) as [[?Hn|?Hn]|?Hn]. + simpl. rewrite leb_correct;[|omega]. replace (n=? a) with false. destruct H. * inversion H;omega. * apply (IHl _ _ H). now inversion Srt. * symmetry. rewrite Nat.eqb_neq. omega. + simpl. subst. rewrite Nat.leb_refl. rewrite Nat.eqb_refl. destruct H. * now inversion H. * apply (sorted_lt a m) in Srt;[|assumption]. omega. + destruct H. * inversion H;omega. * apply (sorted_lt n m) in Srt;[|assumption]. omega. Qed. Theorem fun_coer_sound Y Y' (σ:Y'<: Y) : forall n, n< length Y -> ∃ m, fun_of_coer σ n = Some m /\ m