(** LamFlatPred.v Version 1.3.1 December 2012 *)
(** does not need impredicative Set, runs under V8.4, tested with version 8.4pl1 *)

(** Copyright Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse*)

(**
    forms part of the code that comes with a submission to the journal
    Science of Computer Programming
 *)

Require Import LNMItPred.
Require Import LNGMItPred.
Require Import List.

Set Implicit Arguments.
Require Import Utf8.

Open Scope type_scope.

Definition LambF(X: k1)(A: Set) := A + X A * X A + X(option A).

Instance lambFpEFct : pEFct LambF.
Proof.
  unfold LambF.
  typeclasses eauto.
Defined.

(*
Print lambFpEFct.
lambFpEFct = 
@sumpEFct (λ (X : k1) (A : k0), A + X A * X A)
  (@sumpEFct (λ (_ : k1) (A : k0), A) (@constpEFct (λ A : k0, A) idEFct)
     (λ (X : k1) (A : k0), X A * X A)
     (@prodpEFct (λ (X : k1) (A : k0), X A) idpEFct_eta
        (λ (X : k1) (A : k0), X A) idpEFct_eta))
  (λ (X : k1) (A : k0), X (option A))
  (@comppEFct (λ X : k1, X) idpEFct (λ (_ : k1) (A : k0), option A)
     (@constpEFct (λ A : k0, option A) optionEFct))
     : pEFct LambF

Expanded type for implicit arguments
lambFpEFct : ∀ X : k1, EFct X → EFct (LambF X)
Argument X is implicit
*)

Definition LamF(X: k1)(A: Set) := LambF X A + X (X A).

Instance lamFpEFct_auto : pEFct LamF.
Proof.
  unfold LamF.
  typeclasses eauto.
Defined.

(*
Print lamFpEFct_auto.
lamFpEFct_auto = 
@sumpEFct LambF lambFpEFct (λ (X : k1) (A : k0), X (X A))
  (@comppEFct (λ X : k1, X) idpEFct (λ (X : k1) (A : k0), X A) idpEFct_eta)
     : pEFct LamF

Expanded type for implicit arguments
lamFpEFct_auto : ∀ X : k1, EFct X → EFct (LamF X)

Argument X is implicit
*)

(** The following lemmas loosely correspond to the definition of the term of type
    [forall (X:k1), mon X -> mon(LamF X)] at the end of Section 4.1. Note
    the use of  [idpEFct] and [idpEFct_eta] in the recursive descriptions. *)

Definition pvar (X: k1)(A: Set)(a: A): LamF X A :=
  inl (X (X A)) (inl (X (option A)) (inl (X A * X A) a)).
(* short: inl _ (inl _ (inl _ a)) *)

Lemma pvar_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(a: A):
  m (EFct:= lamFpEFct_auto ef) f (pvar X a) = pvar X (f a).
Proof.
  reflexivity.
Qed.

(** printing t1 %\ensuremath{t_1}% *)
(** printing t2 %\ensuremath{t_2}% *)
Definition papp (X: k1)(A: Set)(t1 t2: X A ): LamF X A :=
  inl (X (X A)) (inl (X (option A)) (inr A (t1, t2))).
(* short: inl _ (inl _ (inr _ (t1, t2))) *)

Lemma papp_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(t1 t2: X A):
  m (EFct:= lamFpEFct_auto ef) f (papp X A t1 t2) = papp X B (m (EFct:= idpEFct_eta ef) f t1) (m (EFct:= idpEFct_eta ef) f t2).
Proof.
  reflexivity.
Qed.

Definition pabs (X: k1)(A: Set)(r: X (option A)): LamF X A :=
  inl (X (X A)) (inr (A + X A * X A) r).
(* short: inl _ (inr _ r) *)

Lemma pabsE_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(r: X (option A)):
  m (EFct:= lamFpEFct_auto ef) f (pabs X A r) = pabs X B (m (EFct:= idpEFct ef) (option_map f) r).
Proof.
  reflexivity.
Qed.

Definition pflat (X: k1)(A: Set)(ee: X (X A)): LamF X A :=
  inr (LambF X A) ee.
(* short: inr _ ee *)

Lemma pflat_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(ee: X(X A)):
  m (EFct:= lamFpEFct_auto ef) f (pflat X A ee) = pflat X B (m (EFct:= idpEFct ef) (m (EFct:= idpEFct_eta ef) f) ee).
Proof.
  reflexivity.
Qed.

(* the following will work perfectly well, but has the unnecessary expansions, as seen above:
Instance lamFpEFct: pEFct LamF := lamFpEFct_auto.
*)

(** the by-hand definition at the end of Section 4.1 in the paper: *)

Definition lamFpEFct_m (X: k1)(mX: mon X): mon (LamF X).
Proof.
  red.
  (* intros X mX. *)
  red.
  red.
  intros A B f t.
  destruct t as [[[a|( t1, t2)]|r]|e].
  exact (pvar X (f a)).
  exact (papp X B (mX A B f t1) (mX A B f t2)).
  exact (pabs X B (mX (option A) (option B) (option_map f) r)).
  exact (pflat X B (moncomp(mX:= mX)(mY:= mX) A B f e)).
Defined.

(*
Print Instances pEFct.
*)

Definition lamFpEFct: pEFct LamF.
Proof.
  intros X ef.
  exists (lamFpEFct_m (m(EFct:= ef))).
(* ext *)
  red.
  intros.
  destruct ef;
  destruct r as [[[a|( t1, t2)]|r]|ee]; simpl;
  unfold lamFpEFct_m; unfold LNMItPred.map; unfold LNMItPred.m.
  rewrite H.
  reflexivity.
  do 2 rewrite (e _ _ _ _ H).
  reflexivity.
  assert (forall a: option A, option_map f a = option_map g a).
  destruct a.
  unfold option_map.
  simpl.
  rewrite H.
  reflexivity.
  reflexivity.
  rewrite (e _ _ _ _ H0).
  reflexivity.
  f_equal.
  apply e.
  intro.
  apply e.
  assumption.
(* fct1 *)
  red.
  intros.
  destruct ef;
  destruct x as [[[a|( t1, t2)]|r]|ee]; simpl;
  unfold lamFpEFct_m; unfold LNMItPred.map; unfold LNMItPred.m.
  reflexivity.
  do 2 rewrite f1.
  reflexivity.
  assert (forall a: option A, option_map id a = a).
  destruct a.
  unfold option_map.
  reflexivity.
  reflexivity.
  rewrite (e _ _ _ _ H).
  rewrite f1.
  reflexivity.
  assert (forall x: X A, m A A id x = x).
  apply f1.
  fold (pflat X A ee).
  f_equal.
  unfold moncomp.
  rewrite (e _ _ _ _ H).
  apply f1.
(* fct2 *)
  red.
  intros.
  destruct ef;
  destruct x as [[[a|( t1, t2)]|r]|ee]; simpl;
  unfold lamFpEFct_m; unfold LNMItPred.map; unfold LNMItPred.m; simpl.
  reflexivity.
  do 2 rewrite f2.
  reflexivity.
  assert (forall a: option A, option_map (g o f) a = ((option_map g) o (option_map f)) a).
  destruct a.
  unfold option_map.
  reflexivity.
  reflexivity.
  rewrite (e _ _ _ _ H).
  rewrite f2.
  reflexivity.
  assert (forall x: X A, m A C (g o f) x = ((m B C g) o (m A B f)) x).
  apply f2.
  unfold moncomp.
  rewrite (e _ _ _ _ H).
  rewrite f2.
  reflexivity.
Defined.

Existing Instance lamFpEFct.

(*
Print Instances pEFct.
*)

(** the obvious consequence *)

Lemma lamFpEFctlamFpEFct_m (X: k1)(ef: EFct X): @m _ (lamFpEFct ef) = lamFpEFct_m (@m _ ef).
Proof.
  reflexivity.
Qed.

(** some preparations for lists *)

(** [listk1] is needed because of sort polymorphism *)

Definition listk1 (A: Set) : Set := list A.


Fixpoint filterSome (A: Type)(l: list(option A)){struct l} : list A :=
  match l with nil => nil
     | None :: rest => filterSome rest
     | Some a :: rest => a :: filterSome rest
  end.

Lemma filterSomeIn (A: Type)(a: A)(l: list(option A)):
   In (Some a) l <-> In a (filterSome l).
Proof.
  intros.
  split.
  intro.
  induction l.
  inversion H.
  destruct a0.
  elim (in_inv H).
  intro.
  inversion H0.
  simpl.
  left.
  reflexivity.
  intro.
  simpl.
  right.
  apply IHl.
  assumption.
  simpl.
  apply IHl.
  simpl in H.
  destruct H.
  inversion H.
  assumption.
(* the other direction *)
  intros.
  induction l.
  inversion H.
  destruct a0.
  simpl in H.
  destruct H.
  rewrite H.
  simpl.
  left.
  reflexivity.
  simpl.
  right.
  apply IHl.
  assumption.
  simpl.
  right.
  apply IHl.
  simpl in H.
  assumption.
Qed.


Instance listmap: LNMItPred.mon listk1.
Proof.
  exact map.
Defined.

Definition optionk1 (A: Set) : Set := option A.

Instance filterSomeNAT: NAT filterSome (mX:= moncomp(X:= listk1)(Y:= optionk1)(mX:= map)(mY:= option_map))(Y:= listk1).
Proof.
  red.
  intros.
  unfold LNMItPred.map.
  induction t. (* if there are no arguments (X:=listk1)(Y:=optionk1), this will raise an error for bad typing:
Error: Abstracting over the term "t" leads to a term
"fun t : list (option A) =>
 @filterSome B
   (@moncomp list (fun A B : Set => @map A B) option
      (fun A B : Set => @option_map A B) A B f t) =
 @listmap A B f (@filterSome A t)" which is ill-typed.
This also holds of Coq 8.2-1.
*)
  reflexivity.
  destruct a.
  simpl.
  rewrite <- IHt.
  reflexivity.
  simpl.
  rewrite <- IHt.
  reflexivity.
Qed. (* if (Y:= listk1) is not given in the formulation of the lemma, this will raise a type error *)



Lemma flat_mapext (A B: Set)(f g: A -> list B)(l: list A): 
   (forall a, f a = g a) -> flat_map f l = flat_map g l.
Proof.
  intros.
  induction l; intros; simpl.
  reflexivity.
  rewrite H.
  rewrite IHl.
  reflexivity.
Qed.

