## POPLMark 1a solution

Original development by Rafaël Bocquet: POPLmark part 1A with inductive definition of scope and well-scoped variables (and terms, types and environments).

Require Import Program.
From Equations Require Import Equations.
Require Import Coq.Classes.EquivDec.
Require Import Arith.

Definition scope := nat.
Inductive var : scope Set :=
| FO : {n}, var (S n)
| FS : {n}, var n var (S n)
.
Derive Signature NoConfusion NoConfusionHom for var.

Inductive scope_le : scope scope Set :=
(* We use an equality in the constructor here to avoid requiring UIP on nat. *)
| scope_le_n : {n m}, n = m scope_le n m
| scope_le_S : {n m}, scope_le n m scope_le n (S m)
| scope_le_map : {n m}, scope_le n m scope_le (S n) (S m).

Derive Signature NoConfusion NoConfusionHom Subterm for scope_le.

Equations scope_le_app {a b c} (p : scope_le a b) (q : scope_le b c) : scope_le a c :=
(* by wf (signature_pack q) scope_le_subterm := *)
scope_le_app p (scope_le_n eq_refl) := p;
scope_le_app p (scope_le_S q) := scope_le_S (scope_le_app p q);
scope_le_app p (scope_le_map q) with p :=
{ | scope_le_n eq_refl := scope_le_map q;
| scope_le_S p' := scope_le_S (scope_le_app p' q);
| (scope_le_map p') := scope_le_map (scope_le_app p' q) }.
(* Proof. all:repeat constructor. Defined. *)

Lemma scope_le_app_len n m (q : scope_le n m) : scope_le_app (scope_le_n eq_refl) q = q.
Proof.
depind q; simp scope_le_app; trivial. destruct e; reflexivity. now rewrite IHq.
Qed.
#[local] Hint Rewrite scope_le_app_len : scope_le_app.

Inductive type : scope Type :=
| tvar : {n}, var n type n
| ttop : {n}, type n
| tarr : {n}, type n type n type n
| tall : {n}, type n type (S n) type n
.
Derive Signature NoConfusion NoConfusionHom for type.

Inductive env : scope scope Set :=
| empty : {n m}, n = m env n m
| cons : {n m}, type m env n m env n (S m)
.
Derive Signature NoConfusion NoConfusionHom for env.

Lemma env_scope_le : {n m}, env n m scope_le n m.
Proof. intros n m Γ; depind Γ. constructor; auto. constructor 2; auto. Defined.

Equations env_app {a b c} (Γ : env a b) (Δ : env b c) : env a c :=
env_app Γ (empty eq_refl) := Γ;
env_app Γ (cons t Δ) := cons t (env_app Γ Δ).

Lemma cons_app : {a b c} (Γ : env a b) (Δ : env b c) t, cons t (env_app Γ Δ) = env_app Γ (cons t Δ).
Proof. intros. autorewrite with env_app. reflexivity. Qed.
#[local] Hint Rewrite @cons_app.

Equations map_var {n m} (f : var n var m) (t : var (S n)) : var (S m) :=
map_var f FO := FO;
map_var f (FS x) := FS (f x).

Lemma map_var_a : {n m o} f g a, @map_var n o (fun tf (g t)) a = @map_var m o f (@map_var n m g a).
Proof. depind a; autorewrite with map_var; auto. Qed.

Lemma map_var_b : {n m} (f g : var n var m), ( x, f x = g x)
a, map_var f a = map_var g a.
Proof. depind a; autorewrite with map_var; try f_equal; auto. Qed.

Equations lift_var_by {n m} (p : scope_le n m) : var n var m :=
lift_var_by (scope_le_n eq_refl) := fun tt;
lift_var_by (scope_le_S p) := fun tFS (lift_var_by p t);
lift_var_by (scope_le_map p) := map_var (lift_var_by p).

Equations lift_type_by {n m} (f : scope_le n m) (t : type n) : type m :=
lift_type_by f (tvar x) := tvar (lift_var_by f x);
lift_type_by f ttop := ttop;
lift_type_by f (tarr a b) := tarr (lift_type_by f a) (lift_type_by f b);
lift_type_by f (tall a b) := tall (lift_type_by f a) (lift_type_by (scope_le_map f) b).

Lemma lift_var_by_app : {b c} (p : scope_le b c) {a} (q : scope_le a b) t,
lift_var_by p (lift_var_by q t) = lift_var_by (scope_le_app q p) t.
Proof with autorewrite with lift_var_by map_var scope_le_app in *; auto.
intros b c p; induction p; intros a q t; try destruct e...
- rewrite IHp; auto.
- generalize dependent p. generalize dependent t.
depind q; subst; intros...
rewrite IHp...
specialize (IHp _ q).
rewrite (map_var_b (lift_var_by (scope_le_app q p)) (fun tlift_var_by p (lift_var_by q t))); eauto.
rewrite <- map_var_a; auto.
Qed.
#[local] Hint Rewrite @lift_var_by_app : lift_var_by.

