(** LamPred.v Version 0.7 January 2008 *)

(** does not need impredicative Set, runs under V8.1, tested with 8.1pl3 *)

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

(** We do not use Coq's native Lam. *)
(** the full development of Lam, depending on a hypothetical theory *)

Set Implicit Arguments.

Require Import LNMItPred.
Require Import LNGMItPred.


Section Monad.

Variable T:k1.
Variable eta: forall A:k0, A -> T A.
Variable bind: forall A B:k0, (A -> T B) -> T A -> T B.

Definition monad1:= forall (A B:k0)(f:A -> T B)(a:A), bind f (eta a) = f a.
Definition monad2:= forall (A:k0)(t:T A), bind (eta(A:=A)) t = t.
Definition monad3:= forall (A B C:k0)(f:A->T B)(g:B->T C)(t:T A),
  bind g (bind f t) = bind ((bind g) o f) t.

End Monad.

Open Scope type_scope.

Definition LamF(X:k1)(A:k0) := A + X A * X A + X(option A).

Definition lampEFct : pEFct LamF.
Proof.
  unfold LamF.
  apply sumpEFct.
  apply sumpEFct.
  apply constpEFct.
  apply idEFct.
  apply prodpEFct.
  apply idpEFct_eta.
  apply idpEFct_eta.
  apply comppEFct.
  apply idpEFct.
  apply constpEFct.
  apply optionEFct.
Defined.

Require Import List.

(** some preparations for lists *)

(* needed because of sort polymorphism *)
Definition listk1 (A:k0) : k0 := list A.


Fixpoint filterSome (A:k0)(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:Set)(a:A)(l:list(option A)):
   In (Some a) l -> In a (filterSome l).
Proof.
  intros.
  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.
Qed.
  

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

Module Lam (LamBase:LAM).

Module LamM := LNGMItDef LamBase.
(* Module LamMMItBase := LamBase.LNM. *)
Module LamMMItDef := LamM.LNMItDef.


Definition Lam : k1 := LamBase.mu2.

Definition lam : mon Lam := LamBase.mapmu2.

Lemma lamext: ext lam.
Proof.
  exact LamMMItDef.mapmu2Ext.
Qed.

Lemma lamfct1: fct1 lam.
Proof.
  exact LamMMItDef.mapmu2Id.
Qed.  
 
Lemma lamfct2 : fct2 lam.
Proof.
  exact LamMMItDef.mapmu2Comp.
Qed.


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

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

Lemma app_cong(A:k0)(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:k0)(r: Lam (option A)): Lam A := 
  LamMMItDef.InCan (inr _ r).

Lemma lam_var (A B:k0)(f:A->B)(a:A) : lam f (var a) = var (f a).
Proof.
  intros.
  unfold lam, var at 1.
  rewrite LamMMItDef.mapmu2RedCan.
  reflexivity.
Qed.
 
Lemma lam_app (A B:k0)(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:k0)(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.


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

Lemma lift_map (A B C:k0)(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 at 1.
  simpl.
  rewrite lam_var.
  reflexivity.
Qed.
  

Definition subst (A B:k0)(f:A -> Lam B)(t:Lam A) :Lam B.
Proof.
  refine (LamBase.GMIt (H:=Lam)(G:=Lam)(fun (X:k1)(it: X <_{Lam} Lam)
        (A B:k0)(f:A -> Lam B)(t:LamF X A)=> _)).
  destruct t as [[a|(t1,t2)]|r].
  exact (f a).
  exact (app (it _ _ f t1)(it _ _ f t2)).
  exact (abs (it _ _ (lift f) r)).
Defined.

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

Lemma s_subst_ok (A B:k0)(f:A -> Lam B)(t:Lam A): 
  LamBase.GMIt s_subst B f t = subst f t.
Proof.
  reflexivity.
Qed.

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].
  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.
Qed.

Lemma substext (A B:k0)(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 <- s_subst_ok.  would be a way that is unconcious of convertibility *)
  rewrite (LamM.GMItsExt s_subst substpGext B f g H t).
  reflexivity.
Qed.  


(* this is a proof that directly incorporates the verification of preservation of gext: *)
Lemma substext_ALT (A B:k0)(f g:A -> Lam B)(t:Lam A): 
  (forall a, f a = g a) -> subst f t = subst g t.
Proof.
  intros.
  unfold subst.
  apply LamM.GMItsExt.
  clear A B f g t H.
  red.  
  intros.
  destruct r as [[a|(t1,t2)]|r].
  apply H0.
  do 2 rewrite (H A B f g H0).
  reflexivity.
  rewrite (H (option A) (option B) (lift f) (lift g)).
  reflexivity.
  destruct a.
  simpl.  
  rewrite H0.
  reflexivity.
  reflexivity.
  assumption.
Qed.



(* a more fine-grained version of the substitution lemma, based
   on free variable occurrences *)

(* first the notion of free variables *)

(* lambda terms into lists of free variables, just with plain Mendler iteration *)
Definition LamToFV : 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].
  exact (a::nil).
  exact (it _ t1 ++ it _ t2).
  exact (filterSome (it _ r)).
Defined.

Definition occursFreeIn(A:k0)(a:A)(t:Lam A): Prop := In a (LamToFV t).

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

(* the very first approach: 
Inductive occursFreeIn: forall (A:k0), A -> Lam A -> Prop :=

 | occ_var: forall(A:k0)(a:A), occursFreeIn a (var a)
 | occ_appl: forall(A:k0)(a:A)(t1 t2:Lam A), 
      occursFreeIn a t1 -> occursFreeIn a (EFlat.app t1 t2)
 | occ_appr: forall(A:k0)(a:A)(t1 t2:Lam A), 
      occursFreeIn a t2 -> occursFreeIn a (EFlat.app t1 t2)
 | occ_abs: forall(A:k0)(a:A)(r:Lam(option A)),
      occursFreeIn (Some a) r -> occursFreeIn a (abs r).

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

Beware: This would only concern canonical terms! *)

(* the second inductive approach that would be viable but extend
    to LamE only with inversion laws for nested datatypes 
Inductive occursFreeIn: forall (A:k0), A -> Lam A -> Prop :=

 | occ_var: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A),
      occursFreeIn a (LamBase.In ef n (inl (X (option A)) (inl (X A * X A) a)))
 | occ_appl: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A)(t1 t2 : X A), 
         (occursFreeIn a (j A t1)) -> 
     occursFreeIn a (LamBase.In ef n (inl (X (option A)) (inr A (t1, t2))))
 | occ_appr: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A)(t1 t2 : X A), 
         (occursFreeIn a (j A t2)) -> 
      occursFreeIn a (LamBase.In ef n (inl (X (option A)) (inr A (t1, t2))))
 | occ_abs: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A)(r: X (option A)),
         (occursFreeIn (Some a)(j (option A) r)) -> 
      occursFreeIn a (LamBase.In ef n (inr (A + X A * X A) r)).

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

