Library finprod


Require Import Setoid.
Require Import List.
Require Import NArith.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import cpo.
Require Import profinite.

Require Import atoms.
Require Import permutations.

Finite products for type contexts

First, a short development of cast morphisms. These are useful for dealing wiht cases where we have types that are provably equal, but not convertable.
Section cast.
  Variable hf:bool.
  Variable A:Type.
  Variable F:A -> PLT.PLT hf.

  Definition cast_rel (x y:A) (H:x = y) : erel (F x) (F y) :=
    esubset_dec
      (PLT.prod (F x) (F y))
      (fun xy => eq_rect x F (fst xy) y H snd xy)
      (fun xy => eff_ord_dec _ (PLT.effective (F y)) _ _)
      (eprod (eff_enum _ (PLT.effective (F x))) (eff_enum _ (PLT.effective (F y)))).

  Lemma cast_rel_elem (x y:A) (H:x = y) a b :
    (a,b) cast_rel x y H <-> eq_rect x F a y H b.

  Program Definition cast (x y:A) (H:x = y) : F x F y :=
    PLT.Hom hf (F x) (F y) (cast_rel x y H) _ _.

  Lemma cast_refl x :
    cast x x (Logic.eq_refl x) id (F x).

  Lemma cast_compose x y z H1 H2 :
    cast y z H2 cast x y H1 cast x z (Logic.eq_trans H1 H2).

  Lemma cast_iso1 x y H :
    cast y x (eq_sym H) cast x y H id.

  Lemma cast_iso2 x y H :
    cast x y H cast y x (eq_sym H) id.

  Hypothesis Adec : forall (x y:A), {x=y}+{x<>y}.

  Lemma cast_dec_id : forall x (H:x=x), cast x x H id.
End cast.

Definition maybe A B (b:B) (f:A->B) (x:option A) : B :=
  match x with
  | None => b
  | Some x => f x
  end.

The input module type for contexts. Type I is the index type, but type A are proxies for object language types. The functon F interprets the types A as objects of PLT.
Module Type FINPROD_INPUT.
  Parameter Inline A:Type.
  Parameter Inline Adec : forall x y:A, {x=y}+{x<>y}.
  Parameter Inline F: A -> PLT.
End FINPROD_INPUT.

