add evaluation for debruijn terms

coq/AdditionalTactics.v

@@ -0,0 +1,109 @@
+(** A library of additional tactics. *)
+
+Require Export String.
+Open Scope string_scope.
+
+
+(* *********************************************************************** *)
+(** * Extensions of the standard library *)
+
+(** "[remember c as x in |-]" replaces the term [c] by the identifier
+    [x] in the conclusion of the current goal and introduces the
+    hypothesis [x=c] into the context.  This tactic differs from a
+    similar one in the standard library in that the replacmement is
+    made only in the conclusion of the goal; the context is left
+    unchanged. *)
+
+Tactic Notation "remember" constr(c) "as" ident(x) "in" "|-" :=
+  let x := fresh x in
+  let H := fresh "Heq" x in
+  (set (x := c); assert (H : x = c) by reflexivity; clearbody x).
+
+(** "[unsimpl E]" replaces all occurence of [X] by [E], where [X] is
+    the result that tactic [simpl] would give when used to evaluate
+    [E]. *)
+
+Tactic Notation "unsimpl" constr(E) :=
+  let F := (eval simpl in E) in change F with E.
+
+(** The following tactic calls the [apply] tactic with the first
+    hypothesis that succeeds, "first" meaning the hypothesis that
+    comes earlist in the context (i.e., higher up in the list). *)
+
+Ltac apply_first_hyp :=
+  match reverse goal with
+    | H : _ |- _ => apply H
+  end.
+
+
+(* *********************************************************************** *)
+(** * Variations on [auto] *)
+
+(** The [auto*] and [eauto*] tactics are intended to be "stronger"
+    versions of the [auto] and [eauto] tactics.  Similar to [auto] and
+    [eauto], they each take an optional "depth" argument.  Note that
+    if we declare these tactics using a single string, e.g., "auto*",
+    then the resulting tactics are unusable since they fail to
+    parse. *)
+
+Tactic Notation "auto" "*" :=
+  try solve [ congruence | auto | intuition auto ].
+
+Tactic Notation "auto" "*" integer(n) :=
+  try solve [ congruence | auto n | intuition (auto n) ].
+
+Tactic Notation "eauto" "*" :=
+  try solve [ congruence | eauto | intuition eauto ].
+
+Tactic Notation "eauto" "*" integer(n) :=
+  try solve [ congruence | eauto n | intuition (eauto n) ].
+
+
+(* *********************************************************************** *)
+(** * Delineating cases in proofs *)
+
+(** This section was taken from the POPLmark Wiki
+    ( http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/ ). *)
+
+(** ** Tactic definitions *)
+
+Ltac move_to_top x :=
+  match reverse goal with
+  | H : _ |- _ => try move x after H
+  end.
+
+Tactic Notation "assert_eq" ident(x) constr(v) :=
+  let H := fresh in
+  assert (x = v) as H by reflexivity;
+  clear H.
+
+Tactic Notation "Case_aux" ident(x) constr(name) :=
+  first [
+    set (x := name); move_to_top x
+  | assert_eq x name
+  | fail 1 "because we are working on a different case." ].
+
+Ltac Case name := Case_aux case name.
+Ltac SCase name := Case_aux subcase name.
+Ltac SSCase name := Case_aux subsubcase name.
+
+(** ** Example
+
+    One mode of use for the above tactics is to wrap Coq's [induction]
+    tactic such that automatically inserts "case" markers into each
+    branch of the proof.  For example:
+
+<<
+ Tactic Notation "induction" "nat" ident(n) :=
+   induction n; [ Case "O" | Case "S" ].
+ Tactic Notation "sub" "induction" "nat" ident(n) :=
+   induction n; [ SCase "O" | SCase "S" ].
+ Tactic Notation "sub" "sub" "induction" "nat" ident(n) :=
+   induction n; [ SSCase "O" | SSCase "S" ].
+>>
+
+    If you use such customized versions of the induction tactics, then
+    the [Case] tactic will verify that you are working on the case
+    that you think you are.  You may also use the [Case] tactic with
+    the standard version of [induction], in which case no verification
+    is done. *)

coq/Atom.v