(* the old defining rules become lemmas *)
Lemma occ_var: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A),
      a occ (LamBase.In ef n (inl (X (option A)) (inl (X A * X A) a))).
Proof.
  intros.
  unfold occursFreeIn.
  unfold LamToFV.
  rewrite LamBase.MItRed.
  simpl.
  left.
  reflexivity.
Qed.

Lemma   occ_appl: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A)(t1 t2 : X A), 
         (a occ (j A t1)) -> 
     a occ (LamBase.In ef n (inl (X (option A)) (inr A (t1, t2)))).
Proof.
  intros.
  unfold occursFreeIn.
  unfold LamToFV.
  rewrite LamBase.MItRed.
  apply in_or_app.
  left.
  assumption.
Qed.

Lemma occ_appr: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A)(t1 t2 : X A), 
         (a occ (j A t2)) -> 
      a occ (LamBase.In ef n (inl (X (option A)) (inr A (t1, t2)))).
Proof.
  intros.
  unfold occursFreeIn.
  unfold LamToFV.
  rewrite LamBase.MItRed.
  apply in_or_app.
  right.
  assumption.
Qed.

Lemma occ_abs: forall (X : k1) (ef : EFct X) (j : X c_k1 Lam)
     (n : NAT j (m ef) lam) (A : Set) (a : A)(r: X (option A)),
         (occursFreeIn (Some a)(j (option A) r)) -> 
      occursFreeIn a (LamBase.In ef n (inr (A + X A * X A) r)).
Proof.
  intros.
  unfold occursFreeIn.
  unfold LamToFV.
  rewrite LamBase.MItRed.
  apply filterSomeIn.
  assumption.
Qed.


Lemma substext' (A B:k0)(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.
  generalize B f g H; clear B f g H.
  generalize A t; clear A t.
  apply (LamBase.mu2Ind (fun A t => forall (B : k0) (f g : A -> Lam B),
    (forall a : A, (a occ t) -> f a = g a) -> subst f t = subst g t)).
  intros.
  destruct t as [[a|(t1,t2)]|r]. 
(* var *)
  unfold subst; do 2 rewrite LamBase.GMItRed.
  apply H0.
  apply occ_var.
(* app *)
  change subst with (LamBase.GMIt s_subst). (* ! *)
  do 2 rewrite LamBase.GMItRed.
  simpl.
  apply app_cong; change (LamBase.GMIt s_subst) with subst.
  unfold comp.  
  apply H.
  intros.
  apply H0.
  apply occ_appl.
  assumption.
  unfold comp.  
  apply H.
  intros.
  apply H0.
  apply occ_appr.
  assumption.
