Mercurial > cpdt > repo

comparison src/Intensional.v @ 185:303e9d866597

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ccTerm_correct
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 19:42:32 -0500
parents 699fd70c04a7
children ecd231ba5c8b
comparison
equal deleted inserted replaced
184:699fd70c04a7 185:303e9d866597
824 induction fs; crush. 824 induction fs; crush.
825 Qed. 825 Qed.
826 End spliceFuncs_correct. 826 End spliceFuncs_correct.
827 827
828 828
829 Notation "var <| to" := (match to with 829 Notation "var <| to" := (match to return Set with
830 | None => unit 830 | None => unit
831 | Some t => var (ccType t) 831 | Some t => var (ccType t)
832 end) (no associativity, at level 70). 832 end) (no associativity, at level 70).
833 833
834 Section packing_correct. 834 Section packing_correct.
923 (packExp fvs1 fvs2 Hincl env))). 923 (packExp fvs1 fvs2 Hincl env))).
924 induction envT; my_crush. 924 induction envT; my_crush.
925 Qed. 925 Qed.
926 End packing_correct. 926 End packing_correct.
927 927
928 (*Lemma typeDenote_same : forall t, 928 About packExp_correct.
929 Closed.typeDenote (ccType t) = Source.typeDenote t. 929 Implicit Arguments packExp_correct [v envT fvs1].
930 induction t; crush. 930
931 Qed.*) 931 Implicit Arguments lookup_type_more [v2 envT fvs t b v].
932 932
933 Lemma typeDenote_same : forall t, 933 Lemma typeDenote_same : forall t,
934 Source.typeDenote t = Closed.typeDenote (ccType t). 934 Source.typeDenote t = Closed.typeDenote (ccType t).
935 induction t; crush. 935 induction t; crush.
936 Qed. 936 Qed.
943 crush. 943 crush.
944 Qed. 944 Qed.
945 945
946 Implicit Arguments look [envT n fvs t]. 946 Implicit Arguments look [envT n fvs t].
947 947
948 Lemma cast_jmeq : forall (T1 T2 : Set) (pf : T1 = T2) (T2' : Set) (v1 : T1) (v2 : T2'), 948 Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop :=
949 v1 == v2 949 match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with
950 -> T2' = T2 950 | Nat => @eq nat
951 -> match pf in _ = T return T with 951 | dom --> ran => fun f1 f2 =>
952 | refl_equal => v1 952 forall x1 x2, lr dom x1 x2
953 end == v2. 953 -> lr ran (f1 x1) (f2 x2)
954 intros; generalize pf; subst. 954 end.
955 intro.
956 rewrite (UIP_refl _ _ pf).
957 auto.
958 Qed.
959
960 Hint Resolve cast_jmeq.
961 955
962 Theorem ccTerm_correct : forall t G 956 Theorem ccTerm_correct : forall t G
963 (e1 : Source.exp Source.typeDenote t) 957 (e1 : Source.exp Source.typeDenote t)
964 (e2 : Source.exp natvar t), 958 (e2 : Source.exp natvar t),
965 exp_equiv G e1 e2 959 exp_equiv G e1 e2
968 (forall t (v1 : Source.typeDenote t) (v2 : natvar t), 962 (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
969 In (existT _ _ (v1, v2)) G 963 In (existT _ _ (v1, v2)) G
970 -> v2 < length envT) 964 -> v2 < length envT)
971 -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t), 965 -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
972 In (existT _ _ (v1, v2)) G 966 In (existT _ _ (v1, v2)) G
973 -> lookup_type v2 fvs = Some t 967 -> forall pf,
974 -> lookup Closed.typeDenote v2 env == v1) 968 lr t v1 (match lok pf in _ = T return T with
975 -> Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env) 969 | refl_equal => lookup Closed.typeDenote v2 env
976 == Source.expDenote e1. 970 end))
971 (*-> forall pf : lookup_type v2 fvs = Some t,
972 lr t v1 (match pf in _ = T return Closed.typeDenote <| T with
973 | refl_equal => lookup Closed.typeDenote v2 env
974 end))*)
975 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)).
977 976
978 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt. 977 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
979 Hint Resolve packExp_correct lookup_type_inner. 978 Hint Resolve packExp_correct lookup_type_inner.
980 979
981 induction 1. 980 induction 1.
983 crush. 982 crush.
984 crush. 983 crush.
985 crush. 984 crush.
986 crush. 985 crush.
987 986
988 Lemma app_jmeq : forall dom1 dom2 ran1 ran2 987 crush.
989 (f1 : dom1 -> ran1) (f2 : dom2 -> ran2) 988 apply (H0 x1 (length envT) (t1 :: envT) (true, snd (fvsExp (f2 (length envT)) (t1 :: envT)))).
990 (x1 : dom1) (x2 : dom2), 989 clear H0.
991 ran1 = ran2 990 crush.
992 -> f1 == f2 991 eauto.
993 -> x1 == x2 992 generalize (H1 _ _ _ H4).
994 -> f1 x1 == f2 x2. 993 crush.
995 crush. 994
996 assert (dom1 = dom2). 995 crush.
997 inversion H1; trivial. 996 generalize H3; clear_all.
998 crush. 997 match goal with
999 Qed. 998 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
1000 999 end.
1001 Lemma app_jmeq : forall dom ran
1002 (f1 : Closed.typeDenote (ccType dom) -> Closed.typeDenote (ccType ran))
1003 (f2 : Source.typeDenote dom -> Source.typeDenote ran)
1004 (x1 : dom1) (x2 : dom2),
1005 ran1 = ran2
1006 -> f1 == f2
1007 -> x1 == x2
1008 -> f1 x1 == f2 x2.
1009 crush.
1010 assert (dom1 = dom2).
1011 inversion H1; trivial.
1012 crush.
1013 Qed.
1014
1015 simpl. 1000 simpl.
1016 refine (app_jmeq _ _ _). 1001 destruct (eq_nat_dec (length envT) (length envT)); crush.
1017 apply app_jmeq. 1002 rewrite (UIP_refl _ _ e0); assumption.
1018 dependent rewrite <- IHexp_equiv1. 1003
1004 match goal with
1005 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
1006 end; simpl.
1007 destruct (eq_nat_dec v2 (length envT)); crush.
1008 generalize (H1 _ _ _ H5).
1009 crush.
1010 generalize (H2 _ _ _ H5).
1011 clear H2; intro H2.
1012 generalize (H2 (lookup_type_inner _ _ _ _ _ wf pf)).
1013 clear H2; intro H2.
1014 generalize H2; clear_all.
1015 repeat match goal with
1016 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
1017 end; simpl.
1018
1019 match type of pf with
1020 | ?X = _ => assert (X <> None)
1021 end.
1022 congruence.
1023 assert (forall (n : nat) (t0 : Source.type),
1024 lookup_type (envT:=envT) n (snd (fvsExp (f2 (length envT)) (t1 :: envT))) = Some t0 ->
1025 lookup_type (envT:=envT) n fvs = Some t0).
1026 eauto.
1027 generalize (packExp_correct fvs (inclusion t1 envT fvs (f2 (length envT)) wf) env H).
1028 simpl.
1029 match goal with
1030 | [ |- ?X == ?Y -> _ ] =>
1031 generalize X Y
1032 end.
1033 rewrite pf.
1034 rewrite (lookup_type_inner _ _ _ _ _ wf pf).
1035 crush.
1036 rewrite (UIP_refl _ _ e0).
1037 rewrite (UIP_refl _ _ e1) in H2.
1038 crush.
1039 rewrite <- H1.
1040 assumption.
1019 Qed. 1041 Qed.
1020 1042
1021 1043
1022 (** * Parametric version *) 1044 (** * Parametric version *)
1023 1045