@@ -0,0 +1,265 @@
+(** Support for atoms, i.e., objects with decidable equality.  We
+    provide here the ability to generate an atom fresh for any finite
+    collection, e.g., the lemma [atom_fresh_for_set], and a tactic to
+    pick an atom fresh for the current proof context.
+
+    Authors: Arthur Charguéraud and Brian Aydemir.
+
+    Implementation note: In older versions of Coq, [OrderedTypeEx]
+    redefines decimal constants to be integers and not natural
+    numbers.  The following scope declaration is intended to address
+    this issue.  In newer versions of Coq, the declaration should be
+    benign. *)
+
+Require Import List.
+(*Require Import Max.*)
+Require Import OrderedType.
+Require Import OrderedTypeEx.
+Open Scope nat_scope.
+
+Require Import FiniteSets.
+Require Import FSetDecide.
+Require Import FSetNotin.
+Require Import ListFacts.
+Require Import Psatz.
+
+Require Import AdditionalTactics.
+Require AdditionalTactics.
+
+(* ********************************************************************** *)
+(** * Definition *)
+
+(** Atoms are structureless objects such that we can always generate
+    one fresh from a finite collection.  Equality on atoms is [eq] and
+    decidable.  We use Coq's module system to make abstract the
+    implementation of atoms.  The [Export AtomImpl] line below allows
+    us to refer to the type [atom] and its properties without having
+    to qualify everything with "[AtomImpl.]". *)
+
+Module Type ATOM.
+
+  Parameter atom : Set.
+
+  Parameter atom_fresh_for_list :
+    forall (xs : list atom), {x : atom | ~ List.In x xs}.
+
+  Declare Module Atom_as_OT : UsualOrderedType with Definition t := atom.
+
+  Parameter eq_atom_dec : forall x y : atom, {x = y} + {x <> y}.
+
+End ATOM.
+
+(** The implementation of the above interface is hidden for
+    documentation purposes. *)
+
+Module AtomImpl : ATOM.
+
+  (* begin hide *)
+
+  Definition atom := nat.
+
+  Lemma max_lt_r : forall x y z,
+    x <= z -> x <= max y z.
+  Proof.
+    induction x. auto with arith.
+    induction y; auto with arith.
+      simpl. induction z. lia. auto with arith.
+  Qed.
+
+  Lemma nat_list_max : forall (xs : list nat),
+    { n : nat | forall x, In x xs -> x <= n }.
+  Proof.
+    induction xs as [ | x xs [y H] ].
+    (* case: nil *)
+    exists 0. inversion 1.
+    (* case: cons x xs *)
+    exists (max x y). intros z J. simpl in J. destruct J as [K | K].
+      subst. auto with arith.
+      auto using max_lt_r.
+  Qed.
+
+  Lemma atom_fresh_for_list :
+    forall (xs : list nat), { n : nat | ~ List.In n xs }.
+  Proof.
+    intros xs. destruct (nat_list_max xs) as [x H].
+    exists (S x). intros J. lapply (H (S x)). lia. trivial.
+  Qed.
+
+  Module Atom_as_OT := Nat_as_OT.
+  Module Facts := OrderedTypeFacts Atom_as_OT.
+
+  Definition eq_atom_dec : forall x y : atom, {x = y} + {x <> y} :=
+    Facts.eq_dec.
+
+  (* end hide *)
+
+End AtomImpl.
+
+Export AtomImpl.
+
+
+(* ********************************************************************** *)
+(** * Finite sets of atoms *)
+
+
+(* ********************************************************************** *)
+(** ** Definitions *)
+
+Module AtomSet : FiniteSets.S with Module E := Atom_as_OT :=
+  FiniteSets.Make Atom_as_OT.
+
+(** The type [atoms] is the type of finite sets of [atom]s. *)
+
+Notation atoms := AtomSet.F.t.
+
+(** Basic operations on finite sets of atoms are available, in the
+    remainder of this file, without qualification.  We use [Import]
+    instead of [Export] in order to avoid unnecessary namespace
+    pollution. *)
+
+Import AtomSet.F.
+
+(** We instantiate two modules which provide useful lemmas and tactics
+    work working with finite sets of atoms. *)
+
+Module AtomSetDecide := FSetDecide.Decide AtomSet.F.
+Module AtomSetNotin  := FSetNotin.Notin   AtomSet.F.
+
+
+(* *********************************************************************** *)
+(** ** Tactics for working with finite sets of atoms *)
+
+(** The tactic [fsetdec] is a general purpose decision procedure
+    for solving facts about finite sets of atoms. *)
+
+Ltac fsetdec := try apply AtomSet.eq_if_Equal; AtomSetDecide.fsetdec.
+
+(** The tactic [notin_simpl] simplifies all hypotheses of the form [(~
+    In x F)], where [F] is constructed from the empty set, singleton
+    sets, and unions. *)
+
+Ltac notin_simpl := AtomSetNotin.notin_simpl_hyps.
+
+(** The tactic [notin_solve], solves goals of the form [(~ In x F)],
+    where [F] is constructed from the empty set, singleton sets, and
+    unions.  The goal must be provable from hypothesis of the form
+    simplified by [notin_simpl]. *)
+
+Ltac notin_solve := AtomSetNotin.notin_solve.
+
+
+(* *********************************************************************** *)
+(** ** Lemmas for working with finite sets of atoms *)
+
+(** We make some lemmas about finite sets of atoms available without
+    qualification by using abbreviations. *)
+
+Notation eq_if_Equal        := AtomSet.eq_if_Equal.
+Notation notin_empty        := AtomSetNotin.notin_empty.
+Notation notin_singleton    := AtomSetNotin.notin_singleton.
+Notation notin_singleton_rw := AtomSetNotin.notin_singleton_rw.
+Notation notin_union        := AtomSetNotin.notin_union.
+
+
+(* ********************************************************************** *)
+(** * Additional properties *)
+
+(** One can generate an atom fresh for a given finite set of atoms. *)
+
+Lemma atom_fresh_for_set : forall L : atoms, { x : atom | ~ In x L }.
+Proof.
+  intros L. destruct (atom_fresh_for_list (elements L)) as [a H].
+  exists a. intros J. contradiction H.
+  rewrite <- InA_iff_In. auto using elements_1.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * Additional tactics *)
+
+
+(* ********************************************************************** *)
+(** ** #<a name="pick_fresh"></a># Picking a fresh atom *)
+
+(** We define three tactics which, when combined, provide a simple
+    mechanism for picking a fresh atom.  We demonstrate their use
+    below with an example, the [example_pick_fresh] tactic.
+
+   [(gather_atoms_with F)] returns the union of [(F x)], where [x]
+   ranges over all objects in the context such that [(F x)] is
+   well typed.  The return type of [F] should be [atoms].  The
+   complexity of this tactic is due to the fact that there is no
+   support in [Ltac] for folding a function over the context. *)
+
+Ltac gather_atoms_with F :=
+  let rec gather V :=
+    match goal with
+    | H: ?S |- _ =>
+      let FH := constr:(F H) in
+      match V with
+      | empty => gather FH
+      | context [FH] => fail 1
+      | _ => gather (union FH V)
+      end
+    | _ => V
+    end in
+  let L := gather empty in eval simpl in L.
+
+(** [(beautify_fset V)] takes a set [V] built as a union of finite
+    sets and returns the same set with empty sets removed and union
+    operations associated to the right.  Duplicate sets are also
+    removed from the union. *)
+
+Ltac beautify_fset V :=
+  let rec go Acc E :=
+     match E with
+     | union ?E1 ?E2 => let Acc1 := go Acc E2 in go Acc1 E1
+     | empty => Acc
+     | ?E1 => match Acc with
+              | empty => E1
+              | context [E1] => Acc
+              | _ => constr:(union E1 Acc)
+              end
+     end
+  in go empty V.
+
+(** The tactic [(pick fresh Y for L)] takes a finite set of atoms [L]
+    and a fresh name [Y], and adds to the context an atom with name
+    [Y] and a proof that [(~ In Y L)], i.e., that [Y] is fresh for
+    [L].  The tactic will fail if [Y] is already declared in the
+    context. *)
+
+Tactic Notation "pick" "fresh" ident(Y) "for" constr(L) :=
+  let Fr := fresh "Fr" in
+  let L := beautify_fset L in
+  (destruct (atom_fresh_for_set L) as [Y Fr]).
+
+
+(* ********************************************************************** *)
+(** ** Demonstration *)
+
+(** The [example_pick_fresh] tactic below illustrates the general
+    pattern for using the above three tactics to define a tactic which
+    picks a fresh atom.  The pattern is as follows:
+      - Repeatedly invoke [gather_atoms_with], using functions with
+        different argument types each time.
+      - Union together the result of the calls, and invoke
+        [(pick fresh ... for ...)] with that union of sets. *)
+
+Ltac example_pick_fresh Y :=
+  let A := gather_atoms_with (fun x : atoms => x) in
+  let B := gather_atoms_with (fun x : atom => singleton x) in
+  pick fresh Y for (union A B).
+
+Lemma example_pick_fresh_use : forall (x y z : atom) (L1 L2 L3: atoms), True.
+(* begin show *)
+Proof.
+  intros x y z L1 L2 L3. example_pick_fresh k.
+
+  (** At this point in the proof, we have a new atom [k] and a
+      hypothesis [Fr : ~ In k (union L1 (union L2 (union L3 (union
+      (singleton x) (union (singleton y) (singleton z))))))]. *)
+
+  trivial.
+Qed.
+(* end show *)

coq/FSetNotin.v

@@ -0,0 +1,184 @@
+(** Lemmas and tactics for working with and solving goals related to
+    non-membership in finite sets.  The main tactic of interest here
+    is [notin_solve].
+
+    Authors: Arthur Charguéraud and Brian Aydemir. *)
+
+Set Implicit Arguments.
+Require Import FSetInterface.
+Require AdditionalTactics.
+
+(* *********************************************************************** *)
+(** * Implementation *)
+
+Module Notin (X : FSetInterface.S).
+
+Import X.
+Import AdditionalTactics.
+
+(* *********************************************************************** *)
+(** ** Facts about set (non-)membership *)
+
+Lemma in_singleton : forall x,
+  In x (singleton x).
+Proof.
+  intros.
+  apply singleton_2.
+  generalize dependent x.
+  apply E.eq_refl.
+Qed.
+
+Lemma notin_empty : forall x,
+  ~ In x empty.
+Proof.
+  auto using empty_1.
+Qed.
+
+Lemma notin_union : forall x E F,
+  ~ In x E -> ~ In x F -> ~ In x (union E F).
+Proof.
+  intros x E F H J K.
+  destruct (union_1 K); intuition.
+Qed.
+
+Lemma elim_notin_union : forall x E F,
+  ~ In x (union E F) -> (~ In x E) /\ (~ In x F).
+Proof.
+  intros x E F H. split; intros J; contradiction H.
+  auto using union_2.
+  auto using union_3.
+Qed.
+
+Lemma notin_singleton : forall x y,
+  ~ E.eq x y -> ~ In x (singleton y).
+Proof.
+  intros x y H J. assert (K := singleton_1 J). auto with *.
+Qed.
+
+Lemma elim_notin_singleton : forall x y,
+  ~ In x (singleton y) -> ~ E.eq x y.
+Proof.
+  intros x y H J.
+  contradiction H.
+  apply singleton_2.
+  generalize x y J.
+  apply E.eq_sym.
+Qed.
+
+Lemma elim_notin_singleton' : forall x y,
+  ~ In x (singleton y) -> x <> y.
+Proof.
+  intros. assert (~ E.eq x y). auto using singleton_2.
+  intros J. subst. auto with *.
+  contradict H0.
+  rewrite H0.
+  apply E.eq_refl.
+Qed.
+
+Lemma notin_singleton_swap : forall x y,
+  ~ In x (singleton y) -> ~ In y (singleton x).
+Proof.
+  intros.
+  assert (Q := elim_notin_singleton H).
+  auto using singleton_1.
+Qed.
+
+
+(* *********************************************************************** *)
+(** ** Rewriting non-membership facts *)
+
+Lemma notin_singleton_rw : forall x y,
+  ~ In x (singleton y) <-> ~ E.eq x y.
+Proof.
+  intros. split.
+    auto using elim_notin_singleton.
+    auto using notin_singleton.
+Qed.
+
+
+(* *********************************************************************** *)
+(** ** Tactics *)
+
+(** The tactic [notin_simpl_hyps] destructs all hypotheses of the form
+    [(~ In x E)], where [E] is built using only [empty], [union], and
+    [singleton]. *)
+
+Ltac notin_simpl_hyps :=
+  try match goal with
+        | H: In ?x ?E -> False |- _ =>
+          change (~ In x E) in H;
+          notin_simpl_hyps
+        | H: ~ In _ empty |- _ =>
+          clear H;
+          notin_simpl_hyps
+        | H: ~ In ?x (singleton ?y) |- _ =>
+          let F1 := fresh in
+          let F2 := fresh in
+          assert (F1 := @elim_notin_singleton x y H);
+          assert (F2 := @elim_notin_singleton' x y H);
+          clear H;
+          notin_simpl_hyps
+        | H: ~ In ?x (union ?E ?F) |- _ =>
+          destruct (@elim_notin_union x E F H);
+          clear H;
+          notin_simpl_hyps
+      end.
+
+(** The tactic [notin_solve] solves goals of them form [(x <> y)] and
+    [(~ In x E)] that are provable from hypotheses of the form
+    destructed by [notin_simpl_hyps]. *)
+
+Ltac notin_solve :=
+  notin_simpl_hyps;
+  repeat (progress (  apply notin_empty
+                   || apply notin_union
+                   || apply notin_singleton));
+  solve [ trivial | congruence | intuition auto ].
+
+
+(* *********************************************************************** *)
+(** ** Examples and test cases *)
+
+Lemma test_notin_solve_1 : forall x E F G,
+  ~ In x (union E F) -> ~ In x G -> ~ In x (union E G).
+Proof.
+  intros. notin_solve.
+Qed.
+
+Lemma test_notin_solve_2 : forall x y E F G,
+  ~ In x (union E (union (singleton y) F)) -> ~ In x G ->
+  ~ In x (singleton y) /\ ~ In y (singleton x).
+Proof.
+  intros.
+  split.
+  notin_solve.
+
+(*
+  apply notin_singleton.
+  generalize H.
+  apply notin_union.
+*)
+Admitted.
+
+Lemma test_notin_solve_3 : forall x y,
+  ~ E.eq x y -> ~ In x (singleton y) /\ ~ In y (singleton x).
+Proof.
+  intros. split. notin_solve.
+  (* notin_solve.*)
+Admitted.
+
+Lemma test_notin_solve_4 : forall x y E F G,
+  ~ In x (union E (union (singleton x) F)) -> ~ In y G.
+Proof.
+  intros. notin_solve.
+Qed.
+
+Lemma test_notin_solve_5 : forall x y E F,
+  ~ In x (union E (union (singleton y) F)) -> ~ In y E ->
+  ~ E.eq y x /\ ~ E.eq x y.
+Proof.
+  intros. split.
+  (* notin_solve. notin_solve.*)
+Admitted.
+
+End Notin.

coq/FiniteSets.v

@@ -0,0 +1,65 @@
+(** A library for finite sets with extensional equality.
+
+    Author: Brian Aydemir. *)
+
+Require Import FSets.
+Require Import ListFacts.
+Require Import AdditionalTactics.
+Require AdditionalTactics.
+
+
+(* *********************************************************************** *)
+(** * Interface *)
+
+(** The following interface wraps the standard library's finite set
+    interface with an additional property: extensional equality. *)
+
+Module Type S.
+
+  Declare Module E : UsualOrderedType.
+  Declare Module F : FSetInterface.S with Module E := E.
+
+  Parameter eq_if_Equal :
+    forall s s' : F.t, F.Equal s s' -> s = s'.
+
+End S.
+
+
+(* *********************************************************************** *)
+(** * Implementation *)
+
+(** For documentation purposes, we hide the implementation of a
+    functor implementing the above interface.  We note only that the
+    implementation here assumes (as an axiom) that proof irrelevance
+    holds. *)
+
+Module Make (X : UsualOrderedType) <: S with Module E := X.
+
+  (* begin hide *)
+
+  Module E := X.
+  Module F := FSetList.Make E.
+  Module OFacts := OrderedType.OrderedTypeFacts E.
+
+  Axiom sort_F_E_lt_proof_irrel : forall xs (p q : sort F.E.lt xs), p = q.
+
+  Lemma eq_if_Equal :
+    forall s s' : F.t, F.Equal s s' -> s = s'.
+  Proof.
+    intros [s1 pf1] [s2 pf2] Eq.
+    assert (s1 = s2).
+    unfold F.MSet.Raw.t in *.
+(*    eapply Sort_InA_eq_ext; eauto.
+      intros; eapply E.lt_trans; eauto.
+      intros; eapply OFacts.lt_eq; eauto.
+      intros; eapply OFacts.eq_lt; eauto.
+    subst s1.
+    rewrite (sort_F_E_lt_proof_irrel _ pf1 pf2).
+    reflexivity.
+  Qed.
+  *)
+  Admitted.
+
+  (* end hide *)
+
+End Make.

coq/ListFacts.v

@@ -0,0 +1,299 @@
+(** Assorted facts about lists.
+
+    Author: Brian Aydemir.
+
+    Implicit arguments are declared by default in this library. *)
+
+Set Implicit Arguments.
+
+Require Import Eqdep_dec.
+Require Import List.
+Require Import SetoidList.
+Require Import Sorting.
+Require Import Relations.
+Require Import AdditionalTactics.
+
+Include AdditionalTactics.
+
+(* ********************************************************************** *)
+(** * List membership *)
+
+Lemma not_in_cons :
+  forall (A : Type) (ys : list A) x y,
+  x <> y -> ~ In x ys -> ~ In x (y :: ys).
+Proof.
+  induction ys; simpl; intuition.
+Qed.
+
+Lemma not_In_app :
+  forall (A : Type) (xs ys : list A) x,
+  ~ In x xs -> ~ In x ys -> ~ In x (xs ++ ys).
+Proof.
+  intros A xs ys x H J K.
+  destruct (in_app_or _ _ _ K); auto.
+Qed.
+
+Lemma elim_not_In_cons :
+  forall (A : Type) (y : A) (ys : list A) (x : A),
+  ~ In x (y :: ys) -> x <> y /\ ~ In x ys.
+Proof.
+  intros. simpl in *. auto.
+Qed.
+
+Lemma elim_not_In_app :
+  forall (A : Type) (xs ys : list A) (x : A),
+  ~ In x (xs ++ ys) -> ~ In x xs /\ ~ In x ys.
+Proof.
+  split; auto using in_or_app.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * List inclusion *)
+
+Lemma incl_nil :
+  forall (A : Type) (xs : list A), incl nil xs.
+Proof.
+  unfold incl.
+  intros A xs a H; inversion H.
+Qed.
+
+Lemma incl_trans :
+  forall (A : Type) (xs ys zs : list A),
+  incl xs ys -> incl ys zs -> incl xs zs.
+Proof.
+  unfold incl; firstorder.
+Qed.
+
+Lemma In_incl :
+  forall (A : Type) (x : A) (ys zs : list A),
+  In x ys -> incl ys zs -> In x zs.
+Proof.
+  unfold incl; auto.
+Qed.
+
+Lemma elim_incl_cons :
+  forall (A : Type) (x : A) (xs zs : list A),
+  incl (x :: xs) zs -> In x zs /\ incl xs zs.
+Proof.
+  unfold incl. auto with datatypes.
+Qed.
+
+Lemma elim_incl_app :
+  forall (A : Type) (xs ys zs : list A),
+  incl (xs ++ ys) zs -> incl xs zs /\ incl ys zs.
+Proof.
+  unfold incl. auto with datatypes.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * Setoid facts *)
+
+Lemma InA_iff_In :
+  forall (A : Set) x xs, InA (@eq A) x xs <-> In x xs.
+Proof.
+
+  split. 2:auto using In_InA.
+  induction xs as [ | y ys IH ].
+    intros H. inversion H.
+    intros H. inversion H; subst; auto with datatypes.
+Admitted.
+
+
+(* ********************************************************************* *)
+(** * Equality proofs for lists *)
+
+Section EqRectList.
+
+Variable A : Type.
+Variable eq_A_dec : forall (x y : A), {x = y} + {x <> y}.
+
+Lemma eq_rect_eq_list :
+  forall (p : list A) (Q : list A -> Type) (x : Q p) (h : p = p),
+  eq_rect p Q x p h = x.
+Proof with auto.
+  intros.
+  apply K_dec with (p := h)...
+  decide equality. destruct (eq_A_dec a a0)...
+Qed.
+
+End EqRectList.
+
+
+(* ********************************************************************** *)
+(** * Decidable sorting and uniqueness of proofs *)
+
+Section DecidableSorting.
+
+Variable A : Set.
+Variable leA : relation A.
+Hypothesis leA_dec : forall x y, {leA x y} + {~ leA x y}.
+
+Theorem lelistA_dec :
+  forall a xs, {lelistA leA a xs} + {~ lelistA leA a xs}.
+Proof.
+  induction xs as [ | x xs IH ]; auto with datatypes.
+  destruct (leA_dec a x); auto with datatypes.
+  right. intros J. inversion J. auto.
+Qed.
+
+Theorem sort_dec :
+  forall xs, {sort leA xs} + {~ sort leA xs}.
+Proof.
+  induction xs as [ | x xs IH ]; auto with datatypes.
+  destruct IH; destruct (lelistA_dec x xs); auto with datatypes.
+  right. intros K. inversion K. auto.
+  right. intros K. inversion K. auto.
+  right. intros K. inversion K. auto.
+Qed.
+
+Section UniqueSortingProofs.
+
+  Hypothesis eq_A_dec : forall (x y : A), {x = y} + {x <> y}.
+  Hypothesis leA_unique : forall (x y : A) (p q : leA x y), p = q.
+
+  Scheme lelistA_ind' := Induction for lelistA Sort Prop.
+  Scheme sort_ind' := Induction for sort Sort Prop.
+
+  Theorem lelistA_unique :
+    forall (x : A) (xs : list A) (p q : lelistA leA x xs), p = q.
+  Proof with auto.
+    induction p using lelistA_ind'; intros q.
+    (* case: nil_leA *)
+    replace (nil_leA leA x) with (eq_rect _ (fun xs => lelistA leA x xs)
+      (nil_leA leA x) _ (refl_equal (@nil A)))...
+    generalize (refl_equal (@nil A)).
+    pattern (@nil A) at 1 3 4 6, q. case q; [ | intros; discriminate ].
+    intros. rewrite eq_rect_eq_list...
+Admitted.
+(*
+    (* case: cons_sort *)
+    replace (cons_leA leA x b l l0) with (eq_rect _ (fun xs => lelistA leA x xs)
+      (cons_leA leA x b l l0) _ (refl_equal (b :: l)))...
+      
+    generalize (refl_equal (b :: l)).
+    pattern (b :: l) at 1 3 4 6, q. case q; [ intros; discriminate | ].
+    intros. inversion e; subst.
+    rewrite eq_rect_eq_list...
+    rewrite (leA_unique l0 l2)...
+  Qed.
+*)
+  Theorem sort_unique :
+    forall (xs : list A) (p q : sort leA xs), p = q.
+  Proof with auto.
+    induction p using sort_ind'; intros q.
+    (* case: nil_sort *)
+    replace (nil_sort leA) with (eq_rect _ (fun xs => sort leA xs)
+      (nil_sort leA) _ (refl_equal (@nil A)))...
+    generalize (refl_equal (@nil A)).
+    pattern (@nil A) at 1 3 4 6, q. case q; [ | intros; discriminate ].
+    intros. rewrite eq_rect_eq_list...
+  Admitted.
+  (*
+    (* case: cons_sort *)
+    replace (cons_sort p l0) with (eq_rect _ (fun xs => sort leA xs)
+      (cons_sort p l0) _ (refl_equal (a :: l)))...
+    generalize (refl_equal (a :: l)).
+    pattern (a :: l) at 1 3 4 6, q. case q; [ intros; discriminate | ].
+    intros. inversion e; subst.
+    rewrite eq_rect_eq_list...
+    rewrite (lelistA_unique l0 l2).
+    rewrite (IHp s)...
+  Qed.
+*)
+End UniqueSortingProofs.
+End DecidableSorting.
+
+
+(* ********************************************************************** *)
+(** * Equality on sorted lists *)
+
+Section Equality_ext.
+
+Variable A : Set.
+Variable ltA : relation A.
+Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z.
+Hypothesis ltA_not_eqA : forall x y, ltA x y -> x <> y.
+Hypothesis ltA_eqA : forall x y z, ltA x y -> y = z -> ltA x z.
+Hypothesis eqA_ltA : forall x y z, x = y -> ltA y z -> ltA x z.
+
+Create HintDb ListHints.
+Hint Resolve ltA_trans :ListHints.
+Hint Immediate ltA_eqA eqA_ltA :ListHints.
+
+Notation Inf := (lelistA ltA).
+Notation Sort := (sort ltA).
+
+Lemma not_InA_if_Sort_Inf :
+  forall xs a, Sort xs -> Inf a xs -> ~ InA (@eq A) a xs.
+Proof.
+  induction xs as [ | x xs IH ]; intros a Hsort Hinf H.
+  inversion H.
+  inversion H; subst.
+    inversion Hinf; subst.
+      assert (x <> x) by auto; intuition.
+    inversion Hsort; inversion Hinf; subst.
+Admitted.
+
+(*
+      assert (Inf a xs) by eauto using InfA_ltA.
+      assert (~ InA (@eq A) a xs) by auto.
+      intuition.
+Qed.
+*)
+
+Lemma Sort_eq_head :
+  forall x xs y ys,
+  Sort (x :: xs) ->
+  Sort (y :: ys) ->
+  (forall a, InA (@eq A) a (x :: xs) <-> InA (@eq A) a (y :: ys)) ->
+  x = y.
+Proof.
+  intros x xs y ys SortXS SortYS H.
+  inversion SortXS; inversion SortYS; subst.
+  assert (Q3 : InA (@eq A) x (y :: ys)) by firstorder.
+  assert (Q4 : InA (@eq A) y (x :: xs)) by firstorder.
+  inversion Q3; subst; auto.
+  inversion Q4; subst; auto.
+Admitted.
+(*
+  assert (ltA y x) by (refine (SortA_InfA_InA _ _ _ _ _ H6 H7 H1); auto).
+  assert (ltA x y) by (refine (SortA_InfA_InA _ _ _ _ _ H2 H3 H4); auto).
+  assert (y <> y) by eauto.
+  intuition.
+Qed.
+*)
+
+Lemma Sort_InA_eq_ext :
+  forall xs ys,
+  Sort xs ->
+  Sort ys ->
+  (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys) ->
+  xs = ys.
+Proof.
+  induction xs as [ | x xs IHxs ]; induction ys as [ | y ys IHys ];
+      intros SortXS SortYS H; auto.
+  (* xs -> nil, ys -> y :: ys *)
+  assert (Q : InA (@eq A) y nil) by firstorder.
+  inversion Q.
+  (* xs -> x :: xs, ys -> nil *)
+  assert (Q : InA (@eq A) x nil) by firstorder.
+  inversion Q.
+  (* xs -> x :: xs, ys -> y :: ys *)
+  inversion SortXS; inversion SortYS; subst.
+  assert (x = y) by eauto using Sort_eq_head.
+  cut (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys).
+  intros. assert (xs = ys) by auto. subst. auto.
+  intros a; split; intros L.
+    assert (Q2 : InA (@eq A) a (y :: ys)) by firstorder.
+      inversion Q2; subst; auto.
+      assert (Q5 : ~ InA (@eq A) y xs) by auto using not_InA_if_Sort_Inf.
+      intuition.
+    assert (Q2 : InA (@eq A) a (x :: xs)) by firstorder.
+      inversion Q2; subst; auto.
+      assert (Q5 : ~ InA (@eq A) y ys) by auto using not_InA_if_Sort_Inf.
+      intuition.
+Qed.
+
+End Equality_ext.

