(** EFlatCoqImp.v Version 2.0 January 2008 *)
(** needs impredicative Set, runs under V8.1, tested with 8.1pl3 *)

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

(** we want to enjoy that we have the rich notion of convertibility
    that comes from the implementation in LNMItImp.v *)

(** this is code that conforms to the description in the article
    "An induction principle for nested datatypes in intensional type theory"
    by the author, to appear in the Journal of Functional Programming *)

Set Implicit Arguments.

Require Import LNMItPred.
Require Import EFlatCoqPred.
Require Import LNMItImp.

Axiom pirr: forall (A:Prop) (a1 a2:A), a1 = a2.

(** here, we fix our parameters for the impredicative implementation *)
Module LamEParam : LNMItParam with Definition F:=LamEFlatF
                                   with Definition FpEFct:=lamEFlatpEFct
                                   with Definition pirr:=pirr.

Definition F:=LamEFlatF.
Definition FpEFct:=lamEFlatpEFct.
Definition pirr:=pirr.

End LamEParam.

(** the impredicative implementation is used *)
Module LamEBase := LNMIt LamEParam.
Module LamEM := LNMItDef LamEBase.

(** we reuse the predicative development *)
Module EFlatDef := EFlat LamEBase.
Import EFlatDef.

(** an easier proof: *)
Lemma evalFlat (A:Set)(ee:LamE(LamE A)): 
  eval (flat ee) = subst (eval(A:=A)) (eval ee).
Proof.
  reflexivity.
Qed.  
(** Here, we just used convertibility. *)

(** naturality is proven as in the predicative/axiomatic development *)

(** an easier proof: *)
Lemma evalNATcor (A:Set)(ee:LamE(LamE A)):
  eval (flat ee) = subst (id(A:= Lam A)) (eval (lamE (eval(A:=A)) ee)).
Proof.
  intros.
  rewrite evalNAT.
  rewrite (substLaw1Inst (eval (A:=A)) (eval ee)).
  reflexivity.
Qed.
(** again, we used the enriched convertibility relation *)

(** for a slightly more interesting use of the extended convertibility relation, we relate
     eval and substitution *)

Definition varE (A:Set)(a:A) : LamE A.
Proof.
  intros.
  apply LamEM.InCan.
  left.
  left.
  left.
  assumption.
Defined.

Definition appE (A:Set)(t1 t2:LamE A) : LamE A.
Proof.
  intros.
  apply LamEM.InCan.
  left.
  left.
  right.
  exact (t1,t2).
Defined.

Definition absE (A:Set)(r:LamE (option A)) : LamE A.
Proof.
  intros.
  apply LamEM.InCan.
  left.
  right.
  assumption.
Defined.

(** embed Lam into LamE *)
Fixpoint emb (A:Set)(t:Lam A) : LamE A :=
  match t with
     | var a => varE a
     | app t1 t2 => appE(emb t1)(emb t2)
     | abs r => absE (emb r)
  end.

Lemma embNAT: NAT emb lam lamE.
Proof.
  red.
  intros.
  generalize B f; clear B f.
  induction t; intros.
  reflexivity.
  change (lamE f (emb (app t1 t2))) with (appE (lamE f (emb t1))(lamE f (emb t2))).
  rewrite <- IHt1; rewrite <- IHt2; reflexivity.
  change (lamE f (emb (abs t))) with (absE (lamE (option_map f) (emb t))).
  rewrite <- IHt; reflexivity.
Qed.  
(** the change command uses the "richer" convertibility relation *) 

(** half explicit substitution (flattening is explicit but renaming is carried out *)
Definition esubst (A B:Set)(f: A -> LamE B)(t: LamE A) : LamE B :=
  flat (lamE f t).

(** we get a retraction *)
Lemma evalEmb (A:Set)(t:Lam A): eval (emb t) = t.
Proof.
  intros.
  induction t.
  reflexivity.
  simpl emb.
  transitivity (app(eval(emb t1))(eval (emb t2))).
  reflexivity.
  rewrite IHt1; rewrite IHt2; reflexivity.
  transitivity (abs (eval(emb t))).
  reflexivity.
  rewrite IHt; reflexivity.
Qed.
(** three out of the five uses of reflexivity use convertibility for eval *)
 

(** subst on Lam is properly represented by esubst on LamE *) 
Lemma esubst_ok (A B:Set)(f: A -> Lam B)(t: Lam A) :
  eval (esubst (emb(A:=B) o f) (emb t)) = subst f t.
Proof.
  intros.
  unfold esubst.
  rewrite evalFlat.
  rewrite evalNAT.
  rewrite evalEmb. 
  rewrite substLaw1.
  apply substext.
  intro.
  unfold comp.
  apply evalEmb.
Qed.