This module type provides an object of contexts, which is the universal object for finite collections of objects.
These are designed specifically to handle contexts of typed λ-calculi.
Module Type FINPROD.
  Parameter Inline A:Type.
  Parameter Inline Adec : forall x y:A, {x=y}+{x<>y}.
  Parameter Inline F: A -> PLT.

  Fixpoint lookup (i:atom) (l:list (atom*A)) : option A :=
    match l with
    | nil => None
    | (i',a)::l' =>
         match string_dec i' i with
         | left Hi => Some a
         | right _ => lookup i l'
         end
    end.

  Lemma lookup_eq : forall i i' a ls,
    i = i' ->
    Some a = if string_dec i i' then Some a else lookup i' ls.

  Lemma lookup_neq : forall i i' a ls,
    i <> i' ->
    lookup i' ls = if string_dec i i' then Some a else lookup i' ls.

  Definition ty (a:option A) : PLT := maybe 1 F a.

  Parameter finprod : list (atom*A) -> PLT.
  Parameter proj : forall ls i, finprod ls ty (lookup i ls).
  Parameter mk_finprod : forall ls (X:PLT),
       (forall i, X ty (lookup i ls)) -> X finprod ls.

  Definition bind ls i a : finprod ls × F a finprod ((i,a)::ls) :=
   mk_finprod ((i,a)::ls) (finprod ls × F a)
   (fun i' =>
     match string_dec i i' as Hi return
       (finprod ls × F a) ty (if Hi then Some a else lookup i' ls)
     with
     | left _ => π
     | right _ => proj ls i' π
     end).

  Lemma unbind_lemma ls i i' : lookup i ls = None -> i = i' -> None = lookup i' ls.

  Definition unbind ls i a (Hi:lookup i ls = None) :
    finprod ((i,a)::ls) finprod ls :=

    mk_finprod ls (finprod ((i,a)::ls))
     (fun i' =>
       match string_dec i i' as Hi return
         ty (if Hi then Some a else lookup i' ls) ty (lookup i' ls)
       with
       | left H => cast ty (unbind_lemma ls i i' Hi H) PLT.terminate _ _
       | right _ => id
       end proj ((i,a)::ls) i').

  Axiom finprod_proj_commute : forall ls i X f,
    proj ls i mk_finprod ls X f f i.

  Axiom finprod_universal : forall ls X f (z:X finprod ls),
    (forall i, proj ls i z f i) -> z mk_finprod ls X f.

  Axiom bind_unbind : forall ls i a Hi,
    unbind ls i a Hi bind ls i a π.

  Axiom proj_bind_neq : forall i a i' ls (Hneq:i <> i'),
    proj ((i,a)::ls) i' bind ls i a
       cast ty (lookup_neq i i' a ls Hneq) proj ls i' π.

  Axiom proj_bind_eq : forall i a i' ls (Heq:i = i'),
    proj ((i,a)::ls) i' bind ls i a
       cast ty (lookup_eq i i' a ls Heq) π.

  Axiom proj_bind : forall i a i' ls,
    proj ((i,a)::ls) i' bind ls i a
    match string_dec i i' as H return
      finprod ls × F a ty (if H then Some a else lookup i' ls)
    with
    | left Heq => π
    | right Hneq => proj ls i' π
    end.

  Axiom mk_finprod_compose_commute : forall ls X Y f (h:X Y),
    mk_finprod ls Y f h
    mk_finprod ls X (fun i => f i h).

End FINPROD.

Module finprod (FI:FINPROD_INPUT) <: FINPROD.
  Include FI.

  Fixpoint lookup (i:atom) (l:list (atom*A)) : option A :=
    match l with
    | nil => None
    | (i',a)::l' =>
         match string_dec i' i with
         | left Hi => Some a
         | right _ => lookup i l'
         end
    end.

  Lemma lookup_app i l1 l2 :
    lookup i (l1++l2) =
    match lookup i l1 with
    | None => lookup i l2
    | Some a => Some a
    end.

  Lemma lookup_eq : forall i i' a ls,
    i = i' ->
    Some a = if string_dec i i' then Some a else lookup i' ls.

  Lemma lookup_neq : forall i i' a ls,
    i <> i' ->
    lookup i' ls = if string_dec i i' then Some a else lookup i' ls.

  Definition ty (a:option A) : PLT := maybe 1 F a.

  Module internals.

  Inductive finprod_codom (avd:list atom) z i :=
    | codom_avoid : In i avd -> finprod_codom avd z i
    | codom_elem : ~In i avd -> ty z -> finprod_codom avd z i.

  Definition finprod_elem (avd:list atom) ls :=
    forall i, finprod_codom avd (lookup i ls) i.

  Definition finprod_codom_ord avd z i (x y:finprod_codom avd z i) :=
      match x, y with
      | codom_avoid _, codom_avoid _ => True
      | codom_elem _ a, codom_elem _ b => a b
      | _, _ => False
      end.

  Program Definition finprod_codom_ord_mixin avd z i :
    Preord.mixin_of (finprod_codom avd z i) :=
    Preord.Mixin (finprod_codom avd z i) (finprod_codom_ord avd z i) _ _.

  Canonical Structure codom avd z i :=
    Preord.Pack (finprod_codom avd z i) (finprod_codom_ord_mixin avd z i).

  Definition codom_enum avd z i (n:N) : option (finprod_codom avd z i) :=
    match In_dec string_dec i avd with
    | left Hin => Some (codom_avoid Hin)
    | right Hnin =>
        match eff_enum _ (PLT.effective (ty z)) n with
        | None => None
        | Some x => Some (codom_elem Hnin x)
        end
    end.

  Program Definition codom_eff avd z i : effective_order (codom avd z i)
   := EffectiveOrder (codom avd z i) _ (codom_enum avd z i) _.

  Definition codom_out avd z i (Hnin:~In i avd)
    (x:codom avd z i) : ty z :=
    match x with
    | codom_avoid H => False_rect _ (Hnin H)
    | codom_elem H x => x
    end.

  Program Definition codom_out' avd z i (Hnin:~In i avd) :
    Preord.hom (codom avd z i) (ty z)
    :=
    Preord.Hom _ _ (codom_out avd z i Hnin) _.

  Program Definition codom_in' avd z i (Hnin:~In i avd) :
    Preord.hom (ty z) (codom avd z i)
    := Preord.Hom _ _ (@codom_elem avd z i Hnin) _.

  Lemma codom_has_normals avd z i : has_normals (codom avd z i) (codom_eff avd z i) false.

  Definition codom_plotkin avd z i : plotkin_order false (codom avd z i)
    := norm_plt (codom avd z i) (codom_eff avd z i) false (codom_has_normals avd z i).

  Definition finprod_ord avd l (x y:finprod_elem avd l) :=
    forall i, x i y i.

  Program Definition finprod_ord_mixin avd l : Preord.mixin_of (finprod_elem avd l) :=
    Preord.Mixin (finprod_elem avd l) (finprod_ord avd l) _ _.

  Canonical Structure ord avd l :=
    Preord.Pack (finprod_elem avd l) (finprod_ord_mixin avd l).

  Definition finprod_dec l avd (x y:finprod_elem avd l) : {xy}+{xy}.

  Definition f_hd i a ls avd
    (f:finprod_elem avd ((i,a)::ls)) : finprod_codom avd (Some a) i :=
      match string_dec i i as Hi
        return finprod_codom avd (if Hi then (Some a) else lookup i ls) i ->
               finprod_codom avd (Some a) i
      with
      | left Hi => fun x => x
      | right Hn => False_rect _ (Hn (Logic.eq_refl i))
      end (f i).

  Definition f_tl i a (ls:list (atom*A)) (avd:list atom)
    (f:finprod_elem avd ((i,a)::ls)) : finprod_elem (i::avd) ls :=
    
    fun i' =>
      match f i' with
      | codom_avoid H => @codom_avoid (i::avd) _ i' (or_intror H)
      | codom_elem H x =>
         match string_dec i i' as Hi return
           ty (if Hi then Some a else lookup i' ls) ->
             finprod_codom (i::avd) (lookup i' ls) i'
         with
         | left Hi => fun _ => @codom_avoid (i::avd) _ i' (or_introl Hi)
         | right Hn => fun x' => @codom_elem (i::avd) _ i' (or_ind Hn H) x'
         end x
      end.

  Definition f_cons i a (ls:list (atom*A)) (avd:list atom)
    (h:finprod_codom avd (Some a) i)
    (f:finprod_elem (i::avd) ls) : finprod_elem avd ((i,a)::ls) :=

    fun i' =>
      match in_dec string_dec i' avd with
      | left Hin => codom_avoid Hin
      | right Hnin => @codom_elem avd _ i' Hnin
         match string_dec i i' as Hi
           return ty (if Hi then Some a else lookup i' ls)
         with
         | left Hi =>
             match h with
             | codom_avoid H => False_rect _ (Hnin (eq_rect i (fun i => In i avd) H i' Hi))
             | codom_elem H x => x
             end
         | right Hn =>
             match f i' with
             | codom_avoid H => False_rect _ (or_ind Hn Hnin H)
             | codom_elem H x => x
             end
         end
      end.

  Lemma f_cons_mono i a ls avd
    hd hd' (tl tl':ord (i::avd) ls) :
    hd hd' ->
    tl tl' ->
    f_cons i a ls avd hd tl f_cons i a ls avd hd' tl'.

  Lemma f_cons_reflects1 i a ls avd
    hd hd' (tl tl':ord (i::avd) ls) :
    f_cons i a ls avd hd tl f_cons i a ls avd hd' tl' ->
    hd hd'.

  Lemma f_cons_reflects2 i a ls avd
    hd hd' (tl tl':ord (i::avd) ls) :
      f_cons i a ls avd hd tl f_cons i a ls avd hd' tl' ->
      tl tl'.

  Lemma f_cons_hd_tl i a ls avd
    (f:ord avd ((i,a)::ls)) :
    forall (hd:codom avd (Some a) i) (tl : ord (i::avd) ls),
      hd f_hd i a ls avd f ->
      tl f_tl i a ls avd f ->
      f f_cons i a ls avd hd tl.

  Fixpoint enum_finprod (ls:list (atom*A)) (avd:list atom) (z:N) :
    option (finprod_elem avd ls) :=

    match ls as ls' return option (finprod_elem avd ls') with
    | nil => Some (fun i:atom =>
          match in_dec string_dec i avd with
            | left Hin => codom_avoid Hin
            | right Hnin => @codom_elem avd None i Hnin tt
          end)
    | (i,a)::ls' =>
       match in_dec string_dec i avd with
       | left IN =>
         match enum_finprod ls' (i::avd) z with
         | None => None
         | Some f => Some (f_cons i a ls' avd (codom_avoid IN) f)
         end
       | right NIN =>
         let (p,q) := pairing.unpairing z in
         match enum_finprod ls' (i::avd) q with
         | None => None
         | Some f =>
             match eff_enum _ (PLT.effective (F a)) p with
             | None => None
             | Some xi => Some (f_cons i a ls' avd (@codom_elem avd (Some a) i NIN xi) f)
             end
         end
      end
    end.

  Lemma enum_finprod_complete ls : forall avd (f:finprod_elem avd ls),
    f (enum_finprod ls avd : eset (ord avd ls)).

  Program Definition finprod_effective avd ls : effective_order (ord avd ls) :=
    EffectiveOrder (ord avd ls) (finprod_dec ls avd) (enum_finprod ls avd)
      (enum_finprod_complete ls avd).

  Program Definition f_cons' i a ls avd :
    Preord.hom
     (codom avd (Some a) i × ord (i::avd) ls)%cat_ob
     (ord avd ((i,a)::ls))
    :=
    Preord.Hom _ _ (fun hf => f_cons i a ls avd (fst hf) (snd hf)) _.

  Program Definition f_hd' i a ls avd :
    Preord.hom (ord avd ((i,a)::ls)) (codom avd (Some a) i)
    :=
    Preord.Hom _ _ (f_hd i a ls avd) _.

  Program Definition f_tl' i a ls avd :
    Preord.hom (ord avd ((i,a)::ls)) (ord (i::avd) ls)
    :=
    Preord.Hom _ _ (f_tl i a ls avd) _.

  Lemma finprod_has_normals ls avd :
    has_normals (ord avd ls) (finprod_effective avd ls) false.

  Definition finprod_plotkin ls avd : plotkin_order false (ord avd ls) :=
    norm_plt (ord avd ls) (finprod_effective avd ls) false (finprod_has_normals ls avd).

  Canonical Structure finprod ls avd : PLT :=
    PLT.Ob false (finprod_elem avd ls)
      (PLT.Class _ _
        (finprod_ord_mixin avd ls)
        (finprod_effective avd ls)
        (finprod_plotkin ls avd)).

  Definition empty_cxt_rel (X:PLT) : erel X (finprod nil nil) :=
    eprod (eff_enum _ (PLT.effective X)) (enum_finprod nil nil).

  Program Definition empty_ctx (X:PLT) : X finprod nil nil :=
    PLT.Hom false X (finprod nil nil) (empty_cxt_rel X) _ _.

  Definition proj_rel ls avd (i:atom) (Hnin:~In i avd)
    : erel (finprod ls avd) (ty (lookup i ls)) :=
    esubset_dec
      (ord avd ls × ty (lookup i ls))%cat_ob
      (fun fx => fst fx i @codom_elem avd (lookup i ls) i Hnin (snd fx))
      (fun x => eff_ord_dec _ (codom_eff avd (lookup i ls) i) _ _)
      (eprod (eff_enum _ (PLT.effective (finprod ls avd)))
             (eff_enum _ (PLT.effective (ty (lookup i ls))))).

  Lemma proj_rel_elem ls avd (i:atom) Hnin f x :
    (f,x) proj_rel ls avd i Hnin <-> f i @codom_elem avd (lookup i ls) i Hnin x.

  Program Definition proj ls avd i Hnin : finprod ls avd ty (lookup i ls) :=
    PLT.Hom false (finprod ls avd) (ty (lookup i ls)) (proj_rel ls avd i Hnin) _ _.

  Definition finprod_codom_weaken avd z i i'
    (x:finprod_codom avd z i) : finprod_codom (i'::avd) z i :=
    match x with
    | codom_avoid H => @codom_avoid (i'::avd) z i (or_intror H)
    | codom_elem H x =>
        match string_dec i' i with
        | left Hi => @codom_avoid (i'::avd) z i (or_introl Hi)
        | right Hn => @codom_elem (i'::avd) z i (or_ind Hn H) x
        end
    end.

  Definition ord_weaken avd i a ls
    (x:ord avd ((i,a)::ls)) : ord (i::avd) ls :=
    
    fun i' =>
      match string_dec i i' as Hi return
        finprod_codom avd (if Hi then Some a else lookup i' ls) i' ->
        finprod_codom (i::avd) (lookup i' ls) i'
      with
      | left H => fun _ => @codom_avoid (i::avd) _ i' (or_introl H)
      | right H => finprod_codom_weaken avd _ _ _
      end (x i').

  Program Definition finprod_univ_rel
      (ls:list (atom*A))
      (avd:list atom)
      (X:PLT)
      (f:forall i, ~In i avd -> X ty (lookup i ls))
      (Hf : forall i H1 H2, f i H1 f i H2) :=
      esubset
        (fun q : (PLT.ord X × ord avd ls)%cat_ob =>
          forall i Hnin, exists h,
               (fst q, h) PLT.hom_rel (f i Hnin) /\
               snd q i @codom_elem avd (lookup i ls) i Hnin h)
        _
        (eprod (eff_enum _ (PLT.effective X))
               (eff_enum _ (PLT.effective (finprod ls avd)))).

  Section finprod_univ_rel.
    Variable ls:list (atom*A).
    Variable avd:list atom.
    Variable X:PLT.
    Variable f:forall i, ~In i avd -> X ty (lookup i ls).
    Variable Hf : forall i H1 H2, f i H1 f i H2.

    Let finprod_univ_rel := finprod_univ_rel ls avd X f Hf.

    Lemma finprod_univ_rel_elem : forall x g,
      (x,g) finprod_univ_rel <->
      forall i Hnin, exists h, (x,h) PLT.hom_rel (f i Hnin) /\
        g i @codom_elem avd (lookup i ls) i Hnin h.

    Program Definition finprod_univ : X finprod ls avd
      := PLT.Hom false X (finprod ls avd) finprod_univ_rel _ _.

    Lemma finprod_univ_commute : forall i Hnin,
      proj ls avd i Hnin finprod_univ f i Hnin.

    Lemma finprod_univ_axiom : forall (z: X finprod ls avd),
      (forall i Hi, proj ls avd i Hi z f i Hi) -> z finprod_univ.

  End finprod_univ_rel.
  End internals.

  Definition finprod ls := internals.finprod ls nil.
  Definition proj ls i := internals.proj ls nil i (fun H => H).
  Definition mk_finprod ls X (f:forall i, X ty (lookup i ls)) : X finprod ls :=
    internals.finprod_univ ls nil X (fun i _ => f i) (fun i H1 H2 => eq_refl _ _).

  Definition empty_cxt_inh : finprod nil :=
    fun i => @internals.codom_elem nil None i (fun H =>H) tt.

  Lemma empty_cxt_le : forall a b : finprod nil, a b.

  Lemma empty_cxt_uniq : forall a b : finprod nil, a b.

  Lemma finprod_proj_commute : forall ls i X f,
    proj ls i mk_finprod ls X f f i.

  Lemma finprod_universal : forall ls X f (z:X finprod ls),
    (forall i, proj ls i z f i) -> z mk_finprod ls X f.

  Definition bind ls i a : finprod ls × F a finprod ((i,a)::ls) :=
   mk_finprod ((i,a)::ls) (finprod ls × F a)
   (fun i' =>
     match string_dec i i' as Hi return
       (finprod ls × F a) ty (if Hi then Some a else lookup i' ls)
     with
     | left _ => π
     | right _ => proj ls i' π
     end).

  Lemma unbind_lemma ls i i' : lookup i ls = None -> i = i' -> None = lookup i' ls.

  Definition unbind ls i a (Hi:lookup i ls = None) :
    finprod ((i,a)::ls) finprod ls :=

    mk_finprod ls (finprod ((i,a)::ls))
     (fun i' =>
       match string_dec i i' as Hi return
         ty (if Hi then Some a else lookup i' ls) ty (lookup i' ls)
       with
       | left H => cast ty (unbind_lemma ls i i' Hi H) PLT.terminate _ _
       | right _ => id
       end proj ((i,a)::ls) i').

  Lemma bind_unbind ls i a Hi :
    unbind ls i a Hi bind ls i a π.

  Lemma proj_bind_neq i a i' ls (Hneq:i <> i') :
    proj ((i,a)::ls) i' bind ls i a
       cast ty (lookup_neq i i' a ls Hneq) proj ls i' π.

  Lemma proj_bind_eq i a i' ls (Heq:i = i') :
    proj ((i,a)::ls) i' bind ls i a
       cast ty (lookup_eq i i' a ls Heq) π.

  Lemma proj_bind : forall i a i' ls,
    proj ((i,a)::ls) i' bind ls i a
    match string_dec i i' as H return
      finprod ls × F a ty (if H then Some a else lookup i' ls)
    with
    | left Heq => π
    | right Hneq => proj ls i' π
    end.

  Lemma mk_finprod_compose_commute ls X Y f (h:X Y) :
    mk_finprod ls Y f h
    mk_finprod ls X (fun i => f i h).

  Definition inenv (Γ:list (string*A)) (x:string) (σ:A) :=
    lookup x Γ = Some σ.

  Definition env_incl (Γ₁ Γ₂:list (atom*A)):=
    forall x τ, inenv Γ₁ x τ -> inenv Γ₂ x τ.

  Definition env := list (atom*A).

  Definition env_supp (Γ:env) := map (@fst atom A) Γ.

  Canonical Structure env_supported :=
    Supported env env_supp.

  Lemma env_incl_wk (Γ₁ Γ₂:env) y σ :
    env_incl Γ₁ Γ₂ ->
    env_incl ((y,σ)::Γ₁) ((y,σ)::Γ₂).

  Lemma weaken_fresh
    (Γ Γ' : env) (σ: A) x' :
    x' Γ' ->
    forall (x : atom) (τ : A),
      inenv Γ' x τ -> inenv ((x', σ) :: Γ') x τ.

  Notation cxt := finprod.
  Notation castty := (cast ty).

  Section varmap.
    Variable tm : env -> A -> Type.
    Variable tm_weaken :
      forall Γ₁ Γ₂ τ, env_incl Γ₁ Γ₂ -> tm Γ₁ τ -> tm Γ₂ τ.
    Variable tm_var : forall Γ a τ (H:inenv Γ a τ), tm Γ τ.

    Definition varmap (Γ₁ Γ₂:env) :=
      forall a τ, inenv Γ₁ a τ -> tm Γ₂ τ.

    Definition extend_map Γ Γ'
      (VAR:varmap Γ Γ') x σ (m:tm Γ' σ) : varmap ((x,σ)::Γ) Γ'.

    Definition weaken_map Γ Γ'
      (VAR:varmap Γ Γ')
      x' σ (Hx:x' Γ') :
      varmap Γ ((x',σ)::Γ')
      
      := fun a τ H =>
        tm_weaken Γ' ((x', σ) :: Γ') τ (weaken_fresh Γ Γ' σ x' Hx) (VAR a τ H).

    Program Definition newestvar Γ x σ : tm ((x,σ)::Γ) σ := tm_var _ x σ _.

    Definition shift_vars Γ Γ' x x' σ
      (Hx:x' Γ')
      (VAR:varmap Γ Γ')
      : varmap ((x,σ)::Γ) ((x',σ)::Γ')

    := extend_map Γ ((x', σ) :: Γ')
        (weaken_map Γ Γ' VAR x' σ Hx)
         x σ (newestvar Γ' x' σ).

    Lemma shift_vars' : forall Γ Γ' x σ,
      let x' := fresh[ Γ' ] in
        varmap Γ Γ' ->
        varmap ((x,σ)::Γ) ((x',σ)::Γ').
  End varmap.

  Definition varmap_denote
    (tm : env -> A -> Type)
    (tm_denote : forall Γ σ, tm Γ σ -> cxt Γ F σ)
    (thingy:env -> atom -> A -> Type)
    (thingy_term : forall Γ x σ, thingy Γ x σ -> tm Γ σ)
  
    (Γ₁ Γ₂:env)
    (VAR:forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ)
    : cxt Γ₂ cxt Γ₁
    := mk_finprod Γ₁ (cxt Γ₂)
         (fun i => match lookup i Γ₁ as a return
                     lookup i Γ₁ = a -> cxt Γ₂ ty a
                   with
                   | None => fun H => PLT.terminate _ _
                   | Some a => fun H => tm_denote _ _ (thingy_term _ _ _ (VAR i a H))
                   end refl_equal).

  Class termmodel (tm:env -> A -> Type) :=
    TermModel
    { tm_var : forall Γ a τ (H:inenv Γ a τ), tm Γ τ
    ; tm_traverse : forall
       (thingy:env -> atom -> A -> Type)
       (thingy_term : forall Γ x σ, thingy Γ x σ -> tm Γ σ)
       (rename_var : env -> atom -> atom)
       (weaken_vars : forall Γ₁ Γ₂ y τ,
          (forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ) ->
          (forall x σ, inenv ((y,τ)::Γ₁) x σ -> thingy ((rename_var Γ₂ y,τ)::Γ₂) x σ))

       (Γ₁ Γ₂:env) (σ:A)
       (VAR:forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ),
       tm Γ₁ σ -> tm Γ₂ σ

    ; tm_denote : forall Γ τ, tm Γ τ -> cxt Γ ty (Some τ)

    ; tm_traverse_correct : forall
         (thingy:env -> atom -> A -> Type)
         (thingy_term : forall Γ x σ, thingy Γ x σ -> tm Γ σ)
         (rename_var : env -> atom -> atom)
         (weaken_vars : forall Γ₁ Γ₂ y τ,
           (forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ) ->
           (forall x σ, inenv ((y,τ)::Γ₁) x σ -> thingy ((rename_var Γ₂ y,τ)::Γ₂) x σ))
         (weaken_sem_bind : forall Γ₁ Γ₂ x σ VAR,
           bind Γ₁ x σ PLT.pair_map (varmap_denote tm tm_denote thingy thingy_term Γ₁ Γ₂ VAR) id
            varmap_denote tm tm_denote thingy thingy_term ((x,σ)::Γ₁) ((rename_var Γ₂ x,σ)::Γ₂)
           (weaken_vars Γ₁ Γ₂ x σ VAR) bind Γ₂ (rename_var Γ₂ x) σ)
         (varmap_denote_proj : forall Γ₁ Γ₂ VAR x σ i,
           tm_denote _ _ (thingy_term Γ₂ x σ (VAR x σ i))
            castty i proj Γ₁ x varmap_denote tm tm_denote thingy thingy_term Γ₁ Γ₂ VAR)

         (Γ₁ Γ₂:env) (σ:A)
         (m:tm Γ₁ σ)
         (VAR : forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ),

         tm_denote _ _ (tm_traverse thingy thingy_term rename_var weaken_vars Γ₁ Γ₂ σ VAR m)
         tm_denote _ _ m varmap_denote tm tm_denote thingy thingy_term Γ₁ Γ₂ VAR

    ; tm_denote_var : forall Γ i (a : A) (H : inenv Γ i a),
         tm_denote Γ a (tm_var Γ i a H) castty H proj Γ i
    }.

  Section termmodel.
    Variable (tm:env -> A -> Type).
    Context {tmmodel:termmodel tm}.

    Definition weaken_denote :
      forall (Γ₁ Γ₂:env)
        (VAR:forall x σ, inenv Γ₁ x σ -> inenv Γ₂ x σ),
        cxt Γ₂ cxt Γ₁

      := varmap_denote tm tm_denote
           (fun Γ x σ => inenv Γ x σ)
           tm_var.

    Definition subst_denote :
      forall (Γ₁ Γ₂:env)
        (VAR:forall x σ, inenv Γ₁ x σ -> tm Γ₂ σ),
        cxt Γ₂ cxt Γ₁

      := varmap_denote tm tm_denote
           (fun Γ x σ => tm Γ σ)
           (fun Γ x σ t => t).

    Definition tm_wk : forall
      (Γ₁ Γ₂:env) (σ:A)
      (H:forall x τ, inenv Γ₁ x τ -> inenv Γ₂ x τ)
      (m:tm Γ₁ σ), tm Γ₂ σ
      := tm_traverse
           (fun Γ x σ => inenv Γ x σ)
           tm_var
           (fun Γ x => x)
           env_incl_wk.

    Definition tm_subst : forall
      (Γ₁ Γ₂:env) (τ:A)
      (VAR:forall x τ, inenv Γ₁ x τ -> tm Γ₂ τ)
      (m:tm Γ₁ τ), tm Γ₂ τ
      := tm_traverse
           (fun Γ x σ => tm Γ σ)
           (fun Γ x σ t => t)
           (fun Γ x => fresh[ Γ ])
           (shift_vars' tm tm_wk tm_var).

    Lemma varmap_extend_bind Γ Γ'
      (VAR:varmap tm Γ Γ') x σ (m:tm Γ' σ) :

      subst_denote _ _ (extend_map tm Γ Γ' VAR x σ m)
      bind Γ x σ subst_denote _ _ VAR, tm_denote _ _ m.

    Lemma varmap_var_id Γ :
      subst_denote Γ Γ (tm_var Γ) id.

    Section varmap_compose.
      Variables Γ₁ Γ₂ Γ₃:env.
      Variable g:varmap tm Γ₂ Γ₃.
      Variable f:varmap tm Γ₁ Γ₂.

      Program Definition varmap_compose : varmap tm Γ₁ Γ₃ :=
        fun a τ (IN:inenv Γ₁ a τ) => tm_subst Γ₂ Γ₃ τ g (f a τ IN).
    End varmap_compose.

    Lemma varmap_compose_denote Γ₁ Γ₂ Γ₃ f g :
      (forall i a e,
        tm_denote Γ₃ a (tm_subst Γ₂ Γ₃ a f (g i a e))
         tm_denote Γ₂ a (g i a e) subst_denote Γ₂ Γ₃ f)
      ->
      subst_denote _ _ (varmap_compose Γ₁ Γ₂ Γ₃ f g)
      subst_denote _ _ g subst_denote _ _ f.

    Program Definition subst (Γ:env) (τ τ:A) (a:atom)
      (m:tm ((a,τ)::Γ) τ) (z:tm Γ τ) : tm Γ τ :=

      tm_subst ((a,τ)::Γ) Γ τ (extend_map tm Γ Γ (tm_var Γ) a τ z) m.

    Lemma subst_soundness_lemma Γ x σ σ n₁ n₂ :
      (forall Γ τ m Γ' (VAR:varmap tm Γ Γ'),
        tm_denote _ _ (tm_subst Γ Γ' τ VAR m)
        tm_denote _ _ m subst_denote Γ Γ' VAR) ->

      tm_denote _ _ n₁ bind Γ x σ id, tm_denote _ _ n₂
      tm_denote _ _ (subst Γ σ σ x n₁ n₂).

    Lemma weaken_map_denote Γ Γ'
      (VAR:varmap tm Γ Γ')
      x' σ (Hx:x' Γ') Hx' :

      (forall Γ a m Γ' H,
        tm_denote _ _ m weaken_denote Γ Γ' H tm_denote _ _ (tm_wk Γ Γ' a H m)) ->

      subst_denote _ _ (weaken_map tm tm_wk Γ Γ' VAR x' σ Hx)
      
      subst_denote _ _ VAR unbind Γ' x' σ Hx'.

Lemma varmap_denote_proj Γ Γ' (VAR:varmap tm Γ Γ') x σ (i1 i2:inenv Γ x σ) :
  tm_denote _ _ (VAR x σ i2) castty i1 proj Γ x subst_denote Γ Γ' VAR.

Lemma bind_weaken Γ Γ' x σ H :
   bind Γ x σ PLT.pair_map (weaken_denote Γ Γ' H) id
    weaken_denote ((x, σ) :: Γ) ((x, σ) :: Γ')
       (env_incl_wk Γ Γ' x σ H) bind Γ' x σ.

Lemma proj_weaken Γ Γ' x σ H i :
   castty i proj Γ x weaken_denote Γ Γ' H
    castty (H x σ i) proj Γ' x.

Lemma varmap_shift_bind (Γ Γ':env) x σ VAR :
  (forall Γ₁ Γ₂ a m H,
    tm_denote Γ₁ a m weaken_denote Γ₁ Γ₂ H
    tm_denote Γ₂ a (tm_wk Γ₁ Γ₂ a H m)) ->

  let x' := fresh[ Γ' ] in
   subst_denote ((x, σ) :: Γ) ((x', σ) :: Γ')
     (shift_vars' tm tm_wk tm_var Γ Γ' x σ VAR)
    bind Γ' x' σ
    bind Γ x σ PLT.pair_map (subst_denote Γ Γ' VAR) id.

Lemma weaken_term_denote Γ a m : forall Γ' VAR,
  tm_denote _ _ (tm_wk Γ Γ' a VAR m)
  tm_denote _ _ m weaken_denote Γ Γ' VAR.

Lemma term_subst_soundness Γ τ m : forall Γ' (VAR:varmap tm Γ Γ'),
  tm_denote _ _ (tm_subst Γ Γ' τ VAR m)
  tm_denote _ _ m subst_denote Γ Γ' VAR.

Lemma subst_soundness Γ x σ σ n₁ n₂ :
  tm_denote _ _ n₁ bind Γ x σ id, tm_denote _ _ n₂
  tm_denote _ _ (subst Γ σ σ x n₁ n₂).
  End termmodel.

End finprod.