Lemma lift_type_by_id : {n} (t : type n) P, ( x, lift_var_by P x = x) lift_type_by P t = t.
Proof.
depind t; intros; autorewrite with lift_type_by; rewrite ?H, ?IHt1, ?IHt2; auto.
intros; depelim x; autorewrite with lift_var_by map_var; try f_equal; auto.
Qed.

Lemma lift_type_by_n : {n} (t : type n), lift_type_by (scope_le_n eq_refl) t = t.
Proof. intros; eapply lift_type_by_id; intros; autorewrite with lift_var_by; auto. Qed.
#[local] Hint Rewrite @lift_type_by_n : lift_type_by.

Lemma lift_type_by_app : {a} t {b c} (p : scope_le b c) (q : scope_le a b),
lift_type_by p (lift_type_by q t) = lift_type_by (scope_le_app q p) t.
Proof.
depind t; intros b c p; depind p; intros q;
repeat (autorewrite with scope_le_app lift_var_by lift_type_by;
rewrite ?IHt1, ?IHt2; auto).
Qed.
#[local] Hint Rewrite @lift_type_by_app : lift_type_by.

Equations lookup {n} (Γ : env O n) (x : var n) : type n :=
lookup (n:=(S _)) (cons a Γ) FO := lift_type_by (scope_le_S (scope_le_n eq_refl)) a;
lookup (n:=(S _)) (cons a Γ) (FS x) := lift_type_by (scope_le_S (scope_le_n eq_refl)) (lookup Γ x)
.

Lemma lookup_app {n} (Γ : env O (S n)) {m} (Δ : env (S n) (S m)) x :
lookup (env_app Γ Δ) (lift_var_by (env_scope_le Δ) x) =
lift_type_by (env_scope_le Δ) (lookup Γ x).
Proof with autorewrite with lookup scope_le_app env_app lift_var_by lift_type_by; auto.
induction Δ; subst; simpl...
rewrite IHΔ...
Qed.
#[local] Hint Rewrite @lookup_app : lookup.

The subtyping judgment

Inductive sa : {n}, env O n type n type n Prop :=
| sa_top : {n} (Γ : env O n) s, sa Γ s ttop
| sa_var_refl : {n} (Γ : env O n) x, sa Γ (tvar x) (tvar x)
| sa_var_trans : {n} (Γ : env O (S n)) x t,
sa Γ (lookup Γ x) t
sa Γ (tvar x) t
| sa_arr : {n} {Γ : env O n} {t1 t2 s1 s2},
sa Γ t1 s1
sa Γ s2 t2
sa Γ (tarr s1 s2) (tarr t1 t2)
| sa_all : {n} {Γ : env O n} {t1 t2 s1 s2},
sa Γ t1 s1
sa (cons t1 Γ) s2 t2
sa Γ (tall s1 s2) (tall t1 t2)
.
Derive Signature for sa.

Inductive sa_env : {n}, env O n env O n Prop :=
| sa_empty : sa_env (empty eq_refl) (empty eq_refl)
| sa_cons : {n} (Γ Δ : env O n) a b,
sa Γ a b
sa_env Γ Δ sa_env (cons a Γ) (cons b Δ)
.
Derive Signature for sa_env.

Lemma sa_refl : {n} (Γ : env O n) x, sa Γ x x.
Proof. depind x; constructor; auto. Qed.

Lemma sa_env_refl : {n} (Γ : env O n), sa_env Γ Γ.
Proof. depind Γ; subst; constructor; auto using sa_refl. Qed.

Inductive env_extend : {b c}, env O b env O c scope_le b c Prop :=
| env_extend_refl : {b} (Γ : env O b), env_extend Γ Γ (scope_le_n eq_refl)
| env_extend_cons : {b c} (Γ : env O b) (Δ : env O c) p a,
env_extend Γ Δ p env_extend (cons a Γ) (cons (lift_type_by p a) Δ) (scope_le_map p)
| env_extend_2 : {b c} (Γ : env O b) (Δ : env O c) p a,
env_extend Γ Δ p env_extend Γ (cons a Δ) (scope_le_S p)
.
Derive Signature for env_extend.

Lemma env_app_extend {b c} (Γ : env O b) (Δ : env b c) : env_extend Γ (env_app Γ Δ) (env_scope_le Δ).
Proof.
depind Δ; subst; intros; autorewrite with env_app scope_le_app in *; simpl;
constructor; auto.
Qed.

Lemma env_extend_lookup {b c} (Γ : env O b) (Δ : env O c) P :
env_extend Γ Δ P x, lift_type_by P (lookup Γ x) = lookup Δ (lift_var_by P x).
Proof with autorewrite with lift_type_by lift_var_by map_var lookup scope_le_app; auto.
intros A; depind A; intros x; depelim x...
all:rewrite <- IHA...
Qed.

