Imports
Require Import FsubN FsubD.
Require Import Lia Arith.
From Equations Require Import Equations.
Require Import Vector Utils.Various_utils.
Require Import Utils.psyntax Utils.syntax.
Import VectorNotations.
Require Import Lia Arith.
From Equations Require Import Equations.
Require Import Vector Utils.Various_utils.
Require Import Utils.psyntax Utils.syntax.
Import VectorNotations.
Fact all_inj `{arrow_flag} {s1 s2 t1 t2} : all s1 s2 = all t1 t2 -> s1=t1 /\ s2=t2.
Proof. intro H1. inversion H1. split. apply (DPI H2). apply (DPI H3). Qed.
The flip property is immediate for the height-agnostic system
Definition neg (t : type0) : type0 := all t (var_type 0).
Derive Signature for subN.
Fact flipNeg Γ s t : (Γ |-N neg s <: neg t) <-> (Γ |-N t <: s).
Proof. unfold neg. split; intro.
-depind H; try discriminate. destruct (all_inj H1) as [-> _]. destruct (all_inj H2) as [-> _]. auto.
-apply NAll. auto. apply NRefl.
Qed.
Derive Signature for subN.
Fact flipNeg Γ s t : (Γ |-N neg s <: neg t) <-> (Γ |-N t <: s).
Proof. unfold neg. split; intro.
-depind H; try discriminate. destruct (all_inj H1) as [-> _]. destruct (all_inj H2) as [-> _]. auto.
-apply NAll. auto. apply NRefl.
Qed.
Section argument.
Context {w:nat}.
Variable (Hw: 0<w).
Fixpoint mkBounded {n} (v : Vector.t type0 n) (b : type0) {struct v} : type0
:= match v with
| [] => neg b
| Vector.cons _ h n0 v0 => all h (mkBounded v0 b)
end.
Fixpoint mkUnbounded (n : nat)(b : type0) : type0
:= match n with
| 0 => neg b
| S n => all top (mkUnbounded n b)
end.
Fixpoint iterShift (n:nat) (t: fin) : fin := match n with
| 0 => t
| S n0 => ↑(iterShift n0 t)
end.
Fixpoint addShiftings {n} i (v : Vector.t type0 n) : Vector.t type0 n :=
match v in (t _ n0) return (t type0 n0) with
| [] => []
| Vector.cons _ h n0 v0 => ( ren_type (iterShift i) h :: addShiftings (S i) v0)%vector
end.
Fixpoint ptranslation {n} (t : @ptype w n) : type0 := match t with
| psyntax.top => syntax.top
| bAllN t1 t2 => mkBounded (addShiftings 0 (Vector.map (ntranslation) t1)) (ntranslation t2)
end
with ntranslation {n} (s: @ntype w n) : type0 := match s with
| var_ntype i j => var_type (fins2nat i j)
| uAllN t => mkUnbounded w (ptranslation t)
end.
Facts about the translation.
Fact nth'_addShiftings {l x} {v: Vector.t type0 l} (H : x<l) y :
nth' (addShiftings y v) (nat2nif H) = ren_type (iterShift (l-S x+y)) (nth' v (nat2nif H)).
Proof. revert y. induction v; intro. lia. simpl. destruct (le_lt_dec n x); simpl.
-assert (n-x+y=y). lia. now rewrite H0.
-rewrite (nat2nif_ext _ l). rewrite (IHv l). assert (n-S x+S y=n-x+y). lia. now rewrite H0.
Qed.
Fact nth'_addShiftings' {l x} {v: Vector.t type0 l} (H : x<l) y :
nth' (addShiftings y v) (nat2fin H) = ren_type (iterShift (x+y)) (nth' v (nat2fin H)).
Proof. revert x H y. induction v; intros. lia. destruct x. auto. simpl.
rewrite IHv. now rewrite Nat.add_succ_r.
Qed.
Fact nth_addShiftings {l x y d} {v: Vector.t type0 l} : x<l ->
nth x (to_list (addShiftings y v)) d = ren_type (iterShift (x+y)) (nth x (to_list v) d).
Proof. revert x y. induction v; intros. lia. destruct x. auto.
change (to_list (h::v)) with (cons h (to_list v)). simpl addShiftings.
change (to_list (ren_type (iterShift y) h :: addShiftings (S y) v)) with
(cons (ren_type (iterShift y) h) (to_list (addShiftings (S y) v))).
simpl nth. rewrite IHv. now rewrite Nat.add_succ_r. lia.
Qed.
Fixpoint ptrans_noVar {m i t} : var_type i <> @ptranslation m t.
Proof. destruct t. discriminate. simpl. induction t; simpl; discriminate.
Qed.
Fact mkBnd_noTop {n v b } : syntax.top <> @mkBounded n v b.
Proof. destruct v; discriminate. Qed.
Fact mkUnd_noVar {n i b} : var_type i <> @mkUnbounded n b.
Proof. destruct n; discriminate. Qed.
Fact mkBnd_noVar {n i v b} : var_type i <> @mkBounded n v b.
Proof. destruct v; discriminate. Qed.
Fact congr_mkUnbounded {n s t} : s=t -> mkUnbounded n s = mkUnbounded n t.
Proof. congruence. Qed.
Fact congr_mkBounded {n} {u v : Vector.t type0 n} {s t} : u=v -> s=t -> mkBounded u s = mkBounded v t.
Proof. congruence. Qed.
Fixpoint iterFnShift {m} n (i : fintype.fin m) {struct n} : fintype.fin (n+m).
Proof. destruct n.
-exact i.
-apply (fintype.shift),(iterFnShift _ _ i).
Defined.
Fixpoint iterLift (n : nat) (r : fin->fin) {struct n} : fin-> fin := match n with
| 0 => r
| S n0 => upRen_type_type (iterLift n0 r)
end.
Fixpoint iterPLift (n : nat) {m m'} (r : fintype.fin m ->fintype.fin m') {struct n} : fintype.fin (n+m) ->fintype.fin (n+m').
Proof. destruct n.
-exact r.
-apply upRen_ntype_ntype,(iterPLift _ _ _ r).
Defined.
Fact iterShiftR n (t : type0) : ren_type (iterShift (S n)) t = ren_type ↑ (ren_type (iterShift n) t).
Proof. induction n.
-change (iterShift 0) with (@id fin). asimpl. now simpl.
-simpl in *. change (fun t0 : fin => ↑ (↑ (iterShift n t0))) with ((fun t : fin => ↑ (iterShift n t)) >> ↑).
erewrite <- compRenRen_type; eauto.
Qed.
Fact iterShiftLR n (t: type0) : ren_type (iterShift n) (ren_type ↑ t) = ren_type ↑ (ren_type (iterShift n) t).
Proof. induction n.
-change (iterShift 0) with (@id fin). asimpl. now simpl.
-simpl in *.
change (ren_type (fun t0 : fin => ↑ (iterShift n t0)) (ren_type ↑ t)) with (ren_type (iterShift n >> ↑) (ren_type ↑ t)).
change (ren_type (fun t0 : fin => ↑ (iterShift n t0)) t) with (ren_type (iterShift n >> ↑) t ).
assert (ren_type (iterShift n >> ↑) (ren_type ↑ t)=ren_type ↑ (ren_type (iterShift n) (ren_type ↑ t))).
{ erewrite <- compRenRen_type; try eauto. }
assert (ren_type (iterShift n >> ↑) t = ren_type ↑ (ren_type (iterShift n) t)).
{ erewrite <- compRenRen_type. 2:eauto. auto. }
rewrite H. rewrite IHn. now rewrite H0.
Qed.
Fact iterShiftAdd n m (t:type0) : ren_type (iterShift n) (ren_type (iterShift m) t) = ren_type (iterShift (n+m)) t.
Proof. revert n. induction m; intro.
-change (iterShift 0) with (@id fin). rewrite Nat.add_0_r. now asimpl.
-rewrite iterShiftR. rewrite iterShiftLR. rewrite <- iterShiftR. rewrite IHm. now rewrite Nat.add_succ_r.
Qed.
Fact iterLiftL n r : upRen_type_type (iterLift n r) = iterLift (S n) r.
Proof. auto. Qed.
Fact iterLiftLR n r : (upRen_type_type (iterLift n r)) = iterLift n (upRen_type_type r).
Proof. induction n; auto. simpl. now rewrite IHn. Qed.
Fact iterPnLiftL n {m m'} (r : fintype.fin m ->fintype.fin m') : upRen_ntype_ntype (iterPLift n r) = iterPLift (S n) r.
Proof. auto. Qed.
Fact iter_unfold' n x: iterShift n x = n+x.
Proof. induction n; simpl; [ change (fun i:fin=>i) with (@id fin) | rewrite IHn]; now asimpl.
Qed.
Fact iter_unfold n: iterShift n = fun i=>n+i.
Proof. fext. intro. apply iter_unfold'.
Qed.
Fact shif_lift n (t:type0): ren_type (iterShift (n+w)) t = ren_type (iterShift n >> iterLift n (iterShift w)) t.
Proof. induction n.
-change (iterShift 0) with (@id fin). asimpl. now simpl.
-change (S n+w) with (S (n+w)). rewrite iterShiftR. rewrite IHn.
erewrite compRenRen_type; eauto.
Qed.
Fact ren_Ubnd r n t : ren_type r (mkUnbounded n t) = mkUnbounded n (ren_type (iterLift n r) t).
Proof. revert r. induction n; intro; simpl. auto. apply congr_all. auto. rewrite IHn. now rewrite iterLiftLR. Qed.
Fixpoint renBounds {n} r (v : Vector.t type0 n) : Vector.t type0 n :=
match v in (t _ n0) return (t type0 n0) with
| [] => []
| Vector.cons _ h n0 v0 => ( ren_type r h :: renBounds (upRen_type_type r) v0)%vector
end.
Fact nth'_renBounds {l x} {v: Vector.t type0 l} (H : x<l) r : nth' (renBounds r v) (nat2fin H) = (nth' v (nat2fin H)) ⟨iterLift x r⟩.
Proof. revert x H r. induction v; intros. lia. destruct x. auto.
simpl. rewrite IHv. now rewrite iterLiftLR.
Qed.
Fact ren_Bnd {n} r (v:Vector.t type0 n) i t : ren_type r (mkBounded (addShiftings i v) t) = mkBounded (renBounds r (addShiftings i v)) (ren_type (iterLift n r) t).
Proof. revert r i. induction v; intros; simpl. auto. apply congr_all. auto. rewrite IHv. now rewrite iterLiftLR. Qed.
Definition tRen {n m} (r : fintype.fin n -> fintype.fin m) : fin -> fin.
Proof. intros x. destruct (le_lt_dec (w*n) x). exact x. destruct (nat2fins l) as [i j]. exact (fins2nat i (r j)).
Defined.
Fact aux i j n : i < w -> j < (S n) -> w * (S n) <= j * w + i -> False.
Proof. intro. revert j. induction n; intros.
-assert (j=0). lia. rewrite H2 in H1. simpl in H1. lia.
-revert H1. rewrite (@Nat.mul_comm w). destruct j. lia. simpl. intro. apply (IHn (S j)).
{ destruct (le_lt_dec n j). assert (j=n). lia. rewrite H2 in H1. lia. lia. } lia.
Qed.
Fixpoint tRen_char {n m} (i: fintype.fin w) (j: fintype.fin n) (r : fintype.fin n -> fintype.fin m) {struct n}: tRen r (fins2nat i j) = fins2nat i (r j).
Proof. destruct n. contradiction. unfold tRen. destruct (le_lt_dec (w * S n) (fins2nat i j)).
{exfalso. revert l. unfold fins2nat. destruct (nif2nat i) as [i' [H0 H1]]. destruct (fin2nat' j) as [j' [H2 H3]]. now apply (aux i' j' n). }
now rewrite n2fs_unfold.
Qed.
Fact iterL_ge {r n x} : n<=x -> iterLift n r x = iterShift n (r (x-n)).
Proof. revert x. induction n; intros.
-simpl. now rewrite Nat.sub_0_r.
-destruct x; simpl. lia. unfold funcomp. erewrite IHn. auto. lia.
Qed.
Fact iterL_lt {r n x} : x<n -> iterLift n r x = x.
Proof. revert x. induction n. lia. intros. simpl. asimpl.
destruct x; simpl. auto. asimpl. rewrite IHn; lia.
Qed.
Fact renBounds_shifts {n m r s} {t : Vector.t (@ntype w m) n} (Hrs : forall x, x < w * m -> r x = s x ) :
Vector.Forall (fun n => forall r s, (forall x, x < w * m -> r x = s x) -> (ntranslation n) ⟨r⟩ = (ntranslation n) ⟨s⟩) t->
renBounds r (addShiftings 0 (Vector.map ntranslation t)) = renBounds s (addShiftings 0 (Vector.map ntranslation t)).
Proof. intro. apply ext_nth'. intro. destruct (fin2nat' i) as [x [Hx <-]].
repeat rewrite nth'_renBounds. repeat rewrite nth'_addShiftings'. rewrite nth'_map. rewrite Nat.add_0_r.
rewrite iter_unfold. asimpl. unfold funcomp.
edestruct (@Forall_nth' (@ntype w m)
(fun t => ren_type (fun x0 : fin => iterLift x r (x + x0)) (ntranslation t)=ren_type (fun x0 : fin => iterLift x s (x + x0)) (ntranslation t)) n t).
apply H0. clear H0 H1. revert H. eapply Vector.Forall_impl. intros. apply H.
intros. destruct (le_lt_dec x (x+x0)).
-repeat erewrite iterL_ge; auto. rewrite minus_plus. rewrite Hrs; auto.
-repeat erewrite iterL_lt; auto.
Qed.
Fact ext_lift {m r s} (Hrs : forall x, x < w * m -> r x = s x ) {x} (Hx: x < w * S m): iterLift w r x = iterLift w s x.
Proof. destruct (le_lt_dec w x).
-repeat rewrite (iterL_ge l). repeat rewrite iter_unfold. erewrite Hrs. auto. lia.
-now repeat rewrite (iterL_lt l).
Qed.
Fact ext_trans : forall m,
(forall (t: @ptype w m) r s, (forall x, x<w*m -> r x = s x) -> ren_type r (ptranslation t) = ren_type s (ptranslation t))
/\ (forall (t: @ntype w m) r s, (forall x, x<w*m -> r x = s x) -> ren_type r (ntranslation t) = ren_type s (ntranslation t)).
Proof. eapply ptype_ntype_mutind; intros; simpl. auto.
-repeat rewrite ren_Bnd. apply congr_mkBounded. apply renBounds_shifts,H0. exact H1. apply H. now apply ext_lift.
-asimpl. now rewrite (H _ (fins2nat_lt t t0)).
-repeat rewrite ren_Ubnd. apply congr_mkUnbounded. apply H. now apply ext_lift.
Qed.
Fact tRen_up {n m} (r : fintype.fin m -> fintype.fin n) x : x < w * S m -> tRen (upRen_ntype_ntype r) x = iterLift w (tRen r) x.
Proof. intro. unfold tRen. destruct (le_lt_dec (w * S m) x). lia. clear H. unfold nat2fins.
destruct (nat2fins' l) as [i [j H]]. rewrite <- H. destruct j; simpl.
- unfold axioms.funcomp. change Datatypes.Some with (@fintype.shift m) in *. repeat rewrite fs2nS.
erewrite iterL_ge. 2: lia. rewrite minus_plus. destruct (le_lt_dec (w * m) (fins2nat i f)).
{exfalso. pose (fins2nat_lt i f). lia. } rewrite <- iter_unfold. destruct (nat2fins' l0) as [i' [j' H']].
now destruct (fins2nat_eq H') as [-> ->].
- erewrite iterL_lt. auto. apply (@fins2nat_0lt _ m).
Qed.
Fact shifts_ren {n m m'} {t:Vector.t (@ntype w m) n} (r : fintype.fin m -> fintype.fin m')
(Hv:Vector.Forall (fun n : ntype m => forall (n0 : fin) (r : fintype.fin m -> fintype.fin n0), ntranslation (ren_ntype r n) = (ntranslation n) ⟨tRen r⟩) t) :
addShiftings 0 (Vector.map ntranslation (Vector.map (ren_ntype r) t)) = renBounds (tRen r) (addShiftings 0 (Vector.map ntranslation t)).
Proof. apply ext_nth'. intro. destruct (fin2nat' i) as [x [Hx <-]].
rewrite nth'_renBounds. repeat rewrite nth'_addShiftings'. rewrite Vector.map_map. repeat rewrite nth'_map.
rewrite Nat.add_0_r. rewrite iter_unfold. asimpl. edestruct (@Forall_nth' (@ntype w m)
(fun t => ren_type (fun i : fin => x + i) (ntranslation (ren_ntype r t))=ren_type ((fun i : fin => x + i) >> iterLift x (tRen r)) (ntranslation t))).
apply H. clear H H0. revert Hv. eapply Vector.Forall_impl. intros. rewrite H.
asimpl. apply ext_trans. intros. unfold funcomp. rewrite iterL_ge. 2: apply Nat.le_add_r.
rewrite minus_plus. now rewrite <- iter_unfold'.
Qed.
Fact trans_ren : forall m,
(forall (t: @ptype w m) n (r: fintype.fin m -> fintype.fin n),
ptranslation (ren_ptype r t) = ren_type (tRen r) (ptranslation t))
/\ (forall (t: @ntype w m) n (r: fintype.fin m -> fintype.fin n),
ntranslation (ren_ntype r t) = ren_type (tRen r) (ntranslation t)).
Proof. eapply ptype_ntype_mutind; intros; simpl. auto.
-rewrite ren_Bnd. apply congr_mkBounded.
+apply shifts_ren,H0.
+rewrite H. apply ext_trans, tRen_up.
-asimpl. now rewrite tRen_char.
-rewrite ren_Ubnd. apply congr_mkUnbounded. rewrite H. apply ext_trans,tRen_up.
Qed.
Fact ntransUp {m} (t: @ntype w m) : ntranslation (ren_ntype fintype.shift t) = ren_type (iterShift w) (ntranslation t).
Proof. destruct (trans_ren m). rewrite H0. apply ext_trans. rewrite iter_unfold.
intros. unfold tRen. destruct (le_lt_dec (w * m) x). lia. clear H H0 H1.
revert l. generalize m. induction m0. lia.
intro. unfold nat2fins. destruct (nat2fins' l) as [i [j H]].
rewrite fs2nS. now rewrite H.
Qed.
Fact cons_comp {X} {x:X} f (g : X->X) : g x .: (f >> g) = (x.:f) >> g.
Proof. now asimpl. Qed.
Fixpoint foldAdd {n} (v : Vector.t type0 n) (Γ : list type0) {struct v} : list type0.
Proof. destruct v. exact Γ. apply (foldAdd _ v (map (ren_type ↑) (h :: Γ))). Defined.
Fact length_foldAdd {n Γ} {v : Vector.t type0 n} : length (foldAdd v Γ) = n + length Γ.
Proof. revert Γ. induction v; intro; simpl. auto. rewrite IHv. simpl. rewrite map_length. now rewrite Nat.add_succ_r.
Qed.
Fixpoint foldAdd_ge {l d} {v : Vector.t type0 l} {Γ : list type0} {i : unscoped.fin} : l<=i ->
nth i (foldAdd v Γ) d = nth (i-l) (map (ren_type (iterShift l)) Γ) d.
Proof. destruct v; intros; simpl. change (fun t : fin => t) with (@id fin). asimpl. now rewrite <- minus_n_O,map_id.
destruct i. lia. simpl. rewrite foldAdd_ge. 2: lia. assert (S i-n=S (i-n)). lia. rewrite H0. simpl.
rewrite map_map. assert (forall {A x d1} {l1 l2 : list A}, l1 =l2 -> nth x l1 d1 = nth x l2 d1) by congruence.
eapply H1. apply map_ext. intro. rewrite iterShiftLR. erewrite compRenRen_type; eauto.
Qed.
Fixpoint foldAdd_lt {l d} {v : Vector.t type0 l} {Γ : list type0} {i : unscoped.fin} (H:i<l) :
nth i (foldAdd v Γ) d = ren_type (iterShift (S i)) (nth (l-S i) (to_list v) d).
Proof. induction v. lia. simpl foldAdd. destruct (le_lt_dec n i).
-rewrite (foldAdd_ge l). assert (i=n). lia. rewrite H0. repeat rewrite Nat.sub_diag. rewrite <- map_cons.
rewrite map_map. change (to_list (h::v)) with (cons h (to_list v)). simpl.
erewrite compRenRen_type; eauto. intro. unfold funcomp. rewrite iter_unfold'.
change ↑ with S. apply Nat.add_succ_r.
-rewrite (foldAdd_lt _ _ _ _ _ l). rewrite Nat.sub_succ_l. 2:lia.
change (to_list (h::v)) with (cons h (to_list v)). now simpl.
Qed.
Fact congr_NORM `{arrow_flag} : forall Γ Γ' s s' t t', Γ=Γ' -> s=s' -> t=t' -> Γ |-N s <: t -> Γ' |-N s'<: t'.
Proof. congruence. Qed.
Fact comp_assoc {A B C D} {f:A->B} {g:B->C} {h:C->D} : f >> (g >> h) = (f >> g) >> h.
Proof. now fext. Qed.
nth' (addShiftings y v) (nat2nif H) = ren_type (iterShift (l-S x+y)) (nth' v (nat2nif H)).
Proof. revert y. induction v; intro. lia. simpl. destruct (le_lt_dec n x); simpl.
-assert (n-x+y=y). lia. now rewrite H0.
-rewrite (nat2nif_ext _ l). rewrite (IHv l). assert (n-S x+S y=n-x+y). lia. now rewrite H0.
Qed.
Fact nth'_addShiftings' {l x} {v: Vector.t type0 l} (H : x<l) y :
nth' (addShiftings y v) (nat2fin H) = ren_type (iterShift (x+y)) (nth' v (nat2fin H)).
Proof. revert x H y. induction v; intros. lia. destruct x. auto. simpl.
rewrite IHv. now rewrite Nat.add_succ_r.
Qed.
Fact nth_addShiftings {l x y d} {v: Vector.t type0 l} : x<l ->
nth x (to_list (addShiftings y v)) d = ren_type (iterShift (x+y)) (nth x (to_list v) d).
Proof. revert x y. induction v; intros. lia. destruct x. auto.
change (to_list (h::v)) with (cons h (to_list v)). simpl addShiftings.
change (to_list (ren_type (iterShift y) h :: addShiftings (S y) v)) with
(cons (ren_type (iterShift y) h) (to_list (addShiftings (S y) v))).
simpl nth. rewrite IHv. now rewrite Nat.add_succ_r. lia.
Qed.
Fixpoint ptrans_noVar {m i t} : var_type i <> @ptranslation m t.
Proof. destruct t. discriminate. simpl. induction t; simpl; discriminate.
Qed.
Fact mkBnd_noTop {n v b } : syntax.top <> @mkBounded n v b.
Proof. destruct v; discriminate. Qed.
Fact mkUnd_noVar {n i b} : var_type i <> @mkUnbounded n b.
Proof. destruct n; discriminate. Qed.
Fact mkBnd_noVar {n i v b} : var_type i <> @mkBounded n v b.
Proof. destruct v; discriminate. Qed.
Fact congr_mkUnbounded {n s t} : s=t -> mkUnbounded n s = mkUnbounded n t.
Proof. congruence. Qed.
Fact congr_mkBounded {n} {u v : Vector.t type0 n} {s t} : u=v -> s=t -> mkBounded u s = mkBounded v t.
Proof. congruence. Qed.
Fixpoint iterFnShift {m} n (i : fintype.fin m) {struct n} : fintype.fin (n+m).
Proof. destruct n.
-exact i.
-apply (fintype.shift),(iterFnShift _ _ i).
Defined.
Fixpoint iterLift (n : nat) (r : fin->fin) {struct n} : fin-> fin := match n with
| 0 => r
| S n0 => upRen_type_type (iterLift n0 r)
end.
Fixpoint iterPLift (n : nat) {m m'} (r : fintype.fin m ->fintype.fin m') {struct n} : fintype.fin (n+m) ->fintype.fin (n+m').
Proof. destruct n.
-exact r.
-apply upRen_ntype_ntype,(iterPLift _ _ _ r).
Defined.
Fact iterShiftR n (t : type0) : ren_type (iterShift (S n)) t = ren_type ↑ (ren_type (iterShift n) t).
Proof. induction n.
-change (iterShift 0) with (@id fin). asimpl. now simpl.
-simpl in *. change (fun t0 : fin => ↑ (↑ (iterShift n t0))) with ((fun t : fin => ↑ (iterShift n t)) >> ↑).
erewrite <- compRenRen_type; eauto.
Qed.
Fact iterShiftLR n (t: type0) : ren_type (iterShift n) (ren_type ↑ t) = ren_type ↑ (ren_type (iterShift n) t).
Proof. induction n.
-change (iterShift 0) with (@id fin). asimpl. now simpl.
-simpl in *.
change (ren_type (fun t0 : fin => ↑ (iterShift n t0)) (ren_type ↑ t)) with (ren_type (iterShift n >> ↑) (ren_type ↑ t)).
change (ren_type (fun t0 : fin => ↑ (iterShift n t0)) t) with (ren_type (iterShift n >> ↑) t ).
assert (ren_type (iterShift n >> ↑) (ren_type ↑ t)=ren_type ↑ (ren_type (iterShift n) (ren_type ↑ t))).
{ erewrite <- compRenRen_type; try eauto. }
assert (ren_type (iterShift n >> ↑) t = ren_type ↑ (ren_type (iterShift n) t)).
{ erewrite <- compRenRen_type. 2:eauto. auto. }
rewrite H. rewrite IHn. now rewrite H0.
Qed.
Fact iterShiftAdd n m (t:type0) : ren_type (iterShift n) (ren_type (iterShift m) t) = ren_type (iterShift (n+m)) t.
Proof. revert n. induction m; intro.
-change (iterShift 0) with (@id fin). rewrite Nat.add_0_r. now asimpl.
-rewrite iterShiftR. rewrite iterShiftLR. rewrite <- iterShiftR. rewrite IHm. now rewrite Nat.add_succ_r.
Qed.
Fact iterLiftL n r : upRen_type_type (iterLift n r) = iterLift (S n) r.
Proof. auto. Qed.
Fact iterLiftLR n r : (upRen_type_type (iterLift n r)) = iterLift n (upRen_type_type r).
Proof. induction n; auto. simpl. now rewrite IHn. Qed.
Fact iterPnLiftL n {m m'} (r : fintype.fin m ->fintype.fin m') : upRen_ntype_ntype (iterPLift n r) = iterPLift (S n) r.
Proof. auto. Qed.
Fact iter_unfold' n x: iterShift n x = n+x.
Proof. induction n; simpl; [ change (fun i:fin=>i) with (@id fin) | rewrite IHn]; now asimpl.
Qed.
Fact iter_unfold n: iterShift n = fun i=>n+i.
Proof. fext. intro. apply iter_unfold'.
Qed.
Fact shif_lift n (t:type0): ren_type (iterShift (n+w)) t = ren_type (iterShift n >> iterLift n (iterShift w)) t.
Proof. induction n.
-change (iterShift 0) with (@id fin). asimpl. now simpl.
-change (S n+w) with (S (n+w)). rewrite iterShiftR. rewrite IHn.
erewrite compRenRen_type; eauto.
Qed.
Fact ren_Ubnd r n t : ren_type r (mkUnbounded n t) = mkUnbounded n (ren_type (iterLift n r) t).
Proof. revert r. induction n; intro; simpl. auto. apply congr_all. auto. rewrite IHn. now rewrite iterLiftLR. Qed.
Fixpoint renBounds {n} r (v : Vector.t type0 n) : Vector.t type0 n :=
match v in (t _ n0) return (t type0 n0) with
| [] => []
| Vector.cons _ h n0 v0 => ( ren_type r h :: renBounds (upRen_type_type r) v0)%vector
end.
Fact nth'_renBounds {l x} {v: Vector.t type0 l} (H : x<l) r : nth' (renBounds r v) (nat2fin H) = (nth' v (nat2fin H)) ⟨iterLift x r⟩.
Proof. revert x H r. induction v; intros. lia. destruct x. auto.
simpl. rewrite IHv. now rewrite iterLiftLR.
Qed.
Fact ren_Bnd {n} r (v:Vector.t type0 n) i t : ren_type r (mkBounded (addShiftings i v) t) = mkBounded (renBounds r (addShiftings i v)) (ren_type (iterLift n r) t).
Proof. revert r i. induction v; intros; simpl. auto. apply congr_all. auto. rewrite IHv. now rewrite iterLiftLR. Qed.
Definition tRen {n m} (r : fintype.fin n -> fintype.fin m) : fin -> fin.
Proof. intros x. destruct (le_lt_dec (w*n) x). exact x. destruct (nat2fins l) as [i j]. exact (fins2nat i (r j)).
Defined.
Fact aux i j n : i < w -> j < (S n) -> w * (S n) <= j * w + i -> False.
Proof. intro. revert j. induction n; intros.
-assert (j=0). lia. rewrite H2 in H1. simpl in H1. lia.
-revert H1. rewrite (@Nat.mul_comm w). destruct j. lia. simpl. intro. apply (IHn (S j)).
{ destruct (le_lt_dec n j). assert (j=n). lia. rewrite H2 in H1. lia. lia. } lia.
Qed.
Fixpoint tRen_char {n m} (i: fintype.fin w) (j: fintype.fin n) (r : fintype.fin n -> fintype.fin m) {struct n}: tRen r (fins2nat i j) = fins2nat i (r j).
Proof. destruct n. contradiction. unfold tRen. destruct (le_lt_dec (w * S n) (fins2nat i j)).
{exfalso. revert l. unfold fins2nat. destruct (nif2nat i) as [i' [H0 H1]]. destruct (fin2nat' j) as [j' [H2 H3]]. now apply (aux i' j' n). }
now rewrite n2fs_unfold.
Qed.
Fact iterL_ge {r n x} : n<=x -> iterLift n r x = iterShift n (r (x-n)).
Proof. revert x. induction n; intros.
-simpl. now rewrite Nat.sub_0_r.
-destruct x; simpl. lia. unfold funcomp. erewrite IHn. auto. lia.
Qed.
Fact iterL_lt {r n x} : x<n -> iterLift n r x = x.
Proof. revert x. induction n. lia. intros. simpl. asimpl.
destruct x; simpl. auto. asimpl. rewrite IHn; lia.
Qed.
Fact renBounds_shifts {n m r s} {t : Vector.t (@ntype w m) n} (Hrs : forall x, x < w * m -> r x = s x ) :
Vector.Forall (fun n => forall r s, (forall x, x < w * m -> r x = s x) -> (ntranslation n) ⟨r⟩ = (ntranslation n) ⟨s⟩) t->
renBounds r (addShiftings 0 (Vector.map ntranslation t)) = renBounds s (addShiftings 0 (Vector.map ntranslation t)).
Proof. intro. apply ext_nth'. intro. destruct (fin2nat' i) as [x [Hx <-]].
repeat rewrite nth'_renBounds. repeat rewrite nth'_addShiftings'. rewrite nth'_map. rewrite Nat.add_0_r.
rewrite iter_unfold. asimpl. unfold funcomp.
edestruct (@Forall_nth' (@ntype w m)
(fun t => ren_type (fun x0 : fin => iterLift x r (x + x0)) (ntranslation t)=ren_type (fun x0 : fin => iterLift x s (x + x0)) (ntranslation t)) n t).
apply H0. clear H0 H1. revert H. eapply Vector.Forall_impl. intros. apply H.
intros. destruct (le_lt_dec x (x+x0)).
-repeat erewrite iterL_ge; auto. rewrite minus_plus. rewrite Hrs; auto.
-repeat erewrite iterL_lt; auto.
Qed.
Fact ext_lift {m r s} (Hrs : forall x, x < w * m -> r x = s x ) {x} (Hx: x < w * S m): iterLift w r x = iterLift w s x.
Proof. destruct (le_lt_dec w x).
-repeat rewrite (iterL_ge l). repeat rewrite iter_unfold. erewrite Hrs. auto. lia.
-now repeat rewrite (iterL_lt l).
Qed.
Fact ext_trans : forall m,
(forall (t: @ptype w m) r s, (forall x, x<w*m -> r x = s x) -> ren_type r (ptranslation t) = ren_type s (ptranslation t))
/\ (forall (t: @ntype w m) r s, (forall x, x<w*m -> r x = s x) -> ren_type r (ntranslation t) = ren_type s (ntranslation t)).
Proof. eapply ptype_ntype_mutind; intros; simpl. auto.
-repeat rewrite ren_Bnd. apply congr_mkBounded. apply renBounds_shifts,H0. exact H1. apply H. now apply ext_lift.
-asimpl. now rewrite (H _ (fins2nat_lt t t0)).
-repeat rewrite ren_Ubnd. apply congr_mkUnbounded. apply H. now apply ext_lift.
Qed.
Fact tRen_up {n m} (r : fintype.fin m -> fintype.fin n) x : x < w * S m -> tRen (upRen_ntype_ntype r) x = iterLift w (tRen r) x.
Proof. intro. unfold tRen. destruct (le_lt_dec (w * S m) x). lia. clear H. unfold nat2fins.
destruct (nat2fins' l) as [i [j H]]. rewrite <- H. destruct j; simpl.
- unfold axioms.funcomp. change Datatypes.Some with (@fintype.shift m) in *. repeat rewrite fs2nS.
erewrite iterL_ge. 2: lia. rewrite minus_plus. destruct (le_lt_dec (w * m) (fins2nat i f)).
{exfalso. pose (fins2nat_lt i f). lia. } rewrite <- iter_unfold. destruct (nat2fins' l0) as [i' [j' H']].
now destruct (fins2nat_eq H') as [-> ->].
- erewrite iterL_lt. auto. apply (@fins2nat_0lt _ m).
Qed.
Fact shifts_ren {n m m'} {t:Vector.t (@ntype w m) n} (r : fintype.fin m -> fintype.fin m')
(Hv:Vector.Forall (fun n : ntype m => forall (n0 : fin) (r : fintype.fin m -> fintype.fin n0), ntranslation (ren_ntype r n) = (ntranslation n) ⟨tRen r⟩) t) :
addShiftings 0 (Vector.map ntranslation (Vector.map (ren_ntype r) t)) = renBounds (tRen r) (addShiftings 0 (Vector.map ntranslation t)).
Proof. apply ext_nth'. intro. destruct (fin2nat' i) as [x [Hx <-]].
rewrite nth'_renBounds. repeat rewrite nth'_addShiftings'. rewrite Vector.map_map. repeat rewrite nth'_map.
rewrite Nat.add_0_r. rewrite iter_unfold. asimpl. edestruct (@Forall_nth' (@ntype w m)
(fun t => ren_type (fun i : fin => x + i) (ntranslation (ren_ntype r t))=ren_type ((fun i : fin => x + i) >> iterLift x (tRen r)) (ntranslation t))).
apply H. clear H H0. revert Hv. eapply Vector.Forall_impl. intros. rewrite H.
asimpl. apply ext_trans. intros. unfold funcomp. rewrite iterL_ge. 2: apply Nat.le_add_r.
rewrite minus_plus. now rewrite <- iter_unfold'.
Qed.
Fact trans_ren : forall m,
(forall (t: @ptype w m) n (r: fintype.fin m -> fintype.fin n),
ptranslation (ren_ptype r t) = ren_type (tRen r) (ptranslation t))
/\ (forall (t: @ntype w m) n (r: fintype.fin m -> fintype.fin n),
ntranslation (ren_ntype r t) = ren_type (tRen r) (ntranslation t)).
Proof. eapply ptype_ntype_mutind; intros; simpl. auto.
-rewrite ren_Bnd. apply congr_mkBounded.
+apply shifts_ren,H0.
+rewrite H. apply ext_trans, tRen_up.
-asimpl. now rewrite tRen_char.
-rewrite ren_Ubnd. apply congr_mkUnbounded. rewrite H. apply ext_trans,tRen_up.
Qed.
Fact ntransUp {m} (t: @ntype w m) : ntranslation (ren_ntype fintype.shift t) = ren_type (iterShift w) (ntranslation t).
Proof. destruct (trans_ren m). rewrite H0. apply ext_trans. rewrite iter_unfold.
intros. unfold tRen. destruct (le_lt_dec (w * m) x). lia. clear H H0 H1.
revert l. generalize m. induction m0. lia.
intro. unfold nat2fins. destruct (nat2fins' l) as [i [j H]].
rewrite fs2nS. now rewrite H.
Qed.
Fact cons_comp {X} {x:X} f (g : X->X) : g x .: (f >> g) = (x.:f) >> g.
Proof. now asimpl. Qed.
Fixpoint foldAdd {n} (v : Vector.t type0 n) (Γ : list type0) {struct v} : list type0.
Proof. destruct v. exact Γ. apply (foldAdd _ v (map (ren_type ↑) (h :: Γ))). Defined.
Fact length_foldAdd {n Γ} {v : Vector.t type0 n} : length (foldAdd v Γ) = n + length Γ.
Proof. revert Γ. induction v; intro; simpl. auto. rewrite IHv. simpl. rewrite map_length. now rewrite Nat.add_succ_r.
Qed.
Fixpoint foldAdd_ge {l d} {v : Vector.t type0 l} {Γ : list type0} {i : unscoped.fin} : l<=i ->
nth i (foldAdd v Γ) d = nth (i-l) (map (ren_type (iterShift l)) Γ) d.
Proof. destruct v; intros; simpl. change (fun t : fin => t) with (@id fin). asimpl. now rewrite <- minus_n_O,map_id.
destruct i. lia. simpl. rewrite foldAdd_ge. 2: lia. assert (S i-n=S (i-n)). lia. rewrite H0. simpl.
rewrite map_map. assert (forall {A x d1} {l1 l2 : list A}, l1 =l2 -> nth x l1 d1 = nth x l2 d1) by congruence.
eapply H1. apply map_ext. intro. rewrite iterShiftLR. erewrite compRenRen_type; eauto.
Qed.
Fixpoint foldAdd_lt {l d} {v : Vector.t type0 l} {Γ : list type0} {i : unscoped.fin} (H:i<l) :
nth i (foldAdd v Γ) d = ren_type (iterShift (S i)) (nth (l-S i) (to_list v) d).
Proof. induction v. lia. simpl foldAdd. destruct (le_lt_dec n i).
-rewrite (foldAdd_ge l). assert (i=n). lia. rewrite H0. repeat rewrite Nat.sub_diag. rewrite <- map_cons.
rewrite map_map. change (to_list (h::v)) with (cons h (to_list v)). simpl.
erewrite compRenRen_type; eauto. intro. unfold funcomp. rewrite iter_unfold'.
change ↑ with S. apply Nat.add_succ_r.
-rewrite (foldAdd_lt _ _ _ _ _ l). rewrite Nat.sub_succ_l. 2:lia.
change (to_list (h::v)) with (cons h (to_list v)). now simpl.
Qed.
Fact congr_NORM `{arrow_flag} : forall Γ Γ' s s' t t', Γ=Γ' -> s=s' -> t=t' -> Γ |-N s <: t -> Γ' |-N s'<: t'.
Proof. congruence. Qed.
Fact comp_assoc {A B C D} {f:A->B} {g:B->C} {h:C->D} : f >> (g >> h) = (f >> g) >> h.
Proof. now fext. Qed.
Fixpoint mkCtx {m} (Γ : @ctx w m) : list type0.
Proof. destruct Γ. exact nil. apply (map (ren_type (iterShift w))). apply Datatypes.app.
-eapply rev,to_list,(Vector.map ntranslation),t.
-eapply mkCtx,Γ.
Defined.
Fact length_mkCtx {m} (Γ : @ctx w m) : length (mkCtx Γ) = m*w.
Proof. induction Γ; simpl. auto. rewrite map_length. rewrite app_length. rewrite rev_length.
rewrite length_to_list. change (@type' arrow_off) with type0. now rewrite IHΓ.
Qed.
Fact mkCtx_eq {m i j} {Γ : @ctx w m} : nth_default (var_type (fins2nat i j)) (mkCtx Γ) (fins2nat i j) = ntranslation (ctx_at Γ i j).
Proof. induction Γ. contradiction. destruct j.
-change (Datatypes.Some f) with (fintype.shift f). rewrite fs2nS. simpl.
rewrite map_app. rewrite nth_default_eq. rewrite app_nth2.
assert (length (list_map (@ren_type arrow_off (iterShift w))
(@rev (@type' arrow_off) (@to_list (@type' arrow_off) w
(@Vector.map (@ntype w m) type0 (@ntranslation m) w t)))) = w) as ->.
{ rewrite map_length. rewrite rev_length. now rewrite length_to_list. }
assert (w + fins2nat i f - w = fins2nat i f) as ->. lia.
assert (@var_type arrow_off (w + fins2nat i f) = ren_type (iterShift w) (var_type (fins2nat i f))) as -> by reflexivity.
rewrite map_nth. rewrite <- nth_default_eq. rewrite IHΓ. now rewrite ntransUp.
rewrite map_length. rewrite rev_length. rewrite length_to_list. lia.
-simpl. unfold fins2nat. destruct (nif2nat i) as [x [Hxw Hi]]. simpl. rewrite nth_default_eq.
rewrite map_app. rewrite app_nth1. erewrite nth_indep'. rewrite to_list_map.
rewrite rev_nth. erewrite nth_indep'. rewrite ntransUp.
erewrite nth_nth'. now rewrite <- Hi.
rewrite map_length. now rewrite length_to_list.
rewrite map_length. rewrite length_to_list. lia.
rewrite map_length. now rewrite length_to_list.
rewrite rev_length. now rewrite length_to_list.
rewrite map_length. rewrite rev_length. now rewrite length_to_list.
Unshelve. exact top. apply uAllN. exact psyntax.top.
Qed.
Reduction
The proof is split in two general cases, namely when w=0 and when w>0.Fact load {l} {Γ} {t1 : Vector.t type0 l} {s t2}: foldAdd t1 Γ |-N t2 <: s ->
Γ |-N mkUnbounded l s <: mkBounded t1 t2.
Proof. revert Γ s t2. induction t1; simpl; intros.
-now apply flipNeg.
-apply NAll. apply NTop. now apply IHt1.
Qed.
Lemma d2n {m} (Γ :@ctx w m) s t : (exists h, Γ |-D h; s <: t) ->
mkCtx Γ |-N ntranslation s <: ptranslation t.
Proof. intros [h H]. induction H; simpl; try constructor. now rewrite mkCtx_eq.
apply load. revert IHsubD. apply congr_NORM; auto.
simpl. rewrite map_app. eapply nth_ext.
-rewrite app_length. repeat rewrite map_length. now rewrite rev_length, length_to_list, length_foldAdd.
-rewrite app_length. repeat rewrite map_length. rewrite rev_length,length_to_list,length_mkCtx.
intros. destruct (le_lt_dec w n).
+erewrite app_nth2. rewrite map_length, rev_length, length_to_list. now rewrite (foldAdd_ge l).
now rewrite map_length,rev_length,length_to_list.
+erewrite app_nth1. erewrite map_nth, rev_nth, length_to_list. rewrite (foldAdd_lt l).
rewrite nth_addShiftings, iterShiftAdd. assert (S n + (w-S n+0)=w) as -> by lia.
erewrite nth_indep. eauto. rewrite length_to_list. lia. lia. rewrite length_to_list. lia.
now rewrite map_length,rev_length,length_to_list. Unshelve. exact top.
Qed.
at this point we need the height of the derivations in the Normal System
height indexed system
Reserved Notation "Γ '|-IN' i ; s <: t" (at level 68, i, s, t at next level).
Inductive iSub : forall {b:arrow_flag}, (list (@type' b)) -> nat -> @type' b -> @type' b-> Prop:=
| iTop {b: arrow_flag} Γ s : Γ |-IN 0; s <: syntax.top
| iRefl {b: arrow_flag} Γ n : Γ |-IN 0; var_type n <: var_type n
| iVar {b: arrow_flag} Γ s n i : Γ |-IN i; nth_default (var_type n) Γ n <: s -> Γ |-IN (S i); var_type n <: s
| iArr Γ {s1 s2 t1 t2 i} j : Γ |-IN j; t1 <: s1 -> Γ |-IN i; s2 <: t2 ->
Γ |-IN (S (max i j)); (arr s1 s2) <: (arr t1 t2)
| iAll {b: arrow_flag} Γ {s1 s2 t1 t2 i} j : Γ |-IN j; t1 <: s1 -> map (ren_type ↑) (cons t1 Γ) |-IN i; s2 <: t2 ->
Γ |-IN (S (max i j)); (all s1 s2) <: (all t1 t2)
where "Γ '|-IN' i ; s <: t" := (iSub Γ i s t).
Derive Signature for iSub.
Fact norm_in `{arrow_flag} {Γ} {s t} : Γ |-N s <: t -> exists i, Γ |-IN i; s <: t.
Proof. induction 1. 1,3: exists 0. constructor. constructor.
-destruct IHsubN. exists (S x). now constructor.
-destruct IHsubN1. destruct IHsubN2. exists (S (max x0 x)). now apply iArr.
-destruct IHsubN1. destruct IHsubN2. exists (S (max x0 x)). now apply iAll.
Qed.
Fact in_norm `{arrow_flag} {Γ s t i} : Γ |-IN i; s <: t -> Γ |-N s <: t.
Proof. induction 1; now constructor. Qed.
Fact congr_IN `{arrow_flag} {i0 i1 Γ0 Γ1 s0 s1 t0 t1} : i0=i1 -> Γ0=Γ1 -> s0=s1 -> t0=t1 ->
Γ0 |-IN i0; s0 <: t0 -> Γ1 |-IN i1; s1 <: t1.
Proof. congruence. Qed.
Fact in_load {Γ n p s i} {t : Vector.t type0 n} : Γ |-IN i; mkUnbounded n p <: mkBounded t s ->
exists j, foldAdd t Γ |-IN j; s <: p /\ j<i.
Proof. revert i Γ. induction t; simpl; intros.
-unfold neg in H. depind H; try discriminate.
exists j. split. 2:apply le_lt_n_Sm,Nat.le_max_r.
destruct (all_inj H1) as [-> _]. destruct (all_inj H2) as [-> _]. auto.
-depind H; try discriminate. clear IHiSub1 IHiSub2.
destruct (all_inj H1). destruct (all_inj H2).
rewrite <- H4 in H0. rewrite <- H6 in H0. destruct (IHt _ _ H0) as [j' [Hj' Hji]].
exists j'. split. now rewrite H5. apply (Nat.lt_trans _ i _ Hji),le_lt_n_Sm,Nat.le_max_l.
Qed.
Inductive iSub : forall {b:arrow_flag}, (list (@type' b)) -> nat -> @type' b -> @type' b-> Prop:=
| iTop {b: arrow_flag} Γ s : Γ |-IN 0; s <: syntax.top
| iRefl {b: arrow_flag} Γ n : Γ |-IN 0; var_type n <: var_type n
| iVar {b: arrow_flag} Γ s n i : Γ |-IN i; nth_default (var_type n) Γ n <: s -> Γ |-IN (S i); var_type n <: s
| iArr Γ {s1 s2 t1 t2 i} j : Γ |-IN j; t1 <: s1 -> Γ |-IN i; s2 <: t2 ->
Γ |-IN (S (max i j)); (arr s1 s2) <: (arr t1 t2)
| iAll {b: arrow_flag} Γ {s1 s2 t1 t2 i} j : Γ |-IN j; t1 <: s1 -> map (ren_type ↑) (cons t1 Γ) |-IN i; s2 <: t2 ->
Γ |-IN (S (max i j)); (all s1 s2) <: (all t1 t2)
where "Γ '|-IN' i ; s <: t" := (iSub Γ i s t).
Derive Signature for iSub.
Fact norm_in `{arrow_flag} {Γ} {s t} : Γ |-N s <: t -> exists i, Γ |-IN i; s <: t.
Proof. induction 1. 1,3: exists 0. constructor. constructor.
-destruct IHsubN. exists (S x). now constructor.
-destruct IHsubN1. destruct IHsubN2. exists (S (max x0 x)). now apply iArr.
-destruct IHsubN1. destruct IHsubN2. exists (S (max x0 x)). now apply iAll.
Qed.
Fact in_norm `{arrow_flag} {Γ s t i} : Γ |-IN i; s <: t -> Γ |-N s <: t.
Proof. induction 1; now constructor. Qed.
Fact congr_IN `{arrow_flag} {i0 i1 Γ0 Γ1 s0 s1 t0 t1} : i0=i1 -> Γ0=Γ1 -> s0=s1 -> t0=t1 ->
Γ0 |-IN i0; s0 <: t0 -> Γ1 |-IN i1; s1 <: t1.
Proof. congruence. Qed.
Fact in_load {Γ n p s i} {t : Vector.t type0 n} : Γ |-IN i; mkUnbounded n p <: mkBounded t s ->
exists j, foldAdd t Γ |-IN j; s <: p /\ j<i.
Proof. revert i Γ. induction t; simpl; intros.
-unfold neg in H. depind H; try discriminate.
exists j. split. 2:apply le_lt_n_Sm,Nat.le_max_r.
destruct (all_inj H1) as [-> _]. destruct (all_inj H2) as [-> _]. auto.
-depind H; try discriminate. clear IHiSub1 IHiSub2.
destruct (all_inj H1). destruct (all_inj H2).
rewrite <- H4 in H0. rewrite <- H6 in H0. destruct (IHt _ _ H0) as [j' [Hj' Hji]].
exists j'. split. now rewrite H5. apply (Nat.lt_trans _ i _ Hji),le_lt_n_Sm,Nat.le_max_l.
Qed.
Lemma n2d {m} (Γ :@ctx w m) s t : mkCtx Γ |-N ntranslation s <: ptranslation t
-> exists h, Γ |-D h; s <: t.
Proof. intro. destruct (norm_in H) as [n Hin]. clear H.
revert m Γ s t Hin. induction n using Wf_nat.lt_wf_ind; intros.
destruct t. eexists. constructor. destruct s.
-simpl ntranslation in Hin. inversion Hin. apply DPI in H5. exfalso. apply (mkBnd_noTop H5).
apply DPI in H5. exfalso. apply (mkBnd_noVar H5).
assert (Hn : i<n). rewrite <- H3. auto. edestruct (H i Hn _ Γ (ctx_at Γ f f0) (bAllN t n0)).
simpl. rewrite <- (DPI H0). rewrite <- (DPI H4). revert H5. apply congr_IN; auto.
rewrite (DPI H0). now erewrite mkCtx_eq.
exists (S x). now apply DVar.
-simpl in *. destruct (in_load Hin) as [j [Hj Hji]]. edestruct (H j Hji).
2: { exists (S x). apply DAllNeg. exact H0. } revert Hj. apply congr_IN; auto.
simpl. rewrite map_app. eapply nth_ext.
{ rewrite length_foldAdd,app_length. repeat rewrite map_length. now rewrite rev_length,length_to_list. }
rewrite length_foldAdd, length_mkCtx. intros. destruct (le_lt_dec w n1).
+rewrite (foldAdd_ge l),app_nth2,map_length,rev_length,length_to_list. auto.
rewrite map_length,rev_length,length_to_list. auto.
+rewrite (foldAdd_lt l),app_nth1,nth_addShiftings,iterShiftAdd,map_rev,rev_nth.
erewrite map_nth. assert (S n1 + (w - S n1 + 0)=w) as -> by lia.
rewrite map_length,length_to_list. erewrite nth_indep. eauto.
rewrite length_to_list. lia. now rewrite map_length,length_to_list. lia.
now rewrite map_length,rev_length,length_to_list.
Unshelve. exact top.
Qed.
End argument.
For w=0 the polarized syntax collapses, there are no variables and quantifiers bind nothing, therefore the translation are Top flipped any number of times.
The reduction is trivial.
Section argument0.
Lemma d2n0 {m} (Γ :@ctx 0 m) s t : (exists h, Γ |-D h; s<:t) ->
mkCtx Γ |-N ntranslation s <: ptranslation t.
Proof. intros [h H]. induction H. constructor. contradiction. rewrite (isNil t1). unfold ptranslation. unfold ntranslation. simpl.
apply flipNeg. revert IHsubD. simpl. change (fun t : fin => t) with (@id fin). asimpl. apply congr_NORM; auto.
rewrite map_id. rewrite (isNil t1). now simpl.
Qed.
Lemma n2d0 {m} (Γ :@ctx 0 m) s t : mkCtx Γ |-N ntranslation s <: ptranslation t ->
(exists h, Γ |-D h; s<:t).
Proof. intro. destruct (norm_in H) as [i Hin]. clear H.
revert m Γ s t Hin. induction i using Wf_nat.lt_wf_ind; intros.
destruct t. eexists. constructor. destruct s. contradiction. revert Hin.
unfold ntranslation. unfold ptranslation. rewrite (isNil t). simpl. unfold neg.
intro. inversion Hin. edestruct (H j). rewrite <- H4. apply le_lt_n_Sm,Nat.le_max_r.
2: { exists (S x). apply DAllNeg. exact H9. }
revert H6. apply congr_IN. auto. simpl. asimpl. rewrite map_id. now rewrite (DPI H0).
now rewrite (DPI H5). now rewrite (DPI H1).
Qed.
End argument0.
Lemma d2n0 {m} (Γ :@ctx 0 m) s t : (exists h, Γ |-D h; s<:t) ->
mkCtx Γ |-N ntranslation s <: ptranslation t.
Proof. intros [h H]. induction H. constructor. contradiction. rewrite (isNil t1). unfold ptranslation. unfold ntranslation. simpl.
apply flipNeg. revert IHsubD. simpl. change (fun t : fin => t) with (@id fin). asimpl. apply congr_NORM; auto.
rewrite map_id. rewrite (isNil t1). now simpl.
Qed.
Lemma n2d0 {m} (Γ :@ctx 0 m) s t : mkCtx Γ |-N ntranslation s <: ptranslation t ->
(exists h, Γ |-D h; s<:t).
Proof. intro. destruct (norm_in H) as [i Hin]. clear H.
revert m Γ s t Hin. induction i using Wf_nat.lt_wf_ind; intros.
destruct t. eexists. constructor. destruct s. contradiction. revert Hin.
unfold ntranslation. unfold ptranslation. rewrite (isNil t). simpl. unfold neg.
intro. inversion Hin. edestruct (H j). rewrite <- H4. apply le_lt_n_Sm,Nat.le_max_r.
2: { exists (S x). apply DAllNeg. exact H9. }
revert H6. apply congr_IN. auto. simpl. asimpl. rewrite map_id. now rewrite (DPI H0).
now rewrite (DPI H5). now rewrite (DPI H1).
Qed.
End argument0.
Require Import Undecidability.Synthetic.Definitions.
Definition translation : {w : fin & {m : fin & (@ctx w m * (@ntype w m * @ptype w m))%type}} ->
(@FsubN.ctx arrow_off * (type0 * type0))%type.
Proof. intros [w [m [Γ [s t]]]]. split. exact (mkCtx Γ). split.
exact (ntranslation s). exact (ptranslation t).
Defined.
Theorem reduction : FsubD_SUBTYPE ⪯ FsubN_off_SUBTYPE.
Proof.
exists translation.
unfold FsubN_SUBTYPE. intros [[|w] [m [Γ [s t]]]]; cbn.
-split; [ apply d2n0 | apply n2d0].
-split; [ apply d2n | apply n2d]; apply Nat.lt_0_succ.
Qed.
Definition translation : {w : fin & {m : fin & (@ctx w m * (@ntype w m * @ptype w m))%type}} ->
(@FsubN.ctx arrow_off * (type0 * type0))%type.
Proof. intros [w [m [Γ [s t]]]]. split. exact (mkCtx Γ). split.
exact (ntranslation s). exact (ptranslation t).
Defined.
Theorem reduction : FsubD_SUBTYPE ⪯ FsubN_off_SUBTYPE.
Proof.
exists translation.
unfold FsubN_SUBTYPE. intros [[|w] [m [Γ [s t]]]]; cbn.
-split; [ apply d2n0 | apply n2d0].
-split; [ apply d2n | apply n2d]; apply Nat.lt_0_succ.
Qed.