(** interaction of [flat_map] with [map] *)
(** printing o %\ensuremath{\circ}% *)

Lemma flat_mapLaw1 (A B C: Set)(f: A -> B)(g: B -> list C)(l: list A): 
  flat_map g (map f l) = flat_map (g o f) l.
Proof.
  intros.
  induction l; intros; simpl.
  reflexivity.
  rewrite IHl.
  reflexivity.
Qed.  

(** an instructive instance, but not needed in the sequel: *)

Lemma flat_mapLaw1Inst (A B: Set)(f: A -> list B)(l: list A): 
  flat_map (id(A:= list B)) (map f l) = flat_map f l.
Proof.
  intros.
  rewrite flat_mapLaw1.
  apply flat_mapext.
  reflexivity.
Qed.

 Lemma flat_mapLaw2 (A B C : Set) (f : A -> list B) (g : B -> C) (l : list A):
  map g (flat_map f l) = flat_map (map g o f) l.
Proof.
  intros.
  induction l; intros; simpl.
  reflexivity.
  rewrite map_app.
  rewrite IHl.
  reflexivity.
Qed.  

(** we use [moncomp] from [LNMItPred.v] *)
(** printing c_k1 %\ensuremath{\subseteq}% *)

Lemma flat_mapNAT (X: k1)(mX: mon X)(h: X c_k1 listk1)(n: NAT h (mX:= mX) (mY:= map)): NAT(Y:= listk1) (fun A => flat_map (h A)) (mX:= moncomp(X:= listk1)(mX:= map)(mY:= mX)) (mY:= map).
Proof.  
  red.
  intros.
  transitivity (flat_map (map f o h A) t).
  unfold LNMItPred.map.
  unfold moncomp.
  rewrite flat_mapLaw1.
  apply (flat_mapext(B:= B) (h B o mX A B f) (map f o h A) t).
  intro.
  unfold comp.
  unfold NAT in n.
  exact (n A B f a).
(* the second part *)
  apply sym_eq.
  exact (flat_mapLaw2 (h A) f t).
Qed.


Module Type LAM := LNGMIt_Type with Definition LNM.F:= LamF
                               with Definition LNM.FpEFct := lamFpEFct.

Module LamFlat (LamBase: LAM).


Module LamM := LNGMItDef LamBase.
Module LamMMItDef := LamM.LNMItDef.

Definition Lam : k1 := LamBase.mu2.

(** the canonical datatype constructors *)

Definition var (A: Set)(a: A): Lam A :=  
  LamMMItDef.InCan (inl _ (inl _ (inl _ a))).

(** printing t1 %\ensuremath{t_1}% *)
(** printing t2 %\ensuremath{t_2}% *)

Definition app (A: Set)(t1 t2: Lam A): Lam A := 
  LamMMItDef.InCan (inl _ (inl _ (inr _ (t1, t2)))).

(** there is a conflict with [List.app]! *)
(** printing s1 %\ensuremath{s_1}% *)
(** printing s2 %\ensuremath{s_2}% *)

Lemma app_cong(A: Set)(s1 s2 t1 t2: Lam A):
  s1 = t1 -> s2 = t2 -> app s1 s2 = app t1 t2.
Proof.
  intros.
  rewrite H.
  rewrite H0.
  reflexivity.
Qed.

Definition abs (A: Set)(r: Lam(option A)): Lam A := LamMMItDef.InCan (inl _ (inr _ r)).

Definition flat (A: Set)(ee: Lam(Lam A)): Lam A := LamMMItDef.InCan (inr _ ee).


(** lists of free variables of lambda terms, just with plain Mendler iteration
   see Section 2.2 in the paper *)

Definition FV : Lam c_k1 listk1. 
Proof.
  refine (LamBase.MIt (fun (X: k1)(it: X c_k1 listk1)(A: Set)(t: LamF X A) => _)).
  destruct t as [[[a|( t1, t2)]|r]|e].
  exact (a::nil).
  exact (it _ t1 ++ it _ t2).
  exact (filterSome (it _ r)).
  exact (flat_map(it A)(it (X A) e)).
Defined.

Definition sFV := fun (X : k1) (it : X c_k1 listk1) (A : Set) (t : LamF X A) =>
   match t with
   | inl (inl (inl a)) => a :: nil
   | inl (inl (inr (pair t1 t2))) => it A t1 ++ it A t2
   | inl (inr r) => filterSome (it (option A) r)
   | inr e => flat_map (it A) (it (X A) e)
   end.

Lemma sFV_ok: FV = LamBase.MIt sFV.
Proof.
  reflexivity.
Qed.


Lemma FV_var (A: Set)(a: A): FV(var a) = a :: nil.
Proof.
  intros.
  unfold var.
  unfold FV.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

Lemma FV_app (A: Set)(t1 t2: Lam A): FV(app t1 t2) = FV t1 ++ FV t2.
Proof.
  intros.
  unfold app.
  unfold FV at 1.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

Lemma FV_abs (A: Set)(r: Lam (option A)): FV(abs r) = filterSome (FV r).
Proof.
  intros.
  unfold abs.
  unfold FV at 1.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

Lemma FV_flat (A: Set)(ee: Lam (Lam A)): 
  FV(flat ee) = flat_map (FV(A:= A)) (FV ee).
Proof.
  intros.
  unfold flat.
  unfold FV at 1.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

(** renaming, see Section 2.2 in the paper *)

Instance lam : LNMItPred.mon Lam.   (* it does not suffice with mon *)
Proof.
  exact LamBase.mapmu2.
Defined.

(** behaviour of [lam] on canonical elements *)

Lemma lam_var (A B: Set)(f: A -> B)(a: A) : lam f (var a) = var (f a).
Proof.
  intros.
  unfold lam at 1, var at 1; rewrite LamMMItDef.mapmu2RedCan.
  reflexivity.
Qed.
 
Lemma lam_app (A B: Set)(f: A -> B)(t1 t2: Lam A): 
  lam f (app t1 t2) = app (lam f t1)(lam f t2).
Proof.
  intros.
  unfold lam at 1, app at 1; rewrite LamMMItDef.mapmu2RedCan.
  reflexivity.
Qed.

Lemma lam_abs (A B: Set)(f: A -> B)(r: Lam (option A)): 
  lam f (abs r) = abs (lam (option_map f) r).
Proof.
  intros.
  unfold lam at 1, abs at 1; rewrite LamMMItDef.mapmu2RedCan.
  reflexivity.
Qed.

Lemma lam_flat (A B: Set)(f: A -> B)(ee: Lam (Lam A)): 
  lam f (flat ee) = flat (lam (lam f) ee).
Proof.
  intros.
  unfold lam at 1, flat at 1.
  rewrite LamMMItDef.mapmu2RedCan.
  simpl.
  reflexivity.
Qed.


(** The "interesting question" at the end of Section 2.2 of the paper: *)

Instance FVNAT: NAT FV.
Proof.
  unfold FV.
  apply LamMMItDef.MItNAT.
  red.
  intros.
  destruct t as [[[a|( t1, t2)]|r]|ee];
  induction ef; simpl; unfold LNMItPred.map.
(* var *)
  reflexivity.
(* app *)
  unfold listmap.
  rewrite map_app.
  do 2 rewrite H.
  reflexivity.
(* abs *)
  unfold moncomp.
  rewrite H.
  rewrite <- filterSomeNAT.
  reflexivity.
(* flat *)
  rewrite <- (flat_mapNAT(mX:= m)); try assumption.
  f_equal.
  unfold moncomp at 1.
  rewrite H.
  reflexivity.
Qed.

(** how renaming works on the list of free variables: *)

Corollary FV_ok (A B: Set)(f: A -> B)(t: Lam A): FV(lam f t) = map f (FV t).
Proof.
  intros.
  apply FVNAT.
Qed.

(** towards substitution, see Section 2.3 of the paper *)

Implicit Arguments Some [[A]].

Definition lift (A B: Set)(f: A -> Lam B)(x: option A): Lam(option B) :=
  match x with
    | None => var None
    | Some a => lam Some (f a)
  end.

Definition subst (A B: Set)(f: A -> Lam B)(t: Lam A): Lam B.
Proof.
  revert A B f t. (* new for 8.3 *)
  refine (LamBase.GMIt (H:= Lam)(G:= Lam)(fun (X: k1)(it: X <_{ Lam } Lam)
        (A B: Set)(f: A -> Lam B)(t: LamF X A)=> _)).
  destruct t as [[[a|( t1, t2)]|r]|ee].
  exact (f a).
  exact (app (it _ _ f t1)(it _ _ f t2)).
  exact (abs (it _ _ (lift f) r)).
  exact (flat (it (X A) (Lam B)
            (var(A:= Lam B) o (it A B f)) ee)).
(* not:
  exact (flat (it (X A) (Lam B)
            (it A (Lam B) (var(A:= Lam B) o f)) ee)). *)
Defined.

(* the following definition is just by inspection of the defined subst *)
Definition s_subst :=
  fun (X : k1) (it : X <_{ Lam } Lam) (A B : Set) (f : A -> Lam B)
     (t : LamF X A) =>
   match t with
   | inl (inl (inl a)) => f a
   | inl (inl (inr (pair t1 t2))) => app (it A B f t1) (it A B f t2)
   | inl (inr r) => abs (it (option A) (option B) (lift f) r)
   | inr ee => flat (it (X A) (Lam B) (var (A:= Lam B) o it A B f) ee)
   end.

Lemma s_subst_ok: LamBase.GMIt s_subst = subst.
Proof.
  reflexivity.
Qed.

Lemma subst_var (A B: Set)(f: A -> Lam B)(a: A):
  subst f (var a) = f a.
Proof.
  intros.
  change subst with (LamBase.GMIt s_subst).
  unfold var.
  rewrite LamM.GMItRedCan.
  reflexivity.
Qed.

Lemma substMonad1 (A B: Set)(f: A -> Lam B)(a: A): subst f (var a) = f a.
Proof.
  apply subst_var.
Qed.

Lemma subst_app (A B: Set)(f: A -> Lam B)(t1 t2: Lam A):
  subst f (app t1 t2) = app (subst f t1)(subst f t2).
Proof.
  intros.
  change subst with (LamBase.GMIt s_subst).
  unfold app at 1.
  rewrite LamM.GMItRedCan.
  reflexivity.
Qed.

Lemma subst_abs (A B: Set)(f: A -> Lam B)(r: Lam (option A)):
  subst f (abs r) = abs (subst (lift f) r).