(* abs *)
  change subst with (LamBase.GMIt s_subst).
  do 2 rewrite LamBase.GMItRed.
  simpl.
  apply (f_equal (fun x => abs(A:=B) x)).
  change (LamBase.GMIt s_subst) with subst.
  unfold comp.  
  apply H.
  intros.
  destruct a.
  simpl.
  rewrite H0.
  reflexivity.
  generalize H1.
  apply occ_abs.
  reflexivity.
Qed.  

Lemma substGnat1: forall (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.
  apply (LamM.GMItsNat1 s_subst substpGext).
  red. 
  intros.
  destruct x as [[a|(t1,t2)]|r].
  simpl.
  reflexivity.
  simpl s_subst.
  rewrite lam_app.
  do 2 rewrite H0.
  reflexivity.
  simpl s_subst.
  rewrite lam_abs.
  rewrite H0.
  apply (f_equal (fun x => abs(A:=C) x)).
  apply H.
  intro.  
  apply lift_map.
Qed.

 Lemma substGnat2 (A B C:k0)(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].
  simpl.
  reflexivity.
  simpl.
  do 2 rewrite H0.
  reflexivity.
  simpl.
  unfold moncomp.
  rewrite H0.
  apply (f_equal (fun x => abs(A:=C) x)).
  apply H.
  intro.  
  destruct a; reflexivity.
Qed.

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

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

(** Just before embarking on explicit flattening, we verify the
     monad laws for substitution. *)

Lemma substMonad1: monad1 Lam var subst.
Proof.
  red.
  intros.
  change subst with (LamBase.GMIt s_subst).
  unfold var.
  rewrite LamM.GMItRedCan.
  reflexivity.
Qed.

(** we will only be able to prove a weakened version of the
      second monad law *)

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).


Lemma substMonad2 (A:k0)(t:Lam A): can t -> subst (var(A:=A)) t = t.
Proof.
  intros.
  induction H.
  change subst with (LamBase.GMIt s_subst).
  unfold var.
  rewrite LamM.GMItRedCan.
  reflexivity.
(* app *)
  change subst with (LamBase.GMIt s_subst).
  unfold app at 1.
  rewrite LamM.GMItRedCan.
  simpl.
  change (LamBase.GMIt s_subst) with subst.
  rewrite IHcan1.
  rewrite IHcan2.
  reflexivity.
(* abs *)
  change subst with (LamBase.GMIt s_subst).
  unfold abs at 1.
  rewrite LamM.GMItRedCan.
  simpl.
  change (LamBase.GMIt s_subst) with subst.
  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.
Qed.
  

Lemma substMonad3: monad3 Lam subst.
Proof.
  red.
  intros.
  generalize B C f g; clear B C f g.
  generalize A t; clear A t.
  apply (LamBase.mu2Ind (fun A t => forall (B C : k0) (f : A -> Lam B) (g : B -> Lam C),
     subst g (subst f t) = subst (subst g o f) t)).
  intros.
  destruct ef as [m0 e0 f01 f02].
  destruct t as [[a|(t1,t2)]|r].
  change subst with (LamBase.GMIt s_subst).
  do 2 rewrite LamBase.GMItRed.
  reflexivity.
  change subst with (LamBase.GMIt s_subst).
  do 2 rewrite LamBase.GMItRed.
  simpl.
  unfold app.
  rewrite LamM.GMItRedCan.
  simpl.
  change (LamBase.GMIt s_subst) with subst.
  unfold comp at 1 2.
  do 2 rewrite H.
  reflexivity.
  change subst with (LamBase.GMIt s_subst).
  do 2 rewrite LamBase.GMItRed.
  simpl.
  unfold abs.
  rewrite LamM.GMItRedCan.
  simpl.
  change (LamBase.GMIt s_subst) with subst.
  unfold comp at 1.
  rewrite H.
  unfold abs.
  apply (f_equal (fun x => LamMMItDef.InCan
  (inr (C + LamBase.mu2 C * LamBase.mu2 C)x))).
  unfold comp.
  apply substext.
  clear X m0 e0 f01 f02 j n H r.
  intro.
  destruct a.
  simpl.
  rewrite substGnat1.
  rewrite substGnat2.
  apply substext.
  clear A f a.
  intro.
  reflexivity.
  simpl.
  rewrite substMonad1.
  reflexivity.
Qed.

Definition flat (A:k0): Lam(Lam A) -> Lam A := subst (id(A:=Lam A)).

Lemma flatNAT: NAT flat (moncomp lam lam) lam.
Proof.
  unfold flat.
  apply substNAT.
  red.  
  reflexivity.
Qed.

End Lam.