Mercurial > cpdt > repo

comparison src/Intensional.v @ 186:ecd231ba5c8b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CcExp_correct
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 19:58:01 -0500
parents 303e9d866597
children 71c076dd5f31
comparison
equal deleted inserted replaced
185:303e9d866597 186:ecd231ba5c8b
806 match fs with 806 match fs with
807 | Main v => Main (f v) 807 | Main v => Main (f v)
808 | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x)) 808 | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x))
809 end. 809 end.
810 810
811 Definition CcTerm' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) := 811 Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) :=
812 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf). 812 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf).
813 813
814 814
815 (** * Correctness *) 815 (** * Correctness *)
816 816
951 | dom --> ran => fun f1 f2 => 951 | dom --> ran => fun f1 f2 =>
952 forall x1 x2, lr dom x1 x2 952 forall x1 x2, lr dom x1 x2
953 -> lr ran (f1 x1) (f2 x2) 953 -> lr ran (f1 x1) (f2 x2)
954 end. 954 end.
955 955
956 Theorem ccTerm_correct : forall t G 956 Theorem ccExp_correct : forall t G
957 (e1 : Source.exp Source.typeDenote t) 957 (e1 : Source.exp Source.typeDenote t)
958 (e2 : Source.exp natvar t), 958 (e2 : Source.exp natvar t),
959 exp_equiv G e1 e2 959 exp_equiv G e1 e2
960 -> forall (envT : list Source.type) (fvs : isfree envT) 960 -> forall (envT : list Source.type) (fvs : isfree envT)
961 (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2), 961 (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2),
1042 1042
1043 1043
1044 (** * Parametric version *) 1044 (** * Parametric version *)
1045 1045
1046 Section wf. 1046 Section wf.
1047 Variable result : ptype. 1047 Lemma Exp_wf' : forall G t (e1 e2 : Source.exp natvar t),
1048 1048 exp_equiv G e1 e2
1049 Lemma Pterm_wf' : forall G (e1 e2 : pterm natvar result),
1050 pterm_equiv G e1 e2
1051 -> forall envT (fvs : isfree envT), 1049 -> forall envT (fvs : isfree envT),
1052 (forall t (v1 v2 : natvar t), In (vars (v1, v2)) G 1050 (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G
1053 -> lookup_type v1 fvs = Some t) 1051 -> lookup_type v1 fvs = Some t)
1054 -> wfTerm fvs e1. 1052 -> wfExp fvs e1.
1055 Hint Extern 3 (Some _ = Some _) => contradictory; eapply lookup_bound_contra; eauto. 1053 Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto.
1056 1054
1057 apply (pterm_equiv_mut 1055 induction 1; crush.
1058 (fun G (e1 e2 : pterm natvar result) => 1056 eapply H0.
1059 forall envT (fvs : isfree envT), 1057 eauto.
1060 (forall t (v1 v2 : natvar t), In (vars (v1, v2)) G 1058
1061 -> lookup_type v1 fvs = Some t) 1059 apply H0 with (length envT).
1062 -> wfTerm (envT:=envT) fvs e1) 1060 my_crush.
1063 (fun G t (p1 p2 : pprimop natvar result t) => 1061 eauto.
1064 forall envT (fvs : isfree envT),
1065 (forall t (v1 v2 : natvar t), In (vars (v1, v2)) G
1066 -> lookup_type v1 fvs = Some t)
1067 -> wfPrimop (envT:=envT) fvs p1));
1068 simpler;
1069 match goal with
1070 | [ envT : list ptype, H : _ |- _ ] =>
1071 apply (H (length envT) (length envT)); simpler
1072 end.
1073 Qed. 1062 Qed.
1074 1063
1075 Theorem Pterm_wf : forall (E : Pterm result), 1064 Theorem Exp_wf : forall t (E : Source.Exp t),
1076 wfTerm (envT := nil) tt (E _). 1065 wfExp (envT := nil) tt (E _).
1077 intros; eapply Pterm_wf'; 1066 intros; eapply Exp_wf';
1078 [apply Pterm_equiv 1067 [apply Exp_equiv
1079 | simpler]. 1068 | crush].
1080 Qed. 1069 Qed.
1081 End wf. 1070 End wf.
1082 1071
1083 Definition CcTerm result (E : Pterm result) : Cprog result := 1072 Definition CcExp t (E : Source.Exp t) : Prog (ccType t) :=
1084 CcTerm' E (Pterm_wf E). 1073 CcExp' E (Exp_wf E).
1085 1074
1086 Lemma map_funcs_correct : forall result T1 T2 (f : T1 -> T2) (fs : cfuncs ctypeDenote result T1) k, 1075 Lemma map_funcs_correct : forall T1 T2 (f : T1 -> T2) (fs : funcs Closed.typeDenote T1),
1087 cfuncsDenote (map_funcs f fs) k = f (cfuncsDenote fs k). 1076 funcsDenote (map_funcs f fs) = f (funcsDenote fs).
1088 induction fs; equation. 1077 induction fs; crush.
1089 Qed. 1078 Qed.
1090 1079
1091 Theorem CcTerm_correct : forall result (E : Pterm result) k, 1080 Theorem CcExp_correct : forall (E : Source.Exp Nat),
1092 PtermDenote E k 1081 Source.ExpDenote E
1093 = CprogDenote (CcTerm E) k. 1082 = ProgDenote (CcExp E).
1094 Hint Rewrite map_funcs_correct : ltamer. 1083 Hint Rewrite map_funcs_correct : cpdt.
1095 1084
1096 unfold PtermDenote, CprogDenote, CcTerm, CcTerm', cprogDenote; 1085 unfold Source.ExpDenote, ProgDenote, CcExp, CcExp', progDenote; crush;
1097 simpler; 1086 apply (ccExp_correct
1098 apply (ccTerm_correct (result := result)
1099 (G := nil) 1087 (G := nil)
1100 (e1 := E _) 1088 (e1 := E _)
1101 (e2 := E _) 1089 (e2 := E _)
1102 (Pterm_equiv _ _ _) 1090 (Exp_equiv _ _ _)
1103 nil 1091 nil
1104 tt 1092 tt
1105 tt); 1093 tt); crush.
1106 simpler.
1107 Qed. 1094 Qed.