Proof.
  intros.
  change subst with (LamBase.GMIt s_subst).
  unfold abs at 1.
  rewrite LamM.GMItRedCan.
  reflexivity.
Qed.

Lemma subst_flat (A B: Set)(f: A -> Lam B)(ee: Lam(Lam A)):
  subst f (flat ee) = flat (subst (var(A:= Lam B) o (subst f)) ee).
Proof.
  intros.
  change subst with (LamBase.GMIt s_subst).
  unfold flat at 1.
  rewrite LamM.GMItRedCan.
  reflexivity.
Qed.
(** we would have liked to see
  [subst f (flat ee) = flat (lam (subst f) ee)],
  but this would need a full second monad law *)


(** the generic properties of renaming: *)

Lemma lamext: LNMItPred.ext(mX:= lam).
Proof.
  exact LamMMItDef.mapmu2Ext.
Qed.

Lemma lamfct1: fct1(mX:= lam).
Proof.
  exact LamMMItDef.mapmu2Id.
Qed.  
 
Lemma lamfct2 : fct2(mX:= lam).
Proof.
  exact LamMMItDef.mapmu2Comp.
Qed.

(** show that the definition of [subst] qualifies for Theorem 5 in the paper *)

Lemma substpGext: forall (X : k1) (h : X <_{ Lam } Lam), gext h -> gext (s_subst h).
Proof.
  red.  
  intros.
  destruct r as [[[a|( t1, t2)]|r]|ee].
  simpl.
  apply H0.
  simpl.
  do 2 rewrite (H A B f g H0).
  reflexivity.
  simpl.
  rewrite (H (option A) (option B) (lift f) (lift g)).
  reflexivity.
  destruct a.
  simpl.  
  rewrite H0.
  reflexivity.
  reflexivity.
(* flat *)
  simpl.
  f_equal.
  apply H.
  clear ee.
  intro.
  unfold comp.
  f_equal.
  apply H.
  assumption.
Qed.

(** the first item in Theorem 1 in the paper: *)

Lemma substext (A B: Set)(f g: A -> Lam B)(t: Lam A): 
  (forall a, f a = g a) -> subst f t = subst g t.
Proof.
  intros.
  change (subst f t) with (LamBase.GMIt s_subst B f t).
  rewrite (LamM.GMItsExt s_subst substpGext B f g H t).
  reflexivity.
Qed.

(* some preparations for the second item in Theorem 1 in the paper *)

Lemma FV_var_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A): 
  FV (LamBase.In ef n (pvar X a)) = a :: nil.
Proof.
  intros.
  unfold FV.
  rewrite LamBase.MItRed.
  reflexivity.
Qed.

Lemma FV_app_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(t1 t2: X A): 
  FV (LamBase.In ef n (papp X A t1 t2)) = FV (j A t1) ++ FV (j A t2).
Proof.
  intros.
  unfold FV at 1.
  rewrite LamBase.MItRed.
  reflexivity.
Qed.

Lemma FV_abs_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(r: X (option A)): 
  FV (LamBase.In ef n (pabs X A r)) = filterSome (FV (j (option A) r)).
Proof.
  intros.
  unfold FV at 1.
  rewrite LamBase.MItRed.
  reflexivity.
Qed.

Lemma FV_flat_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(ee: X(X A)): FV (LamBase.In ef n (pflat X A ee)) = flat_map (FV(A:= A) o (j A)) (FV (j (X A) ee)).
Proof.
  intros.
  unfold FV at 1.
  rewrite LamBase.MItRed.
  reflexivity.
Qed.


Definition occursFreeIn(A: Set)(a: A)(t: Lam A): Prop := In a (FV t).

Infix "occ" := occursFreeIn (at level 90).


Lemma occ_var (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A):
      a occ (LamBase.In ef n (pvar X a)).
Proof.
  intros.
  unfold occursFreeIn.
  rewrite FV_var_gen.
  left.
  reflexivity.
Qed.

Lemma occ_appl (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A)(t1 t2 : X A): (a occ (j A t1)) -> a occ (LamBase.In ef n (papp X A t1 t2)).
Proof.
  intros.
  unfold occursFreeIn.
  rewrite FV_app_gen.
  apply in_or_app.
  left.
  assumption.
Qed.

Lemma occ_appr (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A)(t1 t2 : X A): (a occ (j A t2)) -> a occ (LamBase.In ef n (papp X A t1 t2)).
Proof.
  intros.
  unfold occursFreeIn.
  rewrite FV_app_gen.
  apply in_or_app.
  right.
  assumption.
Qed.

Lemma occ_abs (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A)(r: X (option A)): ((Some a) occ (j (option A) r)) -> a occ (LamBase.In ef n (pabs X A r)).
Proof.
  intros.
  unfold occursFreeIn.
  rewrite FV_abs_gen.
  apply (proj1 (filterSomeIn _ _) H).
Qed.

(** printing a0 %\ensuremath{a_0}% *)
Lemma occ_flat (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a: X A)(ee: X(X A)):
      occursFreeIn a (j (X A) ee) ->
      forall a0 : A, occursFreeIn a0 (j A a) -> 
         occursFreeIn a0 (LamBase.In ef n (pflat X A ee)).
Proof.
  intros.
  unfold occursFreeIn.
  rewrite FV_flat_gen.
  apply (proj2(in_flat_map (FV(A:=A) o j A) (FV (j _ ee)) a0)).
  exists a.
  split; assumption.
Qed.

(** now the interpretation for canonical terms although not needed for Theorem 1: *)

Lemma occCan_var (A: Set)(a: A): a occ (var a).
Proof.
  intros.
  unfold var, LamMMItDef.InCan.
  apply occ_var.
Qed.

Lemma occCan_appl (A: Set)(a: A)(t1 t2: Lam A): 
      a occ t1 -> a occ (app t1 t2).
Proof.
  intros.
  unfold app, LamMMItDef.InCan.
  apply occ_appl.
  assumption.
Qed.

Lemma occCan_appr (A: Set)(a: A)(t1 t2: Lam A): 
      a occ t2 -> a occ (app t1 t2).
Proof.
  intros.
  unfold app, LamMMItDef.InCan.
  apply occ_appr.
  assumption.
Qed.

Lemma occCan_abs (A: Set)(a: A)(r: Lam(option A)):
      (Some a) occ r -> a  occ (abs r).
Proof.
  intros.
  unfold abs, LamMMItDef.InCan.
  apply occ_abs.
  assumption.
Qed.

Lemma occCan_flat (A: Set)(a: A)(t: Lam A)(ee: Lam(Lam A)):
   a occ t -> t occ ee -> a occ (flat ee).
Proof.
  intros.
  unfold flat, LamMMItDef.InCan.
(*
Check (occ_flat LamMMItDef.mapmu2EFct (j:= fun _ x => x)
  (fun _ _ _ _ => refl_equal _) t ee H0 a H).
*)
  apply (occ_flat LamMMItDef.mapmu2EFct (j:= fun _ x => x)
  (fun _ _ _ _ => refl_equal _) t ee H0 a H).
Qed.


(** the second item in Theorem 1 in the paper: *)

Lemma substext' (A B: Set)(f g: A -> Lam B)(t: Lam A): 
  (forall a, a occ t -> f a = g a) -> subst f t = subst g t.
Proof.
  intros.
  revert B f g H. revert A t.
  refine (LamBase.mu2Ind _ _).
  intros.
  destruct t as [[[a|( t1, t2)]|r]|ee];
  change subst with (LamBase.GMIt s_subst);
  do 2 rewrite LamBase.GMItRed;
  simpl.
(* var *)
  apply H0.
  exact (occ_var ef n a).
(* app *)
  apply app_cong; change (LamBase.GMIt s_subst) with subst.
  unfold comp.  
  apply H.
  intros.
  apply H0.
  apply (occ_appl ef n a).
  assumption.
  unfold comp.  
  apply H.
  intros.
  apply H0.
  apply (occ_appr ef n a).
  assumption.
(* abs *)
  f_equal.
  change (LamBase.GMIt s_subst) with subst.
  unfold comp.  
  apply H.
  intros.
  destruct a.
  simpl.
  rewrite H0.
  reflexivity.
  generalize H1.
  apply (occ_abs ef n a).
  reflexivity.
(* flat *)
  f_equal.
  change (LamBase.GMIt s_subst) with subst.
  unfold comp at 1 4.  
  apply H.
  intros.
  unfold comp.
  f_equal.
  apply H.
  intros.
  apply H0.
  apply (occ_flat ef n a); assumption.    
Qed.  

(** the third item in Theorem 1 in the paper needs one extra lemma: *)

Lemma lift_map (A B C: Set)(a: option A)(f: A -> Lam B)(g: B -> C):
  (lam (option_map g) o lift f) a = lift (lam g o f) a.
Proof.
  intros.
  destruct a.
  unfold comp.
  simpl.
  do 2 rewrite <- lamfct2.
  apply lamext.
  reflexivity.
  unfold comp.
  simpl.
  rewrite lam_var.
  reflexivity.
Qed.

(** the third item in Theorem 1 in the paper: *)

Lemma substGnat1 (A B C : Set) (f : A -> Lam B) (g : B -> C) (t : Lam A):
  lam g (subst f t) = subst (lam g o f) t.
Proof.
  apply (LamM.GMItsNat1 s_subst substpGext).
  red. 
  intros.
  destruct x as [[[a|( t1, t2)]|r]|ee].
  simpl.
  reflexivity.
  simpl s_subst.
  rewrite lam_app.
  do 2 rewrite H0.
  reflexivity.
  simpl s_subst.
  rewrite lam_abs.
  rewrite H0.
  f_equal.
  apply H.
  intro.  
  apply lift_map.
(* flat *)
  simpl s_subst.
  rewrite lam_flat.
  f_equal.
  rewrite H0.
  apply H.
  clear ee.
  intro.
  unfold comp at 1 2 3.
  rewrite lam_var.
  f_equal.
  rewrite H0.
  reflexivity.
Qed.

(** the fourth item in Theorem 1 in the paper: *)

Lemma substGnat2 (A B C: Set)(f: A -> B)(g: B -> Lam C)(t: Lam A): 
  subst g (lam f t) = subst (g o f) t.