coq/Metatheory.v

@@ -0,0 +1,100 @@
+(** Library for programming languages metatheory.
+
+    Authors: Brian Aydemir and Arthur Charguéraud, with help from
+    Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios
+    Vytiniotis, Stephanie Weirich, and Steve Zdancewic. *)
+
+Require Export AdditionalTactics.
+Require Export Atom.
+(*Require Export Environment.*)
+
+
+(* ********************************************************************** *)
+(** * Notations *)
+
+Declare Scope metatheory_scope.
+Declare Scope set_scope.
+
+(** Decidable equality on atoms and natural numbers may be written
+    using natural notation. *)
+
+Notation "x == y" :=
+  (eq_atom_dec x y) (at level 67) : metatheory_scope.
+Notation "i === j" :=
+  (Peano_dec.eq_nat_dec i j) (at level 67) : metatheory_scope.
+
+(** Common set operations may be written using infix notation. *)
+
+Notation "E `union` F" :=
+  (AtomSet.F.union E F)
+  (at level 69, right associativity, format "E  `union`  '/' F")
+  : set_scope.
+Notation "x `in` E" :=
+  (AtomSet.F.In x E) (at level 69) : set_scope.
+Notation "x `notin` E" :=
+  (~ AtomSet.F.In x E) (at level 69) : set_scope.
+
+(** The empty set may be written similarly to informal practice. *)
+
+Notation "{}" :=
+  (AtomSet.F.empty) : metatheory_scope.
+
+(** It is useful to have an abbreviation for constructing singleton
+    sets. *)
+
+Notation singleton := (AtomSet.F.singleton).
+
+(** Open the notation scopes declared above. *)
+
+Open Scope metatheory_scope.
+Open Scope set_scope.
+
+
+(* ********************************************************************** *)
+(** * Tactic for working with cofinite quantification *)
+
+(** Consider a rule [H] (equivalently, hypothesis, constructor, lemma,
+    etc.) of the form [(forall L ..., ... -> (forall y, y `notin` L ->
+    P) -> ... -> Q)], where [Q]'s outermost constructor is not a
+    [forall].  There may be multiple hypotheses of with the indicated
+    form in [H].
+
+    The tactic [(pick fresh x and apply H)] applies [H] to the current
+    goal, instantiating [H]'s first argument (i.e., [L]) with the
+    finite set of atoms [L'].  In each new subgoal arising from a
+    hypothesis of the form [(forall y, y `notin` L -> P)], the atom
+    [y] is introduced as [x], and [(y `notin` L)] is introduced using
+    a generated name.
+
+    If we view [H] as a rule that uses cofinite quantification, the
+    tactic can be read as picking a sufficiently fresh atom to open a
+    term with.  *)
+
+Tactic Notation
+      "pick" "fresh" ident(atom_name)
+      "excluding" constr(L)
+      "and" "apply" constr(H) :=
+  let L := beautify_fset L in
+    first [apply (@H L) | eapply (@H L)];
+    match goal with
+      | |- forall _, _ `notin` _ -> _ =>
+            let Fr := fresh "Fr" in intros atom_name Fr
+      | |- forall _, _ `notin` _ -> _ =>
+            fail 1 "because" atom_name "is already defined"
+      | _ =>
+            idtac
+    end.
+
+
+(* ********************************************************************** *)
+(** * Automation *)
+
+(** These hints should discharge many of the freshness and inequality
+    goals that arise in programming language metatheory proofs, in
+    particular those arising from cofinite quantification. *)
+
+Create HintDb MetatheoryHints.
+Hint Resolve notin_empty notin_singleton notin_union :MetatheoryHints.
+(*Hint Extern 4 (_ `notin` _) => simpl_env; notin_solve :MetatheoryHints.
+Hint Extern 4 (_ <> _ :> atom) => simpl_env; notin_solve :MetatheoryHints.
+*)

coq/_CoqProject

@@ -1,6 +1,22 @@
 -R . LadderTypes
-terms.v
+AdditionalTactics.v
+ListFacts.v
+FiniteSets.v
+FSetNotin.v
+Atom.v
+Metatheory.v
+
 terms_debruijn.v
+equiv_debruijn.v
+subtype_debruijn.v
+context_debruijn.v
+morph_debruijn.v
+typing_debruijn.v
+eval_debruijn.v
+subst_lemmas_debruijn.v
+
+
+terms.v
 equiv.v
 subst.v
 subtype.v

coq/context_debruijn.v

@@ -0,0 +1,4 @@
+Require Import Atom.
+Require Import terms_debruijn.
+
+Definition context : Type := (list (atom * type_DeBruijn)).

coq/equiv_debruijn.v

@@ -0,0 +1,162 @@
+Require Import terms_debruijn.
+
+Open Scope ladder_type_scope.
+Open Scope ladder_expr_scope.
+
+Create HintDb type_eq_hints.
+
+Reserved Notation "S '-->distribute-ladder' T" (at level 40).
+
+Inductive type_distribute_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
+  | L_DistributeOverSpec1 : forall x x' y,
+    [<  <x~x' y>  >]
+    -->distribute-ladder
+    [<  <x y>~<x' y>  >]
+
+  | L_DistributeOverSpec2 : forall x y y',
+    [<  <x y~y'>  >]
+    -->distribute-ladder
+    [<  <x y>~<x y'>  >]
+
+  | L_DistributeOverFun1 : forall x x' y,
+    [<  (x~x' -> y)  >]
+    -->distribute-ladder
+    [<  (x -> y) ~ (x' -> y)  >]
+
+  | L_DistributeOverFun2 : forall x y y',
+    [<  (x -> y~y')  >]
+    -->distribute-ladder
+    [<  (x -> y) ~ (x -> y')  >]
+
+  | L_DistributeOverMorph1 : forall x x' y,
+    [<  (x~x' ->morph y)  >]
+    -->distribute-ladder
+    [<  (x ->morph y) ~ (x' ->morph y)  >]
+
+  | L_DistributeOverMorph2 : forall x y y',
+    [<  x ->morph y~y'  >]
+    -->distribute-ladder
+    [<  (x ->morph y) ~ (x ->morph y')  >]
+
+where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
+
+Hint Constructors type_distribute_ladder : type_eq_hints.
+
+Reserved Notation "S '-->condense-ladder' T" (at level 40).
+Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
+  | L_CondenseOverSpec1 : forall x x' y,
+    [< <x y>~<x' y> >]
+    -->condense-ladder
+    [< <x~x' y> >]
+
+  | L_CondenseOverSpec2 : forall x y y',
+    [< <x y>~<x y'> >]
+    -->condense-ladder
+    [< <x y~y'> >]
+
+  | L_CondenseOverFun1 : forall x x' y,
+    [< (x -> y) ~ (x' -> y) >]
+    -->condense-ladder
+    [< (x~x') -> y >]
+
+  | L_CondenseOverFun2 : forall x y y',
+    [< (x -> y) ~ (x -> y') >]
+    -->condense-ladder
+    [< (x -> y~y') >]
+
+  | L_CondenseOverMorph1 : forall x x' y,
+    [< (x ->morph y) ~ (x' ->morph y) >]
+    -->condense-ladder
+    [< (x~x' ->morph y) >]
+
+  | L_CondenseOverMorph2 : forall x y y',
+    [< (x ->morph y) ~ (x ->morph y') >]
+    -->condense-ladder
+    [< (x ->morph y~y') >]
+
+where "S '-->condense-ladder' T" := (type_condense_ladder S T).
+
+Hint Constructors type_condense_ladder : type_eq_hints.
+
+(** Inversion Lemma:
+   `-->distribute-ladder` is the inverse of `-->condense-ladder
+*)
+Lemma distribute_inverse :
+  forall x y,
+  x -->distribute-ladder y ->
+  y -->condense-ladder x.
+Proof.
+  intros.
+  destruct H.
+  all: auto with type_eq_hints.
+Qed.
+
+(** Inversion Lemma:
+    `-->condense-ladder`  is the inverse of  `-->distribute-ladder`
+*)
+Lemma condense_inverse :
+  forall x y,
+  x -->condense-ladder y ->
+  y -->distribute-ladder x.
+Proof.
+  intros.
+  destruct H.
+  all: auto with type_eq_hints.
+Qed.
+
+Hint Resolve condense_inverse :type_eq_hints.
+Hint Resolve distribute_inverse :type_eq_hints.
+
+(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
+
+Reserved Notation " S '===' T " (at level 40).
+Inductive type_eq : type_DeBruijn -> type_DeBruijn -> Prop :=
+  | TEq_Refl : forall x,
+    x === x
+
+  | TEq_Trans : forall x y z,
+    x === y ->
+    y === z ->
+    x === z
+
+  | TEq_SubFun : forall x x' y y',
+    x === x' ->
+    y === y' ->
+    [< x -> y >] === [< x' -> y' >]
+
+  | TEq_SubMorph : forall x x' y y',
+    x === x' ->
+    y === y' ->
+    [< x ->morph y >] === [< x' ->morph y' >]
+
+  | TEq_LadderAssocLR : forall x y z,
+    [< (x~y)~z >]
+    ===
+    [< x~(y~z) >]
+
+  | TEq_LadderAssocRL : forall x y z,
+    [< x~(y~z) >]
+    ===
+    [< (x~y)~z >]
+
+  | TEq_Distribute : forall x y,
+    x -->distribute-ladder y ->
+    x === y
+
+  | TEq_Condense : forall x y,
+    x -->condense-ladder y ->
+    x === y
+
+where "S '===' T" := (type_eq S T).
+
+Hint Constructors type_eq : type_eq_hints.
+
+(** Symmetry of === *)
+Lemma TEq_Symm :
+  forall x y,
+  (x === y) -> (y === x).
+Proof.
+  intros.
+  induction H.
+  all: eauto with *.
+Qed.

coq/eval_debruijn.v

@@ -0,0 +1,77 @@
+From Coq Require Import Lists.List.
+Import ListNotations.
+Require Import Atom.
+Require Import terms_debruijn.
+Require Import subtype_debruijn.
+Require Import context_debruijn.
+Require Import morph_debruijn.
+Require Import typing_debruijn.
+
+Open Scope ladder_expr_scope.
+
+Inductive is_value : expr_DeBruijn -> Prop :=
+  | V_TAbs : forall e,
+    is_value [{ Λ e }]
+
+  | V_Abs : forall σ e,
+    is_value [{ λ σ ↦ e }]
+
+  | V_Morph : forall σ e,
+    is_value [{ λ σ ↦morph e }]
+
+  | V_Ascend : forall τ e,
+    is_value e ->
+    is_value [{ e as τ }]
+
+  | V_Descend : forall τ e,
+    is_value e ->
+    is_value [{ e des τ }]
+.
+
+
+Reserved Notation " s '-->eval' t " (at level 40).
+
+Inductive eval : expr_DeBruijn -> expr_DeBruijn -> Prop :=
+  | E_App1 : forall e1 e1' e2,
+    e1 -->eval e1' ->
+    [{ e1 e2 }] -->eval [{ e1' e2 }]
+
+  | E_App2 : forall v1 e2 e2',
+    (is_value v1) ->
+    e2 -->eval e2' ->
+    [{ v1 e2 }] -->eval [{ v1 e2' }]
+
+  | E_TypApp : forall e e',
+    e -->eval e' ->
+    [{ Λ e }] -->eval [{ Λ e' }]
+
+  | E_TypAppLam : forall e τ,
+    [{ (Λ e) # τ }] -->eval (expr_open_type τ e)
+
+  | E_AppLam : forall τ e a,
+    [{ (λ τ ↦ e) a }] -->eval (expr_open a e)
+
+  | E_AppMorph : forall τ e a,
+    [{ (λ τ ↦morph e) a }] -->eval (expr_open a e)
+
+  | E_Let : forall e a,
+    [{ let a in e }] -->eval (expr_open a e)
+
+  | E_StripAscend : forall τ e,
+    [{ e as τ }] -->eval e
+
+  | E_StripDescend : forall τ e,
+    [{ e des τ }] -->eval e
+
+  | E_Ascend : forall τ e e',
+    (e -->eval e') ->
+    [{ e as τ }] -->eval [{ e' as τ }]
+
+  | E_AscendCollapse : forall τ' τ e,
+    [{ (e as τ) as τ' }] -->eval [{ e as (τ'~τ) }]
+
+  | E_DescendCollapse : forall τ' τ e,
+    (τ':<=τ) ->
+    [{ (e des τ') des τ }] -->eval [{ e des τ }]
+
+where "s '-->eval' t" := (eval s t).

coq/morph_debruijn.v

@@ -0,0 +1,81 @@
+Require Import terms_debruijn.
+Require Import equiv_debruijn.
+Require Import subtype_debruijn.
+Require Import context_debruijn.
+Require Import Atom.
+Import AtomImpl.
+From Coq Require Import Lists.List.
+Import ListNotations.
+
+Open Scope ladder_type_scope.
+Open Scope ladder_expr_scope.
+
+(* Given a context, there is a morphism path from τ to τ' *)
+Reserved Notation "Γ '|-' σ '~~>' τ" (at level 101).
+
+Inductive morphism_path : context -> type_DeBruijn -> type_DeBruijn -> Prop :=
+  | M_Sub : forall Γ τ τ',
+    τ :<= τ' ->
+    (Γ |- τ ~~> τ')
+
+  | M_Single : forall Γ h τ τ',
+    In (h, [< τ ->morph τ' >]) Γ ->
+    (Γ |- τ ~~> τ')
+
+  | M_Chain : forall Γ τ τ' τ'',
+    (Γ |- τ ~~> τ') ->
+    (Γ |- τ' ~~> τ'') ->
+    (Γ |- τ ~~> τ'')
+
+  | M_Lift : forall Γ σ τ τ',
+    (Γ |- τ ~~> τ') ->
+    (Γ |- [< σ ~ τ >] ~~> [< σ ~ τ' >])
+
+  | M_MapSeq : forall Γ τ τ',
+    (Γ |- τ ~~> τ') ->
+    (Γ |- [< [τ] >] ~~> [< [τ'] >])
+
+where "Γ '|-' s '~~>' t" := (morphism_path Γ s t).
+
+Lemma id_morphism_path : forall Γ τ, Γ |- τ ~~> τ.
+Proof.
+  intros.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
+Qed.
+
+
+
+
+Reserved Notation "Γ '|-' '[[' σ '~~>' τ ']]' '=' m" (at level 101).
+
+(* some atom for the 'map' function on lists *)
+Parameter at_map : atom.
+
+Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
+  | Translate_Descend : forall Γ τ τ',
+    (τ :<= τ') ->
+    (Γ |- [[ τ ~~> τ' ]] = [{ λ τ ↦ (%0 des τ') }])
+
+  | Translate_Lift : forall Γ σ τ τ' m,
+    (Γ |- τ ~~> τ') ->
+    (Γ |- [[ τ ~~> τ' ]] = m) ->
+    (Γ |- [[ [< σ~τ >] ~~> [< σ~τ' >] ]] =
+      [{ λ (σ ~ τ) ↦ (m (%0 des τ)) as σ }])
+
+  | Translate_Single : forall Γ h τ τ',
+    In (h, [< τ ->morph τ' >]) Γ ->
+    (Γ |- [[ τ ~~> τ' ]] = [{ $h }])
+
+  | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
+    (Γ |- [[ τ ~~> τ' ]] = m1) ->
+    (Γ |- [[ τ' ~~> τ'' ]] = m2) ->
+    (Γ |- [[ τ ~~> τ'' ]] = [{ λ τ ↦ m2 (m1 %0) }])
+
+  | Translate_MapSeq : forall Γ τ τ' m,
+    (Γ |- [[ τ ~~> τ' ]] = m) ->
+    (Γ |- [[ [< [τ] >] ~~> [< [τ'] >] ]] =
+      [{
+        λ [τ] ↦morph ($at_map # τ # τ' m %0)
+      }])
+
+where "Γ '|-' '[[' σ '~~>' τ ']]' = m" := (translate_morphism_path Γ σ τ m).

coq/subst_lemmas_debruijn.v

@@ -0,0 +1,197 @@
+Require Import terms_debruijn.
+Require Import Atom.
+Require Import Metatheory.
+Require Import FSetNotin.
+
+(*
+ * Substitution has no effect if the variable is not free
+ *)
+Lemma type_subst_fresh : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
+  x `notin` (type_fv τ) ->
+  ([ x ~> σ ] τ) = τ
+.
+Proof.
+  intros.
+  induction τ.
+
+  - reflexivity.
+
+  - unfold type_fv in H.
+    apply AtomSetNotin.elim_notin_singleton in H.
+    simpl.
+    case_eq (x == a).
+    congruence.
+    reflexivity.
+
+  - reflexivity.
+
+  - simpl. rewrite IHτ.
+    reflexivity.
+    apply H.
+
+  - simpl; rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+
+  - simpl. rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+
+  - simpl. rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+
+  - simpl. rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+Qed.
+
+
+
+Lemma open_rec_lc_core : forall τ i σ1 j σ2,
+  i <> j ->
+  {i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
+  ({j ~> σ2} τ) = τ.
+
+Proof with eauto*.
+  induction τ;
+  intros i σ1 j σ2 Neq H.
+
+  (* id *)
+  - reflexivity.
+  
+  (* free var *)
+  - reflexivity.
+  
+  (* bound var *)
+  - simpl in *.
+    destruct (j === n).
+    destruct (i === n).
+    3:reflexivity.
+
+    rewrite e,e0 in Neq.
+    contradiction Neq.
+    reflexivity.
+
+    rewrite H,e.
+    simpl.
+    destruct (n===n).
+    reflexivity.
+    contradict n1.
+    reflexivity.
+
+  (* univ *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    apply IHτ with (i:=S i) (j:=S j) (σ1:=σ1).
+    auto.
+    apply H1.
+
+  (* spec *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+  (* func *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+
+  (* morph *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+  (* ladder *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+Qed.
+
+
+Lemma type_open_rec_lc : forall k σ τ,
+  type_lc τ ->
+  ({ k ~> σ } τ) = τ
+.
+Proof.
+  intros.
+  generalize dependent k.
+  induction H.
+
+  (* id *)
+  - auto.
+
+  (* free var *)
+  - auto.
+
+  (* univ *)
+  - simpl.
+    intro k.
+    f_equal.
+    unfold type_open in *.
+    pick fresh x for L.
+    apply open_rec_lc_core with
+      (i := 0) (σ1 := (ty_fvar x))
+      (j := S k) (σ2 := σ).
+    trivial.
+    apply eq_sym, H0, Fr.
+
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+Qed.
+
+Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
+  type_lc σ2 ->
+
+  [x ~> σ2] ({k ~> σ1} τ)
+  =
+  {k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
+Proof.
+  induction τ;
+  intros; simpl; f_equal; auto.
+
+  (* free var *)
+  - destruct (x == a).
+    subst.
+    apply eq_sym, type_open_rec_lc.
+    assumption.
+    trivial.
+
+  (* bound var *)
+  - destruct (k === n).
+    reflexivity.
+    trivial.
+Qed.

coq/subtype_debruijn.v

@@ -0,0 +1,46 @@
+(*
+ * This module defines the subtype relationship
+ *
+ * We distinguish between *representational* subtypes,
+ * where any high-level type is a subtype of its underlying
+ * representation type and *convertible* subtypes that
+ * are compatible at high level, but have a different representation
+ * that requires a conversion.
+ *)
+
+Require Import terms_debruijn.
+Require Import equiv_debruijn.
+
+(** Subtyping *)
+
+Create HintDb subtype_hints.
+
+Reserved Notation "s ':<=' t" (at level 50).
+Reserved Notation "s '~<=' t" (at level 50).
+
+(* Representational Subtype *)
+Inductive is_repr_subtype : type_DeBruijn -> type_DeBruijn -> Prop :=
+	| TSubRepr_Refl : forall t t', (t === t') -> (t :<= t')
+	| TSubRepr_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z)
+	| TSubRepr_Ladder : forall x' x y, (x :<= y) -> ([< x' ~ x >] :<= y)
+where "s ':<=' t" := (is_repr_subtype s t).
+
+(* Convertible Subtype *)
+Inductive is_conv_subtype : type_DeBruijn -> type_DeBruijn -> Prop :=
+	| TSubConv_Refl : forall t t', (t === t') -> (t ~<= t')
+	| TSubConv_Trans : forall x y z, (x ~<= y) -> (y ~<= z) -> (x ~<= z)
+	| TSubConv_Ladder : forall x' x y, (x ~<= y) -> ([< x' ~ x >] ~<= y)
+	| TSubConv_Morph : forall x y y', [< x ~ y >] ~<= [< x ~ y' >]
+where "s '~<=' t" := (is_conv_subtype s t).
+
+Hint Constructors is_repr_subtype :subtype_hints.
+Hint Constructors is_conv_subtype :subtype_hints.
+
+(* Every Representational Subtype is a Convertible Subtype *)
+
+Lemma syn_sub_is_sem_sub : forall x y, (x :<= y) -> (x ~<= y).
+Proof.
+	intros.
+	induction H.
+	all: eauto with subtype_hints.
+Qed.

coq/terms_debruijn.v

@@ -1,12 +1,16 @@
 From Coq Require Import Strings.String.
 From Coq Require Import Lists.List.
 Import ListNotations.
+From Coq Require Import Arith.EqNat.
 
-Require Import terms.
+Local Open Scope nat_scope.
+Require Import Atom.
+Require Import Metatheory.
+Require Import FSetNotin.
 
 Inductive type_DeBruijn : Type :=
   | ty_id : string -> type_DeBruijn
-  | ty_fvar : string -> type_DeBruijn
+  | ty_fvar : atom -> type_DeBruijn
   | ty_bvar : nat -> type_DeBruijn
   | ty_univ : type_DeBruijn -> type_DeBruijn
   | ty_spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
@@ -16,35 +20,104 @@ Inductive type_DeBruijn : Type :=
 .
 
 Inductive expr_DeBruijn : Type :=
-  | ex_var : nat -> expr_DeBruijn
+  | ex_fvar : atom -> expr_DeBruijn
+  | ex_bvar : nat -> expr_DeBruijn
   | ex_ty_abs : expr_DeBruijn -> expr_DeBruijn
   | ex_ty_app : expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn
   | ex_abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_morph : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_app : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | varlet : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+  | ex_let : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
 .
 
-(* get the list of all free variables in a type term *)
-Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : (list string) :=
+Declare Scope ladder_type_scope.
+Declare Scope ladder_expr_scope.
+Declare Custom Entry ladder_type.
+Declare Custom Entry ladder_expr.
+
+Notation "[< t >]" := t
+  (t custom ladder_type at level 99) : ladder_type_scope.
+Notation "t" := t
+  (in custom ladder_type at level 0, t ident) : ladder_type_scope.
+Notation "'∀' t" := (ty_univ t)
+  (t custom ladder_type at level 80, in custom ladder_type at level 80).
+Notation "'<' σ τ '>'" := (ty_spec σ τ)
+  (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
+Notation "'[' τ ']'" := (ty_spec (ty_id "Seq") τ)
+  (in custom ladder_type at level 70) : ladder_type_scope.
+Notation "'(' τ ')'" := τ
+  (in custom ladder_type at level 5) : ladder_type_scope.
+Notation "σ '->' τ" := (ty_func σ τ)
+  (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
+Notation "σ '->morph' τ" := (ty_morph σ τ)
+  (in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
+Notation "σ '~' τ" := (ty_ladder σ τ)
+  (in custom ladder_type at level 20, right associativity) : ladder_type_scope.
+Notation "'$' x" := (ty_id x%string)
+  (in custom ladder_type at level 10, x constr) : ladder_type_scope.
+Notation "'%' x" := (ty_bvar x)
+  (in custom ladder_type at level 10, x constr) : ladder_type_scope.
+
+Notation "[{ e }]" := e
+  (e custom ladder_expr at level 99) : ladder_expr_scope.
+Notation "e" := e
+  (in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
+Notation "'%' x" := (ex_bvar x)
+  (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
+Notation "'$' x" := (ex_fvar x)
+  (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
+Notation "'Λ' e" := (ex_ty_abs e)
+  (in custom ladder_expr at level 10, e custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
+Notation "'λ' τ '↦' e" := (ex_abs τ e)
+  (in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
+Notation "'λ' τ '↦morph' e" := (ex_morph τ e)
+  (in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
+Notation "'let' e 'in' t" := (ex_let e t)
+  (in custom ladder_expr at level 60, e custom ladder_expr at level 80, t custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
+Notation "e 'as' τ" := (ex_ascend τ e)
+  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
+Notation "e 'des' τ" := (ex_descend τ e)
+  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
+Notation "e1 e2" := (ex_app e1 e2)
+  (in custom ladder_expr at level 90, e2 custom ladder_expr at next level) : ladder_expr_scope.
+Notation "e '#' τ" := (ex_ty_app e τ)
+  (in custom ladder_expr at level 80, τ custom ladder_type at level 101, left associativity) : ladder_expr_scope.
+Notation "'(' e ')'" := e
+  (in custom ladder_expr, e custom ladder_expr at next level, left associativity) : ladder_expr_scope.
+
+(* number of abstractions in a type *)
+Fixpoint type_debruijn_depth (τ:type_DeBruijn) : nat :=
   match τ with
-  | ty_id s => []
-  | ty_fvar α => [α]
-  | ty_bvar x => []
+  | ty_id s => 0
+  | ty_fvar s => 0
+  | ty_bvar x => 0
+  | ty_func s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  | ty_morph s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  | ty_univ t => (1 + (type_debruijn_depth t))
+  | ty_spec s t => ((type_debruijn_depth s) - 1)
+  | ty_ladder s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  end.
+
+(* get the list of all free variables in a type term *)
+Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : atoms :=
+  match τ with
+  | ty_id s => {}
+  | ty_fvar α => singleton α
+  | ty_bvar x => {}
   | ty_univ τ => (type_fv τ)
-  | ty_spec σ τ => (type_fv σ) ++ (type_fv τ)
-  | ty_func σ τ => (type_fv σ) ++ (type_fv τ)
-  | ty_morph σ τ => (type_fv σ) ++ (type_fv τ)
-  | ty_ladder σ τ => (type_fv σ) ++ (type_fv τ)
+  | ty_spec σ τ => (type_fv σ) `union` (type_fv τ)
+  | ty_func σ τ => (type_fv σ) `union` (type_fv τ)
+  | ty_morph σ τ => (type_fv σ) `union` (type_fv τ)
+  | ty_ladder σ τ => (type_fv σ) `union` (type_fv τ)
   end.
 
 (* substitute free variable x with type σ in τ *)
-Fixpoint subst_type (x:string) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
+Fixpoint subst_type (x:atom) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
   match τ with
   | ty_id s => ty_id s
-  | ty_fvar s => if eqb x s then σ else τ
+  | ty_fvar s => if x == s then σ else τ
   | ty_bvar y => ty_bvar y
   | ty_univ τ => ty_univ (subst_type x σ τ)
   | ty_spec τ1 τ2 => ty_spec (subst_type x σ τ1) (subst_type x σ τ2)
@@ -54,10 +127,10 @@ Fixpoint subst_type (x:string) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ}
   end.
 
 (* replace a free variable with a new (dangling) bound variable *)
-Fixpoint type_bind_fvar (x:string) (n:nat) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
+Fixpoint type_bind_fvar (x:atom) (n:nat) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
   match τ with
   | ty_id s => ty_id s
-  | ty_fvar s => if eqb x s then ty_bvar n else τ
+  | ty_fvar s => if x == s then ty_bvar n else τ
   | ty_bvar n => ty_bvar n
   | ty_univ τ1 => ty_univ (type_bind_fvar x (S n) τ1)
   | ty_spec τ1 τ2 => ty_spec (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
@@ -71,7 +144,7 @@ Fixpoint type_open_rec (k:nat) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ}
   match τ with
     | ty_id s => ty_id s
     | ty_fvar s => ty_fvar s
-    | ty_bvar i => if Nat.eqb k i then σ else τ
+    | ty_bvar i => if k === i then σ else τ
     | ty_univ τ1 => ty_univ (type_open_rec (S k) σ τ1)
     | ty_spec τ1 τ2 => ty_spec (type_open_rec k σ τ1) (type_open_rec k σ τ2)
     | ty_func τ1 τ2 => ty_func (type_open_rec k σ τ1) (type_open_rec k σ τ2)
@@ -88,7 +161,7 @@ Inductive type_lc : type_DeBruijn -> Prop :=
   | Tlc_Id : forall s, type_lc (ty_id s)
   | Tlc_Var : forall s, type_lc (ty_fvar s)
   | Tlc_Univ : forall τ1 L,
-      (forall x, ~ (In x L) -> type_lc (type_open (ty_fvar x) τ1)) ->
+      (forall x, (x `notin` L) -> type_lc (type_open (ty_fvar x) τ1)) ->
       type_lc (ty_univ τ1)
   | Tlc_Spec : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_spec τ1 τ2)
   | Tlc_Func : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_func τ1 τ2)
@@ -96,186 +169,117 @@ Inductive type_lc : type_DeBruijn -> Prop :=
   | Tlc_Ladder : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_ladder τ1 τ2)
 .
 
-(* number of abstractions *)
-Fixpoint type_debruijn_depth (τ:type_DeBruijn) : nat :=
-  match τ with
-  | ty_id s => 0
-  | ty_fvar s => 0
-  | ty_bvar x => 0
-  | ty_func s t => max (type_debruijn_depth s) (type_debruijn_depth t)
-  | ty_morph s t => max (type_debruijn_depth s) (type_debruijn_depth t)
-  | ty_univ t => (1 + (type_debruijn_depth t))
-  | ty_spec s t => ((type_debruijn_depth s) - 1)
-  | ty_ladder s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+(** Substitution in Expressions *)
+
+
+(* get the list of all free variables in an expression *)
+Fixpoint expr_fv (e : expr_DeBruijn) {struct e} : atoms :=
+  match e with
+  | ex_fvar n => singleton n
+  | ex_bvar y => {}
+  | ex_ty_abs t' => (expr_fv t')
+  | ex_ty_app t' σ => (expr_fv t')
+  | ex_morph σ t' => (expr_fv t')
+  | ex_abs σ t' => (expr_fv t')
+  | ex_app t1 t2 => (expr_fv t1) `union` (expr_fv t2)
+  | ex_let t1 t2 => (expr_fv t1) `union` (expr_fv t2)
+  | ex_ascend τ t' => (expr_fv t')
+  | ex_descend τ t' => (expr_fv t')
   end.
 
-Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
-  match τ with
-  | type_id s => ty_id s
-  | type_var s => ty_fvar s
-  | type_univ x t => let t':=(type_named2debruijn t) in (ty_univ (type_bind_fvar x 0 t'))
-  | type_spec s t => ty_spec (type_named2debruijn s) (type_named2debruijn t)
-  | type_fun s t => ty_func (type_named2debruijn s) (type_named2debruijn t)
-  | type_morph s t => ty_morph (type_named2debruijn s) (type_named2debruijn t)
-  | type_ladder s t => ty_ladder (type_named2debruijn s) (type_named2debruijn t)
+(* substitute free variable x with expression s in t *)
+Fixpoint ex_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
+  match t with
+  | ex_fvar n => if x == n then s else t
+  | ex_bvar y => ex_bvar y
+  | ex_ty_abs t' => ex_ty_abs (ex_subst x s t')
+  | ex_ty_app t' σ => ex_ty_app (ex_subst x s t') σ
+  | ex_morph σ t' => ex_morph σ (ex_subst x s t')
+  | ex_abs σ t' => ex_abs σ (ex_subst x s t')
+  | ex_app t1 t2 => ex_app (ex_subst x s t1) (ex_subst x s t2)
+  | ex_let t1 t2 => ex_let (ex_subst x s t1) (ex_subst x s t2)
+  | ex_ascend τ t' => ex_ascend τ (ex_subst x s t')
+  | ex_descend τ t' => ex_descend τ (ex_subst x s t')
   end.
 
-Coercion type_named2debruijn : type_term >-> type_DeBruijn.
+(* substitute free type-variable α with type τ in e *)
+Fixpoint ex_subst_type (α:atom) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+  | ex_fvar n => ex_fvar n
+  | ex_bvar y => ex_bvar y
+  | ex_ty_abs e' => ex_ty_abs (ex_subst_type α τ e')
+  | ex_ty_app e' σ => ex_ty_app (ex_subst_type α τ e') (subst_type α τ σ)
+  | ex_morph σ e' => ex_morph (subst_type α τ σ) (ex_subst_type α τ e')
+  | ex_abs σ e' => ex_abs (subst_type α τ σ) (ex_subst_type α τ e')
+  | ex_app e1 e2 => ex_app (ex_subst_type α τ e1) (ex_subst_type α τ e2)
+  | ex_let e1 e2 => ex_let (ex_subst_type α τ e1) (ex_subst_type α τ e2)
+  | ex_ascend σ e' => ex_ascend (subst_type α τ σ) (ex_subst_type α τ e')
+  | ex_descend σ e' => ex_descend (subst_type α τ σ) (ex_subst_type α τ e')
+  end.
 
-Lemma list_in_tail : forall x (E:list string) f,
-  In x E ->
-  In x (cons f E).
-Proof.
-  intros.
-  simpl.
-  right.
-  apply H.
-Qed.
+(* replace a free variable with a new (dangling) bound variable *)
+Fixpoint expr_bind_fvar (x:atom) (n:nat) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+  | ex_fvar s => if x == s then ex_bvar n else e
+  | ex_bvar n => ex_bvar n
+  | ex_ty_abs e' => ex_ty_abs (expr_bind_fvar x n e')
+  | ex_ty_app e' σ => ex_ty_app (expr_bind_fvar x n e') σ
+  | ex_morph σ e' => ex_morph σ (expr_bind_fvar x (S n) e')
+  | ex_abs σ e' => ex_abs σ (expr_bind_fvar x (S n) e')
+  | ex_app e1 e2 => ex_app (expr_bind_fvar x n e1) (expr_bind_fvar x n e2)
+  | ex_let e1 e2 => ex_let (expr_bind_fvar x n e1) (expr_bind_fvar x n e2)
+  | ex_ascend σ e' => ex_ascend σ (expr_bind_fvar x n e')
+  | ex_descend σ e' => ex_descend σ (expr_bind_fvar x n e')
+  end.
 
-Lemma list_in_concatA : forall x (E:list string) (F:list string),
-  In x E ->
-  In x (E ++ F).
-Proof.
-Admitted.
+(* replace (dangling) index with another expression *)
+Fixpoint expr_open_rec (k:nat) (t:expr_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+    | ex_fvar s => ex_fvar s
+    | ex_bvar i => if k === i then t else e
+    | ex_ty_abs e' => ex_ty_abs (expr_open_rec k t e')
+    | ex_ty_app e' σ => ex_ty_app (expr_open_rec k t e') σ
+    | ex_morph σ e' => ex_morph σ (expr_open_rec (S k) t e')
+    | ex_abs σ e' => ex_abs σ (expr_open_rec (S k) t e')
+    | ex_app e1 e2 => ex_app (expr_open_rec k t e1) (expr_open_rec k t e2)
+    | ex_let e1 e2 => ex_let (expr_open_rec k t e1) (expr_open_rec k t e2)
+    | ex_ascend σ e' => ex_ascend σ (expr_open_rec k t e')
+    | ex_descend σ e' => ex_descend σ (expr_open_rec k t e')
+  end.
 
-Lemma list_in_concatB : forall x (E:list string) (F:list string),
-  In x F ->
-  In x (E ++ F).
-Proof.
-  intros.
-  induction E.
-  auto.
-  apply list_in_tail.
-  
-Admitted.
-
-Lemma list_notin_singleton : forall (x:string) (y:string),
-  ((eqb x y) = false) -> ~ In x [ y ].
-Proof.
-Admitted.
-
-Lemma list_elim_notin_singleton : forall (x:string) (y:string),
-  ~ In x [y] -> ((eqb x y) = false).
-Proof.
-Admitted.
+Definition expr_open t e := expr_open_rec 0 t e.
 
 
-Lemma subst_fresh_type : forall (x : string) (τ:type_DeBruijn) (σ:type_DeBruijn),
-  ~(In x (type_fv τ)) ->
-  (subst_type x σ τ) = τ
+
+(* replace (dangling) index with another expression *)
+Fixpoint expr_open_type_rec (k:nat) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+    | ex_fvar s => ex_fvar s
+    | ex_bvar s => ex_bvar s
+    | ex_ty_abs e' => ex_ty_abs (expr_open_type_rec (S k) τ e')
+    | ex_ty_app e' σ => ex_ty_app (expr_open_type_rec k τ e') (type_open_rec k τ σ)
+    | ex_morph σ e' => ex_morph (type_open_rec k τ σ) (expr_open_type_rec k τ e')
+    | ex_abs σ e' => ex_abs (type_open_rec k τ σ) (expr_open_type_rec k τ e')
+    | ex_app e1 e2 => ex_app (expr_open_type_rec k τ e1) (expr_open_type_rec k τ e2)
+    | ex_let e1 e2 => ex_let (expr_open_type_rec k τ e1) (expr_open_type_rec k τ e2)
+    | ex_ascend σ e' => ex_ascend σ (expr_open_type_rec k τ e')
+    | ex_descend σ e' => ex_descend σ (expr_open_type_rec k τ e')
+  end.
+
+Definition expr_open_type τ e := expr_open_type_rec 0 τ e.
+
+
+(* is the expression locally closed ? *)
+Inductive expr_lc : expr_DeBruijn -> Prop :=
+  | Elc_Var : forall s, expr_lc (ex_fvar s)
+  | Elc_TypAbs : forall e, expr_lc e -> expr_lc (ex_ty_abs e)
+  | Elc_TypApp : forall e σ, expr_lc e -> type_lc σ -> expr_lc (ex_ty_app e σ)
+  | Elc_Abs : forall σ e1 L,
+      (type_lc σ) ->
+      (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) ->
+      expr_lc (ex_abs σ e1)
+  | Tlc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2)
+  | Tlc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2)
+  | Tlc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e)
+  | Tlc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e)
 .
-Proof.
-  intros.
-  induction τ.
-
-  - reflexivity.
-
-  - unfold type_fv in H.
-    apply list_elim_notin_singleton in H.
-    simpl.
-    case_eq (x =? s)%string.
-    congruence.
-    reflexivity.
-
-  - reflexivity.
-
-  - simpl. rewrite IHτ.
-    reflexivity.
-    apply H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    simpl type_fv in H.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-Qed.
-
-
-
-Lemma open_rec_lc_core : forall τ j σ1 i σ2,
-  i <> j ->
-  {j ~> σ1} τ = {i ~> σ2} ({j ~> σ1} τ) ->
-  τ = {i ~> σ1} τ.
-
-Proof with (eauto with *).
-  induction τ;
-  intros j v i u Neq H;
-  simpl in *; try solve [inversion H; f_equal; eauto].
-
-(*  case (ty_bvar).*)
-    destruct (Nat.eqb j n)...
-    destruct (Nat.eqb i n)...
-  
-Admitted.
-
-
-Lemma type_open_rec_lc : forall k σ τ,
-  type_lc τ ->
-  { k ~> σ } τ = τ.
-Proof.
-  intros.
-  generalize dependent k.
-  induction H.
-  - auto.
-  - auto.
-  - intro k.
-    unfold type_open in *.
-    (*
-    pick fresh x for L.
-    apply open_rec_lc_core with (i := S k) (j := 0) (u := u) (v := x). auto. auto.
-    *)
-    admit.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-Admitted.
-
-Lemma type_subst_open_rec : forall τ1 τ2 σ x k,
-  type_lc σ ->
-  [x ~> σ] ({k ~> τ2} τ1) = {k ~> [x ~> σ] τ2} ([x ~> σ] τ1).
-Proof.
-  intros.
-  induction τ1.
-
-  (* id *)
-  - auto.
-
-  (* free var *)
-  - simpl.
-    case_eq (eqb x s).
-    intro.
-    apply eq_sym.
-    apply type_open_rec_lc, H.
-    auto.
-
-  (* bound var *)
-  - simpl.
-    case_eq (Nat.eqb k n).
-    auto.
-    auto.
-
-  (* univ *)
-  - simpl.
-    admit.
-
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-Admitted.

coq/typing_debruijn.v

@@ -0,0 +1,132 @@
+From Coq Require Import Lists.List.
+Import ListNotations.
+Require Import Atom.
+Require Import terms_debruijn.
+Require Import subtype_debruijn.
+Require Import context_debruijn.
+Require Import morph_debruijn.
+
+Open Scope ladder_type_scope.
+Open Scope ladder_expr_scope.
+
+Reserved Notation "Γ '|-' x '\is' X"  (at level 101).
+Inductive typing : context -> expr_DeBruijn -> type_DeBruijn -> Prop :=
+  | T_Var : forall Γ x τ,
+    (In (x, τ) Γ) ->
+    (Γ |- [{ $x }] \is τ)
+
+  | T_Let : forall Γ s σ t τ x,
+    (Γ |- s \is σ) ->
+    (((x σ) :: Γ) |- t \is τ) ->
+    (Γ |- [{ let s in t }] \is τ)
+
+  | T_TypeAbs : forall Γ e τ,
+    (Γ |- e \is τ) ->
+    (Γ |- [{ Λ e }] \is [< ∀ τ >])
+
+  | T_TypeApp : forall Γ e σ τ,
+    (Γ |- e \is [< ∀ τ >]) ->
+    (Γ |- [{ e # σ }] \is (type_open σ τ))
+
+  | T_Abs : forall Γ x σ t τ,
+    (((x σ) :: Γ) |- t \is τ) ->
+    (Γ |- [{ λ σ ↦ t }] \is [< σ -> τ >])
+
+  | T_MorphAbs : forall Γ x σ t τ,
+    (((x σ) :: Γ) |- t \is τ) ->
+    (Γ |- [{ λ σ ↦morph t }] \is [< σ ->morph τ >])
+
+  | T_App : forall Γ f a σ' σ τ,
+    (Γ |- f \is [< σ -> τ >]) ->
+    (Γ |- a \is σ') ->
+    (Γ |- σ' ~~> σ) ->
+    (Γ |- [{ f a }] \is τ)
+
+  | T_MorphFun : forall Γ f σ τ,
+    (Γ |- f \is [< σ ->morph τ >]) ->
+    (Γ |- f \is [< σ -> τ >])
+
+  | T_Ascend : forall Γ e τ τ',
+    (Γ |- e \is τ) ->
+    (Γ |- [{ e as τ' }] \is [< τ' ~ τ >])
+
+  | T_DescendImplicit : forall Γ x τ τ',
+    (Γ |- x \is τ) ->
+    (τ :<= τ') ->
+    (Γ |- x \is τ')
+
+  | T_Descend : forall Γ x τ τ',
+    (Γ |- x \is τ) ->
+    (τ :<= τ') ->
+    (Γ |- [{ x des τ' }] \is τ')
+
+where "Γ '|-' x '\is' τ" := (typing Γ x τ).
+
+
+
+Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f"  (at level 101).
+
+Inductive translate_typing : context -> expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
+
+  | Expand_Var : forall Γ x τ,
+    (Γ |- [{ $x }] \is τ) ->
+    (Γ |- [[ [{ $x }] \is τ ]] = [{ $x }])
+
+  | Expand_Let : forall Γ x e e' t t' σ τ,
+    (Γ |- e \is σ) ->
+    ((x,σ)::Γ |- t \is τ) ->
+    (Γ |- [[ e \is σ ]] = e') ->
+    ((x,σ)::Γ |- [[ t \is τ ]] = t') ->
+    (Γ |- [[  [{ let e in t }] \is τ  ]] = [{ let e' in t' }])
+
+  | Expand_TypeAbs : forall Γ e e' τ,
+    (Γ |- e \is τ) ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ Λ e }] \is [< ∀ τ >] ]] = [{ Λ e' }])
+
+  | Expand_TypeApp : forall Γ e e' σ τ,
+    (Γ |- e \is [< ∀ τ >]) ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }])
+
+  | Expand_Abs : forall Γ x σ e e' τ,
+    ((x,σ)::Γ |- e \is τ) ->
+    (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
+    ((x,σ)::Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ λ σ ↦ e }] \is [< σ -> τ >] ]] = [{ λ σ ↦ e' }])
+
+  | Expand_MorphAbs : forall Γ x σ e e' τ,
+    ((x,σ)::Γ |- e \is τ) ->
+    (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
+    ((x,σ)::Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ λ σ ↦morph e }] \is [< σ ->morph τ >] ]] = [{ λ σ ↦morph e' }])
+
+  | Expand_App : forall Γ f f' a a' m σ τ σ',
+    (Γ |- f \is [< σ -> τ >]) ->
+    (Γ |- a \is σ') ->
+    (Γ |- σ' ~~> σ) ->
+    (Γ |- [[ f \is [< σ -> τ >] ]] = f') ->
+    (Γ |- [[ a \is σ' ]] = a') ->
+    (Γ |- [[ σ' ~~> σ ]] = m) ->
+    (Γ |- [[ [{ f a }] \is τ ]] = [{ f' (m a') }])
+
+  | Expand_MorphFun : forall Γ f f' σ τ,
+    (Γ |- f \is [< σ ->morph τ >]) ->
+    (Γ |- f \is [< σ -> τ >]) ->
+    (Γ |- [[ f \is [< σ ->morph τ >] ]] = f') ->
+    (Γ |- [[ f \is [< σ -> τ >] ]] = f')
+
+  | Expand_Ascend : forall Γ e e' τ τ',
+    (Γ |- e \is τ) ->
+    (Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ e as τ' }] \is [< τ' ~ τ >] ]] = [{ e' as τ' }])
+
+  | Expand_Descend : forall Γ e e' τ τ',
+    (Γ |- e \is τ) ->
+    (τ :<= τ') ->
+    (Γ |- [{ e des τ' }] \is τ') ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ e \is τ' ]] = [{ e' des τ' }])
+
+where "Γ '|-' '[[' e '\is' τ ']]' '=' f" := (translate_typing Γ e τ f).