(** EFlatCoqRecPred.v Version 1.0.1 December 2012 *)
(** does not need impredicative Set, runs under V8.4, tested with 8.4pl1 *)
(** We illustrate how MRec allows a different definition of eval but show that the new
and the old eval agree on all arguments. *)
(** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse *)
Set Implicit Arguments.
Require Import LNMItPred.
Require Import LNMRecPred.
Require Import EFlatCoqPred.
Module Type LAMERec := LNMRec_Type with Definition F:=LamEFlatF
with Definition FpEFct := lamEFlatpEFct.
(** we base this on a hypothetical implementation of LAMERec *)
Module EFlatRec (LamERecBase:LAMERec).
Import LamERecBase.
Module LamERecDef := LNMRecDef LamERecBase.
Import LamERecDef.
Module LamEBase := LNMItFromRec LamERecBase.
Module LamEDef := LNMItPred.LNMItDef LamEBase.
Module EFlat := EFlat LamEBase.
Import EFlat.
(** for an even cleaner comparison, we define a slight variant eval1 of eval *)
Definition eval1: LamE c_k1 Lam.
Proof.
refine (LamEBase.MIt (fun (X:k1)(it: X c_k1 Lam)(A:Set)(t:LamEFlatF X A) => _)).
destruct t as [[[a|(t1,t2)]|r]|ee].
exact (var a).
exact (app (it _ t1)(it _ t2)).
exact (abs (it _ r)).
exact (subst (id(A:=Lam A)) (lam (it A) (it (X A) ee))).
Defined.
(** note that subst id is the "real" flattening operation on Lam *)
(** the intended behaviour of eval1 on terms of the form flat ee *)
Lemma eval1Flat (A:Set)(ee:LamE(LamE A)):
eval1 (flat ee) = subst (id(A:=Lam A)) (lam (eval1(A:=A)) (eval1 ee)).
Proof.
intros.
unfold eval1 at 1.
unfold flat.
rewrite LamEM.MItRedCan.
reflexivity.
Qed.
Lemma evaleval1 (A:Set)(t: LamE A): eval t = eval1 t.
Proof.
intros.
unfold eval1.
apply LamEDef.MItUni; clear A t.
(* extensionality *)
red.
intros.
destruct y as [[[a|(t1,t2)]|r]|ee].
reflexivity.
do 2 rewrite H.
reflexivity.
rewrite H.
reflexivity.
rewrite H.
rewrite (lamext (f A) (g A)).
reflexivity.
apply H.
(* behaviour *)
intros.
destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval; rewrite LamEBase.MItRed; reflexivity).
unfold eval at 1.
rewrite LamEBase.MItRed.
rewrite <- substLaw1Inst.
reflexivity.
Qed.
Corollary eval1NAT: NAT eval1 lamE lam.
Proof.
red.
intros.
do 2 rewrite <- evaleval1.
apply evalNAT.
Qed.
Lemma eval1NATcor (A:Set)(ee:LamE(LamE A)):
eval1 (flat ee) = subst (id(A:= Lam A)) (eval1 (lamE (eval1(A:=A)) ee)).
Proof.
intros.
rewrite eval1Flat.
rewrite eval1NAT.
reflexivity.
Qed.
(** evaluation of explicit flattening with access to the monotonicity witness for X *)
Definition eval1': LamE c_k1 Lam.
Proof.
refine (LamERecBase.MRec (fun (X:k1)(mX:mon X)(j: X c_k1 LamE)(rec: X c_k1 Lam)
(A:Set)(t:LamEFlatF X A) => _)).
destruct t as [[[a|(t1,t2)]|r]|ee].
exact (var a).
exact (app (rec _ t1)(rec _ t2)).
exact (abs (rec _ r)).
exact (subst (id(A:=Lam A)) (rec (Lam A) (mX (X A) (Lam A) (rec A) ee))).
Defined.
(** note that we do not use the j argument and hence do not make
use of the primitive recursion facility *)
(* Print eval1'. *)
(** We discover the outcome of this interactive definition: *)
Definition s_eval1'_base: forall (X:k1), mon X -> X c_k1 Lam -> LamEFlatF X c_k1 Lam:=
fun (X : k1) (mX : mon X)(it : X c_k1 Lam) (A : Set)
(t : LamEFlatF X A) =>
match t with
| inl (inl (inl a)) => var a
| inl (inl (inr (pair t1 t2))) => app (it A t1) (it A t2)
| inl (inr r) => abs (it (option A) r)
| inr ee =>
subst (id (A:=Lam A)) (it (Lam A) (mX (X A) (Lam A) (it A) ee))
end.
Lemma s_eval1'_base_ok:
eval1' = MItpl s_eval1'_base.
Proof.
reflexivity.
Qed.
(** the intended behaviour of eval1' on terms of the form flat ee *)
Lemma eval1'Flat (A:Set)(ee:LamE(LamE A)):
eval1' (flat ee) = subst (id(A:=Lam A)) (eval1'(A:=Lam A) (lamE (eval1'(A:=A)) ee)).
Proof.
intros.
unfold eval1' at 1.
unfold flat.
rewrite MRecRedCan.
reflexivity.
Qed.
(** eval1' is a natural transformation *)
Lemma eval1'NAT: NAT eval1' lamE lam.
Proof.
unfold eval1'.
apply MRecNAT.
red.
intros.
clear H.
destruct ef as [m0 e0 f01 f02].
simpl in H0.
destruct t as [[[a|(t1,t2)]|r]|ee]; simpl.
reflexivity.
do 2 rewrite H0.
reflexivity.
unfold moncomp.
rewrite H0.
reflexivity.
unfold moncomp at 1.
rewrite H0.
unfold id at 2.
rewrite <- (substNAT(mX:=lam)(j:=fun A r => r)).
f_equal.
unfold moncomp.
do 2 rewrite H0.
do 2 rewrite <- lamfct2.
apply lamext.
intro.
unfold comp.
rewrite H0.
apply lamext.
reflexivity.
red.
reflexivity.
Qed.
(** the now less intended behaviour of eval1' on terms of the form flat ee *)
Lemma eval1'NATcor (A:Set)(ee:LamE(LamE A)):
eval1' (flat ee) = subst (id(A:=Lam A)) (lam (eval1'(A:=A)) (eval1' ee)).
Proof.
intros.
rewrite eval1'Flat.
rewrite eval1'NAT.
reflexivity.
Qed.
(** we first give a proof by help of MItUni *)
Lemma eval1eval1' (A:Set)(t: LamE A): eval1 t = eval1' t.
Proof.
intros.
apply sym_eq.
unfold eval1.
apply LamEDef.MItUni; clear A t.
(* extensionality *)
red.
intros.
destruct y as [[[a|(t1,t2)]|r]|ee].
reflexivity.
do 2 rewrite H.
reflexivity.
rewrite H.
reflexivity.
rewrite H.
rewrite (lamext (f A) (g A)).
reflexivity.
apply H.
(* behaviour *)
intros.
destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval1'; rewrite MRecRed; reflexivity).
(** we now need eval1'NATcor even for non-canonical elements *)
transitivity (subst (id(A:=Lam A)) ((eval1'(A:=Lam A) o j (Lam A)) (m ef (eval1'(A:=A) o j A) ee))).
unfold eval1' at 1.
rewrite MRecRed.
reflexivity.
unfold comp at 1.
rewrite n.
rewrite eval1'NAT.
reflexivity.
Qed.
(** alternatively, we can use uniqueness of eval1': *)
Lemma eval1eval1'_ALT (A:Set)(t: LamE A): eval1 t = eval1' t.
Proof.
revert A t.
unfold eval1'.
apply MRecUni.
(* extensionality *)
red.
intros.
destruct y as [[[a|(t1,t2)]|r]|ee].
reflexivity.
do 2 rewrite H.
reflexivity.
rewrite H.
reflexivity.
rewrite H.
rewrite (e ef (f A) (g A)).
reflexivity.
apply H.
(* behaviour *)
intros.
destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval1; rewrite LamEBase.MItRed; reflexivity).
(** we now need eval1NATcor even for non-canonical elements *)
transitivity (subst (id (A:=Lam A)) (lam (eval1 (A:=A) o j A) ((eval1 (A:=X A) o j (X A)) ee))).
unfold eval1 at 1.
rewrite LamEBase.MItRed.
reflexivity.
unfold comp at 2.
rewrite <- eval1NAT.
unfold comp at 2.
rewrite n.
reflexivity.
Qed.
(** a test of MMIt *)
Definition LamEFlatFmonbr2: mon2br LamEFlatF.
Proof.
red.
red.
intros X Y mY f A t.
destruct t as [[[a|(t1,t2)]|r]|ee].
left.
left.
left.
assumption.
left.
left.
right.
exact (f _ t1, f _ t2).
left.
right.
exact (f _ r).
right.
exact (mY _ _ (f A) (f (X A) ee)).
Defined.
Definition eval1'': LamE c_k1 Lam := MMIt LamEFlatFmonbr2 lam s_eval1'_base.
(** hence, all of the branches are as in the definition of eval1' *)
(** we now see that eval1'' behaves nearly as eval1 *)
Lemma eval1''_flat (A:Set)(ee:LamE(LamE A)):
eval1'' (flat ee) = subst (id(A:=Lam A)) (lam (id (A:=Lam A)) (lam (eval1''(A:=A)) (eval1'' ee))).
(* not exactly as eval1, i.e.,
subst (id(A:=Lam A)) (lam (eval1''(A:=A)) (eval1'' ee))
and not as eval1', i.e.,
subst (id(A:=Lam A)) (eval1''(A:=Lam A) (lamE (eval1''(A:=A)) ee))
*)
Proof.
intros.
unfold eval1'' at 1.
unfold flat.
rewrite MMItRedCan.
reflexivity.
Qed.
(** the behaviour of eval1 only comes with the first functor law for lam: *)
Lemma eval1''_flat' (A:Set)(ee:LamE(LamE A)):
eval1'' (flat ee) = subst (id(A:=Lam A)) (lam (eval1''(A:=A)) (eval1'' ee)).
Proof.
intros.
rewrite eval1''_flat.
rewrite lamfct1. (** this is an unfriendly artifact of the construction! *)
reflexivity.
Qed.
(** alternatively, one could have used the second functor law and extensionality of lam *)
(** here, we verify the suspicion that eval1'' and eval1 agree on all arguments;
note that this cannot be the basis for a general theorem since eval1 is defined
from a different step term *)
Lemma eval1''eval1 (A:Set)(t: LamE A): eval1'' t = eval1 t.
Proof.
intros.
unfold eval1.
apply LamEDef.MItUni; clear A t.
(* extensionality *)
red.
intros.
destruct y as [[[a|(t1,t2)]|r]|ee].
reflexivity.
do 2 rewrite H.
reflexivity.
rewrite H.
reflexivity.
rewrite H.
rewrite (lamext (f A) (g A)).
reflexivity.
apply H.
(* behaviour *)
intros.
destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval1''; unfold MMIt; rewrite LamEBase.MItRed; reflexivity).
(** we now need eval1''_flat' even for non-canonical elements *)
unfold eval1'' at 1.
unfold MMIt.
rewrite LamEBase.MItRed.
unfold s_MMIt at 1; unfold LamEFlatFmonbr2 at 1.
unfold s_eval1'_base at 1.
change (fun x: Lam A => x) with (id(A:=Lam A)).
rewrite lamfct1. (** again the artifact *)
reflexivity.
Qed.
Definition lamEFct : EFct Lam := mkEFct lamext lamfct1 lamfct2.
(** we now use the general result *)
Lemma eval1''eval1' (A:Set)(t: LamE A): eval1'' t = eval1' t.
Proof.
intros.
unfold eval1''.
change eval1' with (MItpl s_eval1'_base).
refine (MMItsMItpls _ _ _ lamEFct _ _ _ _ t); clear A t; try reflexivity.
(* naturality *)
red.
intros.
destruct t as [[[a|(t1,t2)]|r]|ee].
reflexivity.
simpl lam.
do 2 rewrite <- H.
induction ef.
reflexivity.
simpl lam.
rewrite <- H.
reflexivity.
induction ef.
simpl.
simpl in H.
unfold moncomp.
do 3 rewrite H.
rewrite substLaw2.
rewrite <- lamfct2.
do 2 rewrite substLaw1.
apply substext.
intro.
unfold comp.
unfold id.
transitivity (lam (fun x => f x) (it A a)).
apply H.
apply lamext.
reflexivity.
(* about LamEFlatFmonbr2 *)
red.
intros.
destruct t as [[[a|(t1,t2)]|r]|ee]; simpl.
reflexivity.
induction ef.
simpl.
simpl in H.
do 2 rewrite H.
reflexivity.
induction ef.
simpl.
simpl in H.
unfold moncomp.
rewrite H.
reflexivity.
induction ef.
simpl.
simpl in H.
unfold moncomp.
rewrite H.
do 2 rewrite <- lamfct2.
f_equal.
apply lamext.
intro.
unfold comp.
apply H.
(* extensionality *)
red.
intros.
destruct y as [[[a|(t1,t2)]|r]|ee]; unfold s_eval1'_base.
reflexivity.
do 2 rewrite H.
reflexivity.
rewrite H.
reflexivity.
rewrite H.
rewrite (e ef (f A) (g A)).
reflexivity.
apply H.
(* behaviour *)
intros.
destruct t as [[[a|(t1,t2)]|r]|ee]; try reflexivity.
simpl.
change (fun x : Lam A => x) with (id(A:=Lam A)).
rewrite lamfct1.
rewrite H.
reflexivity.
Qed.
(** we have to reproduce the first two parts of the above proof in the following proof: *)
Lemma eval1''NAT: NAT eval1'' lamE lam.
Proof.
unfold eval1''.
refine (MMItsNAT(mG:=lam) LamEFlatFmonbr2 _ _ lamEFct (refl_equal _) _).
(* about the step term *)
red.
intros.
destruct t as [[[a|(t1,t2)]|r]|ee].
reflexivity.
simpl lam.
do 2 rewrite <- H.
induction ef.
reflexivity.
simpl lam.
rewrite <- H.
reflexivity.
induction ef.
simpl.
simpl in H.
unfold moncomp.
do 3 rewrite H.
rewrite substLaw2.
rewrite <- lamfct2.
do 2 rewrite substLaw1.
apply substext.
intro.
unfold comp.
unfold id.
transitivity (lam (fun x => f x) (it A a)).
apply H.
apply lamext.
reflexivity.
(* about LamEFlatFmonbr2 *)
red.
intros.
destruct t as [[[a|(t1,t2)]|r]|ee]; simpl.
reflexivity.
induction ef.
simpl.
simpl in H.
do 2 rewrite H.
reflexivity.
induction ef.
simpl.
simpl in H.
unfold moncomp.
rewrite H.
reflexivity.
induction ef.
simpl.
simpl in H.
unfold moncomp.
rewrite H.
do 2 rewrite <- lamfct2.
f_equal.
apply lamext.
intro.
unfold comp.
apply H.
Qed.
(** A direct naturality proof is much shorter: *)
Lemma eval1''NAT_ALT: NAT eval1'' lamE lam.
Proof.
unfold eval1''.
unfold MMIt.
apply LamEDef.MItNAT.
red.
intros.
destruct ef as [m0 e0 f01 f02].
simpl in H.
destruct t as [[[a|(t1,t2)]|r]|ee]; unfold s_MMIt; unfold LamEFlatFmonbr2; simpl.
reflexivity.
do 2 rewrite H.
reflexivity.
unfold moncomp.
rewrite H.
reflexivity.
unfold moncomp at 1.
rewrite H.
unfold id at 2.
rewrite <- (substNAT(mX:=lam)(j:=fun A r => r)).
f_equal.
unfold moncomp.
repeat rewrite <- lamfct2.
apply lamext.
intro.
unfold comp.
rewrite H.
apply lamext.
reflexivity.
red.
reflexivity.
Qed.
(** for the sake of completeness, the other datatype constructors are treated explicitly as well *)
Definition varE (A:k0)(a:A): LamE A :=
LamEDef.InCan (inl _ (inl _ (inl _ a))).
Definition appE (A:k0)(t1 t2:LamE A): LamE A :=
LamEDef.InCan (inl _ (inl _ (inr _ (t1,t2)))).
Definition absE (A:k0)(r: LamE (option A)): LamE A :=
LamEDef.InCan (inl _ (inr _ r)).
Lemma eval1'_var (A:k0)(a:A): eval1' (varE a) = var a.
Proof.
intros.
unfold eval1'.
unfold varE.
rewrite MRecRedCan.
reflexivity.
Qed.
Lemma eval1'_app (A:k0)(t1 t2:LamE A): eval1' (appE t1 t2) = app (eval1' t1) (eval1' t2).
Proof.
intros.
unfold eval1' at 1.
unfold appE.
rewrite MRecRedCan.
reflexivity.
Qed.
Lemma eval1'_abs (A:k0)(r:LamE (option A)): eval1' (absE r) = abs (eval1' r).
Proof.
intros.
unfold eval1' at 1.
unfold absE.
rewrite MRecRedCan.
reflexivity.
Qed.
Lemma eval1''_var (A:k0)(a:A): eval1'' (varE a) = var a.
Proof.
intros.
unfold eval1''.
unfold varE.
rewrite MMItRedCan.
reflexivity.
Qed.
Lemma eval1''_app (A:k0)(t1 t2:LamE A): eval1'' (appE t1 t2) = app (eval1'' t1) (eval1'' t2).
Proof.
intros.
unfold eval1'' at 1.
unfold appE.
rewrite MMItRedCan.
reflexivity.
Qed.
Lemma eval1''_abs (A:k0)(r:LamE (option A)): eval1'' (absE r) = abs (eval1'' r).
Proof.
intros.
unfold eval1'' at 1.
unfold absE.
rewrite MMItRedCan.
reflexivity.
Qed.
End EFlatRec.