Proof.
  apply (LamM.GMItsNat2 s_subst substpGext).
  red.
  intros.
  destruct ef as [m0 e0 f01 f02].
  destruct x as [[[a|( t1, t2)]|r]|ee]; simpl; unfold LNMItPred.map.
  simpl.
  reflexivity.
  do 2 rewrite H0.
  reflexivity.
  unfold moncomp.
  rewrite H0.
  f_equal.
  apply H.
  intro.  
  destruct a; reflexivity.
(* flat *)
  f_equal.
  unfold moncomp at 1.
  rewrite H0.
  apply H.
  clear ee.
  intro.
  unfold comp at 1 2 3.
  f_equal.
  unfold moncomp.
  rewrite H0.
  apply H.
  clear a.
  intro.
  reflexivity.
Qed.

(** just an instance *)

Lemma substLaw (A B: Set)(f: A -> Lam B)(t: Lam A): 
  subst id (lam f t) = subst f t.
Proof.
  intros.
  rewrite substGnat2.
  apply substext.
  reflexivity.
Qed.

(** a more elaborate formulation of naturality *)

Instance substNAT (X: k1)(mX: mon X)(h: X c_k1 Lam)(n: NAT(mX:= mX) h): 
  NAT (fun A => subst (h A)) (mX:= moncomp(mX:= lam)(mY:= mX)).
Proof.
  red.
  intros.
  unfold  LNMItPred.map.
  unfold moncomp.
  rewrite substGnat2.
  rewrite substGnat1.
  apply substext.
  intro.
  unfold comp.
  apply n.
Qed.  

Corollary substNATCor (X: k1)(mX: mon X)(h: X c_k1 Lam)(n: NAT(mX:= mX) h)
     (A B: Set) (f: A -> B)(t : Lam (X A)):
            subst (h B) (lam (mX A B f) t) = lam f (subst (h A) t).
Proof.
  intros.
  rewrite <- (substNAT n).
  reflexivity.
Qed.
 

Definition flatimpl: forall (A: Set), Lam(Lam A) -> Lam A := glessTosub subst.

Instance flatimplNAT: NAT flatimpl (mX:= moncomp(mX:= lam)(mY:= lam)).
Proof.
  apply gnat1gnat2NAT.
  red; intros.
  apply substGnat1.
  red; intros.
  apply substGnat2.
Qed.

(** the fifth item in Theorem 1 in the paper: *)

Lemma substMonad3 (A B C: Set)(f: A -> Lam B)(g: B -> Lam C)(t: Lam A):
  subst g (subst f t) = subst ((subst g) o f) t.
Proof.
  intros.
  revert B C f g. revert A t.
  refine (LamBase.mu2Ind _ _).
  intros.
  destruct t as [[[a|( t1, t2)]|r]|ee];
  change subst with (LamBase.GMIt s_subst);
  repeat rewrite LamBase.GMItRed;
  simpl; change (LamBase.GMIt s_subst) with subst.
(* var *)
  reflexivity.
(* app *)
  rewrite subst_app.
  unfold comp at 1 2.
  do 2 rewrite H.
  reflexivity.
(* abs *)
  rewrite subst_abs.
  unfold comp at 1.
  rewrite H.
  do 3 f_equal.
  unfold comp.
  apply substext.
  clear X ef j n H r.
  intro.
  destruct a.
  simpl.
  rewrite substGnat1.
  rewrite substGnat2.
  reflexivity.
  simpl.
  rewrite substMonad1.
  reflexivity.
(* flat *)
  rewrite subst_flat.
  f_equal.
  unfold comp at 2 5.
  rewrite H.
  apply substext.
  clear ee.
  intro.
  unfold comp.
  rewrite substMonad1.
  f_equal. 
  rewrite H.
(* this is an application of H deep inside the proof *)
  reflexivity.  
Qed.

(** Section 5 of the paper *)

(** preparations for the formula for the list of free variables of [subst f t] *)

(** printing l1 %\ensuremath{l_1}% *)
(** printing l2 %\ensuremath{l_2}% *)

Lemma filterSomeAppend (A: Type)(l1 l2: list(option A)):
  filterSome (l1 ++ l2) = filterSome l1 ++ filterSome l2.
Proof.
  intros.
  induction l1.
  reflexivity.
  destruct a.
  simpl.
  rewrite IHl1.
  reflexivity.
  simpl.
  assumption.
Qed.

Lemma filterSomeMapSome (A: Type)(l: list A):
  filterSome (map (Some(A:= A)) l) = l.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  reflexivity.
Qed.

Lemma filterSomeFV (A: Set)(t: Lam A):
  filterSome (FV (lam Some t)) = FV t.
Proof.
  intros.
  rewrite FV_ok.
  apply filterSomeMapSome.
Qed.
(** this needed naturality of [FV] *)


Lemma FVsubst_aux (A B: Set)(f: A -> Lam B)(t: list(option A)):
  filterSome(flat_map(FV(A:= option B) o lift f) t) = flat_map (FV(A:= B) o f)(filterSome t).
Proof.
  intros.
  induction t.
  reflexivity.
  destruct a.
  simpl.
  unfold comp at 1.
  unfold lift at 1.
  rewrite <- IHt.
  rewrite filterSomeAppend.
  rewrite filterSomeFV.
  reflexivity.
  simpl.
  rewrite <- IHt.
  rewrite filterSomeAppend.
  unfold comp at 1.
  simpl.
  rewrite FV_var.
  reflexivity.
Qed.
(** this needed naturality of [FV] through [filterSomeFV] *)

(** further preparations for the last item of Theorem 1 in the paper: *)

Lemma flat_map_app (A B: Set)(f: A -> list B)(l1 l2: list A): 
  flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2.
Proof.
  intros.
  induction l1.
  reflexivity.
  simpl.
  rewrite IHl1.
  rewrite app_ass.
  reflexivity.
Qed.


(** printing o %\ensuremath{\circ}% *)

Lemma flat_mapMonad3 (A B C : Set) (f : A -> list B) (g : B -> list C) (l : list A):
  flat_map g (flat_map f l) = flat_map ((flat_map g) o f) l.
Proof.
  induction l; intros.
  reflexivity.
  simpl.
  rewrite flat_map_app.
  rewrite IHl.
  reflexivity.
Qed.

(** the last item of Theorem 1 in the paper *)

Lemma FVsubst (A B: Set)(f: A -> Lam B)(t: Lam A):
   FV (subst f t) = flat_map (FV(A:= B) o f) (FV t).
Proof.
  intros.
  revert B f. revert A t.
  refine (LamBase.mu2Ind _ _).
  intros.
  destruct t as [[[a|( t1, t2)]|r]|ee];
  change subst with (LamBase.GMIt s_subst);
  rewrite LamBase.GMItRed;
  simpl; change (LamBase.GMIt s_subst) with subst.
(* var *)
  unfold LambF.
  fold (pvar X a).
  rewrite FV_var_gen.
  simpl.
  rewrite <- app_nil_end.
  reflexivity.
(* app *)
  unfold LambF.
  fold (papp X A t1 t2).
  rewrite FV_app_gen.
  rewrite FV_app.
  rewrite flat_map_app.
  unfold comp at 1 2.
  rewrite (H A t1 B f).
  rewrite (H A t2 B f).
  reflexivity.
(* abs *)
  unfold LambF.
  fold (pabs X A r).
  rewrite FV_abs_gen.
  rewrite FV_abs.
  unfold comp at 1.
  rewrite H.
  rewrite FVsubst_aux. (** here enters naturality of [FV] *)

  reflexivity.
(* flat *)
  fold (pflat X A ee).
  rewrite FV_flat_gen.
  rewrite FV_flat.
  unfold comp at 1.
  rewrite H.
  transitivity (flat_map (FV(A:= B)) (flat_map ((fun b: Lam B => b :: nil) o (subst f o j A)) (FV (j (X A) ee)))).
  f_equal.
  apply flat_mapext.
  intro.
  unfold comp.
  apply FV_var.
  do 2 rewrite flat_mapMonad3.
  apply flat_mapext.
  intro.
  unfold comp.
  simpl.
  rewrite <- app_nil_end.
  apply H.
Qed.

(** its consequence close to the end of Section 2.3 of the paper: *)

Lemma subst_occ (A B: Set)(f: A -> Lam B)(t: Lam A)(b: B):
  b occ (subst f t) -> exists a: A, (a occ t) /\ (b occ f a).
Proof.
  unfold occursFreeIn.
  intros.
  rewrite FVsubst in H.
  destruct (proj1 (in_flat_map (FV(A:= B) o f) (FV t) b) H).
  exists x.
  assumption.
Qed.

(** hereditarily canonical terms *)

(** Definition 3 in the paper *)

Inductive can : forall (A: Set), Lam A -> Prop :=
  | can_var : forall (A: Set)(a: A), can (var a)
  | can_app : forall (A: Set)(t1 t2: Lam A), can t1 -> can t2 -> can(app t1 t2)
  | can_abs : forall (A: Set)(r: Lam(option A)), can r -> can (abs r)
  | can_flat: forall (A: Set)(ee: Lam(Lam A)), 
     can ee -> (forall t:Lam A, t occ ee -> can t) -> can (flat ee).


(** Here comes material that did not form part of the original submission
    of the SCP paper. It was stimulated by a question of one of the referees
    how [can] is related to what will be called [LamP] below. Many thanks
    to the anonymous referee for that. It was easy for me to answer that
    question since I had already studied binary versions of those unary predicates
    before. However, those developments would have led too far from the main
    issue of the paper. *)

Definition optionpred (A: Type)(P: A -> Prop): option A -> Prop.
Proof.
  intros (* A P *) x.
  induction x.
  exact (P a).
  exact True.
Defined.

(* a failed truly nested inductive definition in Coq:

Inductive LamP : forall (A: Set), (A -> Prop) -> Lam A -> Prop :=
  | LamP_var: forall (A: Set)(P: A -> Prop)(a: A), P a -> LamP P (var a)
  | LamP_app: forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP P t1 -> LamP P t2 -> LamP P (app t1 t2)
  | LamP_abs: forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP (optionpred P) r -> LamP P (abs r)
  | LamP_flat: forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP (LamP P) ee -> LamP P (flat ee).
yields:
Error: Non strictly positive occurrence of "LamP" in
 "forall A : Set,
  forall P : A -> Prop,
  forall ee : Lam (Lam A), LamP (Lam A) (LamP A P) ee -> LamP A P (flat ee)".

Without the last clause, this works well and yields the following induction principle:
Check LamP_ind
     : forall Q : forall A : Set, (A -> Prop) -> Lam A -> Prop,
       (forall (A : Set) (P : A -> Prop) (a : A), P a -> Q A P (var a)) ->
       (forall (A : Set) (P : A -> Prop) (t1 t2 : Lam A),
          LamP P t1 -> Q A P t1 -> LamP P t2 -> Q A P t2 -> Q A P (app t1 t2)) ->
       (forall (A : Set) (P : A -> Prop) (r : Lam (option A)),
          LamP (optionpred P) r -> Q (option A) (optionpred P) r -> Q A P (abs r)) ->
       forall (A : Set) (P : A -> Prop) (t : Lam A), LamP P t -> Q A P t.
*)