Lemma sa_weakening {b} (Γ : env O b) p q (A : sa Γ p q) :
{c P} (Δ : env O c) (B : env_extend Γ Δ P),
sa Δ (lift_type_by P p) (lift_type_by P q).
Proof.
induction A; intros c P Δ B;
autorewrite with lift_type_by in *;
try (auto; constructor; auto; fail).
- depelim c; [depelim B|].
constructor; rewrite <- (env_extend_lookup _ _ _ B); auto.
- constructor; auto.
eapply IHA2. constructor. auto.
Qed.

Lemma sa_weakening_app {b} (Γ : env O b) p q (A : sa Γ p q) {c} (Δ : env b c) :
sa (env_app Γ Δ) (lift_type_by (env_scope_le Δ) p) (lift_type_by (env_scope_le Δ) q).
Proof.
intros; eapply sa_weakening.
exact A.
auto using env_app_extend.
Qed.

Lemma sa_toname {n m} Γ (Δ : env (S n) m) x :
x lift_var_by (env_scope_le Δ) FO
p q, lookup (env_app (cons p Γ) Δ) x = lookup (env_app (cons q Γ) Δ) x.
Proof.
depind Δ; subst; intros A p q;
depelim x; simpl in *;
autorewrite with env_app lookup lift_var_by in *; auto.
- exfalso; auto.
- specialize (IHΔ Γ x). forward IHΔ by intro; subst; auto.
now rewrite (IHΔ p q).
Qed.

Lemma var_dec_eq : {n} (x y : var n), {x = y} + {x y}.
Proof.
depind x; depelim y.
- left; reflexivity.
- right; intro H; depelim H.
- right; intro H; depelim H.
- destruct (IHx y); subst.
+ left; reflexivity.
+ right; intro H; depelim H. contradiction.
Qed.

Lemma sa_narrowing {s} q :
( {s'} (P : scope_le s s') (Γ : env O s') p (A : sa Γ p (lift_type_by P q))
s'' (Δ : env (S s') s'')
a b (B : sa (env_app (cons (lift_type_by P q) Γ) Δ) a b),
sa (env_app (cons p Γ) Δ) a b)
( {s'} (A : scope_le s s') (Γ : env O s') p (B : sa Γ p (lift_type_by A q))
r (C : sa Γ (lift_type_by A q) r),
sa Γ p r).
Proof.
induction q;
match goal with
| [ |- _ ?Q ] ⇒
assert (PLOP:Q);
[ intros s' A Γ p B; depind B; subst; intros r C;
autorewrite with lift_type_by lift_var_by in *; try noconf H;
try (constructor; auto; fail);
try (constructor; eapply IHB; autorewrite with lift_type_by; auto; fail);
try (depelim C; subst; constructor; destruct_pairs; try noconf H; eauto; fail);
try (specialize (IHB _ _ _ IHq1 IHq2 A); destruct_pairs; try noconf H; constructor; eauto; fail); auto
| split;
[ intros s' P Γ p A; depind A; subst;
intros s'' Δ a b B; destruct_pairs;
remember (env_app (cons _ Γ) Δ) as PPP; depind B;
try (subst; constructor; auto; autorewrite with core; auto; fail);
clear B; constructor; specialize (IHB _ HeqPPP); subst *;
try (noconf H; auto);
match goal with
| [ IHB : sa _ (lookup (env_app (cons ?a _) _) ?x) _
|- sa _ (lookup (env_app (cons ?b _) _) _) _ ] ⇒
destruct (var_dec_eq x (lift_var_by (env_scope_le Δ) FO)) as [Heq|Hneq] ;
[ subst;
autorewrite with lookup lift_type_by lift_var_by in *;
try (noconf H; auto);
autorewrite with lookup lift_type_by lift_var_by scope_le_app in *;
try solve [auto; depelim IHB;
autorewrite with lookup lift_type_by lift_var_by scope_le_app in *;
auto; constructor; auto; fail];
try solve [(apply sa_var_trans in A || assert (A := sa_arr A1 A2) || assert (A := sa_all A1 A2));
match goal with
| [ A : sa _ ?p _ |- _ ] ⇒
(apply sa_weakening_app with (Δ0:=cons p (empty eq_refl)) in A;
apply sa_weakening_app with (Δ0:=Δ) in A;
autorewrite with lookup env_app lift_var_by lift_type_by in *; simpl in *;
eapply PLOP; [exact A | exact IHB])
end; fail]
| rewrite sa_toname with (p:=b) (q:=a); auto
]
end
| assumption
]
]
end.
- clear IHB1 IHB2.
depelim C; [constructor|]; destruct_pairs.
constructor; eauto.
simpl in H. simpl in H0.
apply (H1 _ A Γ _ C1 _ (empty eq_refl) _ _) in B2; autorewrite with env_app in B2; eauto.
Qed.

Print Assumptions sa_narrowing.
(* Closed under the global context *)