(** an axiomatic definition of a truly nested inductive predicate on [Lam]: *)

Parameter LamP: forall A: Set, (A -> Prop) -> Lam A -> Prop.
Axiom LamP_var: forall (A: Set)(P: A -> Prop)(a: A), P a -> LamP P (var a).
Axiom LamP_app: forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP P t1 -> LamP P t2 -> LamP P (app t1 t2).
Axiom LamP_abs: forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP (optionpred P) r -> LamP P (abs r).
Axiom LamP_flat: forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP (LamP P) ee -> LamP P (flat ee).
Axiom LamP_ind: forall (Q: forall A: Set, (A -> Prop) -> Lam A -> Prop),
   (forall (A: Set)(P: A -> Prop)(a: A), P a -> Q A P (var a))
-> (forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP P t1 -> Q A P t1 -> LamP P t2 -> Q A P t2 -> Q A P (app t1 t2))
-> (forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP (optionpred P) r -> Q (option A) (optionpred P) r -> Q A P (abs r))
-> (forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP (LamP P) ee -> Q (Lam A) (Q A P) ee -> Q A P (flat ee))
-> forall (A: Set)(P: A -> Prop)(t: Lam A), LamP P t -> Q A P t.

(** the last clause is in plain analogy with the other ones *)

Definition univpred (A: Type): A -> Prop.
Proof.
  intros.
  exact True.
Defined.

(** a variant that is accepted as inductive definition by Coq: *)

Inductive LamP' : forall (A: Set), (A -> Prop) -> Lam A -> Prop :=
  | LamP'_var: forall (A: Set)(P: A -> Prop)(a: A), P a -> LamP' P (var a)
  | LamP'_app: forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP' P t1 -> LamP' P t2 -> LamP' P (app t1 t2)
  | LamP'_abs: forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP' (optionpred P) r -> LamP' P (abs r)
  | LamP'_flat: forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP' (@univpred (Lam A)) ee -> (forall t: Lam A, t occ ee -> LamP' P t) -> LamP' P (flat ee).

Lemma LamP'ImpCan (A: Set)(P: A -> Prop)(t: Lam A): LamP' P t -> can t.
Proof.
  intros.
  induction H.
  apply can_var.
  apply can_app; assumption.
  apply can_abs; assumption.
  apply can_flat; assumption.
Qed.

(* a failed attempt for an analogous lemma:
Lemma LamPImpCan (A: Set)(P: A -> Prop)(t: Lam A): LamP P t -> can t.
Proof.
  intros.
  revert A P t H.
  apply (LamP_ind (fun (A: Set)(P: A -> Prop)(t: Lam A) => can t)); intros.
  apply can_var.
  apply can_app; assumption.
  apply can_abs; assumption.
  apply can_flat; try assumption.
  intros.
  
no hope! but the statement will follow later
*)


Require Import Setoid.
Require Import Morphisms.

Definition subpredicate (A: Type)(P P': A -> Prop):= forall a:A, P a -> P' a.
(* is this not part of the libraries? *)

Add Parametric Morphism (A: Set): (LamP'(A:=A))
  with signature (subpredicate(A:=A)) ==> (subpredicate(A:=Lam A))
  as LamP'_monM.
Proof.
  red.
  intros P P' Hsub t HP.
  induction HP.
  apply LamP'_var.
  apply Hsub.
  assumption.
  apply LamP'_app.
  apply IHHP1; assumption.
  apply IHHP2; assumption.
  apply LamP'_abs.
  apply IHHP.
  red.
  intros.
  induction a.
  simpl.
  apply Hsub.
  assumption.
  exact I.
  apply LamP'_flat.
  assumption.
  intros.
  apply H0; assumption.
Qed.
  
Lemma CanImpLamP'univ (A: Set)(t: Lam A): can t -> LamP' (@univpred A) t.
Proof.
  intros.
  induction H.
  apply LamP'_var.
  red.
  exact I.
  apply LamP'_app; assumption.
  apply LamP'_abs.
  assert (subpredicate (@univpred (option A)) (optionpred (@univpred A))).
  red.
  intros.
  induction a; assumption.
  apply (LamP'_monM H0).
  assumption.
  apply LamP'_flat; assumption.
Qed.

(** thus, the relation between [can] and [LamP'] is rather trivial *)

(* the following lemma will be needed even outside of this digression *)
Lemma occ_var_inv (A: Set)(a b: A): a occ (var b) -> a = b.
Proof.
  intros.
  unfold occursFreeIn in H.
  rewrite FV_var in H.
  destruct H.
  apply sym_eq.
  assumption.
  inversion H.
Qed.

Lemma occ_app_inv (A: Set)(a: A)(t1 t2: Lam A): a occ (app t1 t2) ->
  (a occ t1) \/ (a occ t2).
Proof.
  intros.
  unfold occursFreeIn in H.
  rewrite FV_app in H.
  destruct (in_app_or (FV t1) (FV t2) _ H).
  left.
  assumption.
  right.
  assumption.
Qed.

Lemma occ_abs_inv (A: Set)(a: A)(r: Lam (option A)): 
  a occ (abs r) -> Some a occ r.
Proof.
  intros.
  unfold occursFreeIn in H.
  rewrite FV_abs in H.
  apply (proj2 (filterSomeIn _ _) H).
Qed.

Lemma occ_flat_inv (A: Set)(a: A)(ee: Lam (Lam A)): 
  a occ (flat ee) -> exists t: Lam A, (a occ t) /\ (t occ ee).
Proof.
  intros.
  unfold occursFreeIn in H.
  rewrite FV_flat in H.
  destruct (proj1 (in_flat_map (FV(A:=A)) (FV ee) a) H).
  exists x.
  destruct H0.
  split; assumption.
Qed.  

(** an auxiliary lemma *)

Lemma LamP'_FV (A: Set)(P: A -> Prop)(t: Lam A)(a: A): LamP' P t -> a occ t -> P a.
Proof.
  intros.
  induction H.
  apply occ_var_inv in H0.
  rewrite H0.
  assumption.
  induction (occ_app_inv _ _ _ H0).
  exact (IHLamP'1 a H2).
  exact (IHLamP'2 a H2).
  apply (occ_abs_inv a r) in H0.
  apply (IHLamP' (Some a) H0).
  destruct (occ_flat_inv _ _ H0).
  destruct H3.
  apply (H2 x); assumption.
Qed.

(** for curiosity, an analogous lemma for [LamP]: *)

Lemma LamP_FV (A: Set)(P: A -> Prop)(t: Lam A)(a: A): LamP P t -> a occ t -> P a.
Proof.
  intros.
  revert a H0.
  revert A P t H.
  apply (LamP_ind (fun (A: Set)(P: A -> Prop)(t: Lam A) => forall a:A, a occ t -> P a)); intros.
  apply occ_var_inv in H0.
  rewrite H0.
  assumption.
  induction (occ_app_inv _ _ _ H3).
  exact (H0 a H4).
  exact (H2 a H4).
  apply (occ_abs_inv a r) in H1.
  apply (H0 (Some a) H1).
  destruct (occ_flat_inv _ _ H1).
  destruct H2.
  apply (H0 x); assumption.
Qed.

(** [LamP'] satisfies the last closure rule of [LamP]: *)

Lemma LamP'_flat' (A: Set)(P: A -> Prop)(ee: Lam(Lam A)): LamP' (LamP' P) ee -> LamP' P (flat ee).
Proof.
  intros.
  apply LamP'_flat.
  assert (subpredicate (LamP' P) (@univpred (Lam A))).
  red.
  intros.
  exact I.
  apply (LamP'_monM H0).
  assumption.
  intros.
  apply (LamP'_FV (t:=ee) t); assumption.
Qed.

Lemma LamPImpLamP' (A: Set)(P: A -> Prop)(t: Lam A): LamP P t -> LamP' P t.
Proof.
  intros.
  refine (LamP_ind _ _ _ _ _ H); clear A P t H; intros.
  apply LamP'_var; assumption.
  apply LamP'_app; assumption.
  apply LamP'_abs; assumption.
  apply LamP'_flat'; assumption.
Qed.
  
(** another auxiliary lemma: *)

Lemma CanImpLamP (A: Set)(t: Lam A): can t -> forall P: A -> Prop, (forall a: A, a occ t -> P a) -> LamP P t.
Proof.
  intros (* A t *) Hyp.
  induction Hyp; intros.
  apply LamP_var.
  apply H.
  apply occCan_var.
  apply LamP_app.
  apply IHHyp1.
  intros.
  apply H.
  apply occCan_appl.
  assumption.
  apply IHHyp2.
  intros.
  apply H.
  apply occCan_appr.
  assumption.
  apply LamP_abs.
  apply IHHyp.
  intros.
  induction a.
  simpl.
  apply H.
  apply occCan_abs.
  assumption.
  exact I.
  apply LamP_flat.
  apply IHHyp.
  intros.
  apply H0.
  assumption.
  intros.
  apply H1.
  apply (occCan_flat a0 a); assumption.
Qed.

(** [LamP] satisfies the last closure rule of [LamP']: *)

Lemma LamP_flat' (A: Set)(P: A -> Prop)(ee: Lam(Lam A)): LamP (@univpred (Lam A)) ee -> (forall t: Lam A, t occ ee -> LamP P t) -> LamP P (flat ee).
Proof.
  intros.
  apply CanImpLamP.
  apply can_flat.
  apply (LamP'ImpCan(P:=@univpred (Lam A))).
  apply LamPImpLamP'.
  assumption.
  intros.
  apply (LamP'ImpCan(P:= P)).
  apply LamPImpLamP'.
  apply H0.
  assumption.
  intros.
  apply occ_flat_inv in H1.
  destruct H1.
  destruct H1.
  assert (LamP P x).
  apply H0; assumption.
  apply LamPImpLamP' in H3.
  apply (LamP'_FV a H3 H1).
Qed.

Lemma LamP'ImpLamP (A: Set)(P: A -> Prop)(t: Lam A): LamP' P t -> LamP P t.
Proof.
  intros.
  refine (LamP'_ind _ _ _ _ _ H); clear A P t H; intros.
  apply LamP_var; assumption.
  apply LamP_app; assumption.
  apply LamP_abs; assumption.
  apply LamP_flat'; assumption.
Qed.

(** Section 5.1 of the paper *)

(** we are only able to prove a weakened version of the
      second monad law, namely Lemma 8 in the paper: *)

Lemma substMonad2 (A: Set)(t: Lam A): can t -> subst (var(A:= A)) t = t.
Proof.
  intros (* A t *) H.
  induction H.
  rewrite substMonad1.
  reflexivity.
(* app *)
  rewrite subst_app.
  rewrite IHcan1.
  rewrite IHcan2.
  reflexivity.
(* abs *)
  rewrite subst_abs.
  replace (subst (lift (var (A:= A))) r) with (subst (var (A:= option A)) r).
Focus 2.
  apply substext.
  intro.
  destruct a.
  simpl.
  rewrite lam_var.
  reflexivity.
  reflexivity.
(* back *) 
  rewrite IHcan.
  reflexivity.
(* flat *)
  rewrite subst_flat.
  f_equal.
  transitivity (subst (var (A:= Lam A)) ee).
  apply substext'.
  intros t Hyp.
  unfold comp.
  f_equal.
  apply H1.
  assumption.
  assumption.
Qed.

Lemma lamext_refined (A B: Set)(f g: A -> B)(t: Lam A):
  can t -> (forall a, a occ t -> f a = g a) -> lam f t = lam g t.
Proof.
  intros.
  revert B f g H0.
(* induction over being canonical: *)
  induction H; intros.
  do 2 rewrite lam_var.
  rewrite H0.
  reflexivity.
  apply occCan_var.
  do 2 rewrite lam_app.
  apply app_cong.
  apply IHcan1.
  intros.
  apply H1.
  apply occCan_appl.
  assumption.
  apply IHcan2.
  intros.
  apply H1.
  apply occCan_appr.
  assumption.
  do 2 rewrite lam_abs.
  f_equal.
  apply IHcan.
  intros.
  destruct a.
  simpl.
  rewrite H0.
  reflexivity.
  apply occCan_abs.
  assumption.
  reflexivity.
  do 2 rewrite lam_flat.
  f_equal.
  apply IHcan.
  intros t Hyp.
  apply H1.
  assumption.
  intros.
  apply H2.
  eapply occCan_flat.
  eexact H3.
  assumption.
Qed.


Lemma lam_occ (A B: Set)(f: A -> B)(t: Lam A)(b: B):
  b occ (lam f t) -> exists a: A, (a occ t) /\ (b = f a).
Proof.
  unfold occursFreeIn.
  intros.
  rewrite FV_ok in H.
  assert (exists a: A, f a = b /\ In a (FV t)).
  exact (proj1 (in_map_iff _ _ _) H).
  destruct H0.
  destruct H0.
  exists x.
  split.
  assumption.
  symmetry.
  assumption.
Qed. 

Lemma lam_can (A B: Set)(f: A -> B)(t: Lam A): can t -> can (lam f t).
Proof.
  intros.
  revert B f.
  induction H; intros.
  rewrite lam_var.
  apply can_var.
  rewrite lam_app.
  apply can_app.
  apply IHcan1.
  apply IHcan2.
  rewrite lam_abs.
  apply can_abs.
  apply IHcan.
(* flat *)
  rewrite lam_flat.
  apply can_flat.
  apply IHcan.
  intros.
(*
Check (lam_occ (fun t : Lam A => lam (fun x : A => f x) t) ee t H2).
*)
  destruct (lam_occ _ _ t H2).
  destruct H3.
  rewrite H4.
  apply H1.
  assumption.
Qed.

(* now earlier in the file
   an auxiliary lemma for preservation of [can] by [subst]:
Lemma occ_var_inv (A: Set)(a b: A): a occ (var b) -> a = b.
Proof.
  intros.
  unfold occursFreeIn in H.
  rewrite FV_var in H.
  destruct H.
  apply sym_eq.
  assumption.
  inversion H.
Qed.
*)

Lemma subst_can (A B: Set)(f: A -> Lam B)(t: Lam A): 
  (forall a: A, a occ t -> can (f a)) -> can t -> can (subst f t).
Proof.
  intros.
  revert B f H.
  induction H0; intros.
  rewrite subst_var.
  apply H.
  apply occCan_var.
  rewrite subst_app.
  apply can_app.
  apply IHcan1.
  intros.
  apply H.
  apply occCan_appl.
  assumption.
  apply IHcan2.
  intros.
  apply H.
  apply occCan_appr.
  assumption.
  rewrite subst_abs.
  apply can_abs.
  apply IHcan.
  intros.
  destruct a.
  simpl.
  apply lam_can.
  apply H.
  apply occCan_abs.
  assumption.
  simpl.
  apply can_var.
(* flat *)
  rewrite subst_flat.
  apply can_flat.
  apply IHcan.
  intros.
  unfold comp.
  apply can_var.
  intros.
(*
Check (subst_occ _ ee _ H3).
*)
  destruct (subst_occ _ ee _ H3).
  destruct H4.
  unfold comp in H5.
(*
Check (occ_var_inv t _ H5).
*)
  rewrite (occ_var_inv t _ H5).
  apply H1.
  assumption.
  intros.
  apply H2.
(*
Check (occCan_flat a x _ H6 H4).
*)
  exact (occCan_flat a x _ H6 H4).
Qed.


Lemma lam_is_subst (A B: Set)(f: A -> B)(t: Lam A):
  can t -> lam f t = subst (var(A:= B) o f) t.
Proof.
  intros.
  rewrite <- substGnat2.
  apply sym_eq.  
  apply substMonad2.
  apply lam_can.
  assumption.
Qed. 
  

(** finally, we obtain the desired rewrite rule for [subst] in the case
      [flat], but only for canonical elements *)

Lemma subst_flat' (A B: Set)(f: A -> Lam B)(ee: Lam(Lam A)):
  can ee -> subst f (flat ee) = flat (lam (subst f) ee).
Proof.
  intros.
  rewrite subst_flat.
  f_equal.
  apply sym_eq.
  apply lam_is_subst.
  assumption.
Qed.

(** Section 5.2 of the paper *)

Definition Lam' (A: Set) : Set := {t: Lam A| can t}.

Inductive Lam'_ALT(A: Set): Set :=
  existLam': forall t: Lam A, can t -> Lam'_ALT A.

Definition Lam'_ALT_Lam' (A: Set): Lam'_ALT A -> Lam' A.
Proof.
  intros.
  destruct H.
  exists t.
  assumption.
Defined.

Definition Lam'_Lam'_ALT (A: Set): Lam' A -> Lam'_ALT A.
Proof.
  intros.
  destruct H.
  exists x.
  assumption.
Defined.

Lemma Lam'_ALT_bij_Lam' (A: Set):
  (forall t: Lam' A,  Lam'_ALT_Lam' (Lam'_Lam'_ALT t) = t) /\
  (forall t: Lam'_ALT A,  Lam'_Lam'_ALT (Lam'_ALT_Lam' t) = t).
Proof.
  intros; split; intros; destruct t; reflexivity.
Qed.  

Definition pi1: Lam' c_k1 Lam.
Proof.
  red.
  intros.
  exact (proj1_sig H).
Defined.

Implicit Arguments pi1 [[A]].


Definition pi1_ALT: Lam'_ALT c_k1 Lam.
Proof.
  red.
  intros.
  destruct H.
  assumption.
Defined.


Definition var' (A: Set)(a: A): Lam' A.
Proof.
  intros.
  red.
  exists (var a).
  apply can_var.
Defined.

(** printing t1' %\ensuremath{t'_1}% *)
(** printing t2' %\ensuremath{t'_2}% *)
(** printing p1 %\ensuremath{p_1}% *)
(** printing p2 %\ensuremath{p_2}% *)

Definition app' (A: Set)(t1 t2: Lam' A): Lam' A.
Proof.
  intros.
  destruct t1 as (t1', p1).
  destruct t2 as (t2', p2).
  exists (app t1' t2').
  apply can_app; assumption.
Defined.

Definition abs' (A: Set)(r: Lam' (option A)): Lam' A.
Proof.
  intros.
  destruct r as (r, p).
  exists (abs r).
  apply can_abs; assumption.
Defined.


Definition flat' (A: Set)(ee: Lam'(Lam' A)): Lam' A.
Proof.
  intros.
  red.
  exists (flat (lam pi1 (pi1 ee))).  
  destruct ee as (ee', p).
  simpl.
  apply can_flat.
  apply lam_can.
  assumption.
  intros.
  destruct (lam_occ _ _ _ H).
  destruct x as (t', p').
  simpl in H0.
  destruct H0.
  rewrite H1.
  assumption.
Defined.
(** unfortunately, this definition has to do something on terms, namely renaming using [pi1] *)

Lemma flat'_ok (A: Set)(ee: Lam'(Lam' A)):
  pi1 (flat' ee) = flat(lam pi1 (pi1 ee)).
Proof.
  reflexivity.
Qed.

Instance lam': LNMItPred.mon Lam'.
Proof.
  red.
  intros A B f t.
  exists (lam f (pi1 t)).
  apply lam_can.
  unfold pi1.
  apply proj2_sig.
Defined.

Lemma lam'_ok (A B: Set)(f: A -> B)(t: Lam' A):
  pi1 (lam' f t) = lam f (pi1 t).
Proof.
  reflexivity.
Qed.
  
Definition subst' (A B: Set)(f: A -> Lam' B)(t: Lam' A): Lam' B.
Proof.
  intros.
  red.
  exists (subst (fun a => pi1 (f a)) (pi1 t)).
  apply subst_can.
  intros a _.
  unfold pi1.
  apply proj2_sig.
  unfold pi1.
  apply proj2_sig.
Defined.

Lemma subst'_ok (A B: Set)(f: A -> Lam' B)(t: Lam' A):
  pi1 (subst' f t) = subst (pi1 o f) (pi1 t).
Proof.
  reflexivity.
Qed.

Definition FV': Lam' c_k1 listk1.
Proof.
  red.
  intros A t.
  apply  FV.
  exact (pi1 t).
Defined.

Instance FV'NAT: NAT FV'.
Proof.
  red.
  intros.
  unfold FV'.
  destruct t as (t', p).
  simpl.
  apply FVNAT.
Qed.

Corollary FV'_ok (A B: Set)(f: A -> B)(t: Lam' A):
  FV'(lam' f t) = map f (FV' t).
Proof.
  intros.
  apply FV'NAT.
Qed.


Lemma FV'_var (A: Set)(a: A): FV'(var' a) = a :: nil.
Proof.
  intros.
  unfold var'.
  unfold FV'.
  simpl.
  apply FV_var.
Qed.


Lemma FV'_app (A: Set)(t1 t2: Lam' A): FV'(app' t1 t2) = FV' t1 ++ FV' t2.
Proof.
  intros.
  destruct t1.
  destruct t2.
  unfold app'.
  unfold FV' at 1.
  simpl.
  rewrite FV_app. 
  reflexivity.
Qed.

Lemma FV'_abs (A: Set)(r: Lam' (option A)): FV'(abs' r) = filterSome (FV' r).
Proof.
  intros.
  destruct r.
  unfold abs'.
  unfold FV' at 1.
  simpl.
  rewrite FV_abs.
  reflexivity.
Qed.

Lemma FV'_flat (A: Set)(ee: Lam' (Lam' A)): 
  FV'(flat' ee) = flat_map (FV'(A:= A)) (FV' ee).
Proof.
  intros.
  destruct ee.
  unfold flat'.
  unfold FV' at 1.
  simpl.
  rewrite FV_flat.
  rewrite FV_ok.
  unfold FV'.
  simpl.
  rewrite flat_mapLaw1.
  reflexivity.
Qed.

(** item 6 of Theorem 1 for [Lam'] in place of [Lam]: *)

Lemma FV'subst' (A B: Set)(f: A -> Lam' B)(t: Lam' A):
   FV'(subst' f t) = flat_map (FV'(A:= B) o f) (FV' t).
Proof.
  intros.
  unfold subst', FV'.
  destruct t as (t', p).
  simpl.
  rewrite FVsubst.
  unfold comp.
  reflexivity.
Qed.
 

Definition occursFreeIn' (A: Set)(a: A)(t: Lam' A): Prop := In a (FV' t).

Infix "occ'" := occursFreeIn' (at level 90). 

Lemma lam'_occ (A B: Set)(f: A -> B)(t: Lam' A)(b: B):
  b occ' (lam' f t) -> exists a: A, (a occ' t) /\ (b = f a).
Proof.
  unfold occursFreeIn'.
  intros.
  rewrite FV'_ok in H.
  assert (exists a: A, f a = b /\ In a (FV' t)).
  exact (proj1 (in_map_iff _ _ _) H).
  destruct H0.
  destruct H0.
  exists x.
  split.
  assumption.
  rewrite H0.
  reflexivity.
Qed. 

Lemma lam'_occ_ALT (A B: Set)(f: A -> B)(t: Lam' A)(b: B):
  b occ' (lam' f t) -> exists a: A, (a occ' t) /\ (b = f a).
Proof.
  intros.
  destruct t.
  unfold occursFreeIn' in H.
  unfold FV' in H.
  rewrite lam'_ok in H.
  simpl in H.
  destruct (lam_occ _ _ _ H).
  exists x0.
  destruct H0.
  split.
  unfold occursFreeIn'.
  assumption.
  assumption.
Qed.


Lemma subst'_occ (A B: Set)(f: A -> Lam' B)(t: Lam' A)(b: B):
  b occ' (subst' f t) -> exists a: A, (a occ' t) /\ (b occ' f a).
Proof.
  unfold occursFreeIn'.
  intros.
  rewrite FV'subst' in H.
  destruct (proj1 (in_flat_map (FV'(A:= B) o f) (FV' t) b) H).
  exists x.
  assumption.
Qed.

Lemma subst'_occ_ALT (A B: Set)(f: A -> Lam' B)(t: Lam' A)(b: B):
  b occ' (subst' f t) -> exists a: A, (a occ' t) /\ (b occ' f a).
Proof.
  unfold occursFreeIn'.
  intros.
  unfold FV' in H.
  destruct t.
  rewrite subst'_ok in H.
  simpl in H.
  destruct (subst_occ _ _ _ H).
  exists x0.
  destruct H0.
  split.
  assumption.
  assumption.
Qed.



Definition EqLam' (A: Set)(t1 t2: Lam' A): Prop := pi1 t1 = pi1 t2.
(** printing ~~ %\ensuremath{\equiv}% *)
(* begin hide *)
Infix "~~" := EqLam' (at level 60).
(* end hide *)

(** [EqLam'] is displayed as the infix $\equiv$#~~#. *)

Lemma EqLam'_refl (A: Set)(t: Lam' A): t ~~ t.
Proof.
  reflexivity.
Qed.

Lemma EqLam'_sym (A: Set)(t1 t2: Lam' A): t1 ~~ t2 -> t2 ~~ t1.
Proof.
  intros.
  symmetry.
  assumption.
Qed.

(** printing t3 %\ensuremath{t_3}% *)

Lemma EqLam'_trans (A: Set)(t1 t2 t3: Lam' A): t1 ~~ t2 -> t2 ~~ t3 -> t1 ~~ t3.
Proof.
  intros.
  red.
  transitivity (pi1 t2); assumption.
Qed.

Add Parametric Relation (A: Set): (Lam' A) (EqLam'(A:= A)) 
  reflexivity proved by (EqLam'_refl(A:= A))
  symmetry proved by (EqLam'_sym(A:= A))
  transitivity proved by (EqLam'_trans(A:= A))
  as bisimilarRel.

(** we do not impose the following axiomatically *)

Definition proof_irrelevance := forall (P: Prop) (p1 p2: P), p1 = p2.

Definition Lam'pirrProp := forall (A: Set)(t1 t2: Lam' A), t1 ~~ t2 -> t1 = t2.

Lemma Lam'pirrFromPirr: proof_irrelevance -> Lam'pirrProp.
Proof.
  intro pirr. red. intros.
  destruct t1 as [t1' H1].
  destruct t2 as [t2' H2].
  red in H.
  simpl in H.
  revert H1 H2.
  destruct H.
  intros.
  rewrite (pirr _ H1 H2).
  reflexivity.
Qed.

(** Theorem 9 in the paper *)

(** item 1: *)

Lemma subst'ext' (A B: Set)(f g: A -> Lam' B)(t: Lam' A): 
  (forall a, a occ' t -> f a ~~ g a) -> subst' f t ~~ subst' g t.
Proof.
  intros.
  destruct t as (t', p').
  red.
  simpl.
  apply substext'.
  intros.
  red in H.
  rewrite H.
  reflexivity.
  unfold occursFreeIn', FV'.
  simpl.
  assumption.
Qed.

Corollary subst'ext (A B: Set)(f g: A -> Lam' B)(t: Lam' A): 
  (forall a, f a ~~ g a) -> subst' f t ~~ subst' g t.
Proof.
  intros.
  apply subst'ext'.
  intros.
  apply H.
Qed.

(** item 2: *)

Lemma subst'Gnat1 (A B C : Set) (f : A -> Lam' B) (g : B -> C) (t : Lam' A):
  lam' g (subst' f t) ~~ subst' (lam' g o f) t.
Proof.
  intros.
  destruct t as (t', p').
  red.
  simpl.
  rewrite substGnat1.
  apply substext.
  intro.
  unfold comp.
  reflexivity.
Qed.

(** item 3: *)

Lemma subst'Gnat2 (A B C: Set)(f: A -> B)(g: B -> Lam' C)(t: Lam' A): 
  subst' g (lam' f t) ~~ subst' (g o f) t.
Proof.
  intros.
  destruct t as (t', p').
  red.
  simpl.
  rewrite substGnat2.
  reflexivity.
Qed.

(** item 4: *)

Definition monad3Lam': Prop :=
  forall (A B C :  Set) (f : A -> Lam' B) (g : B -> Lam' C) (t : Lam' A),
  subst' g (subst' f t) ~~ subst' (subst' g o f) t.

Lemma subst'Monad3: monad3Lam'.
Proof.
  red.
  intros.
  red.
  destruct t as (t', p).
  simpl.
  rewrite substMonad3.
  apply substext.
  intro.
  unfold comp.
  destruct (f a) as (b', p').
  simpl.
  reflexivity.
Qed.

(** the lemmas that no longer need an explicit relativization to
     hereditarily canonical elements *)

(** item 5: *)

Lemma subst'Monad2 (A: Set)(t: Lam' A): subst' (var'(A:= A)) t ~~ t.
Proof.
  intros.
  red.
  rewrite subst'_ok.
  transitivity (subst (var(A:= A)) (pi1 t)).
  apply substext.
  reflexivity.
  apply substMonad2.
  unfold pi1.
  apply proj2_sig.
Qed.

(** item 6: *)

Lemma lam'_is_subst' (A B: Set)(f: A -> B)(t: Lam' A):
  lam' f t ~~ subst' (var'(A:= B) o f) t.
Proof.
  intros.
  red.
  rewrite lam'_ok.
  rewrite subst'_ok.
  rewrite lam_is_subst.
  reflexivity.
  unfold pi1.
  apply proj2_sig.
Qed.

(** item 7: *)
  
Lemma subst'_flat' (A B: Set)(f: A -> Lam' B)(ee: Lam'(Lam' A)):
  subst' f (flat' ee) ~~ flat' (lam' (subst' f) ee).
Proof.
  intros.
  destruct ee as (ee', p).
  red.
  simpl.
  rewrite subst_flat'.
  do 2 rewrite <- lamfct2.
  f_equal.
  apply lam_can.
  assumption.
Qed.

(** This completes Theorem 9 of the paper. *)

Lemma lam'_var (A B: Set)(f: A -> B)(a: A) : lam' f (var' a) ~~ var' (f a).
Proof.
  intros.
  red.
  simpl.
  apply lam_var.
Qed.
 
Lemma lam'_app (A B: Set)(f: A -> B)(t1 t2: Lam' A): 
  lam' f (app' t1 t2) ~~ app' (lam' f t1)(lam' f t2).
Proof.
  intros.
  destruct t1 as [t1' p1].
  destruct t2 as [t2' p2].
  red.
  simpl.
  apply lam_app.
Qed.

Lemma lam'_abs (A B: Set)(f: A -> B)(r: Lam'(option A)): 
  lam' f (abs' r) ~~ abs' (lam' (option_map f) r).
Proof.
  intros.
  destruct r as [r' p].
  red.
  simpl.
  apply lam_abs.
Qed.

Lemma lam'_flat (A B: Set)(f: A -> B)(ee: Lam'(Lam' A)): 
  lam' f (flat' ee) ~~  flat' (lam' (lam' f) ee).
Proof.
  intros.
  destruct ee as [ee' p].
  red.
  simpl.
  rewrite lam_flat.  
  f_equal.
  do 2 rewrite <- lamfct2.
  apply lamext.
  intro t.
  unfold comp.
  rewrite lam'_ok.
  reflexivity. 
Qed.


Lemma lam'ext_refined (A B: Set)(f g: A -> B)(t: Lam' A):
  (forall a, a occ' t -> f a = g a) -> lam' f t ~~ lam' g t.
Proof.
  intros.
  red.
  do 2 rewrite lam'_ok.
  apply lamext_refined.
  destruct t.
  assumption.
  assumption.
Qed.  

Corollary lam'ext (A B: Set)(f g: A -> B):
        (forall a, f a = g a) -> forall r, lam' f r ~~ lam' g r.
Proof.
  intros.
  apply lam'ext_refined.
  intros.
  apply H.
Qed.

Lemma lam'fct1 (A: Set)(t: Lam' A): lam' id t ~~ t.
Proof.
  intros.
  destruct t as (t', p).
  red.
  simpl.
  apply lamfct1.
Qed.  
 
Lemma lam'fct2 (A B C : Set) (f : A -> B) (g : B -> C) (t : Lam' A):
  lam' (g o f) t ~~ lam' g (lam' f t).
Proof.
  intros.
  destruct t as (t', p).
  red.
  simpl.
  apply lamfct2.
Qed.

Definition lift' (A B: Set)(f: A -> Lam' B)(x: option A): Lam'(option B) :=
  match x with
    | None => var' None
    | Some a => lam' Some (f a)
  end.

Lemma lift'_ok (A B: Set)(f: A -> Lam' B)(x: option A):
  pi1 (lift' f x) = lift (pi1 o f) x.
Proof.
  intros.
  destruct x.
  simpl.
  reflexivity.
  reflexivity.
Qed.

Lemma subst'Monad1 (A B: Set)(f: A -> Lam' B)(a: A): 
  subst' f (var' a) ~~ f a.
Proof.
  intros.
  red.
  simpl.
  rewrite subst_var.
  reflexivity.
Qed.

(* now just a repetition: *)
Lemma subst'_var (A B: Set)(f: A -> Lam' B)(a: A):
  subst' f (var' a) ~~ f a.
Proof.
  intros.
  apply subst'Monad1.
Qed.

Lemma subst'_app (A B: Set)(f: A -> Lam' B)(t1 t2: Lam' A):
  subst' f (app' t1 t2) ~~ app' (subst' f t1)(subst' f t2).
Proof.
  intros.
  destruct t1 as [t1' p1].
  destruct t2 as [t2' p2].
  red.
  simpl.
  apply subst_app.
Qed.

Lemma subst'_abs (A B: Set)(f: A -> Lam' B)(r: Lam'(option A)):
  subst' f (abs' r) ~~ abs' (subst' (lift' f) r).
Proof.
  intros.
  destruct r as [r' p].
  red.
  simpl.
  rewrite subst_abs.
  f_equal.
  apply substext.
  intro.
  rewrite lift'_ok.
  reflexivity.
Qed.

Lemma subst'_flat (A B: Set)(f: A -> Lam' B)(ee: Lam'(Lam' A)):
  subst' f (flat' ee) ~~ flat' (subst' (var'(A:= Lam' B) o (subst' f)) ee).
Proof.
  intros.
  destruct ee as [ee' p].
  red.
  simpl.
  rewrite subst_flat.
  f_equal.
  rewrite substGnat1.
  rewrite substGnat2.
  apply substext.
  intro t.
  unfold comp.
  rewrite lam_var.
  destruct t as (t', p').
  simpl.
  reflexivity.
Qed.

(* Is there a problem with the syntax here?
Add Parametric Morphism (A: Set): (@flat' A)
  with signature (@EqLam'(Lam' A)) ==> (@EqLam' A)
  as flat'M.
Proof.
  red.
  intros.
  simpl.
  f_equal.
  rewrite H.
  reflexivity.
Qed.

Lemma subst'_flat_ALT (A B: Set)(f: A -> Lam' B)(ee: Lam'(Lam' A)):
  subst' f (flat' ee) ~~ flat' (subst' (var'(A:= Lam' B) o (subst' f)) ee).
Proof.
  intros.
  transitivity (flat' (lam' (subst' f) ee)).
  apply subst'_flat'.
  rewrite lam'_is_subst'.
  reflexivity.
Qed.
*)

(** Section 5.3 of the paper *)

Definition LamFmon2br: mon2br LamF.
Proof.
  red.  
  red.
  intros X Y mY f A t.
  destruct t as [[[a|( t1, t2)]|r]|ee].
  unfold LamF.
  left; left; left.
  assumption.
  left; left; right.
  exact (f A t1, f A t2).
  left; right.
  exact (f (option A) r).
  exact (inr _ (mY _ _ (f A) (f (X A) ee))).
Defined.

Definition LamToCan: Lam c_k1 Lam := LamMMItDef.canonize LamFmon2br.

Lemma LamToCan_var (A: Set)(a: A): LamToCan(var a) = var a.
Proof.
  intros.
  unfold var.
  unfold LamToCan.
  unfold LamMMItDef.canonize.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

Lemma LamToCan_app (A: Set)(t1 t2: Lam A): LamToCan(app t1 t2) = app (LamToCan t1) (LamToCan t2).
Proof.
  intros.
  unfold app.
  unfold LamFlat.app.
  unfold LamToCan at 1.
  unfold LamMMItDef.canonize.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

Lemma LamToCan_abs (A: Set)(r: Lam (option A)): LamToCan(abs r) = abs(LamToCan r).
Proof.
  intros.
  unfold abs.
  unfold LamToCan at 1.
  unfold LamMMItDef.canonize.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

Lemma LamToCan_flat (A: Set)(ee: Lam (Lam A)): 
  LamToCan(flat ee) = flat (lam (LamToCan(A:= A)) (LamToCan ee)).
Proof.
  intros.
  unfold flat.
  unfold LamToCan at 1.
  unfold LamMMItDef.canonize.
  rewrite LamMMItDef.MItRedCan.
  reflexivity.
Qed.

(** canonical elements are not changed by canonization *)
 
Theorem LamToCan_invariant (A: Set)(t: Lam A): can t -> LamToCan t = t.
Proof.
  intros.
  induction H.
  apply LamToCan_var.
  rewrite LamToCan_app.
  rewrite IHcan1.
  rewrite IHcan2.
  reflexivity.
  rewrite LamToCan_abs.
  rewrite IHcan.
  reflexivity.
  rewrite LamToCan_flat.
  rewrite IHcan.
  f_equal.
  transitivity (lam (id(A:= Lam A)) ee).
  apply lamext_refined.
  assumption.
  intros t Hyp.
  apply H1.
  assumption.
  apply lamfct1.
Qed.

(** canonization yields hereditarily canonical elements *)

Theorem LamToCanCan (A: Set)(t: Lam A): can (LamToCan t).
Proof.
  revert A t. (* new in 8.3 *)
  apply (LamBase.mu2Ind (fun A t => can (LamToCan t))).
  intros;
  destruct t as [[[a|( t1, t2)]|r]|ee];
  unfold LamToCan;
  unfold LamMMItDef.canonize;
  rewrite LamBase.MItRed;
  simpl LamFmon2br.
  assert (can (var a)).
  apply can_var.
  assumption.
  assert (can (app (LamToCan (j A t1)) (LamToCan (j A t2)))).
  apply can_app; apply H.
  apply H0.
  assert (can (abs (LamToCan (j (option A) r)))).
  apply can_abs.
  apply H.
  apply H0.
  assert (can (flat (lam (LamToCan(A:= A) o j A) (LamToCan (j (X A) ee))))).
  apply can_flat.
  apply lam_can.
  apply H.
  intros.
  destruct (lam_occ (LamToCan (A:= A) o j A) (LamToCan (j (X A) ee)) t H0).
  destruct H1.
  rewrite H2.
  unfold comp.
  apply H.
  apply H0.
Qed.

(** canonization can be expressed as follows: *)

Definition LamToLam': Lam c_k1 Lam'.
Proof.
  red.
  intros A t.
  exists (LamToCan t).
  apply LamToCanCan.
Defined.

Lemma LamToLam'_ok (A: Set)(t: Lam A): pi1 (LamToLam' t) = LamToCan t.
Proof.
  reflexivity.
Qed.

Scheme canInd := Induction for can Sort Prop.

Definition IsConstructed' (A: Set)(t: Lam' A) : Prop :=
   (exists a: A, t = var' a) \/ (exists t1, exists t2, t = app' t1 t2) \/ (exists r, t = abs' r) \/ (exists ee, t ~~ flat' ee).
(* Note ~~ in the last disjunct! *)

Lemma Lam'exhausted (A: Set)(t: Lam' A):  IsConstructed' t.
Proof.
  intros.
  destruct t as (t', p).
  induction p using canInd.
(* var *)
  left.
  exists a.
  reflexivity.
(* app *)
  clear IHp1 IHp2.
  right; left.
  exists (exist (fun t : Lam A => can t) t1 p1).
  exists (exist (fun t : Lam A => can t) t2 p2).
  reflexivity.
(* abs *)
  clear IHp.
  right; right; left.
  exists (exist (fun t : Lam(option A) => can t) r p).
  reflexivity.
(* flat *)
  clear IHp H.
  right; right; right.
  set (ee0':= lam (LamToLam'(A:= A)) ee).
  set (p':= lam_can (LamToLam'(A:= A)) p: can ee0').
  exists (exist (fun t : Lam (Lam' A) => can t) ee0' p').
  red; simpl.
  f_equal.
  unfold ee0'.
  rewrite <- lamfct2.
  transitivity (lam (id(A:= Lam A)) ee).
  rewrite lamfct1.
  reflexivity.
  apply lamext_refined.
  assumption.
  intros t Hyp.
  unfold comp.
  rewrite LamToLam'_ok.
  rewrite LamToCan_invariant.
  reflexivity.
  exact (c t Hyp).
Qed.

End LamFlat.